diff --git a/changes-set.txt b/changes-set.txt index 1dbbb68cc3..dc11786b56 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -92,6 +92,18 @@ make a github issue.) DONE: Date Old New Notes +17-Sep-25 psdmul [same] Removed unneeded hypothesis +17-Sep-25 psdvsca [same] Removed unneeded hypothesis +17-Sep-25 psdadd [same] Removed unneeded hypothesis +17-Sep-25 psdmplcl [same] Removed unneeded hypothesis +17-Sep-25 psdcl [same] Removed unneeded hypothesis +17-Sep-25 psdcoef [same] Removed unneeded hypotheses +17-Sep-25 psdval [same] Removed unneeded hypotheses +16-Sep-25 ismhp3 [same] Removed unneeded hypotheses +16-Sep-25 ismhp2 [same] Removed unneeded hypotheses +16-Sep-25 ismhp [same] Removed unneeded hypotheses +16-Sep-25 selvval [same] Removed unneeded hypotheses +16-Sep-25 mplelsfi [same] Removed unused hypothesis 10-Sep-25 soeq12d [same] Moved from SO's mathbox to main set.mm 10-Sep-25 freq12d [same] Moved from SO's mathbox to main set.mm 10-Sep-25 weeq12d [same] Moved from SO's mathbox to main set.mm diff --git a/discouraged b/discouraged index c5928aaef1..c229493528 100644 --- a/discouraged +++ b/discouraged @@ -4719,6 +4719,7 @@ "df-base" is used by "resvbasOLD". "df-base" is used by "rmodislmodOLD". "df-base" is used by "slotsbhcdifOLD". +"df-base" is used by "sn-base0". "df-base" is used by "srabaseOLD". "df-base" is used by "symgvalstructOLD". "df-base" is used by "tngbasOLD". @@ -16029,7 +16030,7 @@ New usage of "df-aj" is discouraged (1 uses). New usage of "df-ass" is discouraged (1 uses). New usage of "df-at" is discouraged (2 uses). New usage of "df-ba" is discouraged (1 uses). -New usage of "df-base" is discouraged (31 uses). +New usage of "df-base" is discouraged (32 uses). New usage of "df-bdop" is discouraged (2 uses). New usage of "df-bj-1upl" is discouraged (6 uses). New usage of "df-bj-2upl" is discouraged (6 uses). @@ -19374,6 +19375,7 @@ New usage of "smfval" is discouraged (17 uses). New usage of "smgrpassOLD" is discouraged (1 uses). New usage of "smgrpismgmOLD" is discouraged (1 uses). New usage of "smgrpmgm" is discouraged (1 uses). +New usage of "sn-base0" is discouraged (0 uses). New usage of "sn-exelALT" is discouraged (0 uses). New usage of "sn-isghm" is discouraged (0 uses). New usage of "sn-wcdeq" is discouraged (0 uses). @@ -21647,6 +21649,7 @@ Proof modification of "slotsbhcdifOLD" is discouraged (96 steps). Proof modification of "smgrpassOLD" is discouraged (54 steps). Proof modification of "smgrpismgmOLD" is discouraged (22 steps). Proof modification of "sn-00id" is discouraged (47 steps). +Proof modification of "sn-base0" is discouraged (4 steps). Proof modification of "sn-exelALT" is discouraged (52 steps). Proof modification of "sn-isghm" is discouraged (432 steps). Proof modification of "snelpwiOLD" is discouraged (20 steps). diff --git a/set.mm b/set.mm index 6cf708df06..50c97ad6b4 100644 --- a/set.mm +++ b/set.mm @@ -286581,13 +286581,12 @@ the same dimension over the same (nonzero) ring. (Contributed by AV, mplelsfi.z $e |- .0. = ( 0g ` R ) $. mplelsfi.f $e |- ( ph -> F e. B ) $. - mplelsfi.r $e |- ( ph -> R e. V ) $. $( A polynomial treated as a coefficient function has finitely many nonzero terms. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 25-Jun-2019.) $) mplelsfi $p |- ( ph -> F finSupp .0. ) $= - ( wcel cfsupp wbr cmps co cbs eqid cfv mplelbas simprbi syl ) AEBNZEHOPZL - UEEFDQRZSUAZNUFUHCDUGBFEHIUGTUHTKJUBUCUD $. + ( wcel cfsupp wbr cmps co cbs cfv eqid mplelbas simprbi syl ) AEBLZEGMNZK + UCEFDOPZQRZLUDUFCDUEBFEGHUESUFSJITUAUB $. $} ${ @@ -288515,43 +288514,42 @@ This function maps an element of the formal polynomial algebra (with TSUVREUYDUWGUVOUVRDEFGJOUYDUVORUYESUBAUVNUVPWEZWBWCZUVRUYJWIWDZAUVNUWEUXJ WFWGZUVPAUYOBDALEMEUWAUVTUVOUMZQUNZUOZUOZUXJWFWGZCDWHUYOBDWHAUYTCDAUVPUKZ UYSVAUJZUYSWJZUXJVAUJZWKZUVOQWLUQZVGUJUYSUXJWLUQVUFWMUYTVUEVUAVUBVUCVUDLE - UYRUXNWNLEUYRXAFVBWOZWPVLVUAUVOQVUADFGUVOOVNQRSUAAUVPWIZAUXQUVPUDVSWQWRVU - AEUYRLVAVUFUXJVUAUVTEVUFWSUJZUKZUYRMEQUOZUXJVUJMEUYQQVUJUYQUWAQQUNQVUJUWA - UYPQQVUAEUYDVAUVOVAVUFUVTQVUADEFGJOUYDUVORUYESUBVUHWBVUAVUFWTUXMVUAUXNVLZ - QVAUJVUAQGVBUAXLVLXBXCUWAQXDXEXFAUXJVUKULUVPVUIAUXJEQXGXHVUKAEFGJOQPUXJRU - BUAUXLUCAUXRGXIUJUXSGXJVPXMMEQXKXEVTXNVULXOVUFUYSVAVAUXJXPXQZXRUYTUYOCBDU - VOUVMULZUYSUWEUXJWFVUNLEUYRUWDVUNMEUYQUWCVUNUWAUYPUWBQUVTUVOUVMXSXCXFXFYA - XTYBYCYDZUVRUWLUYSUXJWFKLEUWKUYRUWGUVTULZMEUWJUYQVUPUWHUWAUWIUYPQKLMUUAUW - GUVTUVOYEUUBXFUUCAUVPUYTUVNVUMYFUUDZYGYHUVREEXHZDUXFFHNVAUXJSUXLAFUUEUJZU - VQAUXPVUSUXTFUUFVPVSZUVRHVMUJZHUUGUJAVVAUVQAHVNUJVVAUEHVOVPVSZHUULVPZVURV - AUJUVREEUXNUXNUUHVLANFHUUIUQUJZUVQANFHUUJUQUJZVVDUFFHNUUKVPVSZUVRUXEDUJZK - EWHLEWHVURDUXFYKUVRVVGLKEEUVRUYBUYJUKZUKZUXPUWDDUJZUWKDUJZVVGAUXPUVQVVHUX - TVTUVRUYBVVJUYJUYIYDUVRUYJVVKUYBUYNYFDFUWNUWDUWKSUXKUUMUUNZUUOLKEEUXEDUXF - UXFVCZUUPYBUVRUXFVAUJZUXFWJZVUDWKZUWEUXJWLUQZUWLUXJWLUQZXHZVGUJZUXFUXJWLU - QVVSWMUXFUXJWFWGVVPUVRVVNVVOVUDLKEEUXEUXNUXNUUQLKEEUXEUXFVVMUURVUGWPVLUVR - VVQVGUJZVVRVGUJZVVTUVRUWEUXJVUOWRZUVRUWLUXJVUQWRZVVQVVRUUSUUTUVRLKDFUWNEE - VAVAUWDUWKUXJSUXLUXKUYAUYIUYNUXOUXOUVAVVSUXFVAVAUXJXPXQYIUVRHLKEEUXENUMZU - TZUPUQHLKEEUWDNUMZUWKNUMZIUQZUTZUPUQZUXIUXAUVRVWFVWJHUPUVRLKEEVWEVWIUVRUY - BUYJVWEVWIULVVIVWEMEUVSUVTUWGUVBUVCUQULUWBUWIGURUMZUQQUNUOZNUMZVWIVVIUXEV - WMNVVIMUYDEFGUWNVWLJUWBUWIOPUVTUWGQRUBUAUYEAUYFUVQVVHUCVTAUXQUVQVVHUDVTUX - KVWLVCUVRUYBUYJWAUVRUYBUYJWEUVRUYBUWBUYDUJUYJUYHYDUVRUYJUWIUYDUJUYBUYMYFU - VDYHAUVQVVHVWNVWIULUGUVEYJUVFUVGYLUVRUXHVWFHUPUVRLKUHEEDUXEUHUIZNUMZVWEUX - FNVVLUVRUXFYMANUHDVWPUOULUVQAUHDHVRUMZNAVVEDVWQNYKZUFFHNDVWQSVWQVCZUVLVPZ - UVHVSZVWOUXENYEUVIYLUVRUXAHLEVWGUOZUPUQZHKEVWHUOZUPUQZIUQVWKUVRUWRVXCUWTV - XEIUVRUWQVXBHUPUVRLUHEDUWDVWPVWGUWENUYIUVRUWEYMVXAVWOUWDNYEYNYLUVRUWSVXDH - UPUVRKUHEDUWKVWPVWHUWLNUYNUVRUWLYMVXAVWOUWKNYEYNYLYOUVRLKVWQHIEEVAVAVWGVW - HHVBUMZVWSTVXFVCZUXOUXOVVBUYCDVWQUWDNAVWRUVQUYBVWTVTUYIYPUYKDVWQUWKNAVWRU - VQUYJVWTVTUYNYPUVRVXBVAUJZVXBWJZVXFVAUJZWKZVWAVXBVXFWLUQVVQWMZVXBVXFWFWGV - XKUVRVXHVXIVXJLEVWGUXNWNLEVWGXAHVBWOZWPVLVWCAVXLUVQALUWDEVANVVQVAUXJVXFAV - VQWTAVVEUXJNUMVXFULUFFHNUXJVXFUXLVXGUVJVPZUWDVAUJAUYBUKMEUWCUXNWNVLVUDAVU - GVLZYQVSVVQVXBVAVAVXFXPXQUVRVXDVAUJZVXDWJZVXJWKZVWBVXDVXFWLUQVVRWMZVXDVXF - WFWGVXRUVRVXPVXQVXJKEVWHUXNWNKEVWHXAVXMWPVLVWDAVXSUVQAKUWKEVANVVRVAUXJVXF - AVVRWTVXNUWKVAUJAUYJUKMEUWJUXNWNVLVXOYQVSVVRVXDVAVAVXFXPXQYGYJYRUVKUVRUXB - UWONUVRUVMUWFUVOUWMUWNUVRMDEFGJLOPUVMQRUBUASAUYFUVQUCVSZAUXRUVQUXSVSZUYGY - SZUVRMDEFGJKOPUVOQRUBUASVXTVYAUYLYSZYOYHUVRUXCUWRUXDUWTIUVRUXCUWFNUMUWRUV - RUVMUWFNVYBYHUVREDUWEFHNVAUXJSUXLVUTVVCUXOVVFUVRLEUWDDUYIYTVUOYIXNUVRUXDU - WMNUMUWTUVRUVOUWMNVYCYHUVREDUWLFHNVAUXJSUXLVUTVVCUXOVVFUVRKEUWKDUYNYTVUQY - IXNYOYR $. + UYRUXNWNLEUYRXAFVBWOZWPVLVUAUVOQVUADFGUVOOQRSUAAUVPWIZWQWRVUAEUYRLVAVUFUX + JVUAUVTEVUFWSUJZUKZUYRMEQUOZUXJVUJMEUYQQVUJUYQUWAQQUNQVUJUWAUYPQQVUAEUYDV + AUVOVAVUFUVTQVUADEFGJOUYDUVORUYESUBVUHWBVUAVUFWTUXMVUAUXNVLZQVAUJVUAQGVBU + AXLVLXBXCUWAQXDXEXFAUXJVUKULUVPVUIAUXJEQXGXHVUKAEFGJOQPUXJRUBUAUXLUCAUXRG + XIUJUXSGXJVPXMMEQXKXEVTXNVULXOVUFUYSVAVAUXJXPXQZXRUYTUYOCBDUVOUVMULZUYSUW + EUXJWFVUNLEUYRUWDVUNMEUYQUWCVUNUWAUYPUWBQUVTUVOUVMXSXCXFXFYAXTYBYCYDZUVRU + WLUYSUXJWFKLEUWKUYRUWGUVTULZMEUWJUYQVUPUWHUWAUWIUYPQKLMUUAUWGUVTUVOYEUUBX + FUUCAUVPUYTUVNVUMYFUUDZYGYHUVREEXHZDUXFFHNVAUXJSUXLAFUUEUJZUVQAUXPVUSUXTF + UUFVPVSZUVRHVMUJZHUUGUJAVVAUVQAHVNUJVVAUEHVOVPVSZHUULVPZVURVAUJUVREEUXNUX + NUUHVLANFHUUIUQUJZUVQANFHUUJUQUJZVVDUFFHNUUKVPVSZUVRUXEDUJZKEWHLEWHVURDUX + FYKUVRVVGLKEEUVRUYBUYJUKZUKZUXPUWDDUJZUWKDUJZVVGAUXPUVQVVHUXTVTUVRUYBVVJU + YJUYIYDUVRUYJVVKUYBUYNYFDFUWNUWDUWKSUXKUUMUUNZUUOLKEEUXEDUXFUXFVCZUUPYBUV + RUXFVAUJZUXFWJZVUDWKZUWEUXJWLUQZUWLUXJWLUQZXHZVGUJZUXFUXJWLUQVVSWMUXFUXJW + FWGVVPUVRVVNVVOVUDLKEEUXEUXNUXNUUQLKEEUXEUXFVVMUURVUGWPVLUVRVVQVGUJZVVRVG + UJZVVTUVRUWEUXJVUOWRZUVRUWLUXJVUQWRZVVQVVRUUSUUTUVRLKDFUWNEEVAVAUWDUWKUXJ + SUXLUXKUYAUYIUYNUXOUXOUVAVVSUXFVAVAUXJXPXQYIUVRHLKEEUXENUMZUTZUPUQHLKEEUW + DNUMZUWKNUMZIUQZUTZUPUQZUXIUXAUVRVWFVWJHUPUVRLKEEVWEVWIUVRUYBUYJVWEVWIULV + VIVWEMEUVSUVTUWGUVBUVCUQULUWBUWIGURUMZUQQUNUOZNUMZVWIVVIUXEVWMNVVIMUYDEFG + UWNVWLJUWBUWIOPUVTUWGQRUBUAUYEAUYFUVQVVHUCVTAUXQUVQVVHUDVTUXKVWLVCUVRUYBU + YJWAUVRUYBUYJWEUVRUYBUWBUYDUJUYJUYHYDUVRUYJUWIUYDUJUYBUYMYFUVDYHAUVQVVHVW + NVWIULUGUVEYJUVFUVGYLUVRUXHVWFHUPUVRLKUHEEDUXEUHUIZNUMZVWEUXFNVVLUVRUXFYM + ANUHDVWPUOULUVQAUHDHVRUMZNAVVEDVWQNYKZUFFHNDVWQSVWQVCZUVLVPZUVHVSZVWOUXEN + YEUVIYLUVRUXAHLEVWGUOZUPUQZHKEVWHUOZUPUQZIUQVWKUVRUWRVXCUWTVXEIUVRUWQVXBH + UPUVRLUHEDUWDVWPVWGUWENUYIUVRUWEYMVXAVWOUWDNYEYNYLUVRUWSVXDHUPUVRKUHEDUWK + VWPVWHUWLNUYNUVRUWLYMVXAVWOUWKNYEYNYLYOUVRLKVWQHIEEVAVAVWGVWHHVBUMZVWSTVX + FVCZUXOUXOVVBUYCDVWQUWDNAVWRUVQUYBVWTVTUYIYPUYKDVWQUWKNAVWRUVQUYJVWTVTUYN + YPUVRVXBVAUJZVXBWJZVXFVAUJZWKZVWAVXBVXFWLUQVVQWMZVXBVXFWFWGVXKUVRVXHVXIVX + JLEVWGUXNWNLEVWGXAHVBWOZWPVLVWCAVXLUVQALUWDEVANVVQVAUXJVXFAVVQWTAVVEUXJNU + MVXFULUFFHNUXJVXFUXLVXGUVJVPZUWDVAUJAUYBUKMEUWCUXNWNVLVUDAVUGVLZYQVSVVQVX + BVAVAVXFXPXQUVRVXDVAUJZVXDWJZVXJWKZVWBVXDVXFWLUQVVRWMZVXDVXFWFWGVXRUVRVXP + VXQVXJKEVWHUXNWNKEVWHXAVXMWPVLVWDAVXSUVQAKUWKEVANVVRVAUXJVXFAVVRWTVXNUWKV + AUJAUYJUKMEUWJUXNWNVLVXOYQVSVVRVXDVAVAVXFXPXQYGYJYRUVKUVRUXBUWONUVRUVMUWF + UVOUWMUWNUVRMDEFGJLOPUVMQRUBUASAUYFUVQUCVSZAUXRUVQUXSVSZUYGYSZUVRMDEFGJKO + PUVOQRUBUASVXTVYAUYLYSZYOYHUVRUXCUWRUXDUWTIUVRUXCUWFNUMUWRUVRUVMUWFNVYBYH + UVREDUWEFHNVAUXJSUXLVUTVVCUXOVVFUVRLEUWDDUYIYTVUOYIXNUVRUXDUWMNUMUWTUVRUV + OUWMNVYCYHUVREDUWLFHNVAUXJSUXLVUTVVCUXOVVFUVRKEUWKDUYNYTVUQYIXNYOYR $. $} ${ @@ -288662,11 +288660,11 @@ This function maps an element of the formal polynomial algebra (with YOYBRABDEFJOYORUAYRUBUDUOVQZVRVSYKYBCDHLJNOUDCGHUEUCVTUFAHWAVGZYJAYMYTU LGHUEWDVKVMAYJWBAOCNVCYJUNVMWEZCGIYDYEUCUGWFWGWHAYGWIVGYGWJZYHWIVGRFVDU RZWKUTZWLVGYGYHWKUTUUDWMYIATDYFWIAJUQWNWOWPWLVGJWQOWRUTDWIUDAWQOWRWSWTX - AUUBATDYFXBXCAGVDXGZARUUCABEFROVLUUCUAUBUUCVOZUOUKXDXEATUPYDYEDCUUDIWIW - IYHYHATYCDWIMUUDWIUUCYHAUUDTDYCVBZUUCWKUTZXFUUHUUDWMARUUGUUCWKATDYORYSX - HXIUUHUUDXJVKAYQMFGXKUTVGUUCMURYHXFUMFGMXLFGMUUCYHUUFYHVOZXQXMYKYBRXGAF - VDXGXNAYLUPUQZCVGYHUUJIUTYHXFYNCGIUUJYHUCUGUUIXOXRYKYCMXGUUAUUEXPUUDYGW - IWIYHXSXTYA $. + AUUBATDYFXBXCAGVDXGZARUUCABEFROUUCUAUBUUCVOZUOXDXEATUPYDYEDCUUDIWIWIYHY + HATYCDWIMUUDWIUUCYHAUUDTDYCVBZUUCWKUTZXFUUHUUDWMARUUGUUCWKATDYORYSXHXIU + UHUUDXJVKAYQMFGXKUTVGUUCMURYHXFUMFGMXLFGMUUCYHUUFYHVOZXQXMYKYBRXGAFVDXG + XNAYLUPUQZCVGYHUUJIUTYHXFYNCGIUUJYHUCUGUUIXOXRYKYCMXGUUAUUEXPUUDYGWIWIY + HXSXTYA $. $} $d x A $. $d b p v w x y z B $. $d b p x y z C $. $d b p v w x y z ph $. @@ -289555,8 +289553,6 @@ Additional definitions for (multivariate) polynomials selvval.t $e |- T = ( J mPoly U ) $. selvval.c $e |- C = ( algSc ` T ) $. selvval.d $e |- D = ( C o. ( algSc ` U ) ) $. - selvval.i $e |- ( ph -> I e. V ) $. - selvval.r $e |- ( ph -> R e. W ) $. selvval.j $e |- ( ph -> J C_ I ) $. selvval.f $e |- ( ph -> F e. B ) $. $( Value of the "variable selection" function. (Contributed by SN, @@ -289566,26 +289562,27 @@ Additional definitions for (multivariate) polynomials ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) $= ( vu vt vc vd vf cslv co cfv cdif cmpl cv ccom wcel cmvr cif cmpt crn ces - cascl csb cbs cvv selvfval wceq coeq2 fveq2d fveq1d csbeq2dv adantl eqtri - fveq2i eleqtrdi fvex csbex fvmptd ovex eqeq2i oveq2 fveq2 coeq2d mpteq2dv - ifeq1d csbeq12dv coeq1 fveq1 ifeq2d fvexi coex rneq fveq12d sylbir eqtrdi - a1i csbie ) AJLKGUJUKULZULUEKLUMZGUNUKZUFLUEUOZUNUKZUGUFUOZVCULZUHUGUOZXB - VCULZUPZBKBUOZLUQZXILXBURUKZULZXIWTGURUKULZXFULZUSZUTZUHUOZJUPZXQVAZKXDVB - UKZULZULZULZVDZVDZVDZVDZBKXJXILIURUKZULZXMDULZUSZUTZEJUPZEVAZKHVBUKZULZUL - ZULZAUIJUEXAUFXCUGXEUHXHXPXQUIUOZUPZYAULZULZVDZVDZVDZVDZYGKGUNUKZVEULZWSV - FABUEUFGUIKLMNUGUHUAUBUCVGYSJVHZUUFYGVHAUUIUEXAUUEYFUUIUFXCUUDYEUUIUGXEUU - CYDUUIUHXHUUBYCUUIXPUUAYBUUIYTXRYAYSJXQVIVJVKVLVLVLVLVMAJCUUHUDCFVEULUUHP - FUUGVEOVOVNVPYGVFUQAUEXAYFUFXCYEUGXEYDUHXHYCXPYBVQVRVRVRVRWQVSUEXAYFYRWTG - UNVTXBXAVHXBIVHZYFYRVHIXAXBQWAUUJYFUFLIUNUKZUGXEUHXFIVCULZUPZBKXJYIXNUSZU - TZYBULZVDZVDZVDYRUUJUFXCYEUUKUURXBILUNWBUUJUGXEYDUUQUUJUHXHYCUUMUUPUUJXGU - ULXFXBIVCWCWDUUJXPUUOYBUUJBKXOUUNUUJXJXLYIXNUUJXIXKYHXBILURWBVKWFWEVJWGVL - WGUFUUKUURYRLIUNVTXDUUKVHXDHVHZUURYRVHHUUKXDRWAUUSUURUGHVCULZUHUUMUUOXRXS - YOULZULZULZVDZVDYRUUSUGXEUUQUUTUVDXDHVCWCUUSUHUUMUUPUVCUUSUUOYBUVBUUSXRYA - UVAUUSXSXTYOXDHKVBWBVKVKVKVLWGUGUUTUVDYRHVCVQXFUUTVHXFDVHZUVDYRVHDUUTXFSW - AUVEUVDUHDUULUPZYLUVBULZVDYRUVEUHUUMUVCUVFUVGXFDUULWHUVEUUOYLUVBUVEBKUUNY - KUVEXJXNYJYIXMXFDWIWJWEVJWGUHUVFUVGYRDUULDHVCSWKIVCVQWLXQUVFVHXQEVHZUVGYR - VHEUVFXQTWAUVHYLUVBYQUVHXRYMUVAYPUVHXSYNYOXQEWMVJXQEJWHWNVKWOWRWPWOWRWPWO - WRWPWOWRWP $. + cascl csb cbs cvv coeq2 fveq2d fveq1d csbeq2dv wa reldmmpl elbasov simpld + wceq syl simprd selvfval fveq2i eqtri eleqtrdi fvex csbex a1i ovex eqeq2i + fvmptd4 oveq2 fveq2 coeq2d ifeq1d csbeq12dv coeq1 fveq1 ifeq2d fvexi coex + mpteq2dv rneq fveq12d sylbir csbie eqtrdi ) AJLKGUFUGUHZUHUAKLUIZGUJUGZUB + LUAUKZUJUGZUCUBUKZUSUHZUDUCUKZXCUSUHZULZBKBUKZLUMZXJLXCUNUGZUHZXJXAGUNUGU + HZXGUHZUOZUPZUDUKZJULZXRUQZKXEURUGZUHZUHZUHZUTZUTZUTZUTZBKXKXJLIUNUGZUHZX + NDUHZUOZUPZEJULZEUQZKHURUGZUHZUHZUHZAUEJUAXBUBXDUCXFUDXIXQXRUEUKZULZYBUHZ + UHZUTZUTZUTZUTYHKGUJUGZVAUHZWTVBYTJVKZUAXBUUFYGUUIUBXDUUEYFUUIUCXFUUDYEUU + IUDXIUUCYDUUIXQUUBYCUUIUUAXSYBYTJXRVCVDVEVFVFVFVFABUAUBGUEKLVBVBUCUDAKVBU + MZGVBUMZAJCUMUUJUUKVGTJCFUJKGVHMNVIVLZVJAUUJUUKUULVMSVNAJCUUHTCFVAUHUUHNF + UUGVAMVOVPVQYHVBUMAUAXBYGUBXDYFUCXFYEUDXIYDXQYCVRVSVSVSVSVTWCUAXBYGYSXAGU + JWAXCXBVKXCIVKZYGYSVKIXBXCOWBUUMYGUBLIUJUGZUCXFUDXGIUSUHZULZBKXKYJXOUOZUP + ZYCUHZUTZUTZUTYSUUMUBXDYFUUNUVAXCILUJWDUUMUCXFYEUUTUUMUDXIYDUUPUUSUUMXHUU + OXGXCIUSWEWFUUMXQUURYCUUMBKXPUUQUUMXKXMYJXOUUMXJXLYIXCILUNWDVEWGWNVDWHVFW + HUBUUNUVAYSLIUJWAXEUUNVKXEHVKZUVAYSVKHUUNXEPWBUVBUVAUCHUSUHZUDUUPUURXSXTY + PUHZUHZUHZUTZUTYSUVBUCXFUUTUVCUVGXEHUSWEUVBUDUUPUUSUVFUVBUURYCUVEUVBXSYBU + VDUVBXTYAYPXEHKURWDVEVEVEVFWHUCUVCUVGYSHUSVRXGUVCVKXGDVKZUVGYSVKDUVCXGQWB + UVHUVGUDDUUOULZYMUVEUHZUTYSUVHUDUUPUVFUVIUVJXGDUUOWIUVHUURYMUVEUVHBKUUQYL + UVHXKXOYKYJXNXGDWJWKWNVDWHUDUVIUVJYSDUUODHUSQWLIUSVRWMXRUVIVKXREVKZUVJYSV + KEUVIXRRWBUVKYMUVEYRUVKXSYNUVDYQUVKXTYOYPXREWOVDXREJWIWPVEWQWRWSWQWRWSWQW + RWSWQWRWS $. $} ${ @@ -289643,16 +289640,28 @@ Additional definitions for (multivariate) polynomials FGUDUJUFZUCUDZUKZGCUQZULZFBUQZVFVGKUKZGCUQZULZFBUQZUHIUMABCDEFGHUCIJLMNOP QRSTUAUNVHKUKZVLVPUKAVQVKVOFBVQVJVNVFVQVIVMGCVHKVGUOUPURUPUSUBVPUMUTAVOFB BDVAQVBVCVDVE $. + $} - $d X f $. $d .0. f $. $d D f $. + ${ + $d I f h $. $d R f $. $d D f g $. $d .0. f $. $d B f $. $d N f g $. + $d X f $. $d g h $. + ismhp.h $e |- H = ( I mHomP R ) $. + ismhp.p $e |- P = ( I mPoly R ) $. + ismhp.b $e |- B = ( Base ` P ) $. + ismhp.0 $e |- .0. = ( 0g ` R ) $. + ismhp.d $e |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } $. + ismhp.n $e |- ( ph -> N e. NN0 ) $. $( Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.) $) ismhp $p |- ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) ) $= - ( vf cfv wcel cv csupp co ccnfld cn0 cress cgsu wceq wss wa mhpval eleq2d - crab oveq1 sseq1d elrab bitrdi ) AMJHUDZUEMUCUFZNUGUHZUIUJUKUHFUFULUHJUMF - CURZUNZUCBURZUEMBUEMNUGUHZVFUNZUOAVCVHMABCDEUCFGHIJKLNOPQRSTUAUBUPUQVGVJU - CMBVDMUMVEVIVFVDMNUGUSUTVAVB $. + ( vf wcel cfv csupp co ccnfld cn0 cress cv cgsu wceq crab wss wa cvv cmhp + reldmmhp id elfvov1 elfvov2 jca anim2i cmpl reldmmpl adantr simprl simprr + elbasov mhpval eleq2d oveq1 sseq1d elrab bitrdi pm5.21nd ) AKJHUAZTZKBTZK + LUBUCZUDUEUFUCFUGUHUCJUIFCUJZUKZULZAIUMTZEUMTZULZULZVOWCAVOWAWBVOEHIUNKJU + OMVOUPZUQVOEHIUNKJUOMWEURUSUTVTWCAVPWCVSKBDVAIEVBNOVFVCUTWDVOKSUGZLUBUCZV + RUKZSBUJZTVTWDVNWIKWDBCDESFGHIJUMUMLMNOPQAWAWBVDAWAWBVEAJUETWCRVCVGVHWHVS + SKBWFKUIWGVQVRWFKLUBVIVJVKVLVM $. ismhp2.1 $e |- ( ph -> X e. B ) $. ${ @@ -289662,8 +289671,8 @@ Additional definitions for (multivariate) polynomials SN, 25-May-2024.) $) ismhp2 $p |- ( ph -> X e. ( H ` N ) ) $= ( cfv wcel csupp co ccnfld cn0 cress cgsu wceq crab wss ismhp mpbir2and - cv ) AMJHUEUFMBUFMNUGUHUIUJUKUHFURULUHJUMFCUNUOUCUDABCDEFGHIJKLMNOPQRST - UAUBUPUQ $. + cv ) AKJHUAUBKBUBKLUCUDUEUFUGUDFUNUHUDJUIFCUJUKSTABCDEFGHIJKLMNOPQRULUM + $. $} $d N d g $. $d D d $. $d .0. d $. $d X d $. $d ph d $. @@ -289671,15 +289680,14 @@ Additional definitions for (multivariate) polynomials same. (Contributed by SN, 22-Jul-2024.) $) ismhp3 $p |- ( ph -> ( X e. ( H ` N ) <-> A. d e. D ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) ) ) $= - ( vg cfv wcel csupp co ccnfld cn0 cress cv cgsu wceq crab wss wa wne wral + ( wcel vg cfv csupp co ccnfld cn0 cress cv cgsu wceq crab wss wa wne wral wi ismhp biantrurd wal wfn cvv wb cbs eqid mplelf c0g fvexi a1i elsuppfng ffnd syl3anc weq oveq2 eqeq1d elrab imbi12d imdistan bitr4di albidv df-ss - df-ral 3bitr4g 3bitr2d ) ALIGUEUFLBUFZLMUGUHZUIUJUKUHZUDULZUMUHZIUNZUDCUO - ZUPZUQWONULZLUEMURZWJWPUMUHZIUNZUTZNCUSZABCDEUDFGHIJKLMOPQRSTUAUBVAAWHWOU - CVBAWPWIUFZWPWNUFZUTZNVCWPCUFZWTUTZNVCWOXAAXDXFNAXDXEWQUQZXEWSUQZUTXFAXBX - GXCXHALCVDWHMVEUFZXBXGVFACEVGUEZLABCDEFHXJLPXJVHQSUCVIVNUCXIAMEVJRVKVLWPL - BVECMVMVOXCXHVFAWMWSUDWPCUDNVPWLWRIWKWPWJUMVQVRVSVLVTXEWQWSWAWBWCNWIWNWDW - TNCWEWFWG $. + df-ral 3bitr4g 3bitr2d ) AJIGUBTJBTZJKUCUDZUEUFUGUDZUAUHZUIUDZIUJZUACUKZU + LZUMWKLUHZJUBKUNZWFWLUIUDZIUJZUPZLCUOZABCDEUAFGHIJKMNOPQRUQAWDWKSURAWLWET + ZWLWJTZUPZLUSWLCTZWPUPZLUSWKWQAWTXBLAWTXAWMUMZXAWOUMZUPXBAWRXCWSXDAJCUTWD + KVATZWRXCVBACEVCUBZJABCDEFHXFJNXFVDOQSVEVJSXEAKEVFPVGVHWLJBVACKVIVKWSXDVB + AWIWOUAWLCUALVLWHWNIWGWLWFUIVMVNVOVHVPXAWMWOVQVRVSLWEWJVTWPLCWAWBWC $. $} ${ @@ -289704,14 +289712,12 @@ Additional definitions for (multivariate) polynomials mhpmpl.b $e |- B = ( Base ` P ) $. mhpmpl.x $e |- ( ph -> X e. ( H ` N ) ) $. $( A homogeneous polynomial is a polynomial. (Contributed by Steven - Nguyen, 25-Aug-2023.) Remove hypotheses using reverse closure. - (Revised by SN, 4-Aug-2025.) $) + Nguyen, 25-Aug-2023.) $) mhpmpl $p |- ( ph -> X e. B ) $= ( vg vh cfv wcel co cn0 cv crab csupp ccnfld cress cgsu wceq ccnv cn cima - c0g cfn cmap wss eqid cmhp reldmmhp elfvov1 elfvov2 mhprcl ismhp simprbda - cvv mpdan ) AHGEOPZHBPZLAVCVDHDUIOZUAQUBRUCQMSUDQGUEMNSUFUGUHUJPNRFUKQTZT - ULABVFCDMNEFGVAVAHVEIJKVEUMVFUMADEFUNHGUOILUPADEFUNHGUOILUQADEFGHILURUSUT - VB $. + c0g cfn cmap wss eqid mhprcl ismhp simprbda mpdan ) AHGEOPZHBPZLAURUSHDUI + OZUAQUBRUCQMSUDQGUEMNSUFUGUHUJPNRFUKQTZTULABVACDMNEFGHUTIJKUTUMVAUMADEFGH + ILUNUOUPUQ $. $} ${ @@ -289724,10 +289730,9 @@ Additional definitions for (multivariate) polynomials (Contributed by Steven Nguyen, 25-Aug-2023.) $) mhpdeg $p |- ( ph -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) $= - ( cfv wcel co cvv eqid cmhp csupp ccnfld cn0 cress cv cgsu wceq crab cmpl - wss cbs reldmmhp elfvov1 elfvov2 mhprcl ismhp simplbda mpdan ) AIHFOPZIJU - AQUBUCUDQDUEUFQHUGDBUHUJZNAUSIGCUIQZUKOZPUTAVBBVACDEFGHRRIJKVASVBSLMACFGT - IHULKNUMACFGTIHULKNUNACFGHIKNUOUPUQUR $. + ( cfv wcel csupp co ccnfld eqid cn0 cv cgsu wceq crab wss cmpl cbs mhprcl + cress ismhp simplbda mpdan ) AIHFOPZIJQRSUAUJRDUBUCRHUDDBUEUFZNAUNIGCUGRZ + UHOZPUOAUQBUPCDEFGHIJKUPTUQTLMACFGHIKNUIUKULUM $. $} ${ @@ -289745,11 +289750,11 @@ Additional definitions for (multivariate) polynomials ~ https://math.stackexchange.com/a/1796314/593843 . (Contributed by SN, 12-Sep-2023.) $) mhp0cl $p |- ( ph -> ( D X. { .0. } ) e. ( H ` N ) ) $= - ( vg co cgrp eqid wcel cmpl cbs cfv csn cxp mpl0 syl2anc grpidcl eqeltrrd + ( vg co cfv eqid wcel cmpl cbs csn cxp mpl0 cgrp syl2anc grpidcl eqeltrrd c0g mplgrp syl csupp ccnfld cn0 cress cgsu wceq crab wss fczsupp0 eqsstri - cv c0 0ss a1i ismhp2 ) AFCUAQZUBUCZBVHCPDEFGHRBIUDUEZIJVHSZVISZKLMNOAVHUJ - UCZVJVIABVHCDFIHVMVKLKVMSZMNUFAVHRTZVMVITAFHTCRTVOMNVHCFHVKUKUGVIVHVMVLVN - UHULUIVJIUMQZUNUOUPQPVCUQQGURPBUSZUTAVPVDVQBIVAVQVEVBVFVG $. + cv c0 0ss a1i ismhp2 ) AFCUAQZUBRZBVHCPDEFGBIUCUDZIJVHSZVISZKLOAVHUJRZVJV + IABVHCDFIHVMVKLKVMSZMNUEAVHUFTZVMVITAFHTCUFTVOMNVHCFHVKUKUGVIVHVMVLVNUHUL + UIVJIUMQZUNUOUPQPVCUQQGURPBUSZUTAVPVDVQBIVAVQVEVBVFVG $. $} ${ @@ -289779,8 +289784,7 @@ Additional definitions for (multivariate) polynomials AYAVESXQAXTCXJHVEPAEUFVOWAVGVPVQYBXTXRXNXTYAXJXTCXJVRVSXRXNXTXLXSULUKZRTX RYKXLUDGRWBZULUKZRXSYLXLULUDGRVTWCXRXLWDSZYHYMRTUIUHWEQSZYNWFUIXLUHXLVFZW GWHYIGUDXLIRYORXLUFQTWFUIXLUHRYPWIWJWHWLWKWMXTXMYKRXHXSXLULWNWOWPWQXCWRAD - WSQZXPDEUBFGRIVJXGXJUAJKYQVFZYGYFNORUISAWTXAAHYQCBABYQDEGHIKYRMLNOXBPXDXE - XF $. + WSQZXPDEUBFGRXGXJUAJKYQVFZYGYFRUISAWTXAAHYQCBABYQDEGHIKYRMLNOXBPXDXEXF $. $} ${ @@ -289804,8 +289808,8 @@ Additional definitions for (multivariate) polynomials NDEFGVPWPIXBTZWPTZXGTADFOXCJVDZABVPOXCKVDAGDOXCLVDZAXCVEVFVGVHVIXDWTXFWRX EUHRZNSXDNUCXEWRDFGURQPVJMOZURWRUEMSVKQWRPURWRTZVLVMVNXNWRVOOXDVKQWRPXOVQ VRXKXLXETNWRVSMZOXDNQXPVTXNQXPSVKQWRPXOWAVNWFWGWBXFWSXMNWNXEWRUHWCVGWDWHW - EADBWIRZVSMZXBXQBUBCDNFVPWMWPUAHXQTZXRTZXJXIJKNQOAVTWGAXRXQBDEFGXSIXTJKLW - JWKWL $. + EADBWIRZVSMZXBXQBUBCDNWMWPUAHXQTZXRTZXJXINQOAVTWGAXRXQBDEFGXSIXTJKLWJWKWL + $. $} ${ @@ -289884,9 +289888,9 @@ Additional definitions for (multivariate) polynomials VAUGGSUYMVXCYQZVVAUGGVYNVYMVIUXPUYMTSSVWTVYSVYRVVAUGGSUXPVXHYQZVYTYRYRWUA UWJVPUWKUYHVUPVUTUWLUWMVVAVWJVWLUXOVWJVWLUXOUPUQVVAVVBHVVDIUHUWNYPUWOUWPV VBHVVDIUWQUWRUWSYOVPVUQDUWTRZUYLTRVUSUXRUPAWUBUYGVUPAVVSWUBNDUXAXHUXBUYKU - DUYFUYDUBUYESGVBUXCYSYSUYLUCDTUXRVVQUXDYMXNUXHUXEUXFUXGAVUJUYFJDUBFGUXOTX - CUXNUXRUAKLVUKVVQVUMVWSNAHIADFGHBKOYTADFGICKPYTUXIAVUJJEBCVUKMAJDGTLVWSNU - XJVUNVUOUXKUXLUXM $. + DUYFUYDUBUYESGVBUXCYSYSUYLUCDTUXRVVQUXDYMXNUXHUXEUXFUXGAVUJUYFJDUBFGUXOUX + NUXRUAKLVUKVVQVUMAHIADFGHBKOYTADFGICKPYTUXIAVUJJEBCVUKMAJDGTLVWSNUXJVUNVU + OUXKUXLUXM $. $} ${ @@ -289935,17 +289939,16 @@ Additional definitions for (multivariate) polynomials 26-Aug-2023.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.) $) mhpaddcl $p |- ( ph -> ( X .+ Y ) e. ( H ` N ) ) $= - ( vh vg wcel co cvv cbs cfv cv ccnv cima cfn cn0 cmap crab cgrp eqid cmhp - c0g reldmmhp elfvov1 mhprcl mplgrp syl2anc mhpmpl grpcld csupp cun ccnfld - cress cgsu wceq cplusg cof mpladd oveq1d ovexd rabexd grpidcl syl grplidd - cn mplelf suppofssd eqsstrd mhpdeg unssd sstrd ismhp2 ) ABUAUBZPUCUDVPUEU - FRZPUGFUHSZUIZBDQPEFGTUJHICSZDUMUBZJKWDUKZWIUKZWGUKZADEFULHGUNJNUOZMADEFG - HJNUPAWDCBHIWJLAFTRDUJRZBUJRWMMBDFTKUQURAWDBDEFGHJKWJNUSZAWDBDEFGIJKWJOUS - ZUTAWHWIVASZHWIVASZIWIVASZVBZVCUGVDSQUCVESGVFQWGUIZAWQHIDVGUBZVHSZWIVASWT - AWHXCWIVAAWDBXBCDFHIKWJXBUKZLWOWPVIVJAWGDUAUBZHITXBWIAWEPWFWGTWLAUGFUHVKV - LAWNWIXERMXEDWIXEUKZWKVMVNZAWDWGBDPFXEHKXFWJWLWOVQAWDWGBDPFXEIKXFWJWLWPVQ - AXEXBDWIWIXFXDWKMXGVOVRVSAWRWSXAAWGDQPEFGHWIJWKWLNVTAWGDQPEFGIWIJWKWLOVTW - AWBWC $. + ( vh vg wcel co eqid cbs cfv cv ccnv cn cima cfn cn0 cmap crab c0g mhprcl + cvv cgrp reldmmhp elfvov1 mplgrp syl2anc mhpmpl grpcld csupp ccnfld cress + cmhp cun cgsu wceq cplusg cof mpladd oveq1d rabexd grpidcl mplelf grplidd + ovexd syl suppofssd eqsstrd mhpdeg unssd sstrd ismhp2 ) ABUAUBZPUCUDUEUFU + GRZPUHFUISZUJZBDQPEFGHICSZDUKUBZJKWDTZWITZWGTZADEFGHJNULAWDCBHIWJLAFUMRDU + NRZBUNRADEFVDHGUOJNUPMBDFUMKUQURAWDBDEFGHJKWJNUSZAWDBDEFGIJKWJOUSZUTAWHWI + VASZHWIVASZIWIVASZVEZVBUHVCSQUCVFSGVGQWGUJZAWPHIDVHUBZVISZWIVASWSAWHXBWIV + AAWDBXACDFHIKWJXATZLWNWOVJVKAWGDUAUBZHIUMXAWIAWEPWFWGUMWLAUHFUIVPVLAWMWIX + DRMXDDWIXDTZWKVMVQZAWDWGBDPFXDHKXEWJWLWNVNAWDWGBDPFXDIKXEWJWLWOVNAXDXADWI + WIXEXCWKMXFVOVRVSAWQWRWTAWGDQPEFGHWIJWKWLNVTAWGDQPEFGIWIJWKWLOVTWAWBWC $. $} ${ @@ -289959,16 +289962,16 @@ Additional definitions for (multivariate) polynomials (Contributed by SN, 12-Sep-2023.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.) $) mhpinvcl $p |- ( ph -> ( M ` X ) e. ( H ` N ) ) $= - ( vh vg cfv wcel co cvv eqid cbs cv ccnv cima cfn cn0 cmap crab cgrp cmhp - cn c0g reldmmhp elfvov1 mhprcl mplgrp mhpmpl grpinvcld csupp ccnfld cress + ( vh vg cfv wcel co eqid cvv cbs cv ccnv cn cima cfn cn0 cmap crab mhprcl + c0g cgrp cmhp reldmmhp elfvov1 mplgrp mhpmpl grpinvcld csupp ccnfld cress syl2anc cgsu wceq cminusg ccom mplneg oveq1d wfn grpinvfn a1i mplelf ovex rabex fvexd grpinvid syl suppcoss eqsstrd mhpdeg sstrd ismhp2 ) ABUAPZNUB - UCUKUDUEQZNUFEUGRZUHZBCONDEGSUIHFPZCULPZIJWCTZWHTZWFTZACDEUJHGUMIMUNZLACD - EGHIMUOAWCBFHWIKAESQCUIQZBUIQWLLBCESJUPVBAWCBCDEGHIJWIMUQZURAWGWHUSRZHWHU - SRZUTUFVAROUBVCRGVDOWFUHAWOCVEPZHVFZWHUSRWPAWGWRWHUSAWCBCEFWQSHJWIWQTZKWL - LWNVGVHACUAPZWFWQHSSWHWHWQWTVIAWTCWQWTTZWSVJVKAWCWFBCNEWTHJXAWIWKWNVLWFSQ - AWDNWEUFEUGVMVNVKACULVOAWMWHWQPWHVDLCWQWHWJWSVPVQVRVSAWFCONDEGHWHIWJWKMVT - WAWB $. + UCUDUEUFQZNUGEUHRZUIZBCONDEGHFPZCUKPZIJWCSZWHSZWFSZACDEGHIMUJAWCBFHWIKAET + QCULQZBULQACDEUMHGUNIMUOZLBCETJUPVBAWCBCDEGHIJWIMUQZURAWGWHUSRZHWHUSRZUTU + GVAROUBVCRGVDOWFUIAWOCVEPZHVFZWHUSRWPAWGWRWHUSAWCBCEFWQTHJWIWQSZKWMLWNVGV + HACUAPZWFWQHTTWHWHWQWTVIAWTCWQWTSZWSVJVKAWCWFBCNEWTHJXAWIWKWNVLWFTQAWDNWE + UGEUHVMVNVKACUKVOAWLWHWQPWHVDLCWQWHWJWSVPVQVRVSAWFCONDEGHWHIWJWKMVTWAWB + $. $} ${ @@ -290006,18 +290009,18 @@ Additional definitions for (multivariate) polynomials (Contributed by SN, 25-Sep-2023.) Remove closure hypotheses. (Revised by SN, 4-Sep-2025.) $) mhpvscacl $p |- ( ph -> ( X .x. F ) e. ( H ` N ) ) $= - ( vh cfv co vg vk cbs cv ccnv cn cima cfn wcel cn0 cmap crab cvv crg eqid - cmhp reldmmhp elfvov1 mhprcl csca mpllmodd eleqtrdi mplsca fveq2d eleqtrd + ( vh cfv co vg vk cbs cv ccnv cima cfn wcel cn0 cmap crab c0g eqid mhprcl + cn csca cvv cmhp reldmmhp elfvov1 mpllmodd eleqtrdi mplsca fveq2d eleqtrd mhpmpl lmodvscld csupp ccnfld cress cgsu wceq mplelf cdif wa cmulr adantr eldifi adantl mplvscaval ssidd fvexd suppssrg oveq2d 3eqtrd suppss mhpdeg - c0g ringrzd sstrd ismhp2 ) ABUCSZRUDUEUFUGUHUIRUJGUKTULZBCUARFGIUMUNJEDTZ - CWHSZKLWLUOZWOUOZWMUOZACFGUPEIUQKQURZOACFGIEKQUSAJDBUTSZWTUCSZWLBEWPWTUOM - XAUOABCGUMLWSOVAAJCUCSZXAAJHXBPNVBACWTUCABCGUMUNLWSOVCVDVEAWLBCFGIEKLWPQV - FZVGZAWNWOVHTEWOVHTZVIUJVJTUAUDVKTIVLUAWMULAWMHUBWNXEWOAWLWMBCRGHWNLNWPWR - XDVMAUBUDZWMXEVNUIZVOZXFWNSJXFESZCVPSZTJWOXJTZWOXHWLWMBCDXJREGHJXFLMNWPXJ - UOZWRAJHUIXGPVQAEWLUIXGXCVQXGXFWMUIAXFWMXEVRVSVTXHXIWOJXJAWMHUMEIFSXEXFWO - AWLWMBCRGHELNWPWRXCVMAXEWAQACWHWBWCWDAXKWOVLXGAHCXJJWONXLWQOPWIVQWEWFAWMC - UARFGIEWOKWQWRQWGWJWK $. + crg ringrzd sstrd ismhp2 ) ABUCSZRUDUEUOUFUGUHRUIGUJTUKZBCUARFGIJEDTZCULS + ZKLWLUMZWOUMZWMUMZACFGIEKQUNAJDBUPSZWSUCSZWLBEWPWSUMMWTUMABCGUQLACFGUREIU + SKQUTZOVAAJCUCSZWTAJHXBPNVBACWSUCABCGUQWHLXAOVCVDVEAWLBCFGIEKLWPQVFZVGZAW + NWOVHTEWOVHTZVIUIVJTUAUDVKTIVLUAWMUKAWMHUBWNXEWOAWLWMBCRGHWNLNWPWRXDVMAUB + UDZWMXEVNUHZVOZXFWNSJXFESZCVPSZTJWOXJTZWOXHWLWMBCDXJREGHJXFLMNWPXJUMZWRAJ + HUHXGPVQAEWLUHXGXCVQXGXFWMUHAXFWMXEVRVSVTXHXIWOJXJAWMHUQEIFSXEXFWOAWLWMBC + RGHELNWPWRXCVMAXEWAQACULWBWCWDAXKWOVLXGAHCXJJWONXLWQOPWIVQWEWFAWMCUARFGIE + WOKWQWRQWGWJWK $. $} ${ @@ -290095,8 +290098,15 @@ Additional definitions for (multivariate) polynomials ZUIZUIZJJEUMTUPAUABCDEFGHIJKLNOPQRUNVKMULZWEWPULAWQGCWDWOWQIDWCWNWQVNWGWA WMWBWQVMWFUDUEVKMVLUOUQWQVSWLVTWQVQWKVLVRWQBJVPWJWQVOWIUDUGVKMWHURUSUTVAV BVCUTUTVDSAGCWOUPCUPVEACFVFOVHVGVIVJ $. + $} - $d F f k $. $d D f k $. $d X f $. $d ph f $. + ${ + $d I f h k y $. $d R f k $. $d X f k y $. $d B f $. $d F f k $. + $d D f k $. $d ph f $. + psdval.s $e |- S = ( I mPwSer R ) $. + psdval.b $e |- B = ( Base ` S ) $. + psdval.d $e |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } $. + psdval.x $e |- ( ph -> X e. I ) $. psdval.f $e |- ( ph -> F e. B ) $. $( Evaluate the partial derivative of a power series. (Contributed by SN, 11-Apr-2025.) $) @@ -290104,12 +290114,12 @@ Additional definitions for (multivariate) polynomials ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) $= - ( vf cv cfv c1 caddc co wceq cc0 cif cmpt cof cmg cpsd cvv psdfval oveq2d - fveq1 mpteq2dv adantl wcel ccnv cn cima cfn cn0 cmap rabex2 mptexd fvmptd - ovex a1i ) AUAIHDMHUBZUCUDUEUFZVLBJBUBMUGUDUHUIUJUEUKUFZUAUBZUCZEULUCZUFZ - UJZHDVMVNIUCZVQUFZUJZCMJEUMUFUCUNABCDEFUAGHJKLMNOPQRSUOVOIUGZVSWBUGAWCHDV - RWAWCVPVTVMVQVNVOIUQUPURUSTAHDWAUNDUNUTAGUBVAVBVCVDUTGVEJVFUFDPVEJVFVJVGV - KVHVI $. + ( cfv co cvv wcel vf cv caddc wceq cc0 cif cmpt cof cmg cpsd fveq1 oveq2d + c1 mpteq2dv cmps reldmpsr elbasov syl simpld simprd psdfval ccnv cima cfn + wa cn cn0 cmap ovex rabex2 mptex a1i fvmptd4 ) AUAIHDKHUBZQUMUCRZVNBJBUBK + UDUMUEUFUGUCUHRZUAUBZQZEUIQZRZUGHDVOVPIQZVSRZUGZCKJEUJRQSVQIUDZHDVTWBWDVR + WAVOVSVPVQIUKULUNABCDEFUAGHJSSKLMNAJSTZESTZAICTWEWFVEPICFUOJEUPLMUQURZUSA + WEWFWGUTOVAPWCSTAHDWBGUBVBVFVCVDTGVGJVHRDNVGJVHVIVJVKVLVM $. $d K k $. $d ph k $. psdcoef.k $e |- ( ph -> K e. D ) $. @@ -290118,94 +290128,90 @@ Additional definitions for (multivariate) polynomials psdcoef $p |- ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` F ) ` K ) = ( ( ( K ` X ) + 1 ) ( .g ` R ) ( F ` ( K oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) $= - ( vk cv cfv c1 caddc co wceq cc0 cif cmpt cof cmg cvv psdval fveq1 oveq1d - cpsd fvoveq1 oveq12d adantl ovexd fvmptd ) AUBJMUBUCZUDZUEUFUGZVDBIBUCMUH - UEUIUJUKZUFULZUGHUDZEUMUDZUGZMJUDZUEUFUGZJVGVHUGHUDZVJUGZDHMIEURUGUDUDUNA - BCDEFGUBHIKLMNOPQRSTUOVDJUHZVKVOUHAVPVFVMVIVNVJVPVEVLUEUFMVDJUPUQVDJVGHVH - USUTVAUAAVMVNVJVBVC $. + ( cfv c1 co vk cv caddc wceq cc0 cif cmpt cof cmg cpsd cvv oveq1d fvoveq1 + fveq1 oveq12d psdval ovexd fvmptd4 ) AUAJKUAUBZRZSUCTZUSBIBUBKUDSUEUFUGZU + CUHZTHRZEUIRZTKJRZSUCTZJVBVCTHRZVETDHKIEUJTRRUKUSJUDZVAVGVDVHVEVIUTVFSUCK + USJUNULUSJVBHVCUMUOABCDEFGUAHIKLMNOPUPQAVGVHVEUQUR $. $} ${ - $d I h k y $. $d V y $. $d X h y $. $d R k $. $d X k $. $d F k $. - $d ph k $. + $d I h k y $. $d X h y $. $d R k $. $d X k $. $d F k $. $d ph k $. psdcl.s $e |- S = ( I mPwSer R ) $. psdcl.b $e |- B = ( Base ` S ) $. - psdcl.i $e |- ( ph -> I e. V ) $. psdcl.r $e |- ( ph -> R e. Mgm ) $. psdcl.x $e |- ( ph -> X e. I ) $. psdcl.f $e |- ( ph -> F e. B ) $. $( The derivative of a power series is a power series. (Contributed by SN, 11-Apr-2025.) $) psdcl $p |- ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B ) $= - ( vk vh wcel cn0 co cfv vy cv ccnv cn cima cfn cmap crab c1 caddc cc0 cif - wceq cmpt cof cmg cbs cpsd cvv fvexd ovex rabex wa cmgm adantr wf psrbagf - a1i eqid ffvelcdmd nn0p1nn syl psrelbas simpr 1nn0 snifpsrbag psrbagaddcl - adantl sylancl syl2anc mulgnncl syl3anc fmpttd elmapdd psdval 3eltr4d - psrbas ) AOPUBUCUDUEUFQZPRFUGSZUHZHOUBZTZUIUJSZWKUAFUAUBHUMUIUKULUNZUJUOS - ZETZCUPTZSZUNZCUQTZWJUGSEHFCURSTTBAWTWJWSUSUSACUQUTWJUSQAWHPWIRFUGVAVBVHA - OWJWRWTAWKWJQZVCZCVDQZWMUDQZWPWTQWRWTQAXCXALVEXBWLRQXDXBFRHWKXAFRWKVFAWJP - WKFWJVIZVGVRAHFQXAMVEVJWLVKVLXBWJWTWOEAWJWTEVFXAABWJCDPFWTEIWTVIZXEJNVMVE - XBXAWNWJQZWOWJQAXAVNAXGXAAFGQUIRQXGKVOUAWJPFUIGHXEVPVSVEWJPWKWNFXEVQVTVJW - TWQCWMWPXFWQVIWAWBWCWDAUABWJCDPOEFGVDHIJXEKLMNWEABWJCDPFWTGIXFXEJKWGWF $. - $} - - ${ - $d I b d h i k y z $. $d V y $. $d X h y $. $d R k n $. - $d ph d i k n $. $d F k z $. $d X b d i k n z $. + ( vk vh vy wcel cn0 co cfv cvv cv ccnv cn cima cfn cmap crab c1 caddc cc0 + wceq cif cmpt cof cmg cbs cpsd fvexd ovex rabex wa cmgm adantr wf psrbagf + eqid adantl ffvelcdmd nn0p1nn psrelbas simpr cmps reldmpsr strov2rcl 1nn0 + a1i snifpsrbag sylancl psrbagaddcl syl2anc mulgnncl syl3anc fmpttd psdval + syl elmapdd psrbas 3eltr4d ) AMNUAUBUCUDUEPZNQFUFRZUGZGMUAZSZUHUIRZWLOFOU + AGUKUHUJULUMZUIUNRZESZCUOSZRZUMZCUPSZWKUFREGFCUQRSSBAXAWKWTTTACUPURWKTPAW + INWJQFUFUSUTVPAMWKWSXAAWLWKPZVAZCVBPZWNUCPZWQXAPWSXAPAXDXBJVCXCWMQPXEXCFQ + GWLXBFQWLVDAWKNWLFWKVFZVEVGAGFPXBKVCVHWMVIWEXCWKXAWPEAWKXAEVDXBABWKCDNFXA + EHXAVFZXFILVJVCXCXBWOWKPZWPWKPAXBVKAXHXBAFTPZUHQPXHAEBPXILBCDVLFEHIVMVNWE + ZVOOWKNFUHTGXFVQVRVCWKNWLWOFXFVSVTVHXAWRCWNWQXGWRVFWAWBWCWFAOBWKCDNMEFGHI + XFKLWDABWKCDNFXATHXGXFIXJWGWH $. + $} + + ${ + $d I b d h i k y z $. $d X h y $. $d R k n $. $d ph d i k n $. + $d F k z $. $d X b d i k n z $. psdmplcl.p $e |- P = ( I mPoly R ) $. psdmplcl.b $e |- B = ( Base ` P ) $. - psdmplcl.i $e |- ( ph -> I e. V ) $. psdmplcl.r $e |- ( ph -> R e. Mnd ) $. psdmplcl.x $e |- ( ph -> X e. I ) $. psdmplcl.f $e |- ( ph -> F e. B ) $. $( The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025.) $) psdmplcl $p |- ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B ) $= - ( vk vh co cfv wcel cn0 vy vz vb vd vi cpsd cmps cbs c0g cfsupp eqid cmnd - vn wbr cmgm mndmgm syl mplbasss sselid psdcl cv ccnv cn cima cmap crab c1 - cfn caddc wceq cc0 cif cmpt cof cmg psdval cvv ovex rabex a1i mptexd wfun - fvexd funmpt csupp ccom wa simpr psrbagsn adantr psrbagaddcl eqidd mplelf - syl2anc feqmptd fveq2 fmptco mplelsfi wf cmin cid cres wf1 fmpttd crn wfn - fnmpti dffn3 sylib fcod fnresi psrbagf adantl ffvelcdmda nn0cnd cc ax-1cn - ffnd 0cn ifcli pncand mpteq2dva 1ex c0ex ifex inidm weq eqeq1 ifbid ofval - fvmptd3 offval 3eqtr4d adantlr fvco3d oveq1 ovexd fveq2d 3eqtrd fvresi - eqfnfvd fcof1 eqbrtrrd fsuppimpd ssidd mulgnn0z sylan ffvelcdmd peano2nn0 - fsuppco suppssov2 ssfid isfsuppd eqbrtrd mplelbas sylanbrc ) AEHFDUFQRRZF - DUGQZUHRZSUUQDUIRZUJUNUUQBSAUUSDUUREFGHUURUKZUUSUKZKADULSZDUOSLDUPUQZMABU - USEUUSCDUURBFIUVAJUVBURNUSZUTAUUQOPVAVBVCVDVHSZPTFVEQZVFZHOVAZRZVGVIQZUVI - UAFUAVAZHVJZVGVKVLZVMZVIVNZQZERZDVORZQZVMZUUTUJAUAUUSUVHDUURPOEFGUOHUVAUV - BUVHUKZKUVDMUVEVPAUWAVQVQUUTAOUVHUVTVQUVHVQSAUVFPUVGTFVEVRVSVTWAADUIWCZUW - AWBAOUVHUVTWDVTAOUVHUVRVMZUUTWEQZUWAUUTWEQAUWDUUTAEOUVHUVQVMZWFUWDUUTUJAO - UBUVHUVHUVQUBVAZERUVRUWFEAUVIUVHSZWGZUWHUVOUVHSZUVQUVHSZAUWHWHAUWJUWHAFGS - ZUWJKUAUVHPFHGUWBWIUQZWJUVHPUVIUVOFUWBWKWNZAUWFWLAUBUVHDUHRZEABUVHCDPFUWO - EIUWOUKZJUWBNWMWOUWGUVQEWPWQAEUWFBVQUVHUVHUUTABCDEFULUUTIJUUTUKZNLWRAUVHU - VHUWFWSUCUVHUCVAZUVOWTVNZQZVMZUWFWFZXAUVHXBZVJUVHUVHUWFXCAOUVHUVQUVHUWNXD - ZAUDUVHUXBUXCAUVHUXAXEZUXBAUVHUVHUXEUXAUWFAUXAUVHXFZUVHUXEUXAWSUXFAUCUVHU - WTUXAUWRUVOUWSVRUXAUKZXGVTUVHUXAXHXIUXDXJXRUXCUVHXFAUVHXKVTAUDVAZUVHSZWGZ - UXHUVOUVPQZUVOUWSQZUXHUXHUXBRZUXHUXCRZUXJUEFUEVAZUXHRZUXOHVJZVGVKVLZVIQZU - XRWTQZVMUEFUXPVMUXLUXHUXJUEFUXTUXPUXJUXOFSZWGZUXPUXRUYBUXPUXJFTUXOUXHUXIF - TUXHWSAUVHPUXHFUWBXLZXMZXNXOUXRXPSUYBUXQVGVKXPXQXSXTVTYAYBUXJUEFFUXSUXRWT - FUXKUVOGGUXJUXKUVHSZUXKFXFUXJUXIUWJUYEAUXIWHZAUWJUXIUWMWJUVHPUXHUVOFUWBWK - WNZUYEFTUXKUVHPUXKFUWBXLXRUQUVOFXFUXJUAFUVNUVOUVMVGVKYCYDYEUVOUKZXGVTZAUW - LUXIKWJZUYJFYFZUXJFFUXPUXRVIFUXHUVOGGUXOUXIUXHFXFAUXIFTUXHUYCXRXMUYIUYJUY - JUYKUYBUXPWLUYBUAUXOUVNUXRFUVOVQUYHUAUEYGUVMUXQVGVKUVLUXOHYHYIUXJUYAWHUXR - VQSUYBUXQVGVKYCYDYEVTYKZYJUYLYLUXJUEFTUXHUYDWOYMUXJUXMUXHUWFRZUXARUXKUXAR - UXLUXJUVHUVHUXHUXAUWFUXJOUVHUVQUVHAUWHUWKUXIUWNYNXDUYFYOUXJUYMUXKUXAUXJOU - XHUVQUXKUVHUWFVQUWFUKUVIUXHUVOUVPYPUYFUXJUXHUVOUVPYQYKYRUXJUCUXKUWTUXLUVH - UXAVQUXGUWRUXKUVOUWSYPUYGUXJUXKUVOUWSYQYKYSUXIUXNUXHVJAUVHUXHYTXMYMUUAUVH - UVHUXAUWFUUBWNUWCNUUJUUCUUDAOUMUVKUVRUVHTUWEUVSVQVQUUTUUTAUWEUUEAUVCUMVAZ - TSUYNUUTUVSQUUTVJLUWOUVSDUYNUUTUWPUVSUKUWQUUFUUGUWIUVJTSUVKTSUWIFTHUVIUWH - FTUVIWSAUVHPUVIFUWBXLXMAHFSUWHMWJUUHUVJUUIUQUWIUVQEWCUWCUUKUULUUMUUNUUSCD - UURBFUUQUUTIUVAUVBUWQJUUOUUP $. - $} - - ${ - $d I b d h y $. $d V y $. $d X b d h y $. $d R b d $. $d ph b d $. - $d G b d $. $d F b d $. $d .+ d $. $d B b $. + ( vk vh co cfv wcel eqid cn0 cvv vy vz vb vd cpsd cmps cbs c0g cfsupp wbr + vi vn cmnd cmgm mndmgm syl mplbasss sselid psdcl cv ccnv cn cima cfn cmap + crab c1 caddc wceq cc0 cif cmpt cof cmg psdval ovex rabex a1i mptexd wfun + fvexd funmpt csupp ccom wa reldmmpl strov2rcl psrbagsn adantr psrbagaddcl + simpr cmpl syl2anc eqidd mplelf feqmptd fveq2 fmptco mplelsfi wf cmin cid + cres wf1 fmpttd crn wfn fnmpti dffn3 sylib fcod fnresi psrbagf ffvelcdmda + ffnd adantl nn0cnd cc ax-1cn 0cn ifcli pncand mpteq2dva 1ex c0ex ifex weq + inidm eqeq1 ifbid fvmptd3 ofval offval 3eqtr4d adantlr fvco3d oveq1 ovexd + fveq2d 3eqtrd fvresi eqfnfvd fcof1 fsuppco eqbrtrrd fsuppimpd ssidd sylan + mulgnn0z ffvelcdmd peano2nn0 suppssov2 isfsuppd eqbrtrd mplelbas sylanbrc + ssfid ) AEGFDUEOPPZFDUFOZUGPZQUURDUHPZUIUJUURBQAUUTDUUSEFGUUSRZUUTRZADUMQ + ZDUNQJDUOUPKABUUTEUUTCDUUSBFHUVBIUVCUQLURZUSAUURMNUTVAVBVCVDQZNSFVEOZVFZG + MUTZPZVGVHOZUVIUAFUAUTZGVIZVGVJVKZVLZVHVMZOZEPZDVNPZOZVLZUVAUIAUAUUTUVHDU + USNMEFGUVBUVCUVHRZKUVEVOAUWATTUVAAMUVHUVTTUVHTQAUVFNUVGSFVEVPVQVRVSADUHWA + ZUWAVTAMUVHUVTWBVRAMUVHUVRVLZUVAWCOZUWAUVAWCOAUWDUVAAEMUVHUVQVLZWDUWDUVAU + IAMUBUVHUVHUVQUBUTZEPUVRUWFEAUVIUVHQZWEZUWHUVOUVHQZUVQUVHQZAUWHWKAUWJUWHA + FTQZUWJAEBQUWLLBDCWLFEHIWFWGUPZUAUVHNFGTUWBWHUPZWIUVHNUVIUVOFUWBWJWMZAUWF + WNAUBUVHDUGPZEABUVHCDNFUWPEHUWPRZIUWBLWOWPUWGUVQEWQWRAEUWFBTUVHUVHUVAABCD + EFUVAHIUVARZLWSAUVHUVHUWFWTUCUVHUCUTZUVOXAVMZOZVLZUWFWDZXBUVHXCZVIUVHUVHU + WFXDAMUVHUVQUVHUWOXEZAUDUVHUXCUXDAUVHUXBXFZUXCAUVHUVHUXFUXBUWFAUXBUVHXGZU + VHUXFUXBWTUXGAUCUVHUXAUXBUWSUVOUWTVPUXBRZXHVRUVHUXBXIXJUXEXKXOUXDUVHXGAUV + HXLVRAUDUTZUVHQZWEZUXIUVOUVPOZUVOUWTOZUXIUXIUXCPZUXIUXDPZUXKUKFUKUTZUXIPZ + UXPGVIZVGVJVKZVHOZUXSXAOZVLUKFUXQVLUXMUXIUXKUKFUYAUXQUXKUXPFQZWEZUXQUXSUY + CUXQUXKFSUXPUXIUXJFSUXIWTAUVHNUXIFUWBXMZXPZXNXQUXSXRQUYCUXRVGVJXRXSXTYAVR + YBYCUXKUKFFUXTUXSXAFUXLUVOTTUXKUXLUVHQZUXLFXGUXKUXJUWJUYFAUXJWKZAUWJUXJUW + NWIUVHNUXIUVOFUWBWJWMZUYFFSUXLUVHNUXLFUWBXMXOUPUVOFXGUXKUAFUVNUVOUVMVGVJY + DYEYFUVORZXHVRZAUWLUXJUWMWIZUYKFYHZUXKFFUXQUXSVHFUXIUVOTTUXPUXJUXIFXGAUXJ + FSUXIUYDXOXPUYJUYKUYKUYLUYCUXQWNUYCUAUXPUVNUXSFUVOTUYIUAUKYGUVMUXRVGVJUVL + UXPGYIYJUXKUYBWKUXSTQUYCUXRVGVJYDYEYFVRYKZYLUYMYMUXKUKFSUXIUYEWPYNUXKUXNU + XIUWFPZUXBPUXLUXBPUXMUXKUVHUVHUXIUXBUWFUXKMUVHUVQUVHAUWHUWKUXJUWOYOXEUYGY + PUXKUYNUXLUXBUXKMUXIUVQUXLUVHUWFTUWFRUVIUXIUVOUVPYQUYGUXKUXIUVOUVPYRYKYSU + XKUCUXLUXAUXMUVHUXBTUXHUWSUXLUVOUWTYQUYHUXKUXLUVOUWTYRYKYTUXJUXOUXIVIAUVH + UXIUUAXPYNUUBUVHUVHUXBUWFUUCWMUWCLUUDUUEUUFAMULUVKUVRUVHSUWEUVSTTUVAUVAAU + WEUUGAUVDULUTZSQUYOUVAUVSOUVAVIJUWPUVSDUYOUVAUWQUVSRUWRUUIUUHUWIUVJSQUVKS + QUWIFSGUVIUWHFSUVIWTAUVHNUVIFUWBXMXPAGFQUWHKWIUUJUVJUUKUPUWIUVQEWAUWCUULU + UQUUMUUNUUTCDUUSBFUURUVAHUVBUVCUWRIUUOUUP $. + $} + + ${ + $d I b d h y $. $d X b d h y $. $d R b d $. $d ph b d $. $d G b d $. + $d F b d $. $d .+ d $. $d B b $. psdadd.s $e |- S = ( I mPwSer R ) $. psdadd.b $e |- B = ( Base ` S ) $. psdadd.p $e |- .+ = ( +g ` S ) $. - psdadd.i $e |- ( ph -> I e. V ) $. psdadd.r $e |- ( ph -> R e. CMnd ) $. psdadd.x $e |- ( ph -> X e. I ) $. psdadd.f $e |- ( ph -> F e. B ) $. @@ -290214,31 +290220,31 @@ Additional definitions for (multivariate) polynomials SN, 12-Apr-2025.) $) psdadd $p |- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( F .+ G ) ) = ( ( ( ( I mPSDer R ) ` X ) ` F ) .+ ( ( ( I mPSDer R ) ` X ) ` G ) ) ) $= - ( co cfv vd vh vy vb cpsd cplusg cof cv ccnv cn cima cfn wcel cn0 cmap c1 - crab caddc wceq cc0 cif cmpt cmg ccmn eqid psdval oveq12d cvv ovex fnmpti - wfn a1i rabex inidm wa weq fveq1 oveq1d fvoveq1 simpr ovexd offval psradd - fvmptd3 adantr fveq1d psrbagsn syl psrbagaddcl syl2anc cbs psrelbas eqidd - ofval syldan eqtrd oveq2d wf psrbagf adantl ffvelcdmd peano2nn0 mulgnn0di - ffnd syl13anc eqtr2d mpteq2dva 3eqtrd cmnd cmgm cmnmndd psraddcl 3eqtr4rd - mndmgm psdcl ) AFJHDUESTZTZGXPTZDUFTZUGZSZUAUBUHUIUJUKULUMZUBUNHUOSZUQZJU - AUHZTZUPURSZYEUCHUCUHJUSUPUTVAVBZURUGZSZFGCSZTZDVCTZSZVBZXQXRCSYKXPTAYAUD - YDJUDUHZTZUPURSZYPYHYISZFTZYMSZVBZUDYDYRYSGTZYMSZVBZXTSUAYDYGYJFTZYMSZYGY - JGTZYMSZXSSZVBYOAXQUUBXRUUEXTAUCBYDDEUBUDFHIVDJKLYDVEZNOPQVFAUCBYDDEUBUDG - HIVDJKLUUKNOPRVFVGAUAYDYDUUGUUIXSYDUUBUUEVHVHUUBYDVKAUDYDUUAUUBYRYTYMVIUU - BVEZVJVLUUEYDVKAUDYDUUDUUEYRUUCYMVIUUEVEZVJVLYDVHUMAYBUBYCUNHUOVIVMVLZUUN - YDVNZAYEYDUMZVOZUDYEUUAUUGYDUUBVHUULUDUAVPZYRYGYTUUFYMUURYQYFUPURJYPYEVQV - RZYPYEYHFYIVSVGAUUPVTZUUQYGUUFYMWAWDUUQUDYEUUDUUIYDUUEVHUUMUURYRYGUUCUUHY - MUUSYPYEYHGYIVSVGUUTUUQYGUUHYMWAWDWBAUAYDUUJYNUUQYNYGUUFUUHXSSZYMSZUUJUUQ - YLUVAYGYMUUQYLYJFGXTSZTZUVAUUQYJYKUVCAYKUVCUSUUPABXSCDEHFGKLXSVEZMQRWCWEW - FAUUPYJYDUMZUVDUVAUSUUQUUPYHYDUMZUVFUUTAUVGUUPAHIUMUVGNUCYDUBHJIUUKWGWHWE - YDUBYEYHHUUKWIWJZAYDYDUUFUUHXSYDFGVHVHYJAYDDWKTZFABYDDEUBHUVIFKUVIVEZUUKL - QWLXDAYDUVIGABYDDEUBHUVIGKUVJUUKLRWLZXDUUNUUNUUOAUVFVOZUUFWMUVLUUHWMWNWOW - PWQUUQDVDUMZYGUNUMZUUFUVIUMUUHUVIUMUVBUUJUSAUVMUUPOWEUUQYFUNUMUVNUUQHUNJY - EUUPHUNYEWRAYDUBYEHUUKWSWTAJHUMUUPPWEXAYFXBWHUUQYDUVIYJFUUQBYDDEUBHUVIFKU - VJUUKLAFBUMUUPQWEWLUVHXAUUQYDUVIYJGAYDUVIGWRUUPUVKWEUVHXAUVIXSYMDYGUUFUUH - UVJYMVEUVEXCXEXFXGXHABXSCDEHXQXRKLUVEMABDEFHIJKLNADXIUMDXJUMADOXKDXNWHZPQ - XOABDEGHIJKLNUVOPRXOWCAUCBYDDEUBUAYKHIVDJKLUUKNOPABCDEHFGKLMUVOQRXLVFXM - $. + ( vh co cfv wcel vd vy vb cpsd cplusg cof cv ccnv cn cima cfn cn0 cmap c1 + crab caddc wceq cc0 cif cmpt cmg eqid psdval oveq12d cvv wfn fnmpti rabex + ovex a1i inidm weq fveq1 oveq1d fvoveq1 simpr ovexd fvmptd3 offval psradd + wa adantr fveq1d cmps reldmpsr strov2rcl syl psrbagsn psrbagaddcl syl2anc + cbs psrelbas ffnd eqidd ofval syldan oveq2d ccmn psrbagf adantl ffvelcdmd + wf peano2nn0 mulgnn0di syl13anc eqtr2d mpteq2dva 3eqtrd cmnd cmgm cmnmndd + eqtrd mndmgm psdcl psraddcl 3eqtr4rd ) AFIHDUDRSZSZGXQSZDUESZUFZRZUAQUGUH + UIUJUKTZQULHUMRZUOZIUAUGZSZUNUPRZYFUBHUBUGIUQUNURUSUTZUPUFZRZFGCRZSZDVASZ + RZUTZXRXSCRYLXQSAYBUCYEIUCUGZSZUNUPRZYQYIYJRZFSZYNRZUTZUCYEYSYTGSZYNRZUTZ + YARUAYEYHYKFSZYNRZYHYKGSZYNRZXTRZUTYPAXRUUCXSUUFYAAUBBYEDEQUCFHIJKYEVBZNO + VCAUBBYEDEQUCGHIJKUULNPVCVDAUAYEYEUUHUUJXTYEUUCUUFVEVEUUCYEVFAUCYEUUBUUCY + SUUAYNVIUUCVBZVGVJUUFYEVFAUCYEUUEUUFYSUUDYNVIUUFVBZVGVJYEVETAYCQYDULHUMVI + VHVJZUUOYEVKZAYFYETZWAZUCYFUUBUUHYEUUCVEUUMUCUAVLZYSYHUUAUUGYNUUSYRYGUNUP + IYQYFVMVNZYQYFYIFYJVOVDAUUQVPZUURYHUUGYNVQVRUURUCYFUUEUUJYEUUFVEUUNUUSYSY + HUUDUUIYNUUTYQYFYIGYJVOVDUVAUURYHUUIYNVQVRVSAUAYEUUKYOUURYOYHUUGUUIXTRZYN + RZUUKUURYMUVBYHYNUURYMYKFGYARZSZUVBUURYKYLUVDAYLUVDUQUUQABXTCDEHFGJKXTVBZ + LOPVTWBWCAUUQYKYETZUVEUVBUQUURUUQYIYETZUVGUVAAUVHUUQAHVETZUVHAFBTZUVIOBDE + WDHFJKWEWFWGUBYEQHIVEUULWHWGWBYEQYFYIHUULWIWJZAYEYEUUGUUIXTYEFGVEVEYKAYED + WKSZFABYEDEQHUVLFJUVLVBZUULKOWLWMAYEUVLGABYEDEQHUVLGJUVMUULKPWLZWMUUOUUOU + UPAUVGWAZUUGWNUVOUUIWNWOWPXLWQUURDWRTZYHULTZUUGUVLTUUIUVLTUVCUUKUQAUVPUUQ + MWBUURYGULTUVQUURHULIYFUUQHULYFXBAYEQYFHUULWSWTAIHTUUQNWBXAYGXCWGUURYEUVL + YKFUURBYEDEQHUVLFJUVMUULKAUVJUUQOWBWLUVKXAUURYEUVLYKGAYEUVLGXBUUQUVNWBUVK + XAUVLXTYNDYHUUGUUIUVMYNVBUVFXDXEXFXGXHABXTCDEHXRXSJKUVFLABDEFHIJKADXITDXJ + TADMXKDXMWGZNOXNABDEGHIJKUVRNPXNVTAUBBYEDEQUAYLHIJKUULNABCDEHFGJKLUVROPXO + VCXP $. $} ${ @@ -290248,7 +290254,6 @@ Additional definitions for (multivariate) polynomials psdvsca.b $e |- B = ( Base ` S ) $. psdvsca.m $e |- .x. = ( .s ` S ) $. psdvsca.k $e |- K = ( Base ` R ) $. - psdvsca.i $e |- ( ph -> I e. V ) $. psdvsca.r $e |- ( ph -> R e. CRing ) $. psdvsca.x $e |- ( ph -> X e. I ) $. psdvsca.f $e |- ( ph -> F e. B ) $. @@ -290257,22 +290262,22 @@ Additional definitions for (multivariate) polynomials (Contributed by SN, 12-Apr-2025.) $) psdvsca $p |- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) = ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) ) $= - ( vd vh vy cv ccnv cima cfn wcel cn0 cmap crab cpsd cfv cbs eqid crg cmgm + ( vh wcel vd vy cv ccnv cima cfn cn0 cmap crab cpsd cfv cbs eqid crg cmgm cn co crngringd ringmgm syl psrvscacl psdcl psrelbas ffnd wa c1 caddc cc0 wceq cif cmpt cof cmg cmulr cz adantr wf adantl ffvelcdmd peano2nn0 nn0zd - psrbagf simpr psrbagsn psrbagaddcl syl2anc mulgass3 syl13anc ccrg psdcoef - oveq2d psrvscaval 3eqtr4rd 3eqtr4d eqfnfvd ) AUAUBUDUEURUFUGUHUBUIHUJUSUK - ZCGFUSZKHDULUSUMZUMZCGWTUMZFUSZAWRDUNUMZXAABWRDEUBHXDXALXDUOZWRUOZMABDEWS - HJKLMPADUPUHZDUQUHADQUTZDVAVBZRABDEFGHICLNOMXHTSVCZVDVEVFAWRXDXCABWRDEUBH - XDXCLXEXFMABDEFXBHICLNOMXHTABDEGHJKLMPXIRSVDZVCVEVFAUAUDZWRUHZVGZKXLUMZVH - VIUSZXLUCHUCUDKVKVHVJVLVMZVIVNUSZWSUMZDVOUMZUSZCXLXBUMZDVPUMZUSZXLXAUMXLX - CUMXNCXPXRGUMZXTUSZYCUSZXPCYEYCUSZXTUSZYDYAXNXGXPVQUHZCIUHZYEIUHYGYIVKAXG - XMXHVRXNXOUIUHZYJXNHUIKXLXMHUIXLVSAWRUBXLHXFWDVTAKHUHXMRVRZWAYLXPXOWBWCVB - AYKXMTVRZXNWRIXRGAWRIGVSXMABWRDEUBHIGLOXFMSVEVRXNXMXQWRUHZXRWRUHAXMWEZAYO - XMAHJUHZYOPUCWRUBHKJXFWFVBVRWRUBXLXQHXFWGWHZWAIDXTYCXPCYEOXTUOYCUOZWIWJXN - YBYFCYCXNUCBWRDEUBGHXLJWKKLMXFAYQXMPVRZADWKUHXMQVRZYMAGBUHXMSVRZYPWLWMXNX - SYHXPXTXNBWRDEFYCUBGHICXRLNOMYSXFYNUUBYRWNWMWOXNUCBWRDEUBWSHXLJWKKLMXFYTU - UAYMAWSBUHXMXJVRYPWLXNBWRDEFYCUBXBHICXLLNOMYSXFYNAXBBUHXMXKVRYPWNWPWQ $. + psrbagf cvv cmps reldmpsr strov2rcl psrbagsn psrbagaddcl syl2anc mulgass3 + simpr syl13anc psdcoef oveq2d psrvscaval 3eqtr4rd 3eqtr4d eqfnfvd ) AUASU + CUDUPUEUFTSUGHUHUQUIZCGFUQZJHDUJUQUKZUKZCGXAUKZFUQZAWSDULUKZXBABWSDESHXEX + BKXEUMZWSUMZLABDEWTHJKLADUNTZDUOTADOURZDUSUTZPABDEFGHICKMNLXIRQVAZVBVCVDA + WSXEXDABWSDESHXEXDKXFXGLABDEFXCHICKMNLXIRABDEGHJKLXJPQVBZVAVCVDAUAUCZWSTZ + VEZJXMUKZVFVGUQZXMUBHUBUCJVIVFVHVJVKZVGVLUQZWTUKZDVMUKZUQZCXMXCUKZDVNUKZU + QZXMXBUKXMXDUKXOCXQXSGUKZYAUQZYDUQZXQCYFYDUQZYAUQZYEYBXOXHXQVOTZCITZYFITY + HYJVIAXHXNXIVPXOXPUGTZYKXOHUGJXMXNHUGXMVQAWSSXMHXGWBVRAJHTXNPVPZVSYMXQXPV + TWAUTAYLXNRVPZXOWSIXSGAWSIGVQXNABWSDESHIGKNXGLQVCVPXOXNXRWSTZXSWSTAXNWKZA + YPXNAHWCTZYPAGBTZYRQBDEWDHGKLWEWFUTUBWSSHJWCXGWGUTVPWSSXMXRHXGWHWIZVSIDYA + YDXQCYFNYAUMYDUMZWJWLXOYCYGCYDXOUBBWSDESGHXMJKLXGYNAYSXNQVPZYQWMWNXOXTYIX + QYAXOBWSDEFYDSGHICXSKMNLUUAXGYOUUBYTWOWNWPXOUBBWSDESWTHXMJKLXGYNAWTBTXNXK + VPYQWMXOBWSDEFYDSXCHICXMKMNLUUAXGYOAXCBTXNXLVPYQWOWQWR $. $} ${ @@ -290295,7 +290300,6 @@ Additional definitions for (multivariate) polynomials psdmul.b $e |- B = ( Base ` S ) $. psdmul.p $e |- .+ = ( +g ` S ) $. psdmul.m $e |- .x. = ( .r ` S ) $. - psdmul.i $e |- ( ph -> I e. V ) $. psdmul.r $e |- ( ph -> R e. CRing ) $. psdmul.x $e |- ( ph -> X e. I ) $. psdmul.f $e |- ( ph -> F e. B ) $. @@ -290306,285 +290310,283 @@ Additional definitions for (multivariate) polynomials psdmul $p |- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( F .x. G ) ) = ( ( ( ( ( I mPSDer R ) ` X ) ` F ) .x. G ) .+ ( F .x. ( ( ( I mPSDer R ) ` X ) ` G ) ) ) ) $= - ( vd vh vy vu vk vi vq vr vs vb vo vm vn vl cv cn wcel cn0 co crab cfv c1 - caddc wceq cc0 cmpt cle wbr cmin cgsu wa eqid adantr syl syl2anc ad2antrr - simpr wf psrbagf adantl ffvelcdmd psrelbas psrbagconcl ringcld mulgnn0cld - elrabi cin c0 a1i wss wral ffvelcdmda nn0red cr ralrimiva ffnd wfn fnmpti + ( wcel cvv vd vh vy vu vk vi vq vr vs vb vo vm vn vl cv cn cn0 co crab c1 + cfv caddc wceq cc0 cmpt cle wbr cmin cgsu wa eqid adantr syl2anc ad2antrr + simpr syl wf psrbagf adantl ffvelcdmd psrelbas elrabi psrbagconcl ringcld + mulgnn0cld cin c0 a1i wss wral ffvelcdmda nn0red cr ralrimiva ffnd fnmpti offn eqidd ofval ofrfval mpbird wi ovex rabex fndmfifsupp wn breq1 notbid - cvv anbi12d elrab clt nn0cnd addridd oveq2d syl5ibrcom imp simprbi sylan2 + wfn anbi12d elrab clt nn0cnd addridd oveq2d syl5ibrcom imp simprbi sylan2 wrex oveq12d adantrr oveq1d mpteq2dva cc offval mpdan eqtrd fmpttd gsumcl - 3eqtr4d 3eqtrd ccrg wfun eqeq2d ad3antrrr nn0cn cz ccnv cima cfn cmap cif - vv vp cof cmg cofr cdif cmulr cplusg cpsd cbs crngringd ringcmnd psrbagsn - ccmn psrbagaddcl psrbaglefi crnggrpd grpmndd peano2nn0 crg sylan disjdifr - cmnd cun 1nn0 ifcli nn0ge0i nn0rei addge01d mpbii elexi inidm eqeq1 ifbid - 0nn0 weq fvmpt w3a nn0re letr syl3an caoftrn mpan2d ss2rabdv undifr sylib - eqcomd gsummptfidmsplit fvexd gsummulg difrab eleq2i fmpti rexnal bitr4di - c0g cfzo wo wne adantlr nn0nlt0 breq2d biimpd ifnefalse impancom necon1bd - imbi1d ancrd ralimdva anim1d rexim fveq2 breq12d ceqsrexbv ltnled biimpar - ex syldan breq2 syl5ibcom mtod neqned elnnne0 sylanbrc syl3anbrc fzostep1 - elfzo0 iftrue rspcv lensymd intn3an3d sylnibr orcnd sylbida anasss nn0cni - sylan2b subadd23d addsubassd eqtr4d adantll simplr eqeltrrd simpl ss2rabi - eldifi pncan3d 1cnd addassd eqtr3d mulgnn0dir difssd ssfid gsummptfidmadd - syl13anc fveq1 eqeq1d simprd subid1d 3eqtrrd difexi sseli grpassd 3eqtr3d - cgrp psrmulval grpcld psrmulcl psdval grpmgmd psdcl psradd csn ccom df-of - cxp cdm vex ssv elimampo biimpa ffund funfnd ad2antrl velsn funmpt mpbiri - funeq sylbi ad2antll wb elsni addsubass caofass fvmptd3 mpteq2i fconstmpt - dmex subidi eqtr4i oveq2i 0zd caofid0r eqtrid eqeltrd oveq1 eleq1d sylbid - sylbird rexlimdvva mpd mptexd elsng mpofun xpss inex1 rgen2w dmmpoga mp1i - mptex sseqtrrid elovimad syl2an2 feq1 npcand feqmptd impbid f1o2d gsumf1o - 3eqtr4rd oveq2 fveq2d fmptco psdcoef 1ex nn0sscn offveq ad2antlr subsub3d - fssd nn0zd simpllr psrbagleadd1 syl3anc eleq1 mulgass2 snex xpex funimaex - simprl rexbidva rexsng bitr3d nn0p1nn nnne0d neneqd intnand elrabd simpld - jca wif mpbid r19.21bi ad4antr an32s breqtrd nn0ge0d eqbrtrd imnan sylibr - pm2.61ne con2d nnge1d ifpimpda brif1 psrbagcon lesubaddd rspceb2dv 3bitrd - pm2.65d eqrdv eqtr4di eqsstrd fmptssfisupp difss disjdif ssdisj psdmullem - mp2an ineqcomi gsumsplit2 mulgass3 ) AUAUBUOUUAUPUUBUUCUQZUBURIUUDUSZUTZK - UAUOZVAZVBVCUSZWXAUCIUCUOZKVDZVBVEUUEZVFZVCUUHZUSZGHFUSZVAZDUUIVAZUSZVFUA - WWTDUDUEUOZWXIVGUUJZVHZUEWWTUTZWXNWXAWXOVHZUEWWTUTZUUKZKUDUOZVAZWYAGVAZWX - IWYAVIUUHZUSZHVAZDUULVAZUSZWXLUSZVFZVJUSZDUDWXSWXRKWXNVAZVEVDZVKZUEWWTUTZ - UUKZWYIVFZVJUSZDUUMVAZUSZDUDWYPKWXAWYAWYDUSZVAZVBVCUSZWYHWXLUSZVFZVJUSZDU - DWYOXUDVFZVJUSZWYSUSZWYSUSZVFZWXJKIDUUNUSVAZVAGXULVAZHFUSZGHXULVAZFUSZCUS - ZAUAWWTWXMXUJAWXAWWTUQZVKZWXCDUDWXQWYHVFZVJUSZWXLUSZWYKWYRXUIWYSUSZWYSUSZ - WXMXUJXUSDUDWXQWXCWYHWXLUSZVFVJUSDUDWXTXVEVFZVJUSZDUDWXSXVEVFVJUSZWYSUSXV - BXVDXUSWXQDUUOVAZWXTWXSWYSUDDXVEXVIVLZWYSVLZADUUSUQXURADADQUUPZUUQVMZXUSW - XIWWTUQZWXQUUCUQXUSXURWXGWWTUQZXVNAXURVQZAXVOXURAIJUQZXVOPUCWWTUBIKJWWTVL - ZUURVNZVMWWTUBWXAWXGIXVRUUTZVOZUEWWTUBWXIIXVRUVAVNZXUSWYAWXQUQZVKZXVIWXLD - WXCWYHXVJWXLVLZADUVHUQZXURXWCADADQUVBZUVCZVPZXUSWXCURUQZXWCXUSWXBURUQZXWJ - XUSIURKWXAXURIURWXAVRZAWWTUBWXAIXVRVSZVTZAKIUQZXURRVMWAZWXBUVDVNZVMXWDXVI - DWYGWYCWYFXVJWYGVLZADUVEUQZXURXWCXVLVPXWDWWTXVIWYAGAWWTXVIGVRZXURXWCABWWT - DEUBIXVIGLXVJXVRMSWBZVPXWCWYAWWTUQZXUSWXPUEWYAWWTWFZVTWAXWDWWTXVIWYEHAWWT - XVIHVRZXURXWCABWWTDEUBIXVIHLXVJXVRMTWBZVPXWDWYEWXQUQZWYEWWTUQZXUSXVNXWCXX - FXWAUEWWTWXQUBWXIIWYAXVRWXQVLZWCUVFWXPUEWYEWWTWFVNWAWDZWEWXTWXSWGWHVDXUSW - XSWXQUVGWIXUSWXTWXSUVIZWXQXUSWXSWXQWJXXJWXQVDXUSWXRWXPUEWWTXUSWXNWWTUQZVK - ZWXRWXAWXIWXOVHZWXPXUSXXMXXKXUSXXMUFUOZWXAVAZXXOXXNKVDZVBVEUUEZVCUSZVGVHZ - UFIWKXUSXXSUFIXUSXXNIUQZVKZVEXXQVGVHXXSXXQXXPVBVEURUVJUVTUVKZUVLXYAXXOXXQ - XYAXXOXUSIURXXNWXAXWNWLWMXXQWNUQZXYAXXQXYBUVMZWIUVNUVOWOXUSUFIIXXOXXRVGIW - XAWXIJJXUSIURWXAXWNWPZXUSIIVCIWXAWXGJJXYEWXGIWQZXUSUCIWXFWXGWXFURWXEVBVEU - RUVJUVTUVKZUVPWXGVLZWRZWIZAXVQXURPVMZXYKIUVQZWSZXYKXYKXYLXYAXXOWTZXUSIIXX - OXXQVCIWXAWXGJJXXNXYEXYJXYKXYKXYLXYNXXTXXNWXGVAXXQVDZXUSUCXXNWXFXXQIWXGUC - UFUWAWXEXXPVBVEWXDXXNKUVRUVSZXYHXXQURXYBUVPUWBZVTXAXBXCVMXXLUGUHUIIVGURVG - VGWXNWXAWXIJAXVQXURXXKPVPXXKIURWXNVRXUSWWTUBWXNIXVRVSVTXUSXWLXXKXWNVMXUSI - URWXIVRZXXKXUSXVNXYRXWAWWTUBWXIIXVRVSZVNVMUGUOZURUQZUHUOZURUQZUIUOZURUQZU - WCZXYTYUBVGVHYUBYUDVGVHVKXYTYUDVGVHXDZXXLYUAXYTWNUQYUCYUBWNUQYUEYUDWNUQYU - GXYTUWDYUBUWDYUDUWDXYTYUBYUDUWEUWFVTUWGUWHUWIZWXSWXQUWJUWKUWLUWMXUSWXQXVI - WXLUDDWXCXKWYHDUXAVAZXVJYUIVLZXWEWXQXKUQXUSWXPUEWWTWWRUBWWSURIUUDXEXFZXFZ - WIXXIXUSWXQXUTXKYUIXUTWXQWQXUSUDWXQWYHXUTWYCWYFWYGXEXUTVLWRWIXWBXUSDUXAUW - NZXGXVMXWQUWOXUSXVGWYKXVHXVCWYSXUSXVFWYJDVJXUSUDWXTXVEWYIXUSWYAWXTUQZVKWX - CWYBWYHWXLYUNXUSWYAWXPWXRXHZVKZUEWWTUTZUQZWXCWYBVDZWXTYUQWYAWXPWXRUEWWTUW - PUWQYURXUSXXBWYAWXIWXOVHZWYAWXAWXOVHZXHZVKZVKYUSYUPYVCUEWYAWWTUEUDUWAZWXP - YUTYUOYVBWXNWYAWXIWXOXIZYVDWXRYVAWXNWYAWXAWXOXIZXJXLXMXUSXXBYVCYUSXUSXXBV - KZYVCXXNWYAVAZXXRVGVHZUFIWKZYVHXXOVGVHZXHZUFIYBZVKZYUSYVGYUTYVJYVBYVMYVGU - FIIYVHXXRVGIWYAWXIJJXXBWYAIWQZXUSXXBIURWYAWWTUBWYAIXVRVSZWPZVTZXUSWXIIWQZ - XXBXYMVMAXVQXURXXBPVPZYVTXYLYVGXXTVKZYVHWTZYVGIIXXOXXQVCIWXAWXGJJXXNXUSWX - AIWQZXXBXYEVMZAXYFXURXXBAIURWXGIURWXGVRZAUCIURWXFWXGXYHWXFURUQWXDIUQXYGWI - UWRZWIWPZVPYVTYVTXYLYWAXXOWTZXXTXYOYVGXYQVTXAXBYVGYVBYVKUFIWKZXHYVMYVGYVA - YWIYVGUFIIYVHXXOVGIWYAWXAJJYVRYWDYVTYVTXYLYWBYWHXBXJYVKUFIUWSUWTXLYVGYVNV - KZWXCVEWYBUXBUSZUQZYUSYWJWXBYWKUQZYWLYUSUXCYWJXWKWYBUPUQZWXBWYBXNVHZYWMXU - SXWKXXBYVNXWPVPZYWJWYBURUQZWYBVEUXDZYWNYVGYWQYVNAXXBYWQXURAXXBVKIURKWYAXX - BIURWYAVRZAYVPVTAXWOXXBRVMWAUXEZVMZYWJWYBVEYWJWYBVEVDZWXBVEXNVHZYWJXWKYXC - XHYWPWXBUXFVNYWJYWOYXBYXCYVGYVNYVLXXPYVLVKZXDZUFIWKZYVMVKZYWOYVGYVNYXGYVG - YVJYXFYVMYVGYVIYXEUFIYWAYVIYXEYWAYVIVKZYVLXXPYXHYVKXXNKYWAXXNKUXDZYVIYVKY - WAYXIYVIYVKXDZYWAYXJYXIYVHXXOVEVCUSZVGVHZYVKXDYWAYXLYVKYWAYXKXXOYVHVGYWAX - XOYWAXXOYVGIURXXNWXAXUSXWLXXBXWNVMWLXOXPUXGUXHYXIYVIYXLYVKYXIXXRYXKYVHVGY - XIXXQVEXXOVCXXNKVBVEUXIZXQUXGUXLXRXSUXJUXKUXMUYBUXNUXOXSYXGYVGWYBWXBVGVHZ - XHZYWOYXGYXDUFIYBZYXOYXFYVMYXPYVLYXDUFIUXPXSYXPXWOYXOYVLYXOUFKIXXPYVKYXNX - XPYVHWYBXXOWXBVGXXNKWYAUXQZXXNKWXAUXQZUXRZXJUXSXTVNYVGYWOYXOYVGWXBWYBYVGW - XBXUSXWKXXBXWPVMWMYVGWYBYWTWMUXTUYAYAUYCZWYBVEWXBXNUYDUYEUYFUYGWYBUYHZUYI - YXTWXBWYBUYLUYJWXBVEWYBUYKVNYWJXWJYWNWXCWYBXNVHZUWCYWLYWJYYBXWJYWNYWJWYBW - XCYWJWYBYXAWMYWJWXCXUSXWJXXBYVNXWQVPWMYVGYVJWYBWXCVGVHZYVMYVGYVJYYCYVGXWO - YVJYYCXDAXWOXURXXBRVPYVIYYCUFKIXXPYVHWYBXXRWXCVGYXQXXPXXOWXBXXQVBVCYXRXXP - VBVEUYMYCUXRUYNVNXSYDUYOUYPWXCWYBUYLUYQUYRUYSUYTVUBVUBYEYFXQXUSXVHDUDWYPX - VEVFZVJUSZDUDWYOXVEVFZVJUSZWYSUSWYRXUFWYSUSZXUHWYSUSXVCXUSWXSXVIWYPWYOWYS - UDDXVEXVJXVKXVMXURWXSUUCUQAUEWWTUBWXAIXVRUVAVTZXUSWYAWXSUQZVKZXVIWXLDWXCW - YHXVJXWEAXWFXURYYJXWHVPZXUSXWJYYJXWQVMYYKXVIDWYGWYCWYFXVJXWRAXWSXURYYJXVL - VPZYYJXUSXXBWYCXVIUQZWXRUEWYAWWTWFZXUSWWTXVIWYAGAXWTXURXXAVMWLYAZYYKWWTXV - IWYEHAXXDXURYYJXXEVPYYKXUAWXGWXHUSZWYEWWTYYKUFIXXOYVHVIUSZXXQVCUSZVFUFIXX - RYVHVIUSZVFZYYQWYEYYKUFIYYSYYTYYKXXTVKZYYSXXOXXQYVHVIUSVCUSYYTUUUBXXOYVHX - XQUUUBXXOYYKIURXXNWXAXUSXWLYYJXWNVMZWLXOZUUUBYVHYYKIURXXNWYAYYJYWSXUSYYJX - XBYWSYYOYVPVNVTZWLXOZXXQYGUQZUUUBXXQXYBVUAZWIZVUCUUUBXXOXXQYVHUUUDUUUIUUU - FVUDVUEYFYYKUFIIYYRXXQVCIXUAWXGJJYYKIURXUAYYKXUAWWTUQZIURXUAVRXURYYJUUUJA - XURYYJVKXUAWXSUQUUUJUEWWTWXSUBWXAIWYAXVRWXSVLZWCWXRUEXUAWWTWFVNVUFZWWTUBX - UAIXVRVSVNZWPXYFYYKXYIWIZAXVQXURYYJPVPZUUUOXYLYYKIIXXOYVHVIIWXAWYAJJXXNYY - KIURWXAUUUCWPZYYKIURWYAUUUEWPZUUUOUUUOXYLUUUBXXOWTZUUUBYVHWTZXAXXTXYOYYKX - YQVTZYHYYKUFIIXXRYVHVIIWXIWYAJJYYKIURWXIYYKXVNXYRYYKXURXVOXVNAXURYYJVUGAX - VOXURYYJXVSVPZXVTVOXYSVNWPUUUQUUUOUUUOXYLYYKIIXXOXXQVCIWXAWXGJJXXNUUUPUUU - NUUUOUUUOXYLUUURUUUTXAUUUSYHYMZYYKUUUJXVOYYQWWTUQUUULUUVAWWTUBXUAWXGIXVRU - UTVOVUHWAZWDZWEWYPWYOWGWHVDXUSWYOWXSUVGWIZXUSWYPWYOUVIZWXSXUSWYOWXSWJZUUV - FWXSVDUUVGXUSWYNWXRUEWWTWYNWXRXDXXKWXRWYMVUIWIVUJZWIZWYOWXSUWJUWKUWLZUWMX - USYYEYYHYYGXUHWYSXUSYYEDUDWYPWYIXUDWYSUSZVFZVJUSYYHXUSYYDUUVLDVJXUSUDWYPX - VEUUVKXUSWYAWYPUQZVKZXVEWYBXUCVCUSZWYHWXLUSZUUVKUUVNWXCUUVOWYHWXLUUVNWYBX - UBVCUSZVBVCUSWXCUUVOUUVNUUVQWXBVBVCUUVNUUVQWYBWXBWYBVIUSZVCUSWXBUUVNXUBUU - VRWYBVCUUVMXUSYYJXUBUUVRVDZWYAWXSWYOVUKZYYKXWOUUVSAXWOXURYYJRVPZYYKIIWXBW - YBVIIWXAWYAJJKUUUPUUUQUUUOUUUOXYLYYKXWOVKZWXBWTUUWBWYBWTXAYIYAXQUUVNWYBWX - BUUVNWYBUUVMXUSYYJYWQUUVTYYKIURKWYAUUUEUUWAWAZYAZXOZXUSWXBYGUQUUVMXUSWXBX - WPXOVMVULYJYEUUVNWYBXUBVBUUWEUUVNXUBUUVMXUSYYJXUBURUQZUUVTYYKIURKXUAUUUMU - UWAWAZYAXOUUVNVUMVUNVUOYEUUVNXWFYWQXUCURUQZWYHXVIUQZUUVPUUVKVDAXWFXURUUVM - XWHVPUUWDUUVMXUSYYJUUWHUUVTYYKUUWFUUWHUUWGXUBUVDVNZYAUUVMXUSYYJUUWIUUVTUU - VDYAXVIWYSWXLDWYBXUCWYHXVJXWEXVKVUPVUTYJYFXQXUSUDWYPXVIWYIXUDWYSWYQDXUEXV - JXVKXVMXUSWXSWYPYYIXUSWXSWYOVUQVURZUUVMXUSYYJWYIXVIUQZUUVTYYKXVIWXLDWYBWY - HXVJXWEYYLUUWCUUVDWEYAZUUVMXUSYYJXUDXVIUQZUUVTYYKXVIWXLDXUCWYHXVJXWEYYLUU - WJUUVDWEZYAZWYQVLZXUEVLZVUSYJXUSYYFXUGDVJXUSUDWYOXVEXUDXUSWYAWYOUQZVKZWXC - XUCWYHWXLUUWTWXBXUBVBVCUUWTXUBUUVRWXBVEVIUSWXBUUWTXWOUUVSAXWOXURUUWSRVPUU - WTIIWXBWYBVIIWXAWYAJJKXUSYWCUUWSXYEVMUUWSYVOXUSUUWSXXBYVOWYNUEWYAWWTWFYVQ - VNVTAXVQXURUUWSPVPZUUXAXYLUUWTXWOVKZWXBWTUUXBWYBWTXAYIUUWTWYBVEWXBVIUUWSY - XBXUSUUWSYVAYXBUUWSXXBYVAYXBVKZWYNUUXCUEWYAWWTYVDWXRYVAWYMYXBYVFYVDWYLWYB - VEKWXNWYAVVAVVBXLZXMXTVVCVTXQUUWTWXBUUWTWXBXUSXWKUUWSXWPVMXOVVDVVEYEYEYFX - QYCXUSXVIWYSDWYRXUFXUHXVJXVKADVVJUQXURXWGVMZXUSWYPXVIWYQDXKYUIXVJYUJXVMWY - PXKUQXUSWXSWYOWXRUEWWTYUKXFZVVFWIZXUSUDWYPWYIXVIUUWMYKXUSWYPWYQXKYUIWYQWY - PWQXUSUDWYPWYIWYQWYBWYHWXLXEZUUWQWRWIUUWKYUMXGYLZXUSWYPXVIXUEDXKYUIXVJYUJ - XVMUUXGXUSUDWYPXUDXVIUUWPYKXUSWYPXUEXKYUIXUEWYPWQXUSUDWYPXUDXUEXUCWYHWXLX - EZUUWRWRWIUUWKYUMXGYLZXUSWYOXVIXUGDXKYUIXVJYUJXVMWYOXKUQXUSWYNUEWWTYUKXFW - IXUSUDWYOXUDXVIUUWSXUSYYJUUWNWYOWXSWYAUUVHVVGUUWOYAYKXUSWYOXUGXKYUIXUGWYO - WQXUSUDWYOXUDXUGUUXJXUGVLWRWIXUSWXSWYOYYIUUVIVURYUMXGYLZVVHYNYCVVIXUSWXKX - VAWXCWXLXUSUEBWWTDEFWYGUBUDGHIWXILMXWROXVRAGBUQZXURSVMZAHBUQZXURTVMZXWAVV - KXQXUSXVIWYSDWYKWYRXUIXVJXVKUUXEXUSWXTXVIWYJDXKYUIXVJYUJXVMWXTXKUQXUSWXQW - XSYULVVFWIXUSUDWXTWYIXVIYUNXUSXWCUUWLWYAWXQWXSVUKXWDXVIWXLDWYBWYHXVJXWEXW - IXWDIURKWYAXWCYWSXUSXWCXXBYWSXXCYVPVNVTAXWOXURXWCRVPWAXXIWEYAYKXUSWXTWYJX - KYUIWYJWXTWQXUSUDWXTWYIWYJUUXHWYJVLWRWIXUSWXQWXTXWBXUSWXQWXSVUQVURYUMXGYL - UUXIXUSXVIWYSDXUFXUHXVJXVKUUXEUUXKUUXLVVLVVHYMYFAUCBWWTDEUBUAWXJIJYOKLMXV - RPQRABDEFIGHLMOXVLSTVVMVVNAXUQXUNXUPWYSUUHUSXUKABWYSCDEIXUNXUPLMXVKNABDEF - IXUMHLMOXVLABDEGIJKLMPADXWGVVOZRSVVPZTVVMZABDEFIGXUOLMOXVLSABDEHIJKLMPUUX - QRTVVPZVVMZVVQAUAWWTWWTWYTXUIWYSWWTXUNXUPXKXKAWWTXVIXUNABWWTDEUBIXVIXUNLX - VJXVRMUUXSWBWPAWWTXVIXUPABWWTDEUBIXVIXUPLXVJXVRMUUYAWBWPWWTXKUQAYUKWIZUUY - BWWTUVQXUSWXAXUNVADUJWXSUJUOZXUMVAZWXAUUYCWYDUSZHVAZWYGUSZVFZVJUSDUUYHUDW - XHWXSWXGVVRZVWAZUUBZWYAWXGWYDUSZVFZVVSZVJUSZWYTXUSUEBWWTDEFWYGUBUJXUMHIWX - ALMXWROXVRAXUMBUQXURUUXRVMUUXPXVPVVKXUSWXSXVIUUYKUUYHDUUYMXKYUIXVJYUJXVMW - XSXKUQXUSUUXFWIXUSUJWXSUUYGXVIXUSUUYCWXSUQZVKZXVIDWYGUUYDUUYFXVJXWRAXWSXU - RUUYPXVLVPUUYPXUSUUYCWWTUQUUYDXVIUQWXRUEUUYCWWTWFXUSWWTXVIUUYCXUMAWWTXVIX - UMVRXURABWWTDEUBIXVIXUMLXVJXVRMUUXRWBVMWLYAUUYQWWTXVIUUYEHAXXDXURUUYPXXEV - PUUYQUUYEWXSUQZUUYEWWTUQXURUUYPUUYRAUEWWTWXSUBWXAIUUYCXVRUUUKWCVUFWXRUEUU - YEWWTWFVNWAWDYKXUSWXSUUYHXKYUIUUYHWXSWQXUSUJWXSUUYGUUYHUUYDUUYFWYGXEUUYHV - LWRWIYYIYUMXGXUSUDUUFUUYKWXSUUYLUUFUOZWXGWXHUSZUUYMUUYMVLXUSWYAUUYKUQZVKZ - WYAUKULUOZVWBZUMUOZVWBZWGZUKUOZUVUCVAZUVUHUVUEVAZVCUSZVFZVDZUMUUYIYBZULWX - SYBZUUYLWXSUQZXUSUVUAUVUOXUSULUMXKXKUVULWYAWXHXKWXSUUYIUKVCULUMVVTZWYAXKU - QXUSUDVWCWIWXSXKWJXUSWXSVWDWIUUYIXKWJXUSUUYIVWDWIVWEZVWFZUVUBUVUMUVUPULUM - WXSUUYIUVUBUVUCWXSUQZUVUEUUYIUQZVKZVKZUVUMWYAUVUCUVUEWXHUSZVDZUVUPUVVCUVV - DUVULWYAUVVCUKUVUDUVUFUVUIUVUJVCUVUGUVUCUVUEXKXKUVUTUVUCUVUDWQZUVUBUVVAUV - UTUVUCUVUTUVUCWWTUQZUVUCYPWXRUEUVUCWWTWFZUVVGIURUVUCWWTUBUVUCIXVRVSZVWGVN - VWHZVWIUVVAUVUEUVUFWQZUVUBUVUTUVVAUVUEWXGVDZUVVKUMWXGVWJUVVLUVUEUVVLUVUEY - PWXGYPUCIWXFVWKUVUEWXGVWMVWLVWHVWNZVWOUVUDXKUQZUVVCUVUCULVWCVXCZWIUVUFXKU - QZUVVCUVUEUMVWCVXCZWIUVUGVLZUVVCUVUHUVUDUQZVKUVUIWTUVVCUVUHUVUFUQZVKUVUJW - TYHYQZUVVCUVVEWYAUVUCWXGWXHUSZVDZUVUPUVVAUVVEUVWCVWPUVUBUVUTUVVAUVVDUVWBW - YAUVVAUVUEWXGUVUCWXHUVUEWXGVWQXQYQVWOZUVUBUVUTUVWCUVUPXDZUVVAUVUBUVUTVKZU - VUPUVWCUVWBWXGWYDUSZWXSUQZUVWFUVWGUVUCWXSUVWFUVWGUVUCWXGWXGWYDUSZWXHUSZUV - UCUFIXXQXXQVIUSZVFZWXHUSZUVUCUVWFUGUHUIIVIVCURVIUVUCWXGWXGVCJAXVQXURUVUAU - VUTPYRZUVUTIURUVUCVRZUVUBUVUTUVVGUVWOUVVHUVVIVNZVTZYWEUVWFYWFWIZUVWRYUFXY - TYUBVCUSYUDVIUSXYTYUBYUDVIUSVCUSVDZUVWFYUAXYTYGUQYUCYUBYGUQYUEYUDYGUQUVWS - XYTYSZYUBYSYUDYSXYTYUBYUDVWRUWFZVTVWSZAUVWJUVWMVDXURUVUAUVUTAUVWIUVWLUVUC - WXHAUFIIXXQXXQVIIWXGWXGJJYWGYWGPPXYLAXXTVKZUCXXNWXFXXQIWXGURXYHXYPAXXTVQX - XQURUQUVXCXYBWIVWTZUVXDYHXQYRZUVWFUVWMUVUCIVEVVRVWAZWXHUSZUVUCUVWLUVXFUVU - CWXHUVWLUFIVEVFUVXFUFIUVWKVEXXQUUUHVXDVXAUFIVEVXBVXEZVXFZUVWFUGIVEVCURUVU - CJYTUVWNUVWQUVWFVXGZYUAXYTVEVCUSXYTVDUVWFYUAXYTUVWTXPVTVXHVXIYNUVUBUVUTVQ - ZVXJUVWCUUYLUVWGWXSWYAUVWBWXGWYDVXKVXLZXRYDVXMVXNVXOVXPXUSUUYSWXSUQZVKZUU - YSWXGWXSUUYIWXHXUSUVXMVQAWXGUUYIUQZXURUVXMAUVXOWXGWXGVDZXYHAWXGXKUQUVXOUV - XPVWPAUCIWXFJPVXQWXGWXGXKVXRVNVWLVPWXHYPZUVXNULUMXKXKUVULWXHUVUQVXSZWIUVX - NXKXKVWAZUUYJWXHVWBZWXSUUYIVXTUVULXKUQZUMXKWKULXKWKUVXTUVXSVDUVXNUVYAULUM - XKXKUKUVUGUVUKUVUDUVUFUVVOVYAVYEVYBULUMXKXKUVULWXHXKUVUQVYCVYDVYFVYGXUSUV - UAUVXMVKZVKZWYAUUYTVDZUUYSUUYLVDZUVYCUVYEUVYDUUYSUUYTWXGWYDUSZVDUVYCUVYFU - UYSUVWIWXHUSUUYSUVWLWXHUSZUUYSUVYCUGUHUIIVIVCURVIUUYSWXGWXGVCJAXVQXURUVYB - PVPZUVXMIURUUYSVRZXUSUVUAUVXMUUYSWWTUQUVYIWXRUEUUYSWWTWFWWTUBUUYSIXVRVSVN - VWOZYWEUVYCYWFWIZUVYKYUFUVWSUVYCUVXAVTVWSUVYCUVWIUVWLUUYSWXHUVYCUFIIXXQXX - QVIIWXGWXGJJAXYFXURUVYBYWGVPZUVYLUVYHUVYHXYLXXTXYOUVYCXYQVTZUVYMYHXQUVYCU - VYGUUYSUVXFWXHUSUUYSUVWLUVXFUUYSWXHUVXHVXFUVYCUUGIVEVCURUUYSJYTUVYHUVYJUV - YCVXGUUGUOZURUQZUVYNVEVCUSUVYNVDZUVYCUVYOUVYNUVYNYSXPZVTVXHVXIVVEUVYDUUYL - UVYFUUYSWYAUUYTWXGWYDVXKYQXRUVYCUVYDUVYEWYAUUYLWXGWXHUSZVDZUVYCUFIYVHXXQV - IUSZXXQVCUSZVFZUFIYVHVFZUVYRWYAUVYCUFIUWUAYVHUVYCXXTVKZYVHXXQUWUDYVHUVYCI - URXXNWYAXUSUVUAYWSUVXMUVUBUVUOYWSUVUSUVUBUVUMYWSULUMWXSUUYIUVVCUVUMUVVEYW - SUVWAUVVCUVVEUVWCYWSUVWDUVVCYWSUVWCIURUVWBVRZUVUBUVUTUWUEUVVAUVWFUVWBWWTU - QZUWUEUVUTUVVGUVUBXVOUWUFUVVHAXVOXURUVUAUVUTXVSYRWWTUBUVUCWXGIXVRUUTZVYHW - WTUBUVWBIXVRVSVNYDIURWYAUVWBVYIXRVXMVXNVXOVXPZYDZWLXOUUUGUWUDUUUHWIVYJYFU - VYCUFIIUVYTXXQVCIUUYLWXGJJUVYCIIVIIWYAWXGJJUVYCIURWYAUWUIWPZUVYLUVYHUVYHX - YLWSUVYLUVYHUVYHXYLUVYCIIYVHXXQVIIWYAWXGJJXXNUWUJUVYLUVYHUVYHXYLUWUDYVHWT - UVYMXAUVYMYHUVYCUFIURWYAUWUIVYKVYOUVYEUUYTUVYRWYAUUYSUUYLWXGWXHVXKYQXRVYL - VYMVYNXUSUUYODUDUUYKWYIVFZVJUSWYTXUSUUYNUWUKDVJXUSUUYNUDUUYKUUYLXUMVAZWXA - UUYLWYDUSZHVAZWYGUSZVFUWUKXUSUDUJUUYKWXSUUYLUUYGUWUOUUYMUUYHUVUBUVUOUVUPU - VUSUVUBUVUMUVUPULUMWXSUUYIUVVCUVUMUVVEUVUPUVWAUVVCUVVEUVWCUVUPUVWDUVUBUVU - TUVWEUVVAUVWFUVUPUVWCUVWHUVWFUVWGUVUCWXSUVWFUVWGUVWJUVWMUVUCUVXBUVXEUVWFU - VWMUVXGUVUCUVXIUVWFUUGIVEVCURUVUCJYTUVWNUVWQUVXJUVYOUVYPUVWFUVYQVTVXHVXIY - NUVXKVXJUVXLXRYDVXMVXNVXOVXPZXUSUUYMWTXUSUUYHWTUUYCUUYLVDZUUYDUWULUUYFUWU - NWYGUUYCUUYLXUMUXQUWUQUUYEUWUMHUUYCUUYLWXAWYDVYPVYQYCVYRXUSUDUUYKUWUOWYIU - VUBUWUOWYBWYCWXLUSZWYFWYGUSZWYIUVUBUWULUWURUWUNWYFWYGUVUBUWULKUUYLVAZVBVC - USZUVYRGVAZWXLUSUWURUVUBUCBWWTDEUBGIUUYLJYOKLMXVRAXVQXURUVUAPVPZADYOUQZXU - RUVUAQVPAXWOXURUVUARVPZAUUXMXURUVUASVPUVUBUVUPUUYLWWTUQZUWUPWXRUEUUYLWWTW - FVNVYSUVUBUWVAWYBUWVBWYCWXLUVUBUWVAWYBVBVIUSZVBVCUSWYBUVUBUWUTUWVGVBVCUVU - BXWOUWUTUWVGVDUWVEUVUBIIWYBVBVIIWYAWXGJJKUVUBIURWYAUWUHWPZUVUBIURWXGYWEUV - UBYWFWIWPZUWVCUWVCXYLUVUBXWOVKWYBWTXWOKWXGVAVBVDZUVUBUCKWXFVBIWXGWXEVBVEU - YMXYHVYTUWBZVTXAYIYEUVUBWYBVBUVUBIYGKWYAUVUBIURYGWYAUWUHURYGWJUVUBWUAWIWU - EUWVEWAUVUBVUMVYJYJUVUBUVYRWYAGUVUBUFIUVYTXXQVCUUYLWXGWYAJUWVCUVUBIIVIIWY - AWXGJJUWVHUWVIUWVCUWVCXYLWSZUWVIUWVHUVUBIIYVHXXQVIIWYAWXGJJXXNUWVHUWVIUWV - CUWVCXYLUVUBXXTVKZYVHWTZXXTXYOUVUBXYQVTZXAZUWVOUWVMYVHXXQUWVMYVHUVUBIURXX - NWYAUWUHWLXOZUUUGUWVMUUUHWIZVYJWUBVYQYCYJUVUBUWUMWYEHUVUBUFIXXOUVYTVIUSZV - FUUUAUWUMWYEUVUBUFIUWVSYYTUWVMXXOYVHXXQUWVMXXOUVUBIURXXNWXAXURXWLAUVUAXWM - WUCWLXOUWVQUWVRWUDYFUVUBUFIIXXOUVYTVIIWXAUUYLJJXUSYWCUVUAXYEVMZUWVLUWVCUW - VCXYLUWVMXXOWTZUWVPYHUVUBUFIIXXRYVHVIIWXIWYAJJUVUBIIVCIWXAWXGJJUWVTUWVIUW - VCUWVCXYLWSUWVHUWVCUWVCXYLUVUBIIXXOXXQVCIWXAWXGJJXXNUWVTUWVIUWVCUWVCXYLUW - WAUWVOXAUWVNYHYMVYQYCUVUBXWSWYBYTUQYYNWYFXVIUQZUWUSWYIVDAXWSXURUVUAXVLVPZ - UVUBWYBUVUBIURKWYAUWUHUWVEWAZWUFUVUBWWTXVIWYAGAXWTXURUVUAXXAVPUVUBWYAUNUO - WXIWXOVHZUNWWTUTZUQZXXBUVUBUVUOUWWGUVUSUVUBUVUMUWWGULUMWXSUUYIUVVCUVUMUVV - EUWWGUVWAUVVCUVVEUVWCUWWGUVWDUVVCUWWGUVWCUVWBUWWFUQZUVVCXURXVOUVUTUWWHAXU - RUVUAUVVBWUGAXVOXURUVUAUVVBXVSYRUVUBUVUTUVVAWUOUEUNWWTWXSUWWFUBWXAWXGIUVU - CXVRUUUKUWWFVLZWUHWUIWYAUVWBUWWFWUJXRVXMVXNVXOVXPZUWWEUNWYAWWTWFVNWAZUVUB - WWTXVIWYEHAXXDXURUVUAXXEVPUVUBWYEUWWFUQZXXGUVUBXVNUWWGUWWLXUSXVNUVUAXWAVM - UWWJUNWWTUWWFUBWXIIWYAXVRUWWIWCVOUWWEUNWYEWWTWFVNWAZXVIDWXLWYGWYBWYCWYFXV - JXWEXWRWUKVUTYJYFYJXQXUSUUYKXVIWXTWYPWYSUDDXKWYIYUIXVJYUJXVKXVMUVXQUUYKXK - UQXUSUVXRWXHUUYJWXSUUYIUUXFWXGWULWUMWUNVYDUVUBXVIWXLDWYBWYHXVJXWEAXWFXURU - VUAXWHVPUWWDUVUBXVIDWYGWYCWYFXVJXWRUWWCUWWKUWWMWDWEXUSUDWXQWYIUUYKXKYUIXU - SWXQUDWXQWYIVFZXKYUIUWWNWXQWQXUSUDWXQWYIUWWNUUXHUWWNVLWRWIXWBYUMXGXUSUUYK - WXQWYOUUKZWXQXUSUUYKWXPWYNXHZVKZUEWWTUTZUWWOXUSUDUUYKUWWRXUSUVUAUVUOUVWCU - LWXSYBWYAUWWRUQZUVURXUSUVUNUVWCULWXSXUSUVUTVKZUVVEUMUUYIYBZUVUNUVWCUWWTUV - VEUVUMUMUUYIUWWTUVVAVKZUVVDUVULWYAUWXBUKUVUDUVUFUVUIUVUJVCUVUGUVUCUVUEXKX - KUVUTUVVFXUSUVVAUVVJWUCUVVAUVVKUWWTUVVMVTUVVNUWXBUVVOWIUVVPUWXBUVVQWIUVVR - UWXBUVVSVKUVUIWTUWXBUVVTVKUVUJWTYHYQWUPUWWTXVOUWXAUVWCVWPAXVOXURUVUTXVSVP - ZUVVEUVWCUMWXGWWTUVVLUVVDUVWBWYAUVUEWXGUVUCWXHVYPYQWUQVNWURWUPXUSUVWCUWWS - UVYSULUUYLWXSUWWTUWWSUVWCUVWBUWWRUQUWWTUWWQUVWBWXIWXOVHZUVWBWXAWXOVHZKUVW - BVAZVEVDZVKZXHZVKUEUVWBWWTWXNUVWBVDZWXPUWXDUWWPUWXIWXNUVWBWXIWXOXIZUWXJWY - NUWXHUWXJWXRUWXEWYMUWXGWXNUVWBWXAWXOXIUWXJWYLUWXFVEKWXNUVWBVVAVVBXLXJXLUV - UTUVVGXUSXVOUWUFUVVHUWXCUWUGVYHUWWTUWXDUWXIUWWTUVWBWXQUQZUWXDUWWTXURXVOUV - UTUWXLAXURUVUTVUGUWXCXUSUVUTVQUEUEWWTWXSWXQUBWXAWXGIUVUCXVRUUUKXXHWUHWUIU - WXLUWUFUWXDWXPUWXDUEUVWBWWTUWXKXMXTVNUWWTUWXGUWXEUWWTUWXFVEUWWTUWXFUWWTUW - XFKUVUCVAZVBVCUSZUPUWWTXWOUWXFUWXNVDAXWOXURUVUTRVPZUWWTIIUWXMVBVCIUVUCWXG - JJKUWWTIURUVUCUVUTUVWOXUSUVWPVTZWPAXYFXURUVUTYWGVPAXVQXURUVUTPVPZUWXQXYLU - WWTXWOVKUWXMWTXWOUWVJUWWTUWVKVTXAYIUWWTUWXMURUQUWXNUPUQUWWTIURKUVUCUWXPUW - XOWAUWXMWUSVNVXJWUTWVAWVBWVEWVCWYAUVWBUWWRWUJXRXUSUWWSVKZWXRUUYLWXAWXOVHZ - UEUUYLWWTWXNUUYLWXAWXOXIUWXRUWVFUUYLWYAWXOVHZUWXRXXBYWEWXGWYAWXOVHZUWVFUW - XTVKUWWSXXBXUSUWWQUEWYAWWTWFZVTYWEUWXRYWFWIUWXRUWYAXXQYVHVGVHZUFIWKUWXRUW - YCUFIUWXRXXTVKZXXPVBYVHVGVHZVEYVHVGVHZWVFUWYCUWYDXXPUWYEUWYFUWYDXXPUWYEUW - YDUWYEXXPVBWYBVGVHZUWXRUWYGXXTUWXRWYBUWXRYWQYWRYWNUWXRIURKWYAUWWSYWSXUSUW - WSXXBYWSUWYBYVPVNVTZAXWOXURUWWSRVPZWAUWXRWYBVEUWXRYXBYVAUWXRYXBYVAUWXRYXB - VKZYVAYWIUWYJYVKUFIUWYJXXTVKZYVKYXNXXNKYXSUWYKYXIVKZYVHXXNWXIVAZXXOVGUWYK - YVHUWYMVGVHZYXIUWYJUWYNUFIUWYJYUTUWYNUFIWKUWXRYUTYXBUWWSYUTXUSUWWSYUTUUXC - XHZUWWSXXBYUTUWYOVKZUWWQUWYPUEWYAWWTYVDWXPYUTUWWPUWYOYVEYVDWYNUUXCUUXDXJX - LXMXTZWVDVTZVMUWYJUFIIYVHUWYMVGIWYAWXIJJUWXRYVOYXBUWWSYVOXUSUWWSXXBYVOUWY - BYVQVNVTZVMZUWXRYVSYXBUWXRXVNYVSXUSXVNUWWSXWAVMXVNIURWXIXYSWPVNZVMAXVQXUR - UWWSYXBPYRZUXUBXYLUWYKYVHWTZUWYKUWYMWTXBWVGWVHVMUWYLUWYMXXRYXKXXOUWYJYXIX - XTUWYMXXRVDUWYJYXIVKZIIXXOXXQVCIWXAWXGJJXXNXUSYWCUWWSYXBYXIXYEYRXYFUXUDXY - IWIAXVQXURUWWSYXBYXIPWVIZUXUEXYLUXUDXXTVKXXOWTXXTXYOUXUDXYQVTXAWVJUWYLXXQ - VEXXOVCYXIXXQVEVDUWYKYXMVTXQUWYLXXOUWYLXXOUWYKXXOURUQYXIUWYJIURXXNWXAXUSX - WLUWWSYXBXWNVPWLVMXOXPYNWVKUWYJYXNXXTUWYJWYBVEWXBVGUWXRYXBVQUWXRVEWXBVGVH - YXBUWXRWXBUWXRIURKWXAXUSXWLUWWSXWNVMZUWYIWAWVLVMWVMVMWVPWOUWYJUFIIYVHXXOV - GIWYAWXAJJUWYTUWXRYWCYXBXUSYWCUWWSXYEVMZVMUXUBUXUBXYLUXUCUWYKXXOWTXBXCUYB - UWXRYVAYXBUWXRUWYOYVAYXBXHXDUWWSUWYOXUSUWWSYUTUWYOUWYQVVCVTYVAYXBWVNWVOWV - QWWEUYGYYAUYIWVRVMXXPYVHWYBVBVGYXQUXGXRXSUWYDUWYFXXPXHUWYDYVHUWXRIURXXNWY - AUWYHWLZWVLVMWVSXXPVBVEYVHVGWVTWVOWOUWXRUFIIXXQYVHVGIWXGWYAJJXYFUWXRXYIWI - ZUWYSAXVQXURUWWSPVPZUXUJXYLXXTXYOUWXRXYQVTZUWYDYVHWTZXBXCWWTUBWYAWXGIXVRW - WAWUIWVDUWXRUWXSUVYTXXOVGVHZUFIWKUWXRUXUMUFIUWYDUXUMYVIUWXRYVIUFIUWXRYUTY - VJUWYRUWXRUFIIYVHXXRVGIWYAWXIJJUWYSUXUAUXUJUXUJXYLUXULUWXRIIXXOXXQVCIWXAW - XGJJXXNUXUGUXUIUXUJUXUJXYLUWYDXXOWTZUXUKXAXBWVGWVHUWYDYVHXXQXXOUWYDYVHUXU - HWMXYCUWYDXYDWIUWYDXXOUWXRIURXXNWXAUXUFWLWMWWBXCWOUWXRUFIIUVYTXXOVGIUUYLW - XAJJUWXRIIVIIWYAWXGJJUWYSUXUIUXUJUXUJXYLWSZUXUGUXUJUXUJXYLUWXRIIYVHXXQVII - WYAWXGJJXXNUWYSUXUIUXUJUXUJXYLUXULUXUKXAZUXUNXBXCWVCUWXRUWUBUWUCUVYRWYAUW - XRUFIUWUAYVHUWYDYVHXXQUWYDYVHUXUHXOUUUGUWYDUUUHWIVYJYFUWXRUFIIUVYTXXQVCIU - UYLWXGJJUXUOUXUIUXUJUXUJXYLUXUPUXUKYHUWXRUFIURWYAUWYHVYKVYOUVUCUUYLVDUVWB - UVYRWYAUVUCUUYLWXGWXHVXKYQWWCWWDWWFWXPWYNUEWWTUWPWWGZXUSWXQWYOVUQWWHYUMWW - IWXTWYPWGWHVDXUSWYPWXTWHWYPWXSWJWXSWXTWGWHVDWYPWXTWGWHVDWXSWYOWWJWXSWXQWW - KWYPWXSWXTWWLWWNWWOWIXUSUUYKUWWOWXTWYPUVIUXUQXUSWXQWXSWYOUUVIYUHWWMVUEWWP - YJYNXUSWXAXUPVADUDWXSWYCXUAXUOVAZWYGUSZVFZVJUSDUDWXSXUDVFZVJUSXUIXUSUEBWW - TDEFWYGUBUDGXUOIWXALMXWROXVRUUXNAXUOBUQXURUUXTVMXVPVVKXUSUXUTUXVADVJXUSUD - WXSUXUSXUDYYKUXUSWYCXUCWYFWXLUSZWYGUSZXUDYYKUXURUXVBWYCWYGYYKUXURXUCYYQHV - AZWXLUSUXVBYYKUCBWWTDEUBHIXUAJYOKLMXVRUUUOAUWVDXURYYJQVPUUWAAUUXOXURYYJTV - PUUULVYSYYKUXVDWYFXUCWXLYYKYYQWYEHUUVBVYQXQYJXQYYKXWSXUCYTUQYYNUWWBUXVCXU - DVDYYMYYKXUCUUWJWUFYYPUUVCXVIDWXLWYGXUCWYCWYFXVJXWEXWRWWQVUTYJYFXQXUSWXSX - VIWYPWYOWYSUDDXUDXVJXVKXVMYYIUUWOUUVEUUVJUWMYNYHYJYM $. + 3eqtr4d 3eqtrd wfun eqeq2d ad3antrrr nn0cn cz oveq1 sylbid sylbird vv cfn + ccnv cima cmap cif cof cmg cofr cdif cmulr cplusg cpsd cbs ccmn crngringd + ringcmnd cmps reldmpsr strov2rcl psrbagsn psrbagaddcl psrbaglefi crnggrpd + vp cmnd grpmndd peano2nn0 crg sylan disjdifr cun 1nn0 0nn0 nn0ge0i nn0rei + ifcli addge01d mpbii elexi inidm weq eqeq1 ifbid fvmpt nn0re letr caoftrn + w3a syl3an mpan2d ss2rabdv undifr sylib eqcomd gsummptfidmsplit c0g fvexd + gsummulg difrab eleq2i fmpti rexnal bitr4di wo wne adantlr nn0nlt0 breq2d + cfzo biimpd ifnefalse imbi1d impancom necon1bd ancrd ralimdva rexim fveq2 + ex anim1d breq12d ceqsrexbv ltnled biimpar syldan breq2 syl5ibcom elnnne0 + neqned sylanbrc elfzo0 syl3anbrc fzostep1 rspcv lensymd intn3an3d sylnibr + mtod iftrue orcnd sylbida anasss sylan2b nn0cni addsubassd eqtr4d adantll + subadd23d simplr eqeltrrd simpl ss2rabi eldifi pncan3d addassd mulgnn0dir + eqtr3d syl13anc difssd ssfid gsummptfidmadd eqeq1d simprd subid1d 3eqtrrd + 1cnd fveq1 difexi sseli grpassd 3eqtr3d psrmulval grpcld psrmulcl grpmgmd + cgrp psdval psdcl psradd csn cxp ccom cdm df-of vex elimampo biimpa ffund + ssv funfnd ad2antrl velsn funmpt funeq mpbiri sylbi ad2antll wb addsubass + elsni caofass fvmptd3 subidi mpteq2i fconstmpt eqtr4i oveq2i 0zd caofid0r + dmex eqtrid eqeltrd eleq1d rexlimdvva mpd mptexd elsng mpofun inex1 mptex + xpss rgen2w dmmpoga mp1i sseqtrrid elovimad syl2an2 feq1 feqmptd 3eqtr4rd + npcand impbid f1o2d gsumf1o fveq2d fmptco psdcoef 1ex nn0sscn fssd offveq + oveq2 ad2antlr subsub3d nn0zd simpllr psrbagleadd1 syl3anc eleq1 mulgass2 + simprl snex funimaex rexbidva rexsng bitr3d nn0p1nn nnne0d neneqd intnand + xpex jca elrabd wif simpld mpbid r19.21bi ad4antr breqtrd nn0ge0d eqbrtrd + an32s pm2.61ne imnan sylibr con2d pm2.65d nnge1d ifpimpda brif1 psrbagcon + lesubaddd rspceb2dv 3bitrd eqrdv eqtr4di eqsstrd fmptssfisupp difss mp2an + disjdif ssdisj ineqcomi psdmullem gsumsplit2 mulgass3 ) AUAUBUOUUCUPUUDUU + BSZUBUQIUUEURZUSZJUAUOZVAZUTVBURZWXAUCIUCUOZJVCZUTVDUUFZVEZVBUUGZURZGHFUR + ZVAZDUUHVAZURZVEUAWWTDUDUEUOZWXIVFUUIZVGZUEWWTUSZWXNWXAWXOVGZUEWWTUSZUUJZ + JUDUOZVAZWYAGVAZWXIWYAVHUUGZURZHVAZDUUKVAZURZWXLURZVEZVIURZDUDWXSWXRJWXNV + AZVDVCZVJZUEWWTUSZUUJZWYIVEZVIURZDUULVAZURZDUDWYPJWXAWYAWYDURZVAZUTVBURZW + YHWXLURZVEZVIURZDUDWYOXUDVEZVIURZWYSURZWYSURZVEZWXJJIDUUMURVAZVAGXULVAZHF + URZGHXULVAZFURZCURZAUAWWTWXMXUJAWXAWWTSZVJZWXCDUDWXQWYHVEZVIURZWXLURZWYKW + YRXUIWYSURZWYSURZWXMXUJXUSDUDWXQWXCWYHWXLURZVEVIURDUDWXTXVEVEZVIURZDUDWXS + XVEVEVIURZWYSURXVBXVDXUSWXQDUUNVAZWXTWXSWYSUDDXVEXVIVKZWYSVKZADUUOSXURADA + DOUUPZUUQVLZXUSWXIWWTSZWXQUUBSXUSXURWXGWWTSZXVNAXURVOZAXVOXURAITSZXVOAGBS + ZXVQQBDEUURIGKLUUSUUTVPZUCWWTUBIJTWWTVKZUVAVPZVLWWTUBWXAWXGIXVTUVBZVMZUEW + WTUBWXIIXVTUVCVPZXUSWYAWXQSZVJZXVIWXLDWXCWYHXVJWXLVKZADUVFSZXURXWEADADOUV + DZUVGZVNZXUSWXCUQSZXWEXUSWXBUQSZXWLXUSIUQJWXAXURIUQWXAVQZAWWTUBWXAIXVTVRZ + VSZAJISZXURPVLVTZWXBUVHVPZVLXWFXVIDWYGWYCWYFXVJWYGVKZADUVISZXURXWEXVLVNXW + FWWTXVIWYAGAWWTXVIGVQZXURXWEABWWTDEUBIXVIGKXVJXVTLQWAZVNXWEWYAWWTSZXUSWXP + UEWYAWWTWBZVSVTXWFWWTXVIWYEHAWWTXVIHVQZXURXWEABWWTDEUBIXVIHKXVJXVTLRWAZVN + XWFWYEWXQSZWYEWWTSZXUSXVNXWEXXHXWCUEWWTWXQUBWXIIWYAXVTWXQVKZWCUVJWXPUEWYE + WWTWBVPVTWDZWEWXTWXSWFWGVCXUSWXSWXQUVKWHXUSWXTWXSUVLZWXQXUSWXSWXQWIXXLWXQ + VCXUSWXRWXPUEWWTXUSWXNWWTSZVJZWXRWXAWXIWXOVGZWXPXUSXXOXXMXUSXXOUFUOZWXAVA + ZXXQXXPJVCZUTVDUUFZVBURZVFVGZUFIWJXUSXYAUFIXUSXXPISZVJZVDXXSVFVGXYAXXSXXR + UTVDUQUVMUVNUVQZUVOXYCXXQXXSXYCXXQXUSIUQXXPWXAXWPWKWLXXSWMSZXYCXXSXYDUVPZ + WHUVRUVSWNXUSUFIIXXQXXTVFIWXAWXITTXUSIUQWXAXWPWOZXUSIIVBIWXAWXGTTXYGWXGIX + IZXUSUCIWXFWXGWXFUQWXEUTVDUQUVMUVNUVQZUVTWXGVKZWPZWHZAXVQXURXVSVLZXYMIUWA + ZWQZXYMXYMXYNXYCXXQWRZXUSIIXXQXXSVBIWXAWXGTTXXPXYGXYLXYMXYMXYNXYPXYBXXPWX + GVAXXSVCZXUSUCXXPWXFXXSIWXGUCUFUWBWXEXXRUTVDWXDXXPJUWCUWDZXYJXXSUQXYDUVTU + WEZVSWSWTXAVLXXNUGUHUIIVFUQVFVFWXNWXAWXITAXVQXURXXMXVSVNXXMIUQWXNVQXUSWWT + UBWXNIXVTVRVSXUSXWNXXMXWPVLXUSIUQWXIVQZXXMXUSXVNXYTXWCWWTUBWXIIXVTVRZVPVL + UGUOZUQSZUHUOZUQSZUIUOZUQSZUWIZYUBYUDVFVGYUDYUFVFVGVJYUBYUFVFVGXBZXXNYUCY + UBWMSYUEYUDWMSYUGYUFWMSYUIYUBUWFYUDUWFYUFUWFYUBYUDYUFUWGUWJVSUWHUWKUWLZWX + SWXQUWMUWNUWOUWPXUSWXQXVIWXLUDDWXCTWYHDUWQVAZXVJYUKVKZXWGWXQTSXUSWXPUEWWT + WWRUBWWSUQIUUEXCXDZXDZWHXXKXUSWXQXUTTYUKXUTWXQXIXUSUDWXQWYHXUTWYCWYFWYGXC + XUTVKWPWHXWDXUSDUWQUWRZXEXVMXWSUWSXUSXVGWYKXVHXVCWYSXUSXVFWYJDVIXUSUDWXTX + VEWYIXUSWYAWXTSZVJWXCWYBWYHWXLYUPXUSWYAWXPWXRXFZVJZUEWWTUSZSZWXCWYBVCZWXT + YUSWYAWXPWXRUEWWTUWTUXAYUTXUSXXDWYAWXIWXOVGZWYAWXAWXOVGZXFZVJZVJYVAYURYVE + UEWYAWWTUEUDUWBZWXPYVBYUQYVDWXNWYAWXIWXOXGZYVFWXRYVCWXNWYAWXAWXOXGZXHXJXK + XUSXXDYVEYVAXUSXXDVJZYVEXXPWYAVAZXXTVFVGZUFIWJZYVJXXQVFVGZXFZUFIXTZVJZYVA + YVIYVBYVLYVDYVOYVIUFIIYVJXXTVFIWYAWXITTXXDWYAIXIZXUSXXDIUQWYAWWTUBWYAIXVT + VRZWOZVSZXUSWXIIXIZXXDXYOVLAXVQXURXXDXVSVNZYWBXYNYVIXYBVJZYVJWRZYVIIIXXQX + XSVBIWXAWXGTTXXPXUSWXAIXIZXXDXYGVLZAXYHXURXXDAIUQWXGIUQWXGVQZAUCIUQWXFWXG + XYJWXFUQSWXDISXYIWHUXBZWHWOZVNYWBYWBXYNYWCXXQWRZXYBXYQYVIXYSVSWSWTYVIYVDY + VMUFIWJZXFYVOYVIYVCYWKYVIUFIIYVJXXQVFIWYAWXATTYVTYWFYWBYWBXYNYWDYWJWTXHYV + MUFIUXCUXDXJYVIYVPVJZWXCVDWYBUXJURZSZYVAYWLWXBYWMSZYWNYVAUXEYWLXWMWYBUPSZ + WXBWYBXLVGZYWOXUSXWMXXDYVPXWRVNZYWLWYBUQSZWYBVDUXFZYWPYVIYWSYVPAXXDYWSXUR + AXXDVJIUQJWYAXXDIUQWYAVQZAYVRVSAXWQXXDPVLVTUXGZVLZYWLWYBVDYWLWYBVDVCZWXBV + DXLVGZYWLXWMYXEXFYWRWXBUXHVPYWLYWQYXDYXEYVIYVPYVNXXRYVNVJZXBZUFIWJZYVOVJZ + YWQYVIYVPYXIYVIYVLYXHYVOYVIYVKYXGUFIYWCYVKYXGYWCYVKVJZYVNXXRYXJYVMXXPJYWC + XXPJUXFZYVKYVMYWCYXKYVKYVMXBZYWCYXLYXKYVJXXQVDVBURZVFVGZYVMXBYWCYXNYVMYWC + YXMXXQYVJVFYWCXXQYWCXXQYVIIUQXXPWXAXUSXWNXXDXWPVLWKXMXNUXIUXKYXKYVKYXNYVM + YXKXXTYXMYVJVFYXKXXSVDXXQVBXXPJUTVDUXLZXOUXIUXMXPXQUXNUXOUXPUXTUXQUYAXQYX + IYVIWYBWXBVFVGZXFZYWQYXIYXFUFIXTZYXQYXHYVOYXRYVNYXFUFIUXRXQYXRXWQYXQYVNYX + QUFJIXXRYVMYXPXXRYVJWYBXXQWXBVFXXPJWYAUXSZXXPJWXAUXSZUYBZXHUYCXRVPYVIYWQY + XQYVIWXBWYBYVIWXBXUSXWMXXDXWRVLWLYVIWYBYXBWLUYDUYEXSUYFZWYBVDWXBXLUYGUYHU + YSUYJWYBUYIZUYKYYBWXBWYBUYLUYMWXBVDWYBUYNVPYWLXWLYWPWXCWYBXLVGZUWIYWNYWLY + YDXWLYWPYWLWYBWXCYWLWYBYXCWLYWLWXCXUSXWLXXDYVPXWSVNWLYVIYVLWYBWXCVFVGZYVO + YVIYVLYYEYVIXWQYVLYYEXBAXWQXURXXDPVNYVKYYEUFJIXXRYVJWYBXXTWXCVFYXSXXRXXQW + XBXXSUTVBYXTXXRUTVDUYTYAUYBUYOVPXQYBUYPUYQWXCWYBUYLUYRVUAVUBVUCVUDVUDYCYD + XOXUSXVHDUDWYPXVEVEZVIURZDUDWYOXVEVEZVIURZWYSURWYRXUFWYSURZXUHWYSURXVCXUS + WXSXVIWYPWYOWYSUDDXVEXVJXVKXVMXURWXSUUBSAUEWWTUBWXAIXVTUVCVSZXUSWYAWXSSZV + JZXVIWXLDWXCWYHXVJXWGAXWHXURYYLXWJVNZXUSXWLYYLXWSVLYYMXVIDWYGWYCWYFXVJXWT + AXXAXURYYLXVLVNZYYLXUSXXDWYCXVISZWXRUEWYAWWTWBZXUSWWTXVIWYAGAXXBXURXXCVLW + KXSZYYMWWTXVIWYEHAXXFXURYYLXXGVNYYMXUAWXGWXHURZWYEWWTYYMUFIXXQYVJVHURZXXS + VBURZVEUFIXXTYVJVHURZVEZYYSWYEYYMUFIUUUAUUUBYYMXYBVJZUUUAXXQXXSYVJVHURVBU + RUUUBUUUDXXQYVJXXSUUUDXXQYYMIUQXXPWXAXUSXWNYYLXWPVLZWKXMZUUUDYVJYYMIUQXXP + WYAYYLYXAXUSYYLXXDYXAYYQYVRVPVSZWKXMZXXSYESZUUUDXXSXYDVUEZWHZVUIUUUDXXQXX + SYVJUUUFUUUKUUUHVUFVUGYDYYMUFIIYYTXXSVBIXUAWXGTTYYMIUQXUAYYMXUAWWTSZIUQXU + AVQXURYYLUUULAXURYYLVJXUAWXSSUUULUEWWTWXSUBWXAIWYAXVTWXSVKZWCWXRUEXUAWWTW + BVPVUHZWWTUBXUAIXVTVRVPZWOXYHYYMXYKWHZAXVQXURYYLXVSVNZUUUQXYNYYMIIXXQYVJV + HIWXAWYATTXXPYYMIUQWXAUUUEWOZYYMIUQWYAUUUGWOZUUUQUUUQXYNUUUDXXQWRZUUUDYVJ + WRZWSXYBXYQYYMXYSVSZYFYYMUFIIXXTYVJVHIWXIWYATTYYMIUQWXIYYMXVNXYTYYMXURXVO + XVNAXURYYLVUJAXVOXURYYLXWAVNZXWBVMYUAVPWOUUUSUUUQUUUQXYNYYMIIXXQXXSVBIWXA + WXGTTXXPUUURUUUPUUUQUUUQXYNUUUTUUVBWSUUVAYFYKZYYMUUULXVOYYSWWTSUUUNUUVCWW + TUBXUAWXGIXVTUVBVMVUKVTZWDZWEWYPWYOWFWGVCXUSWYOWXSUVKWHZXUSWYPWYOUVLZWXSX + USWYOWXSWIZUUVHWXSVCUUVIXUSWYNWXRUEWWTWYNWXRXBXXMWXRWYMVULWHVUMZWHZWYOWXS + UWMUWNUWOZUWPXUSYYGYYJYYIXUHWYSXUSYYGDUDWYPWYIXUDWYSURZVEZVIURYYJXUSYYFUU + VNDVIXUSUDWYPXVEUUVMXUSWYAWYPSZVJZXVEWYBXUCVBURZWYHWXLURZUUVMUUVPWXCUUVQW + YHWXLUUVPWYBXUBVBURZUTVBURWXCUUVQUUVPUUVSWXBUTVBUUVPUUVSWYBWXBWYBVHURZVBU + RWXBUUVPXUBUUVTWYBVBUUVOXUSYYLXUBUUVTVCZWYAWXSWYOVUNZYYMXWQUUWAAXWQXURYYL + PVNZYYMIIWXBWYBVHIWXAWYATTJUUURUUUSUUUQUUUQXYNYYMXWQVJZWXBWRUUWDWYBWRWSYG + XSXOUUVPWYBWXBUUVPWYBUUVOXUSYYLYWSUUWBYYMIUQJWYAUUUGUUWCVTZXSZXMZXUSWXBYE + SUUVOXUSWXBXWRXMVLVUOYHYCUUVPWYBXUBUTUUWGUUVPXUBUUVOXUSYYLXUBUQSZUUWBYYMI + UQJXUAUUUOUUWCVTZXSXMUUVPVVGVUPVURYCUUVPXWHYWSXUCUQSZWYHXVISZUUVRUUVMVCAX + WHXURUUVOXWJVNUUWFUUVOXUSYYLUUWJUUWBYYMUUWHUUWJUUWIXUBUVHVPZXSUUVOXUSYYLU + UWKUUWBUUVFXSXVIWYSWXLDWYBXUCWYHXVJXWGXVKVUQVUSYHYDXOXUSUDWYPXVIWYIXUDWYS + WYQDXUEXVJXVKXVMXUSWXSWYPYYKXUSWXSWYOVUTVVAZUUVOXUSYYLWYIXVISZUUWBYYMXVIW + XLDWYBWYHXVJXWGYYNUUWEUUVFWEXSZUUVOXUSYYLXUDXVISZUUWBYYMXVIWXLDXUCWYHXVJX + WGYYNUUWLUUVFWEZXSZWYQVKZXUEVKZVVBYHXUSYYHXUGDVIXUSUDWYOXVEXUDXUSWYAWYOSZ + VJZWXCXUCWYHWXLUUXBWXBXUBUTVBUUXBXUBUUVTWXBVDVHURWXBUUXBXWQUUWAAXWQXURUUX + APVNUUXBIIWXBWYBVHIWXAWYATTJXUSYWEUUXAXYGVLUUXAYVQXUSUUXAXXDYVQWYNUEWYAWW + TWBYVSVPVSAXVQXURUUXAXVSVNZUUXCXYNUUXBXWQVJZWXBWRUUXDWYBWRWSYGUUXBWYBVDWX + BVHUUXAYXDXUSUUXAYVCYXDUUXAXXDYVCYXDVJZWYNUUXEUEWYAWWTYVFWXRYVCWYMYXDYVHY + VFWYLWYBVDJWXNWYAVVHVVCXJZXKXRVVDVSXOUUXBWXBUUXBWXBXUSXWMUUXAXWRVLXMVVEVV + FYCYCYDXOYAXUSXVIWYSDWYRXUFXUHXVJXVKADVVQSXURXWIVLZXUSWYPXVIWYQDTYUKXVJYU + LXVMWYPTSXUSWXSWYOWXRUEWWTYUMXDZVVIWHZXUSUDWYPWYIXVIUUWOYIXUSWYPWYQTYUKWY + QWYPXIXUSUDWYPWYIWYQWYBWYHWXLXCZUUWSWPWHUUWMYUOXEYJZXUSWYPXVIXUEDTYUKXVJY + ULXVMUUXIXUSUDWYPXUDXVIUUWRYIXUSWYPXUETYUKXUEWYPXIXUSUDWYPXUDXUEXUCWYHWXL + XCZUUWTWPWHUUWMYUOXEYJZXUSWYOXVIXUGDTYUKXVJYULXVMWYOTSXUSWYNUEWWTYUMXDWHX + USUDWYOXUDXVIUUXAXUSYYLUUWPWYOWXSWYAUUVJVVJUUWQXSYIXUSWYOXUGTYUKXUGWYOXIX + USUDWYOXUDXUGUUXLXUGVKWPWHXUSWXSWYOYYKUUVKVVAYUOXEYJZVVKYLYAVVLXUSWXKXVAW + XCWXLXUSUEBWWTDEFWYGUBUDGHIWXIKLXWTNXVTAXVRXURQVLZAHBSZXURRVLZXWCVVMXOXUS + XVIWYSDWYKWYRXUIXVJXVKUUXGXUSWXTXVIWYJDTYUKXVJYULXVMWXTTSXUSWXQWXSYUNVVIW + HXUSUDWXTWYIXVIYUPXUSXWEUUWNWYAWXQWXSVUNXWFXVIWXLDWYBWYHXVJXWGXWKXWFIUQJW + YAXWEYXAXUSXWEXXDYXAXXEYVRVPVSAXWQXURXWEPVNVTXXKWEXSYIXUSWXTWYJTYUKWYJWXT + XIXUSUDWXTWYIWYJUUXJWYJVKWPWHXUSWXQWXTXWDXUSWXQWXSVUTVVAYUOXEYJUUXKXUSXVI + WYSDXUFXUHXVJXVKUUXGUUXMUUXNVVNVVKYKYDAUCBWWTDEUBUAWXJIJKLXVTPABDEFIGHKLN + XVLQRVVOVVRAXUQXUNXUPWYSUUGURXUKABWYSCDEIXUNXUPKLXVKMABDEFIXUMHKLNXVLABDE + GIJKLADXWIVVPZPQVVSZRVVOZABDEFIGXUOKLNXVLQABDEHIJKLUUXRPRVVSZVVOZVVTAUAWW + TWWTWYTXUIWYSWWTXUNXUPTTAWWTXVIXUNABWWTDEUBIXVIXUNKXVJXVTLUUXTWAWOAWWTXVI + XUPABWWTDEUBIXVIXUPKXVJXVTLUUYBWAWOWWTTSAYUMWHZUUYCWWTUWAXUSWXAXUNVADUJWX + SUJUOZXUMVAZWXAUUYDWYDURZHVAZWYGURZVEZVIURDUUYIUDWXHWXSWXGVWAZVWBZUUDZWYA + WXGWYDURZVEZVWCZVIURZWYTXUSUEBWWTDEFWYGUBUJXUMHIWXAKLXWTNXVTAXUMBSXURUUXS + VLUUXQXVPVVMXUSWXSXVIUUYLUUYIDUUYNTYUKXVJYULXVMWXSTSXUSUUXHWHXUSUJWXSUUYH + XVIXUSUUYDWXSSZVJZXVIDWYGUUYEUUYGXVJXWTAXXAXURUUYQXVLVNUUYQXUSUUYDWWTSUUY + EXVISWXRUEUUYDWWTWBXUSWWTXVIUUYDXUMAWWTXVIXUMVQXURABWWTDEUBIXVIXUMKXVJXVT + LUUXSWAVLWKXSUUYRWWTXVIUUYFHAXXFXURUUYQXXGVNUUYRUUYFWXSSZUUYFWWTSXURUUYQU + UYSAUEWWTWXSUBWXAIUUYDXVTUUUMWCVUHWXRUEUUYFWWTWBVPVTWDYIXUSWXSUUYITYUKUUY + IWXSXIXUSUJWXSUUYHUUYIUUYEUUYGWYGXCUUYIVKWPWHYYKYUOXEXUSUDUUAUUYLWXSUUYMU + UAUOZWXGWXHURZUUYNUUYNVKXUSWYAUUYLSZVJZWYAUKULUOZVWDZUMUOZVWDZWFZUKUOZUVU + DVAZUVUIUVUFVAZVBURZVEZVCZUMUUYJXTZULWXSXTZUUYMWXSSZXUSUVUBUVUPXUSULUMTTU + VUMWYAWXHTWXSUUYJUKVBULUMVWEZWYATSXUSUDVWFWHWXSTWIXUSWXSVWJWHUUYJTWIXUSUU + YJVWJWHVWGZVWHZUVUCUVUNUVUQULUMWXSUUYJUVUCUVUDWXSSZUVUFUUYJSZVJZVJZUVUNWY + AUVUDUVUFWXHURZVCZUVUQUVVDUVVEUVUMWYAUVVDUKUVUEUVUGUVUJUVUKVBUVUHUVUDUVUF + TTUVVAUVUDUVUEXIZUVUCUVVBUVVAUVUDUVVAUVUDWWTSZUVUDYMWXRUEUVUDWWTWBZUVVHIU + QUVUDWWTUBUVUDIXVTVRZVWIVPVWKZVWLUVVBUVUFUVUGXIZUVUCUVVAUVVBUVUFWXGVCZUVV + LUMWXGVWMUVVMUVUFUVVMUVUFYMWXGYMUCIWXFVWNUVUFWXGVWOVWPVWKVWQZVWRUVUETSZUV + VDUVUDULVWFVXKZWHUVUGTSZUVVDUVUFUMVWFVXKZWHUVUHVKZUVVDUVUIUVUESZVJUVUJWRU + VVDUVUIUVUGSZVJUVUKWRYFYNZUVVDUVVFWYAUVUDWXGWXHURZVCZUVUQUVVBUVVFUVWDVWSU + VUCUVVAUVVBUVVEUVWCWYAUVVBUVUFWXGUVUDWXHUVUFWXGVXAXOYNVWRZUVUCUVVAUVWDUVU + QXBZUVVBUVUCUVVAVJZUVUQUVWDUVWCWXGWYDURZWXSSZUVWGUVWHUVUDWXSUVWGUVWHUVUDW + XGWXGWYDURZWXHURZUVUDUFIXXSXXSVHURZVEZWXHURZUVUDUVWGUGUHUIIVHVBUQVHUVUDWX + GWXGVBTAXVQXURUVUBUVVAXVSYOZUVVAIUQUVUDVQZUVUCUVVAUVVHUVWPUVVIUVVJVPZVSZY + WGUVWGYWHWHZUVWSYUHYUBYUDVBURYUFVHURYUBYUDYUFVHURVBURVCZUVWGYUCYUBYESYUEY + UDYESYUGYUFYESUVWTYUBYPZYUDYPYUFYPYUBYUDYUFVWTUWJZVSVXBZAUVWKUVWNVCXURUVU + BUVVAAUVWJUVWMUVUDWXHAUFIIXXSXXSVHIWXGWXGTTYWIYWIXVSXVSXYNAXYBVJZUCXXPWXF + XXSIWXGUQXYJXYRAXYBVOXXSUQSUVXDXYDWHVXCZUVXEYFXOYOZUVWGUVWNUVUDIVDVWAVWBZ + WXHURZUVUDUVWMUVXGUVUDWXHUVWMUFIVDVEUVXGUFIUVWLVDXXSUUUJVXDVXEUFIVDVXFVXG + ZVXHZUVWGUGIVDVBUQUVUDTYQUVWOUVWRUVWGVXIZYUCYUBVDVBURYUBVCUVWGYUCYUBUVXAX + NVSVXJVXLYLUVUCUVVAVOZVXMUVWDUUYMUVWHWXSWYAUVWCWXGWYDYRVXNZXPYBYSYTVXOVXP + XUSUUYTWXSSZVJZUUYTWXGWXSUUYJWXHXUSUVXNVOAWXGUUYJSZXURUVXNAUVXPWXGWXGVCZX + YJAWXGTSUVXPUVXQVWSAUCIWXFTXVSVXQWXGWXGTVXRVPVWPVNWXHYMZUVXOULUMTTUVUMWXH + UVURVXSZWHUVXOTTVWBZUUYKWXHVWDZWXSUUYJVYBUVUMTSZUMTWJULTWJUVYAUVXTVCUVXOU + VYBULUMTTUKUVUHUVULUVUEUVUGUVVPVXTVYAVYCULUMTTUVUMWXHTUVURVYDVYEVYFVYGXUS + UVUBUVXNVJZVJZWYAUVUAVCZUUYTUUYMVCZUVYDUVYFUVYEUUYTUVUAWXGWYDURZVCUVYDUVY + GUUYTUVWJWXHURUUYTUVWMWXHURZUUYTUVYDUGUHUIIVHVBUQVHUUYTWXGWXGVBTAXVQXURUV + YCXVSVNZUVXNIUQUUYTVQZXUSUVUBUVXNUUYTWWTSUVYJWXRUEUUYTWWTWBWWTUBUUYTIXVTV + RVPVWRZYWGUVYDYWHWHZUVYLYUHUVWTUVYDUVXBVSVXBUVYDUVWJUVWMUUYTWXHUVYDUFIIXX + SXXSVHIWXGWXGTTAXYHXURUVYCYWIVNZUVYMUVYIUVYIXYNXYBXYQUVYDXYSVSZUVYNYFXOUV + YDUVYHUUYTUVXGWXHURUUYTUVWMUVXGUUYTWXHUVXIVXHUVYDUVEIVDVBUQUUYTTYQUVYIUVY + KUVYDVXIUVEUOZUQSZUVYOVDVBURUVYOVCZUVYDUVYPUVYOUVYOYPXNZVSVXJVXLVVFUVYEUU + YMUVYGUUYTWYAUVUAWXGWYDYRYNXPUVYDUVYEUVYFWYAUUYMWXGWXHURZVCZUVYDUFIYVJXXS + VHURZXXSVBURZVEZUFIYVJVEZUVYSWYAUVYDUFIUWUBYVJUVYDXYBVJZYVJXXSUWUEYVJUVYD + IUQXXPWYAXUSUVUBYXAUVXNUVUCUVUPYXAUVUTUVUCUVUNYXAULUMWXSUUYJUVVDUVUNUVVFY + XAUVWBUVVDUVVFUVWDYXAUVWEUVVDYXAUVWDIUQUVWCVQZUVUCUVVAUWUFUVVBUVWGUVWCWWT + SZUWUFUVVAUVVHUVUCXVOUWUGUVVIAXVOXURUVUBUVVAXWAYOWWTUBUVUDWXGIXVTUVBZVYHW + WTUBUVWCIXVTVRVPYBIUQWYAUVWCVYIXPYSYTVXOVXPZYBZWKXMUUUIUWUEUUUJWHVYLYDUVY + DUFIIUWUAXXSVBIUUYMWXGTTUVYDIIVHIWYAWXGTTUVYDIUQWYAUWUJWOZUVYMUVYIUVYIXYN + WQUVYMUVYIUVYIXYNUVYDIIYVJXXSVHIWYAWXGTTXXPUWUKUVYMUVYIUVYIXYNUWUEYVJWRUV + YNWSUVYNYFUVYDUFIUQWYAUWUJVYJVYKUVYFUVUAUVYSWYAUUYTUUYMWXGWXHYRYNXPVYMVYN + VYOXUSUUYPDUDUUYLWYIVEZVIURWYTXUSUUYOUWULDVIXUSUUYOUDUUYLUUYMXUMVAZWXAUUY + MWYDURZHVAZWYGURZVEUWULXUSUDUJUUYLWXSUUYMUUYHUWUPUUYNUUYIUVUCUVUPUVUQUVUT + UVUCUVUNUVUQULUMWXSUUYJUVVDUVUNUVVFUVUQUVWBUVVDUVVFUVWDUVUQUVWEUVUCUVVAUV + WFUVVBUVWGUVUQUVWDUVWIUVWGUVWHUVUDWXSUVWGUVWHUVWKUVWNUVUDUVXCUVXFUVWGUVWN + UVXHUVUDUVXJUVWGUVEIVDVBUQUVUDTYQUVWOUVWRUVXKUVYPUVYQUVWGUVYRVSVXJVXLYLUV + XLVXMUVXMXPYBYSYTVXOVXPZXUSUUYNWRXUSUUYIWRUUYDUUYMVCZUUYEUWUMUUYGUWUOWYGU + UYDUUYMXUMUXSUWURUUYFUWUNHUUYDUUYMWXAWYDWUCVYPYAVYQXUSUDUUYLUWUPWYIUVUCUW + UPWYBWYCWXLURZWYFWYGURZWYIUVUCUWUMUWUSUWUOWYFWYGUVUCUWUMJUUYMVAZUTVBURZUV + YSGVAZWXLURUWUSUVUCUCBWWTDEUBGIUUYMJKLXVTAXWQXURUVUBPVNZAXVRXURUVUBQVNUVU + CUVUQUUYMWWTSZUWUQWXRUEUUYMWWTWBVPVYRUVUCUWVBWYBUWVCWYCWXLUVUCUWVBWYBUTVH + URZUTVBURWYBUVUCUWVAUWVFUTVBUVUCXWQUWVAUWVFVCUWVDUVUCIIWYBUTVHIWYAWXGTTJU + VUCIUQWYAUWUIWOZUVUCIUQWXGYWGUVUCYWHWHWOZAXVQXURUVUBXVSVNZUWVIXYNUVUCXWQV + JWYBWRXWQJWXGVAUTVCZUVUCUCJWXFUTIWXGWXEUTVDUYTXYJVYSUWEZVSWSYGYCUVUCWYBUT + UVUCIYEJWYAUVUCIUQYEWYAUWUIUQYEWIUVUCVYTWHWUAUWVDVTUVUCVVGVYLYHUVUCUVYSWY + AGUVUCUFIUWUAXXSVBUUYMWXGWYATUWVIUVUCIIVHIWYAWXGTTUWVGUWVHUWVIUWVIXYNWQZU + WVHUWVGUVUCIIYVJXXSVHIWYAWXGTTXXPUWVGUWVHUWVIUWVIXYNUVUCXYBVJZYVJWRZXYBXY + QUVUCXYSVSZWSZUWVOUWVMYVJXXSUWVMYVJUVUCIUQXXPWYAUWUIWKXMZUUUIUWVMUUUJWHZV + YLWUBVYPYAYHUVUCUWUNWYEHUVUCUFIXXQUWUAVHURZVEUUUCUWUNWYEUVUCUFIUWVSUUUBUW + VMXXQYVJXXSUWVMXXQUVUCIUQXXPWXAXURXWNAUVUBXWOWUDWKXMUWVQUWVRWUEYDUVUCUFII + XXQUWUAVHIWXAUUYMTTXUSYWEUVUBXYGVLZUWVLUWVIUWVIXYNUWVMXXQWRZUWVPYFUVUCUFI + IXXTYVJVHIWXIWYATTUVUCIIVBIWXAWXGTTUWVTUWVHUWVIUWVIXYNWQUWVGUWVIUWVIXYNUV + UCIIXXQXXSVBIWXAWXGTTXXPUWVTUWVHUWVIUWVIXYNUWWAUWVOWSUWVNYFYKVYPYAUVUCXXA + WYBYQSYYPWYFXVISZUWUTWYIVCAXXAXURUVUBXVLVNZUVUCWYBUVUCIUQJWYAUWUIUWVDVTZW + UFUVUCWWTXVIWYAGAXXBXURUVUBXXCVNUVUCWYAUNUOWXIWXOVGZUNWWTUSZSZXXDUVUCUVUP + UWWGUVUTUVUCUVUNUWWGULUMWXSUUYJUVVDUVUNUVVFUWWGUVWBUVVDUVVFUVWDUWWGUVWEUV + VDUWWGUVWDUVWCUWWFSZUVVDXURXVOUVVAUWWHAXURUVUBUVVCWUGAXVOXURUVUBUVVCXWAYO + UVUCUVVAUVVBWULUEUNWWTWXSUWWFUBWXAWXGIUVUDXVTUUUMUWWFVKZWUHWUIWYAUVWCUWWF + WUJXPYSYTVXOVXPZUWWEUNWYAWWTWBVPVTZUVUCWWTXVIWYEHAXXFXURUVUBXXGVNUVUCWYEU + WWFSZXXIUVUCXVNUWWGUWWLXUSXVNUVUBXWCVLUWWJUNWWTUWWFUBWXIIWYAXVTUWWIWCVMUW + WEUNWYEWWTWBVPVTZXVIDWXLWYGWYBWYCWYFXVJXWGXWTWUKVUSYHYDYHXOXUSUUYLXVIWXTW + YPWYSUDDTWYIYUKXVJYULXVKXVMUVXRUUYLTSXUSUVXSWXHUUYKWXSUUYJUUXHWXGWUMWVBWU + NVYEUVUCXVIWXLDWYBWYHXVJXWGAXWHXURUVUBXWJVNUWWDUVUCXVIDWYGWYCWYFXVJXWTUWW + CUWWKUWWMWDWEXUSUDWXQWYIUUYLTYUKXUSWXQUDWXQWYIVEZTYUKUWWNWXQXIXUSUDWXQWYI + UWWNUUXJUWWNVKWPWHXWDYUOXEXUSUUYLWXQWYOUUJZWXQXUSUUYLWXPWYNXFZVJZUEWWTUSZ + UWWOXUSUDUUYLUWWRXUSUVUBUVUPUVWDULWXSXTWYAUWWRSZUVUSXUSUVUOUVWDULWXSXUSUV + VAVJZUVVFUMUUYJXTZUVUOUVWDUWWTUVVFUVUNUMUUYJUWWTUVVBVJZUVVEUVUMWYAUWXBUKU + VUEUVUGUVUJUVUKVBUVUHUVUDUVUFTTUVVAUVVGXUSUVVBUVVKWUDUVVBUVVLUWWTUVVNVSUV + VOUWXBUVVPWHUVVQUWXBUVVRWHUVVSUWXBUVVTVJUVUJWRUWXBUVWAVJUVUKWRYFYNWUOUWWT + XVOUWXAUVWDVWSAXVOXURUVVAXWAVNZUVVFUVWDUMWXGWWTUVVMUVVEUVWCWYAUVUFWXGUVUD + WXHWUCYNWUPVPWUQWUOXUSUVWDUWWSUVYTULUUYMWXSUWWTUWWSUVWDUVWCUWWRSUWWTUWWQU + VWCWXIWXOVGZUVWCWXAWXOVGZJUVWCVAZVDVCZVJZXFZVJUEUVWCWWTWXNUVWCVCZWXPUWXDU + WWPUWXIWXNUVWCWXIWXOXGZUWXJWYNUWXHUWXJWXRUWXEWYMUWXGWXNUVWCWXAWXOXGUWXJWY + LUWXFVDJWXNUVWCVVHVVCXJXHXJUVVAUVVHXUSXVOUWUGUVVIUWXCUWUHVYHUWWTUWXDUWXIU + WWTUVWCWXQSZUWXDUWWTXURXVOUVVAUWXLAXURUVVAVUJUWXCXUSUVVAVOUEUEWWTWXSWXQUB + WXAWXGIUVUDXVTUUUMXXJWUHWUIUWXLUWUGUWXDWXPUWXDUEUVWCWWTUWXKXKXRVPUWWTUWXG + UWXEUWWTUWXFVDUWWTUWXFUWWTUWXFJUVUDVAZUTVBURZUPUWWTXWQUWXFUWXNVCAXWQXURUV + VAPVNZUWWTIIUWXMUTVBIUVUDWXGTTJUWWTIUQUVUDUVVAUVWPXUSUVWQVSZWOAXYHXURUVVA + YWIVNAXVQXURUVVAXVSVNZUWXQXYNUWWTXWQVJUWXMWRXWQUWVJUWWTUWVKVSWSYGUWWTUWXM + UQSUWXNUPSUWWTIUQJUVUDUWXPUWXOVTUWXMWURVPVXMWUSWUTWVAWVCWVDWYAUVWCUWWRWUJ + XPXUSUWWSVJZWXRUUYMWXAWXOVGZUEUUYMWWTWXNUUYMWXAWXOXGUWXRUWVEUUYMWYAWXOVGZ + UWXRXXDYWGWXGWYAWXOVGZUWVEUWXTVJUWWSXXDXUSUWWQUEWYAWWTWBZVSYWGUWXRYWHWHUW + XRUWYAXXSYVJVFVGZUFIWJUWXRUWYCUFIUWXRXYBVJZXXRUTYVJVFVGZVDYVJVFVGZWVEUWYC + UWYDXXRUWYEUWYFUWYDXXRUWYEUWYDUWYEXXRUTWYBVFVGZUWXRUWYGXYBUWXRWYBUWXRYWSY + WTYWPUWXRIUQJWYAUWWSYXAXUSUWWSXXDYXAUWYBYVRVPVSZAXWQXURUWWSPVNZVTUWXRWYBV + DUWXRYXDYVCUWXRYXDYVCUWXRYXDVJZYVCYWKUWYJYVMUFIUWYJXYBVJZYVMYXPXXPJYYAUWY + KYXKVJZYVJXXPWXIVAZXXQVFUWYKYVJUWYMVFVGZYXKUWYJUWYNUFIUWYJYVBUWYNUFIWJUWX + RYVBYXDUWWSYVBXUSUWWSYVBUUXEXFZUWWSXXDYVBUWYOVJZUWWQUWYPUEWYAWWTYVFWXPYVB + UWWPUWYOYVGYVFWYNUUXEUUXFXHXJXKXRZWVFVSZVLUWYJUFIIYVJUWYMVFIWYAWXITTUWXRY + VQYXDUWWSYVQXUSUWWSXXDYVQUWYBYVSVPVSZVLZUWXRYWAYXDUWXRXVNYWAXUSXVNUWWSXWC + VLXVNIUQWXIYUAWOVPZVLAXVQXURUWWSYXDXVSYOZUXUBXYNUWYKYVJWRZUWYKUWYMWRWTWVG + WVHVLUWYLUWYMXXTYXMXXQUWYJYXKXYBUWYMXXTVCUWYJYXKVJZIIXXQXXSVBIWXAWXGTTXXP + XUSYWEUWWSYXDYXKXYGYOXYHUXUDXYKWHAXVQXURUWWSYXDYXKXVSWVIZUXUEXYNUXUDXYBVJ + XXQWRXYBXYQUXUDXYSVSWSWVMUWYLXXSVDXXQVBYXKXXSVDVCUWYKYXOVSXOUWYLXXQUWYLXX + QUWYKXXQUQSYXKUWYJIUQXXPWXAXUSXWNUWWSYXDXWPVNWKVLXMXNYLWVJUWYJYXPXYBUWYJW + YBVDWXBVFUWXRYXDVOUWXRVDWXBVFVGYXDUWXRWXBUWXRIUQJWXAXUSXWNUWWSXWPVLZUWYIV + TWVKVLWVLVLWVNWNUWYJUFIIYVJXXQVFIWYAWXATTUWYTUWXRYWEYXDXUSYWEUWWSXYGVLZVL + UXUBUXUBXYNUXUCUWYKXXQWRWTXAUXTUWXRYVCYXDUWXRUWYOYVCYXDXFXBUWWSUWYOXUSUWW + SYVBUWYOUWYQVVDVSYVCYXDWVOWVPWVQWVRUYJYYCUYKWVSVLXXRYVJWYBUTVFYXSUXIXPXQU + WYDUWYFXXRXFUWYDYVJUWXRIUQXXPWYAUWYHWKZWVKVLWVTXXRUTVDYVJVFWWAWVPWNUWXRUF + IIXXSYVJVFIWXGWYATTXYHUWXRXYKWHZUWYSAXVQXURUWWSXVSVNZUXUJXYNXYBXYQUWXRXYS + VSZUWYDYVJWRZWTXAWWTUBWYAWXGIXVTWWBWUIWVFUWXRUWXSUWUAXXQVFVGZUFIWJUWXRUXU + MUFIUWYDUXUMYVKUWXRYVKUFIUWXRYVBYVLUWYRUWXRUFIIYVJXXTVFIWYAWXITTUWYSUXUAU + XUJUXUJXYNUXULUWXRIIXXQXXSVBIWXAWXGTTXXPUXUGUXUIUXUJUXUJXYNUWYDXXQWRZUXUK + WSWTWVGWVHUWYDYVJXXSXXQUWYDYVJUXUHWLXYEUWYDXYFWHUWYDXXQUWXRIUQXXPWXAUXUFW + KWLWWCXAWNUWXRUFIIUWUAXXQVFIUUYMWXATTUWXRIIVHIWYAWXGTTUWYSUXUIUXUJUXUJXYN + WQZUXUGUXUJUXUJXYNUWXRIIYVJXXSVHIWYAWXGTTXXPUWYSUXUIUXUJUXUJXYNUXULUXUKWS + ZUXUNWTXAWVDUWXRUWUCUWUDUVYSWYAUWXRUFIUWUBYVJUWYDYVJXXSUWYDYVJUXUHXMUUUIU + WYDUUUJWHVYLYDUWXRUFIIUWUAXXSVBIUUYMWXGTTUXUOUXUIUXUJUXUJXYNUXUPUXUKYFUWX + RUFIUQWYAUWYHVYJVYKUVUDUUYMVCUVWCUVYSWYAUVUDUUYMWXGWXHYRYNWWDWWEWWFWXPWYN + UEWWTUWTWWGZXUSWXQWYOVUTWWHYUOWWIWXTWYPWFWGVCXUSWYPWXTWGWYPWXSWIWXSWXTWFW + GVCWYPWXTWFWGVCWXSWYOWWJWXSWXQWWLWYPWXSWXTWWMWWKWWNWHXUSUUYLUWWOWXTWYPUVL + UXUQXUSWXQWXSWYOUUVKYUJWWOVUGWWPYHYLXUSWXAXUPVADUDWXSWYCXUAXUOVAZWYGURZVE + ZVIURDUDWXSXUDVEZVIURXUIXUSUEBWWTDEFWYGUBUDGXUOIWXAKLXWTNXVTUUXOAXUOBSXUR + UUYAVLXVPVVMXUSUXUTUXVADVIXUSUDWXSUXUSXUDYYMUXUSWYCXUCWYFWXLURZWYGURZXUDY + YMUXURUXVBWYCWYGYYMUXURXUCYYSHVAZWXLURUXVBYYMUCBWWTDEUBHIXUAJKLXVTUUWCAUU + XPXURYYLRVNUUUNVYRYYMUXVDWYFXUCWXLYYMYYSWYEHUUVDVYPXOYHXOYYMXXAXUCYQSYYPU + WWBUXVCXUDVCYYOYYMXUCUUWLWUFYYRUUVEXVIDWXLWYGXUCWYCWYFXVJXWGXWTWWQVUSYHYD + XOXUSWXSXVIWYPWYOWYSUDDXUDXVJXVKXVMYYKUUWQUUVGUUVLUWPYLYFYHYK $. $} ${ @@ -290599,10 +290601,10 @@ Additional definitions for (multivariate) polynomials ( co cfv wceq eqid wcel ringlidmd cpsd cplusg cmulr cbs psrcrng crngringd crg ringidcl syl psdmul crnggrpd grpmgmd psdcl ringridmd oveq12d 3eqtr3rd fveq2d cgrp wb grpid syl2anc mpbid eqcomd ) AHDGEBUAOPZPZAVEVECUBPZOZVEQZ - HVEQZADDCUCPZOZVDPVEDVJOZDVEVJOZVFOVEVGACUDPZVFBCVJDDEFGIVNRZVFRZVJRZLMNA - CUGSDVNSACABCEFILMUEZUFZVNCDVOJUHUIZVTUJAVKDVDAVNCVJDDVOVQJVSVTTUQAVLVEVM - VEVFAVNCVJDVEVOVQJVSAVNBCDEFGIVOLABABMUKULNVTUMZUNAVNCVJDVEVOVQJVSWATUOUP - ACURSVEVNSVHVIUSACVRUKWAVNVFCVEHVOVPKUTVAVBVC $. + HVEQZADDCUCPZOZVDPVEDVJOZDVEVJOZVFOVEVGACUDPZVFBCVJDDEGIVNRZVFRZVJRZMNACU + GSDVNSACABCEFILMUEZUFZVNCDVOJUHUIZVTUJAVKDVDAVNCVJDDVOVQJVSVTTUQAVLVEVMVE + VFAVNCVJDVEVOVQJVSAVNBCDEGIVOABABMUKULNVTUMZUNAVNCVJDVEVOVQJVSWATUOUPACUR + SVEVNSVHVIUSACVRUKWAVNVFCVEHVOVPKUTVAVBVC $. $} ${ @@ -290621,9 +290623,9 @@ Additional definitions for (multivariate) polynomials eleqtrd asclval syl crg crngringd psrring ringidcl psdvsca oveq2d psrlmod psd1 clmod lmodvs0 syl2anc eqtrd 3eqtrd ) ADBSZIGEUAUBSZSDFUCSZFUDSZUBZVJ SDVKVJSZVLUBZJAVIVMVJADFUESZUFSZUGZVIVMUHADCVQRACEUFSVQNAEVPUFAEFGHUIKOPU - JUKULUMZBVLVKVPVQFDMVPTZVQTZVLTZVKTZUNUOUKAFUFSZDEFVLVKGCHIKWDTZWBNOPQAFU - PUGVKWDUGAEFGHKOAEPUQZURWDFVKWEWCUSUORUTAVODJVLUBZJAVNJDVLAEFVKGHIJKWCLOP - QVCVAAFVDUGVRWGJUHAEFGHKOWFVBVSVLVPVQFDJVTWBWALVEVFVGVH $. + JUKULUMZBVLVKVPVQFDMVPTZVQTZVLTZVKTZUNUOUKAFUFSZDEFVLVKGCIKWDTZWBNPQAFUPU + GVKWDUGAEFGHKOAEPUQZURWDFVKWEWCUSUORUTAVODJVLUBZJAVNJDVLAEFVKGHIJKWCLOPQV + CVAAFVDUGVRWGJUHAEFGHKOWFVBVSVLVPVQFDJVTWBWALVEVFVGVH $. $} ${ @@ -291024,12 +291026,12 @@ According to Wikipedia ("Polynomial", 23-Dec-2019, (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 19-Jul-2019.) $) coe1sfi $p |- ( F e. B -> A finSupp .0. ) $= - ( vx vy wcel cn0 c1o co c0 cfv eqid cvv cmap cmpt ccnv cfsupp df1o2 nn0ex - ccom 0ex mapsncnv coe1fval2 cmpl cbs ply1bascl2 cpl1 elbasfv mplelsfi wf1 - cv wf1o mapsnf1o2 f1ocnv f1of1 mp2b a1i c0g fvexi id fsuppco eqbrtrd ) EB - MZAEKNOUAPZQKURRUBZUCZUGFUDLABCDEVMGHIKLNOVLQUEUFUHVLSZUIUJVJEVMBTNVKFVJO - DUKPZULRZVODEOTFVOSVPSJBCDEIHUMBCUNEDIHUOUPNVKVMUQZVJVKNVLUSNVKVMUSVQKNOV - LQUEUFUHVNUTVKNVLVANVKVMVBVCVDFTMVJFDVEJVFVDVJVGVHVI $. + ( vx vy wcel cn0 c1o co c0 cfv df1o2 eqid cmap cmpt ccnv cfsupp nn0ex 0ex + cv ccom mapsncnv coe1fval2 cvv cmpl cbs ply1bascl2 mplelsfi wf1 mapsnf1o2 + wf1o f1ocnv f1of1 mp2b a1i c0g fvexi id fsuppco eqbrtrd ) EBMZAEKNOUAPZQK + UGRUBZUCZUHFUDLABCDEVKGHIKLNOVJQSUEUFVJTZUIUJVHEVKBUKNVIFVHODULPZUMRZVMDE + OFVMTVNTJBCDEIHUNUONVIVKUPZVHVINVJURNVIVKURVOKNOVJQSUEUFVLUQVINVJUSNVIVKU + TVAVBFUKMVHFDVCJVDVBVHVEVFVG $. coe1fvalcl.k $e |- K = ( Base ` R ) $. $d A g $. $d K g $. $d .0. g $. @@ -294463,8 +294465,8 @@ univariate polynomial evaluation map function for a (sub)ring is a ring LRZUAUMJUOUDZUPZUOUDWBAWDWGVTSSAGUEUQAWEUAWFWGSWGTZAUMJUOURUSZAWGFUEQZWDI HAIFGUTUDRZWJWDIVAOWJWDFGIWJTZWDTZVBVGZABWGDFUAJWJHKWLMWHPVCZVDVEAWBWGGWA UAJWDSWATZWMWHWBTZAHBRJSRPBDFJHKMVFVGVHVIAWGWJWJWDSHISSWCFUFQZAGUFUQAFVJR - ZWRWJRAWKWSOFGIVKVGZWJFWRWLWRTZVLVGWOWNAWJVMWIAFUEUQABDFHJVJWRKMXAPWTVNAW - KWRIQWCVQOFGIWCWRXAWCTZVRVGVOWBEGWACJVTWCLWPWQXBNVPVS $. + ZWRWJRAWKWSOFGIVKVGWJFWRWLWRTZVLVGWOWNAWJVMWIAFUEUQABDFHJWRKMWTPVNAWKWRIQ + WCVQOFGIWCWRWTWCTZVRVGVOWBEGWACJVTWCLWPWQXANVPVS $. $} ${ @@ -371401,22 +371403,22 @@ or are almost disjoint (the interiors are disjoint). (Contributed by mdegldg $p |- ( ( R e. Ring /\ F e. B /\ F =/= Y ) -> E. x e. A ( ( F ` x ) =/= .0. /\ ( H ` x ) = ( D ` F ) ) ) $= ( crg wcel wne w3a cfv csupp co cima cv wceq wa wrex cxr clt csup mdegval - 3ad2ant2 cfn c0 wss wfun wf tdeglem1 ffund simp2 simp1 mplelsfi fsuppimpd - cn0 a1i imafi syl2anc csn cxp simp3 cvv mplrcl cgrp ringgrp 3ad2ant1 mpl0 - neeqtrd wfn wb cbs eqid mplelf ffnd c0g fvexi ccnv cn cmap ovex fnsuppeq0 - rabex2 mp3an2 sylancl necon3bid mpbird suppssdm fnimaeq0 crn imassrn frnd - fssdm sstrid nn0ssre ressxr sstri sstrdi wor fisupcl mpan syl3anc eqeltrd - cr xrltso fvelimabd rexsupp mp3an23 syl bitrd mpbid ) FUAUBZICUBZILUCZUDZ - IDUEZJIMUFUGZUHZUBZAUIZIUEMUCYMJUEYIUJZUKABULZYHYIYKUMUNUOZYKYFYEYIYPUJYG - BCDEFGHIJKMNOPQRSUPUQYHYKURUBZYKUSUCZYKUMUTZYPYKUBZYHJVAYJURUBYQYHBVIJBVI - JVBYHBGHJKRSVCVJZVDYHIMYHCEFIKUAMOPQYEYFYGVEZYEYFYGVFVGVHJYJVKVLYHYRYJUSU - CZYHUUCIBMVMVNZUCYHILUUDYEYFYGVOYHBEFHKMVPLORQTYFYEKVPUBYGCEFKIOPVQUQYEYF - FVRUBYGFVSVTWAWBYHYJUSIUUDYHIBWCZMVPUBZYJUSUJZIUUDUJWDZYHBFWEUEZIYHCBEFHK - UUIIOUUIWFPRUUBWGZWHZMFWIQWJZUUEBVPUBZUUFUUHHUIWKWLUHURUBHVIKWMUGBRVIKWMW - NWPZBIVPVPMWOWQWRWSWTYHYKUSYJUSYHJBWCYJBUTYKUSUJUUGWDYHBVIJUUAWHZYHBUUIYJ - IIMXAUUJXFZBYJJXBVLWSWTYHYKVIUMYHYKJXCVIJYJXDYHBVIJUUAXEXGVIXQUMXHXIXJXKU - MUNXLYQYRYSUDYTXRUMYKUNXMXNXOXPYHYLYNAYJULZYOYHABYJYIJUUOUUPXSYHUUEUUQYOW - DZUUKUUEUUMUUFUURUUNUULYNAIVPVPBMXTYAYBYCYD $. + 3ad2ant2 cfn c0 wss wfun wf tdeglem1 ffund simp2 mplelsfi fsuppimpd imafi + cn0 a1i syl2anc csn cxp cvv mplrcl cgrp ringgrp 3ad2ant1 mpl0 neeqtrd wfn + simp3 wb cbs eqid mplelf ffnd c0g fvexi ccnv cmap rabex2 fnsuppeq0 mp3an2 + cn ovex sylancl necon3bid mpbird suppssdm fssdm fnimaeq0 crn imassrn frnd + sstrid cr nn0ssre ressxr sstri sstrdi xrltso fisupcl mpan syl3anc eqeltrd + wor fvelimabd rexsupp mp3an23 syl bitrd mpbid ) FUAUBZICUBZILUCZUDZIDUEZJ + IMUFUGZUHZUBZAUIZIUEMUCYLJUEYHUJZUKABULZYGYHYJUMUNUOZYJYEYDYHYOUJYFBCDEFG + HIJKMNOPQRSUPUQYGYJURUBZYJUSUCZYJUMUTZYOYJUBZYGJVAYIURUBYPYGBVIJBVIJVBYGB + GHJKRSVCVJZVDYGIMYGCEFIKMOPQYDYEYFVEZVFVGJYIVHVKYGYQYIUSUCZYGUUBIBMVLVMZU + CYGILUUCYDYEYFWBYGBEFHKMVNLORQTYEYDKVNUBYFCEFKIOPVOUQYDYEFVPUBYFFVQVRVSVT + YGYIUSIUUCYGIBWAZMVNUBZYIUSUJZIUUCUJWCZYGBFWDUEZIYGCBEFHKUUHIOUUHWEPRUUAW + FZWGZMFWHQWIZUUDBVNUBZUUEUUGHUIWJWOUHURUBHVIKWKUGBRVIKWKWPWLZBIVNVNMWMWNW + QWRWSYGYJUSYIUSYGJBWAYIBUTYJUSUJUUFWCYGBVIJYTWGZYGBUUHYIIIMWTUUIXAZBYIJXB + VKWRWSYGYJVIUMYGYJJXCVIJYIXDYGBVIJYTXEXFVIXGUMXHXIXJXKUMUNXQYPYQYRUDYSXLU + MYJUNXMXNXOXPYGYKYMAYIULZYNYGABYIYHJUUNUUOXRYGUUDUUPYNWCZUUJUUDUULUUEUUQU + UMUUKYMAIVNVNBMXSXTYAYBYC $. $} ${ @@ -371457,17 +371459,16 @@ or are almost disjoint (the interiors are disjoint). (Contributed by mdegcl $p |- ( F e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) ) $= ( vb va wcel cfn cn0 co cxr clt cmnf eqid c0 cfv cv ccnv cima cmap ccnfld cn crab cgsu cmpt c0g csupp csup csn cun mdegval supeq1 eleq1d wne wa wss - wceq crn imassrn wf tdeglem1 frn mp1i sstrid adantr ssun1 sstrdi wfun cvv - ffun id reldmmpl elbasov simprd mplelsfi fsuppimpd imafi syl2anc simpr cr - cmpl nn0ssre ressxr sstri wor w3a xrltso fisupcl mpan sseldd xrsup0 ssun2 - syl3anc mnfxr elexi snid sselii eqeltri a1i pm2.61ne eqeltrd ) EALZEBUAJK - UBUCUGUDMLKNFUEOUHZUFJUBUIOUJZEDUKUAZULOZUDZPQUMZNRUNZUOZXHABCDJKEXIFXJGH - IXJSZXHSZXISZUPXGXMXOLTPQUMZXOLZXLTXLTVBXMXSXOPXLTQUQURXGXLTUSZUTZXLXOXMY - BXLNXOXGXLNVAYAXGXLXIVCZNXIXKVDXHNXIVEZYCNVAXGXHJKXIFXQXRVFZXHNXIVGVHVIVJ - ZNXNVKVLYBXLMLZYAXLPVAZXMXLLZXGYGYAXGXIVMZXKMLYGYDYJXGYEXHNXIVOVHXGEXJXGA - CDEFVNXJHIXPXGVPXGFVNLDVNLEACWFFDVQHIVRVSVTWAXIXKWBWCVJXGYAWDYBXLNPYFNWEP - WGWHWIVLPQWJYGYAYHWKYIWLPXLQWMWNWRWOXTXGXSRXOWPXNXORXNNWQRRPWSWTXAXBXCXDX - EXF $. + wceq crn imassrn wf tdeglem1 mp1i sstrid adantr ssun1 sstrdi wfun ffun id + frn mplelsfi fsuppimpd imafi syl2anc simpr cr nn0ssre ressxr sstri xrltso + wor w3a fisupcl mpan syl3anc sseldd xrsup0 ssun2 mnfxr elexi snid eqeltri + sselii a1i pm2.61ne eqeltrd ) EALZEBUAJKUBUCUGUDMLKNFUEOUHZUFJUBUIOUJZEDU + KUAZULOZUDZPQUMZNRUNZUOZXCABCDJKEXDFXEGHIXESZXCSZXDSZUPXBXHXJLTPQUMZXJLZX + GTXGTVBXHXNXJPXGTQUQURXBXGTUSZUTZXGXJXHXQXGNXJXBXGNVAXPXBXGXDVCZNXDXFVDXC + NXDVEZXRNVAXBXCJKXDFXLXMVFZXCNXDVOVGVHVIZNXIVJVKXQXGMLZXPXGPVAZXHXGLZXBYB + XPXBXDVLZXFMLYBXSYEXBXTXCNXDVMVGXBEXEXBACDEFXEHIXKXBVNVPVQXDXFVRVSVIXBXPV + TXQXGNPYANWAPWBWCWDVKPQWFYBXPYCWGYDWEPXGQWHWIWJWKXOXBXNRXJWLXIXJRXINWMRRP + WNWOWPWRWQWSWTXA $. $} ${ @@ -698817,6 +698818,14 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) + $( Avoid axioms in ~ base0 by using the discouraged ~ df-base . This kind of + axiom save is probably not worth it. (Contributed by SN, 16-Sep-2025.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + sn-base0 $p |- (/) = ( Base ` (/) ) $= + ( cbs c1 df-base str0 ) ABCD $. + $( $j usage 'sn-base0' avoids 'ax-pow' 'ax-un' 'ax-cnex' 'ax-1cn' + 'ax-addcl'; $) + ${ nelsubginvcld.g $e |- ( ph -> G e. Grp ) $. nelsubginvcld.s $e |- ( ph -> S e. ( SubGrp ` G ) ) $. @@ -700069,16 +700078,16 @@ trivial one ( ~ abvtrivg ). (Contributed by SN, 3-Jul-2025.) $) ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) finSupp ( 0g ` S ) ) $= ( cv cfv co cmpt cgsu c0g cvv wcel ccnv cn cima cfn cn0 cmap rabex2 mptex - ovex a1i fvexd wfun funmpt eqid cress ovexi mplelsfi csupp cdif wa mplelf - cbs ssidd suppssrg csubrg subrg0 syl eqcomd adantr eqtrd oveq1d crngringd - wceq eldifi ccrg simpr evlsvvvallem sylan2 ringlzd suppss2 fsuppsssuppgd - crg ) AMRERULZMUMZPBNBULZXBUMXDCUMLUNUOUPUNZIUNZUOZJUQUMZURURHUQUMZXGURUS - AREXFKULUTVAVBVCUSKVDNVEUNESVDNVEVHVFZVGVIAHUQVJXGVKAREXFVLVIADFJMNURXHTU - BXHVMUJJURUSAJHGVNUAVOVIVPAEXFRURMXHVQUNZXIAXBEXKVRUSZVSZXFXIXEIUNXIXMXCX - IXEIXMXCXHXIAEJWAUMZURMDXKXBXHADEFJKNXNMTXNVMUBSUJVTAXKWBUJAJUQVJWCAXHXIW - LXLAXIXHAGHWDUMUSXIXHWLUIGHJXIUAXIVMZWEWFWGWHWIWJXMOHIXEXIUCUFXOAHXAUSXLA - HUHWKWHXLAXBEUSZXEOUSXBEXKWMAXPVSBCXBEHKLNOPQSUCUDUEANQUSXPUGWHAHWNUSXPUH - WHACONVEUNUSXPUKWHAXPWOWPWQWRWIEURUSAXJVIWSWT $. + ovex a1i fvexd wfun funmpt eqid mplelsfi csupp cdif wa cbs ssidd suppssrg + mplelf wceq csubrg subrg0 syl eqcomd adantr eqtrd oveq1d crngringd eldifi + crg ccrg simpr evlsvvvallem sylan2 ringlzd suppss2 fsuppsssuppgd ) AMRERU + LZMUMZPBNBULZWTUMXBCUMLUNUOUPUNZIUNZUOZJUQUMZURURHUQUMZXEURUSAREXDKULUTVA + VBVCUSKVDNVEUNESVDNVEVHVFZVGVIAHUQVJXEVKAREXDVLVIADFJMNXFTUBXFVMUJVNAEXDR + URMXFVOUNZXGAWTEXIVPUSZVQZXDXGXCIUNXGXKXAXGXCIXKXAXFXGAEJVRUMZURMDXIWTXFA + DEFJKNXLMTXLVMUBSUJWAAXIVSUJAJUQVJVTAXFXGWBXJAXGXFAGHWCUMUSXGXFWBUIGHJXGU + AXGVMZWDWEWFWGWHWIXKOHIXCXGUCUFXMAHWLUSXJAHUHWJWGXJAWTEUSZXCOUSWTEXIWKAXN + VQBCWTEHKLNOPQSUCUDUEANQUSXNUGWGAHWMUSXNUHWGACONVEUNUSXNUKWGAXNWNWOWPWQWH + EURUSAXHVIWRWS $. $} ${ @@ -700121,60 +700130,60 @@ trivial one ( ~ abvtrivg ). (Contributed by SN, 3-Jul-2025.) $) xpex fveq2 ad3antrrr pwsexpg 3eqtr4d eqfnfvd cfsupp psrbagfsupp cc sylan2 wbr 0cnd ringidval mulg0 pws1 pwsgprod oveq12d wss eqsstrrd fssd fconst6g subrgss pwsmulrval fvex fvconst2 ccnv cn cfn rabexd ringcmnd simpl simprr - cima simprl syl21anc ringcld cress mplelsfi subrg0 eqtr4d sylanl2 ringlzd - ovexi cmnmndd pws0g pwsgsum fvmptd4 ) AUNBHSDSUSZNUTZQLOLUSZUWPUTZUWRUNUS - ZUTZMVAZVBZVCVAZIVAZVBZVCVAZHSDUWQQLOUWSUWRBUTZMVAZVBZVCVAZIVAZVBZVCVAPOV - DVAZNFUTZVJUWTBVEZUXFUXMHVCUXPSDUXEUXLUXPUXDUXKUWQIUXPUXCUXJQVCUXPLOUXBUX - IUXPUXAUXHUWSMUWRUWTBVFVGVHVGVGVHVGAUXOHUXNVIVAZSDUWQUOGUXNUOUSZVKZVLZVBZ - UTZUXQVMUTZUWPUOOUPUXNUXRUPUSZUTZVBZVBZUYCVNUTZVOVAZVCVAZUXQVPUTZVAZVBZVC - VAUXQSDUNUXNUXEVBZVBZVCVAUNUXNUXGVBAUONCDEFGHUXQUYKJKUYHUYAUYGOPUYCRUPSTU - AUBUDUEUCUXQVQZUYCVQZUYHVQZUYKVQZUYAVQZUYGVQZUIUJUKULVRAUYMUYOUXQVCASDUYL - UYNAUWPDVSZVTZUYLUXNUWQVKZVLZUQUXNQLOUWSUWRUQUSZUTZMVAZVBZVCVAZVBZUYKVAVU - EVUKIVOVAUYNVUCUYBVUEUYJVUKUYKVUCUOUWQUXTVUEGUYAVJUYTUXRUWQVEUXSVUDUXNUXR - UWQWEWAADGUWPNADGNWBDJWCUTZNWBACDEJKOVULNUAVULVQUBUDULWDZAGVULNDAGHWFUTVS - ZGVULVEUKGHJUCWGZWHWIUUAWJVUEVJVSVUCUXNVUDPOVDWKZUWQUUBUUIWLWMVUCUYJUYCLO - UQUXNVUHVBZVBZVCVAVUKVUCUYIVURUYCVCVUCUYILOUWSUPUXNUWRUYDUTZVBZUYHVAZVBVU - RVUCLOOUWSVUTUYHOUWPUYGRRVUCOWNUWPVUBOWNUWPWBADKUWPOUDUUCWOZWQUYGOWPVUCUO - OUYFUYGUPUXNUYEVUPUUDVUAWRWLAORVSZVUBUIWSZVVDOWTVUCUWROVSZVTZUWSUUEVVFUOU - WRUYFVUTOUYGUXQWCUTZVUAUOLXHUPUXNUYEVUSUXRUWRUYDUUJVHVUCVVEXAVVFPHUXNVVGX - BVUTUXQVJUYPUEVVGVQZAHXBVSZVUBVVEUJXCZVVFPOVDXRZVVFUPUXNVUSPVVEUYDUXNVSZV - USPVSZVUCVVLVVEVVMVVLOPUWRUYDUYDPOXDWJXEXFXGXIZWMXJVUCLOVVAVUQVVFURUXNVVA - VUQVVFUXNPVVAVVFPHUXNVVGXBVVAUXQVJUYPUEVVHVVJVVKVVFVVGUYHUYCUWSVUTVVGUXQU - YCUYQVVHXKUYRAUYCXLVSZVUBVVEAUXQXMVSZVVOAHXMVSZUXNVJVSZVVPAHUJUUFZAPOVDXR - ZHUXNVJUXQUYPUUGXNUXQUYCUYQXOWHXCVUCOWNUWRUWPVVBWJZVVNXPUUHWQVUQUXNWPVVFU - QUXNVUHVUQUWSVUGMWKVUQVQZWRWLVVFURUSZUXNVSZVTZUWSVWCVUTUTZMVAUWSUWRVWCUTZ - MVAZVWCVVAUTVWCVUQUTVWEVWFVWGUWSMVWEUPVWCVUSVWGUXNVUTVJVUTVQUWRUYDVWCVFVV - FVWDXAZVWEUWRVWCXSWMVGVWEVWCVVGHUYHQMUXNUYCUWSVJVUTUXQUYPVVHUYQUFUYRUGAVV - QVUBVVEVWDVVSUUKVWEPOVDXRVVFUWSWNVSZVWDVWAWSVVFVUTVVGVSVWDVVNWSVWIUULVWEU - QVWCVUHVWHUXNVUQVJVWBUQURXHVUGVWGUWSMUWRVUFVWCVFVGVWIVWEUWSVWGMXRWMUUMUUN - XQXTVGVUCUQLPHQVUHUXQYAUTZUXNOUYCVJRUXQUYPUEVWKVQUYQUFVUCPOVDXRZVVDAVVIVU - BUJWSZVUCVUFUXNVSZVVEVTZVTPMQUWSVUGPHQUFUEXKZUGAQXLVSZVUBVWOAVVQVWQVVSHQU - FXOWHXCVUCVVEVWJVWNVWAYBVWOVUGPVSZVUCVWNOPUWRVUFVUFPOXDWJZWOXPVUCUWPVURYR - VJVJVWKVUCLOVUQRVVDYCVUCUXQYAXSVURYDVUCLOVUQYEWLVUBUWPYRUUOUUSADKUWPOUDUU - PWOVUCOVUQLRUWPYRYFVAZVWKVUCUWROVWTYGVSZVTZVUQUQUXNHYAUTZVBZVWKVXBUQUXNVU - HVXCVXBVWNVTZVUHYRVUGMVAZVXCVXBVUHVXFVEVWNVXBUWSYRVUGMVUCOWNUUQUWPRVWTUWR - YRVVBVUCVWTYHVVDVUCUUTYIYJWSVXEVWRVXFVXCVEVXAVWNVWRVUCVWNVXAVWRVXAVWNVVEV - WRUWROVWTYKVWSUURXEXFPMQVUGVXCVWPHVXCQUFVXCVQZUVAUGUVBWHXTXQVXBVXDUXNVXCV - KVLZVWKUQUXNVXCYLAVXHVWKVEZVUBVXAAVVQVVRVXIVVSVVTHVXCUXNVJUXQUYPVXGUVCXNX - CYMXTVVDYNYOUVDXTUVEVUCVVGHUYKIVUEVUKUXNXBVJUXQUYPVVHVWMVWLVUCPHUXNVVGXBV - UEUXQVJUYPUEVVHVWMVWLVUCUWQPVSZUXNPVUEWBADPUWPNADVULPNVUMAVUNVULPUVFUKVUN - VULGPVUOGPHUEUVJUVGWHUVHZWJZUXNUWQPUVIWHZXIVUCPHUXNVVGXBVUKUXQVJUYPUEVVHV - WMVWLVUCUQUXNVUJPVUCVWNVTLVUFUWPDHKMOPQRUDUEUFUGAVVCVUBVWNUIXCAVVIVUBVWNU - JXCVUCVWNXAAVUBVWNYPYQXGXIUHUYSUVKVUCUNUXNUXNUWQUXDIUXNVUEVUKVJVJVUCUXNPV - UEVXMWQVUKUXNWPVUCUQUXNVUJVUKQVUIVCWKVUKVQZWRWLVWLVWLUXNWTUWTUXNVSZUWTVUE - UTUWQVEVUCUXNUWQUWTUWPNUVLUVMWOVUCVXOVTZUQUWTVUJUXDUXNVUKPVXNUQUNXHZVUIUX - CQVCVXQLOVUHUXBVXQVUGUXAUWSMUWRVUFUWTVFVGVHVGVUCVXOXAZVXPLUWTUWPDHKMOPQRU - DUEUFUGAVVCVUBVXOUIXCAVVIVUBVXOUJXCVXRAVUBVXOYPYQZWMXJYSXQVGAUNSPHUXEUXND - VJVJUXQUXQYTUTZUYPUEVXTVQVVTAKUSUVNUVOUWAUVPVSKWNOVDVADVJUDAWNOVDXRUVQZAH - VVSUVRZAVXOVUBVTZVTZPHIUWQUXDUEUHAVVQVYCVVSWSAVUBVXJVXOVXLYBVYDAVUBVXOUXD - PVSZAVYCUVSAVXOVUBUVTAVXOVUBUWBVXSUWCUWDANUYOJYTUTZVJVJVXTASDUYNVJVYAYCAU - XQYTXSUYOYDASDUYNYEWLACEJNOVJVYFUAUBVYFVQULJVJVSAJHGUWEUCUWKWLUWFADUYNSVJ - NVYFYFVAZVXTAUWPDVYGYGVSZVTZUYNUNUXNHYTUTZVBZVXTVYIUNUXNUXEVYJVYIVXOVTZUX - EVYJUXDIVAVYJVYLUWQVYJUXDIVYIUWQVYJVEVXOVYIUWQVYFVYJADPVJNVJVYGUWPVYFVXKA - VYGYHVYAAJYTXSYIAVYJVYFVEZVYHAVUNVYMUKGHJVYJUCVYJVQZUWGWHWSUWHWSYJVYLPHIU - XDVYJUEUHVYNAVVQVYHVXOVVSXCVYHAVUBVXOVYEUWPDVYGYKVXSUWIUWJXTXQAVYKVXTVEVY - HAVYKUXNVYJVKVLZVXTUNUXNVYJYLAHXLVSVVRVYOVXTVEAHVYBUWLVVTHUXNVJUXQVYJUYPV - YNUWMXNYMWSXTVYAYNYOUWNYSUMAHUXMVCXRUWO $. + cima simprl syl21anc ringcld mplelsfi subrg0 eqtr4d sylanl2 ringlzd pws0g + cmnmndd pwsgsum fvmptd4 ) AUNBHSDSUSZNUTZQLOLUSZUWNUTZUWPUNUSZUTZMVAZVBZV + CVAZIVAZVBZVCVAZHSDUWOQLOUWQUWPBUTZMVAZVBZVCVAZIVAZVBZVCVAPOVDVAZNFUTZVJU + WRBVEZUXDUXKHVCUXNSDUXCUXJUXNUXBUXIUWOIUXNUXAUXHQVCUXNLOUWTUXGUXNUWSUXFUW + QMUWPUWRBVFVGVHVGVGVHVGAUXMHUXLVIVAZSDUWOUOGUXLUOUSZVKZVLZVBZUTZUXOVMUTZU + WNUOOUPUXLUXPUPUSZUTZVBZVBZUYAVNUTZVOVAZVCVAZUXOVPUTZVAZVBZVCVAUXOSDUNUXL + UXCVBZVBZVCVAUNUXLUXEVBAUONCDEFGHUXOUYIJKUYFUXSUYEOPUYARUPSTUAUBUDUEUCUXO + VQZUYAVQZUYFVQZUYIVQZUXSVQZUYEVQZUIUJUKULVRAUYKUYMUXOVCASDUYJUYLAUWNDVSZV + TZUYJUXLUWOVKZVLZUQUXLQLOUWQUWPUQUSZUTZMVAZVBZVCVAZVBZUYIVAVUCVUIIVOVAUYL + VUAUXTVUCUYHVUIUYIVUAUOUWOUXRVUCGUXSVJUYRUXPUWOVEUXQVUBUXLUXPUWOWEWAADGUW + NNADGNWBDJWCUTZNWBACDEJKOVUJNUAVUJVQUBUDULWDZAGVUJNDAGHWFUTVSZGVUJVEUKGHJ + UCWGZWHWIUUAWJVUCVJVSVUAUXLVUBPOVDWKZUWOUUBUUIWLWMVUAUYHUYALOUQUXLVUFVBZV + BZVCVAVUIVUAUYGVUPUYAVCVUAUYGLOUWQUPUXLUWPUYBUTZVBZUYFVAZVBVUPVUALOOUWQVU + RUYFOUWNUYERRVUAOWNUWNUYTOWNUWNWBADKUWNOUDUUCWOZWQUYEOWPVUAUOOUYDUYEUPUXL + UYCVUNUUDUYSWRWLAORVSZUYTUIWSZVVBOWTVUAUWPOVSZVTZUWQUUEVVDUOUWPUYDVUROUYE + UXOWCUTZUYSUOLXHUPUXLUYCVUQUXPUWPUYBUUJVHVUAVVCXAVVDPHUXLVVEXBVURUXOVJUYN + UEVVEVQZAHXBVSZUYTVVCUJXCZVVDPOVDXRZVVDUPUXLVUQPVVCUYBUXLVSZVUQPVSZVUAVVJ + VVCVVKVVJOPUWPUYBUYBPOXDWJXEXFXGXIZWMXJVUALOVUSVUOVVDURUXLVUSVUOVVDUXLPVU + SVVDPHUXLVVEXBVUSUXOVJUYNUEVVFVVHVVIVVDVVEUYFUYAUWQVURVVEUXOUYAUYOVVFXKUY + PAUYAXLVSZUYTVVCAUXOXMVSZVVMAHXMVSZUXLVJVSZVVNAHUJUUFZAPOVDXRZHUXLVJUXOUY + NUUGXNUXOUYAUYOXOWHXCVUAOWNUWPUWNVUTWJZVVLXPUUHWQVUOUXLWPVVDUQUXLVUFVUOUW + QVUEMWKVUOVQZWRWLVVDURUSZUXLVSZVTZUWQVWAVURUTZMVAUWQUWPVWAUTZMVAZVWAVUSUT + VWAVUOUTVWCVWDVWEUWQMVWCUPVWAVUQVWEUXLVURVJVURVQUWPUYBVWAVFVVDVWBXAZVWCUW + PVWAXSWMVGVWCVWAVVEHUYFQMUXLUYAUWQVJVURUXOUYNVVFUYOUFUYPUGAVVOUYTVVCVWBVV + QUUKVWCPOVDXRVVDUWQWNVSZVWBVVSWSVVDVURVVEVSVWBVVLWSVWGUULVWCUQVWAVUFVWFUX + LVUOVJVVTUQURXHVUEVWEUWQMUWPVUDVWAVFVGVWGVWCUWQVWEMXRWMUUMUUNXQXTVGVUAUQL + PHQVUFUXOYAUTZUXLOUYAVJRUXOUYNUEVWIVQUYOUFVUAPOVDXRZVVBAVVGUYTUJWSZVUAVUD + UXLVSZVVCVTZVTPMQUWQVUEPHQUFUEXKZUGAQXLVSZUYTVWMAVVOVWOVVQHQUFXOWHXCVUAVV + CVWHVWLVVSYBVWMVUEPVSZVUAVWLOPUWPVUDVUDPOXDWJZWOXPVUAUWNVUPYRVJVJVWIVUALO + VUORVVBYCVUAUXOYAXSVUPYDVUALOVUOYEWLUYTUWNYRUUOUUSADKUWNOUDUUPWOVUAOVUOLR + UWNYRYFVAZVWIVUAUWPOVWRYGVSZVTZVUOUQUXLHYAUTZVBZVWIVWTUQUXLVUFVXAVWTVWLVT + ZVUFYRVUEMVAZVXAVWTVUFVXDVEVWLVWTUWQYRVUEMVUAOWNUUQUWNRVWRUWPYRVUTVUAVWRY + HVVBVUAUUTYIYJWSVXCVWPVXDVXAVEVWSVWLVWPVUAVWLVWSVWPVWSVWLVVCVWPUWPOVWRYKV + WQUURXEXFPMQVUEVXAVWNHVXAQUFVXAVQZUVAUGUVBWHXTXQVWTVXBUXLVXAVKVLZVWIUQUXL + VXAYLAVXFVWIVEZUYTVWSAVVOVVPVXGVVQVVRHVXAUXLVJUXOUYNVXEUVCXNXCYMXTVVBYNYO + UVDXTUVEVUAVVEHUYIIVUCVUIUXLXBVJUXOUYNVVFVWKVWJVUAPHUXLVVEXBVUCUXOVJUYNUE + VVFVWKVWJVUAUWOPVSZUXLPVUCWBADPUWNNADVUJPNVUKAVULVUJPUVFUKVULVUJGPVUMGPHU + EUVJUVGWHUVHZWJZUXLUWOPUVIWHZXIVUAPHUXLVVEXBVUIUXOVJUYNUEVVFVWKVWJVUAUQUX + LVUHPVUAVWLVTLVUDUWNDHKMOPQRUDUEUFUGAVVAUYTVWLUIXCAVVGUYTVWLUJXCVUAVWLXAA + UYTVWLYPYQXGXIUHUYQUVKVUAUNUXLUXLUWOUXBIUXLVUCVUIVJVJVUAUXLPVUCVXKWQVUIUX + LWPVUAUQUXLVUHVUIQVUGVCWKVUIVQZWRWLVWJVWJUXLWTUWRUXLVSZUWRVUCUTUWOVEVUAUX + LUWOUWRUWNNUVLUVMWOVUAVXMVTZUQUWRVUHUXBUXLVUIPVXLUQUNXHZVUGUXAQVCVXOLOVUF + UWTVXOVUEUWSUWQMUWPVUDUWRVFVGVHVGVUAVXMXAZVXNLUWRUWNDHKMOPQRUDUEUFUGAVVAU + YTVXMUIXCAVVGUYTVXMUJXCVXPAUYTVXMYPYQZWMXJYSXQVGAUNSPHUXCUXLDVJVJUXOUXOYT + UTZUYNUEVXRVQVVRAKUSUVNUVOUWAUVPVSKWNOVDVADVJUDAWNOVDXRUVQZAHVVQUVRZAVXMU + YTVTZVTZPHIUWOUXBUEUHAVVOVYAVVQWSAUYTVXHVXMVXJYBVYBAUYTVXMUXBPVSZAVYAUVSA + VXMUYTUVTAVXMUYTUWBVXQUWCUWDANUYMJYTUTZVJVJVXRASDUYLVJVXSYCAUXOYTXSUYMYDA + SDUYLYEWLACEJNOVYDUAUBVYDVQULUWEADUYLSVJNVYDYFVAZVXRAUWNDVYEYGVSZVTZUYLUN + UXLHYTUTZVBZVXRVYGUNUXLUXCVYHVYGVXMVTZUXCVYHUXBIVAVYHVYJUWOVYHUXBIVYGUWOV + YHVEVXMVYGUWOVYDVYHADPVJNVJVYEUWNVYDVXIAVYEYHVXSAJYTXSYIAVYHVYDVEZVYFAVUL + VYKUKGHJVYHUCVYHVQZUWFWHWSUWGWSYJVYJPHIUXBVYHUEUHVYLAVVOVYFVXMVVQXCVYFAUY + TVXMVYCUWNDVYEYKVXQUWHUWIXTXQAVYIVXRVEVYFAVYIUXLVYHVKVLZVXRUNUXLVYHYLAHXL + VSVVPVYMVXRVEAHVXTUWKVVRHUXLVJUXOVYHUYNVYLUWJXNYMWSXTVXSYNYOUWLYSUMAHUXKV + CXRUWM $. $} ${ @@ -700690,15 +700699,15 @@ trivial one ( ~ abvtrivg ). (Contributed by SN, 3-Jul-2025.) $) $( Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.) $) selvcl $p |- ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) e. E ) $= - ( co cfv vx cslv wcel cmvr cdif cascl cif cmpt ccom crn ces cvv ccrg eqid - cv mplrcl syl selvval cmap cpws cbs ssexd difexd mplcrngd ovexd cress crh + ( co cfv vx cslv wcel cmvr cdif cascl cif cmpt ccom crn eqid selvval cmap + cv ces cpws cbs ccrg cvv mplrcl syl ssexd difexd mplcrngd ovexd cress crh cmpl wf selvcllemh rhmf selvcllem4 ffvelcdmd pwselbas selvcllem5 eqeltrd - ) AHJIDUBSTTUAIUAUOZJUCVQJFUDSTVQIJUEZDUDSTEUFTZTUGUHZVSFUFTUIZHUIZWAUJZI - EUKSTZTZTGAUABVSWACDEFHIJULUMKLMNVSUNZWAUNZAHBUCIULUCRBCDIHKLUPUQZPQRURAG - IUSSZGVTWEAGEWIEWIUTSZVATZUMWEWJULWJUNZOWKUNZAEFJULNAJIULWHQVBAFDVRULMAIJ - ULWHVCPVDVDAGIUSVEAIEWCVFSZVHSZVATZWKWBWDAWDWOWJVGSUCWPWKWDVIAGVSWAWDDWNE - FIJULWOWJMNWFWGWDUNWOUNZWNUNZWLOWHPQVJWPWKWOWJWDWPUNZWMVKUQABVSWACDWNEFHI - JWOWPKLMNWFWGWRWQWSPQRVLVMVNAUAVSDEFGVTIJULMNWFOVTUNWHPQVOVMVP $. + ) AHJIDUBSTTUAIUAUNZJUCVQJFUDSTVQIJUEZDUDSTEUFTZTUGUHZVSFUFTUIZHUIZWAUJZI + EUOSTZTZTGAUABVSWACDEFHIJKLMNVSUKZWAUKZQRULAGIUMSZGVTWEAGEWHEWHUPSZUQTZUR + WEWIUSWIUKZOWJUKZAEFJUSNAJIUSAHBUCIUSUCRBCDIHKLUTVAZQVBAFDVRUSMAIJUSWMVCP + VDVDAGIUMVEAIEWCVFSZVHSZUQTZWJWBWDAWDWOWIVGSUCWPWJWDVIAGVSWAWDDWNEFIJUSWO + WIMNWFWGWDUKWOUKZWNUKZWKOWMPQVJWPWJWOWIWDWPUKZWLVKVAABVSWACDWNEFHIJWOWPKL + MNWFWGWRWQWSPQRVLVMVNAUAVSDEFGVTIJUSMNWFOVTUKWMPQVOVMVP $. $} ${ @@ -700718,13 +700727,13 @@ trivial one ( ~ abvtrivg ). (Contributed by SN, 3-Jul-2025.) $) ( ( ( I eval T ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) $= - ( cslv co cfv cv wcel cmvr cdif cif cmpt ccom crn ces cevl cvv mplrcl syl - ccrg selvval cress cmpl cbs eqid ssexd difexd mplcrngd selvcllem3 evlsevl - selvcllem4 fveq1d eqtrd ) AJLKGUBUCUDUDBKBUEZLUFVLLIUGUCUDVLKLUHZGUGUCUDD - UDUIUJZEJUKZEULZKHUMUCUDZUDZUDVNVOKHUNUCZUDZUDABCDEFGHIJKLUOURMNOPQRAJCUF - KUOUFUACFGKJMNUPUQZSTUAUSAVNVRVTAKHVPUTUCZVAUCZVBUDZVQVPHWBVOKVSUOWCVQVCV - SVCWCVCZWBVCZWDVCZWAAHILUOPALKUOWATVDZAIGVMUOOAKLUOWAVEZSVFVFADEGHIVMLUOU - OOPQRWIWHSVGACDEFGWBHIJKLWCWDMNOPQRWFWEWGSTUAVIVHVJVK $. + ( cslv co cfv cv wcel cmvr cdif cif cmpt ccom crn cevl selvval cress cmpl + ces cbs cvv eqid mplrcl syl difexd mplcrngd selvcllem3 selvcllem4 evlsevl + ssexd fveq1d eqtrd ) AJLKGUBUCUDUDBKBUEZLUFVKLIUGUCUDVKKLUHZGUGUCUDDUDUIU + JZEJUKZEULZKHUQUCUDZUDZUDVMVNKHUMUCZUDZUDABCDEFGHIJKLMNOPQRTUAUNAVMVQVSAK + HVOUOUCZUPUCZURUDZVPVOHVTVNKVRUSWAVPUTVRUTWAUTZVTUTZWBUTZAJCUFKUSUFUACFGK + JMNVAVBZAHILUSPALKUSWFTVHZAIGVLUSOAKLUSWFVCZSVDVDADEGHIVLLUSUSOPQRWHWGSVE + ACDEFGVTHIJKLWAWBMNOPQRWDWCWESTUAVFVGVIVJ $. $} ${ @@ -700837,59 +700846,59 @@ trivial one ( ~ abvtrivg ). (Contributed by SN, 3-Jul-2025.) $) AVWRWUNXUGVXIVVQVWSWUCWVAXWIXUOXWOXWLXWTUXCZWOZUXJZACVXIVXIVXEVJVXAVXLVJV JXXCVVQWSSZAVVPWSWGAVVQYLTXYDVXITAVVQWULWIZVXIVVQXYDWUCXYDVIZUXMVKXYBXXTA VXIUXKXXIWVMAUAUKVWAVWSCVXIVWRVXEVJWUNWSSZXYDAGUACVWAVBZEWSSZVJVJXYGXYHVJ - TAUACVWAXXHUXNXQAWUNWSWGXYHUYAAUACVWAUXOXQABDEGHWEXYILMXYIVIZPNUXPACVWAUA - VJGXYIUYBRZXYGAVVRCXYKUNTZWHZVWAXYIVVTSZXYGXYMVVSXYIVVTACWWKVJGBXYKVVRXYI - WWMAXYKUXKPAEWSWGUXQXHAXYNXYGXLXYLAXYNXXCXYGAVVTEVVKXYIVJVVPXXCVYPWVIXYJX - XDWUJWWEUXRAVVPWUNWSWVLXHWRWMWRXXIUXSUXTAXWMUKURZVXITXYGXYOVWRRXYDXLXWNVW - RWUNXYGVXIVVQXYOXYDWUCWVAXWIXYGVIXYFUYCUYDXWJXWTAVVQWSWGXNZAVXLVVQVVPVNRT - ZXYDVXLSXXCXLAVXLVVQVVPVMRTXYQAVXIXXPVVQVVPUJVVMVXLIVJUDVYQWUCXXQVXLVIZWU - IAVVPWUKUXDZXXSUXIVVQVVPVXLWFVKZVVQVVPVXLXXCXYDXYFXXDUYLVKUYEZXTAUCXXAVXG - XXBVXEVXHVJXXLVVLVXFXXAYMACVXEVXMVVPVJXXCWWBXXDXXEXXIXYCYUAYAAVVLXXAWGXIA - VVLXXAVXCAXXAVXBVXLSVXCACVXIVXAVVQVVPVXLVJXYDWUCXYFAVVQXYEYEZAVVPXYSUXEXX - IXYTXYBXYPXTAUDVXBVXKVXCVXIVXLVJXYRVVMVXJVXBYMACVXIVXAVVQVJXYDWUCXYFYUBXX - IXYBXYPYAAVVMVXBWGXIWRYGUYFAVXOEUACJVVRXLZVVSXYIVGZVBZVCREYUEJUYGZUOZVCRZ - VXPAVXNYUEEVCAVXNUACVVLVVMVWTSZSZVBYUEAUAUCCVXEYUIVXGYUJVXMVXHWWHXXPVXEVV - MVWTWWHVXIXXPVVQVVPUJIVXEVWTVYQWWBWUCXXQXYAWPAXXRWWGXXSWMZWNAUAUDCVXIVWTV - XKYUIVXAVXLXYAAVXAYNAVXLYNVVMVXJVWTYMUYHAVXHYNVVLVXFYUIYMUYHAUACYUJYUDWWH - YUJVVLVVSVWJVVMVWQSZVVPVHSZRZVVPVDSZRZSVVSVVLYUNSZEVHSZRZYUDWWHVVLYUIYUPW - WHYUIVWAVVMVWSSZYUMRVWAYUNYUMRZYUPWWHVXIXXPVVQVVPVWRYUMUJVWSIVXEVWAVVMVYQ - XWIWWBWUCYUMVIZXXQXWJXWTYUKYOWWHYUTYUNVWAYUMWWHVXIXXPVVQVVPVWRYUMUJVWQIVX - EVWJVVMVYQXWIWWBWUCYVBXXQXWSXWHYUKYOXOWWHWVEVVSWVCVESZTYUNVXETYVAYUPXLAWV - EWWGWVHWMWWHVVSWWKYVCWWPAWWKYVCXLWWGAEWVCVEWVKXHWMWCWWHVXEVVPYUMVWJYULWWB - YVBAVVPYLTWWGWVPWMZXWSWWHXXPVXEVVMVWQWWHVXIXXPVVQVVPUJIVXEVWQVYQWWBWUCXXQ - XWHWPYUKWNUYIZVVTVVSYUOYUMWVCYVCVXEVVPYUNWVIWVJYVCVIWWBYVBYUOVIZYBXPYDYGW - WHVXEXXJVVPEYUOYURUIYUNVVKWWKVVSVVLVYPYVFWWLWWBYURVIZXXKWWPYVEAVVLXXJTZWW - GXXMWMZYOWWHVVSVVLULXXJULURZVVRVVKUOZXLZEYPSZXYIVGZVBZVVMVVRIUOZXLZVVPYPS - ZXXCVGZYUMRZSZYURRZYUCVVSYVMYURRZVVSXYIYURRZVGZYUSYUDWWHYWBVVSYVQVVLYVKXL - ZYVMXYIVGZXYIVGZYURRZYWEWWHYWAYWHVVSYURWWHYWAYVQVVLYVOYVRYUMRZSZVVLYVOXXC - YUMRZSZVGZYWHYWAVVLYVQYWJYWLVGZSYWNVVLYVTYWOYVQYVOYVRXXCYUMUYJUYKYVQVVLYW - JYWLUYMUYNWWHYVQYWKYWGYWMXYIWWHULVVLYVNYWGXXJYWJVJYVJVVLXLYVLYWFYVMXYIYVJ - VVLYVKUYOYQWWHVXEVVPYUMYVRYVOWWBYVBYVRVIZYVDWWHULVXEXXJVVPEYVMUIVVKVJYVKX - YIVYPWWBXYJYVMVIZXXKXVLAEYLTZWWGWWEWMZWWHCUIFXXJVVRHVVKVJKXXKWXNXURWWNYKZ - UYPZUYQYVIWWHYWFYVMXYIVJWWHEYPWGWWHEWSWGYRUYRWWHYWMVVLXXJXYIUYGVUCZSZXYIW - WHVVLYWLYXBWWHYWLXXCYXBWWHVXEVVPYUMYVOXXCWWBYVBXXDYVDYXAUYSAXXCYXBXLWWGAX - XJVVPEUIVVKXYIVJXXCVYPXXKXYJXXDWUJXXFUYTWMWRYGWWHYVHYXCXYIXLYVIXXJXYIVVLE - WSVUAVUBVKWRVUDVUEXOWWHYWIVVSYVQYWFWHZYVMXYIVGZYURRZYWEYXEYWHVVSYURYVQYWF - YVMXYIVUFVUGWWHVVSYUCYVMXYIVGZYURRYXFYWEWWHYXGYXEVVSYURWWHYUCYXDYVMXYIWWH - JIVVKUVQZYTZVVRYXHYTZYUCYXDVUHWWHYXIJHYTZAYXKWWGAHXEJAJCTZHXEJWLQCFJHKUVB - VKVUIWMWWHYXHHJAYXHHXLZWWGAWYRYXMOIHVUJUWBWMZVUKVULWWHYXJVVRHYTWWHHXEVVRW - XSVUIWWHYXHHVVRYXNVUKVULIVVKJVVRVUMVRYQXOYUCVVSYVMXYIYURUYJVUNVUOWRWWHYWA - YUQVVSYURWWHVVLYVTYUNWWHYVOVWJYVSYULYUMWWHYVOVWBUBVVKVWCYVKSZVWFVWGRZVBZV - CRVWJWWHULXXJVVPEYVMUIUBVWGVWBVVKVWEVJYVKXYIVYPXXKXYJYWQXVLXVAXVCWWDAWVGW - WGNWMYWTVUPWWHYXQVWIVWBVCWWHUBVVKYXPVWHXUAYXOVWDVWFVWGXUAVWCVVKVVRWWHWYIW - QVUQYCXRXOWRWWHVVMUMXXPUMURZYVPXLZYVRXXCVGZVBZSYVSYULWWHUMVVMYXTYVSXXPYYA - VJYYAVIYXRVVMXLYXSYVQYVRXXCYXRVVMYVPUYOYQYUKWWHYVQYVRXXCVJWWHVVPYPWGWWHVV - PWSWGYRXIWWHVVMYYAVWQWWHYYAVWKUBIVWCYVPSZVWMVWNRZVBZVCRVWQWWHUMXXPVVQVVPY - VRUJUBVWNVWKIVWLVJYVPXXCVYQXXQXXDYWPXWEWUDWUEWVOAWUSWWGWUKWMWWHCUJFXXPVVR - HIVJKXXQWXNXVTWWNYKVUPWWHYYDVWPVWKVCWWHUBIYYCVWOXWAYYBVWDVWMVWNXWAVWCIVVR - WWHWYAWQVUQYCXRXOWRYGVURWBYGXOWWHYUCYWCVVSYWDXYIWWHWWKEYURYVMVVSWWLYVGYWQ - YWSWWPUYQWWHWWKEYURVVSXYIWWLYVGXYJYWSWWPUYSVUDVUSYDXRWRXOACWWKYUEEVJYUFXY - IWWLXYJAEWWEYEXXIAUACYUDWWKWWHYUCVVSXYIWWKWWPAXYIWWKTZWWGAYWRYYEWWEWWKEXY - IWWLXYJUXMVKZWMYRWOACYUDUAVJYUFXYIVVRCYUFUNTZYUDXYIXLAYYGYUCVVSXYIYYGVVRJ - VVRCJVUTVVAUWEXGXXIUXSZAYUEVJWWKXYIAUACYUDVJXXIVVDYYFYUEUYAAUACYUDUXOXQAY - UFYUEXYIUYBRYUFYITAJVVEXQYYHVVFVVBVVCAYUHEUAYUFYUDVBZVCRZVXPAYUGYYIEVCAUA - CYUFYUDAJCQVVGXSXOAEXCTYXLVXPWWKTYYJVXPXLXXGQACWWKJGWWMQWNYUDWWKVXPUAEJCW - WLVVRJXLYUDVVSVXPYUDVVSXLJVVRYUCVVSXYIUWSVVHVVRJGXFWRVVIXPWRVVJYD $. + TAUACVWAXXHUXNXQAWUNWSWGXYHUYAAUACVWAUXOXQABDEGHXYILMXYIVIZPUXPACVWAUAVJG + XYIUYBRZXYGAVVRCXYKUNTZWHZVWAXYIVVTSZXYGXYMVVSXYIVVTACWWKVJGBXYKVVRXYIWWM + AXYKUXKPAEWSWGUXQXHAXYNXYGXLXYLAXYNXXCXYGAVVTEVVKXYIVJVVPXXCVYPWVIXYJXXDW + UJWWEUXRAVVPWUNWSWVLXHWRWMWRXXIUXSUXTAXWMUKURZVXITXYGXYOVWRRXYDXLXWNVWRWU + NXYGVXIVVQXYOXYDWUCWVAXWIXYGVIXYFUYCUYDXWJXWTAVVQWSWGXNZAVXLVVQVVPVNRTZXY + DVXLSXXCXLAVXLVVQVVPVMRTXYQAVXIXXPVVQVVPUJVVMVXLIVJUDVYQWUCXXQVXLVIZWUIAV + VPWUKUXDZXXSUXIVVQVVPVXLWFVKZVVQVVPVXLXXCXYDXYFXXDUYLVKUYEZXTAUCXXAVXGXXB + VXEVXHVJXXLVVLVXFXXAYMACVXEVXMVVPVJXXCWWBXXDXXEXXIXYCYUAYAAVVLXXAWGXIAVVL + XXAVXCAXXAVXBVXLSVXCACVXIVXAVVQVVPVXLVJXYDWUCXYFAVVQXYEYEZAVVPXYSUXEXXIXY + TXYBXYPXTAUDVXBVXKVXCVXIVXLVJXYRVVMVXJVXBYMACVXIVXAVVQVJXYDWUCXYFYUBXXIXY + BXYPYAAVVMVXBWGXIWRYGUYFAVXOEUACJVVRXLZVVSXYIVGZVBZVCREYUEJUYGZUOZVCRZVXP + AVXNYUEEVCAVXNUACVVLVVMVWTSZSZVBYUEAUAUCCVXEYUIVXGYUJVXMVXHWWHXXPVXEVVMVW + TWWHVXIXXPVVQVVPUJIVXEVWTVYQWWBWUCXXQXYAWPAXXRWWGXXSWMZWNAUAUDCVXIVWTVXKY + UIVXAVXLXYAAVXAYNAVXLYNVVMVXJVWTYMUYHAVXHYNVVLVXFYUIYMUYHAUACYUJYUDWWHYUJ + VVLVVSVWJVVMVWQSZVVPVHSZRZVVPVDSZRZSVVSVVLYUNSZEVHSZRZYUDWWHVVLYUIYUPWWHY + UIVWAVVMVWSSZYUMRVWAYUNYUMRZYUPWWHVXIXXPVVQVVPVWRYUMUJVWSIVXEVWAVVMVYQXWI + WWBWUCYUMVIZXXQXWJXWTYUKYOWWHYUTYUNVWAYUMWWHVXIXXPVVQVVPVWRYUMUJVWQIVXEVW + JVVMVYQXWIWWBWUCYVBXXQXWSXWHYUKYOXOWWHWVEVVSWVCVESZTYUNVXETYVAYUPXLAWVEWW + GWVHWMWWHVVSWWKYVCWWPAWWKYVCXLWWGAEWVCVEWVKXHWMWCWWHVXEVVPYUMVWJYULWWBYVB + AVVPYLTWWGWVPWMZXWSWWHXXPVXEVVMVWQWWHVXIXXPVVQVVPUJIVXEVWQVYQWWBWUCXXQXWH + WPYUKWNUYIZVVTVVSYUOYUMWVCYVCVXEVVPYUNWVIWVJYVCVIWWBYVBYUOVIZYBXPYDYGWWHV + XEXXJVVPEYUOYURUIYUNVVKWWKVVSVVLVYPYVFWWLWWBYURVIZXXKWWPYVEAVVLXXJTZWWGXX + MWMZYOWWHVVSVVLULXXJULURZVVRVVKUOZXLZEYPSZXYIVGZVBZVVMVVRIUOZXLZVVPYPSZXX + CVGZYUMRZSZYURRZYUCVVSYVMYURRZVVSXYIYURRZVGZYUSYUDWWHYWBVVSYVQVVLYVKXLZYV + MXYIVGZXYIVGZYURRZYWEWWHYWAYWHVVSYURWWHYWAYVQVVLYVOYVRYUMRZSZVVLYVOXXCYUM + RZSZVGZYWHYWAVVLYVQYWJYWLVGZSYWNVVLYVTYWOYVQYVOYVRXXCYUMUYJUYKYVQVVLYWJYW + LUYMUYNWWHYVQYWKYWGYWMXYIWWHULVVLYVNYWGXXJYWJVJYVJVVLXLYVLYWFYVMXYIYVJVVL + YVKUYOYQWWHVXEVVPYUMYVRYVOWWBYVBYVRVIZYVDWWHULVXEXXJVVPEYVMUIVVKVJYVKXYIV + YPWWBXYJYVMVIZXXKXVLAEYLTZWWGWWEWMZWWHCUIFXXJVVRHVVKVJKXXKWXNXURWWNYKZUYP + ZUYQYVIWWHYWFYVMXYIVJWWHEYPWGWWHEWSWGYRUYRWWHYWMVVLXXJXYIUYGVUCZSZXYIWWHV + VLYWLYXBWWHYWLXXCYXBWWHVXEVVPYUMYVOXXCWWBYVBXXDYVDYXAUYSAXXCYXBXLWWGAXXJV + VPEUIVVKXYIVJXXCVYPXXKXYJXXDWUJXXFUYTWMWRYGWWHYVHYXCXYIXLYVIXXJXYIVVLEWSV + UAVUBVKWRVUDVUEXOWWHYWIVVSYVQYWFWHZYVMXYIVGZYURRZYWEYXEYWHVVSYURYVQYWFYVM + XYIVUFVUGWWHVVSYUCYVMXYIVGZYURRYXFYWEWWHYXGYXEVVSYURWWHYUCYXDYVMXYIWWHJIV + VKUVQZYTZVVRYXHYTZYUCYXDVUHWWHYXIJHYTZAYXKWWGAHXEJAJCTZHXEJWLQCFJHKUVBVKV + UIWMWWHYXHHJAYXHHXLZWWGAWYRYXMOIHVUJUWBWMZVUKVULWWHYXJVVRHYTWWHHXEVVRWXSV + UIWWHYXHHVVRYXNVUKVULIVVKJVVRVUMVRYQXOYUCVVSYVMXYIYURUYJVUNVUOWRWWHYWAYUQ + VVSYURWWHVVLYVTYUNWWHYVOVWJYVSYULYUMWWHYVOVWBUBVVKVWCYVKSZVWFVWGRZVBZVCRV + WJWWHULXXJVVPEYVMUIUBVWGVWBVVKVWEVJYVKXYIVYPXXKXYJYWQXVLXVAXVCWWDAWVGWWGN + WMYWTVUPWWHYXQVWIVWBVCWWHUBVVKYXPVWHXUAYXOVWDVWFVWGXUAVWCVVKVVRWWHWYIWQVU + QYCXRXOWRWWHVVMUMXXPUMURZYVPXLZYVRXXCVGZVBZSYVSYULWWHUMVVMYXTYVSXXPYYAVJY + YAVIYXRVVMXLYXSYVQYVRXXCYXRVVMYVPUYOYQYUKWWHYVQYVRXXCVJWWHVVPYPWGWWHVVPWS + WGYRXIWWHVVMYYAVWQWWHYYAVWKUBIVWCYVPSZVWMVWNRZVBZVCRVWQWWHUMXXPVVQVVPYVRU + JUBVWNVWKIVWLVJYVPXXCVYQXXQXXDYWPXWEWUDWUEWVOAWUSWWGWUKWMWWHCUJFXXPVVRHIV + JKXXQWXNXVTWWNYKVUPWWHYYDVWPVWKVCWWHUBIYYCVWOXWAYYBVWDVWMVWNXWAVWCIVVRWWH + WYAWQVUQYCXRXOWRYGVURWBYGXOWWHYUCYWCVVSYWDXYIWWHWWKEYURYVMVVSWWLYVGYWQYWS + WWPUYQWWHWWKEYURVVSXYIWWLYVGXYJYWSWWPUYSVUDVUSYDXRWRXOACWWKYUEEVJYUFXYIWW + LXYJAEWWEYEXXIAUACYUDWWKWWHYUCVVSXYIWWKWWPAXYIWWKTZWWGAYWRYYEWWEWWKEXYIWW + LXYJUXMVKZWMYRWOACYUDUAVJYUFXYIVVRCYUFUNTZYUDXYIXLAYYGYUCVVSXYIYYGVVRJVVR + CJVUTVVAUWEXGXXIUXSZAYUEVJWWKXYIAUACYUDVJXXIVVDYYFYUEUYAAUACYUDUXOXQAYUFY + UEXYIUYBRYUFYITAJVVEXQYYHVVFVVBVVCAYUHEUAYUFYUDVBZVCRZVXPAYUGYYIEVCAUACYU + FYUDAJCQVVGXSXOAEXCTYXLVXPWWKTYYJVXPXLXXGQACWWKJGWWMQWNYUDWWKVXPUAEJCWWLV + VRJXLYUDVVSVXPYUDVVSXLJVVRYUCVVSXYIUWSVVHVVRJGXFWRVVIXPWRVVJYD $. $} ${ @@ -701038,81 +701047,81 @@ trivial one ( ~ abvtrivg ). (Contributed by SN, 3-Jul-2025.) $) VWFXXLXVMWYJXVPWYKXTWQXXHVWGVVSWEXXKWURVWFXNWEYAYBWWMKEVWOWUTWVDOXWCAWYMW UQWWLWXPVRXWIXWGWHWURUKUQWUTWVDVXQKVWOKVQXXCXXCWURVWBUKVXQWUTVMZXWPVQVQXX CXXNVQVAWURUKVXQWUTXWTUXDWLWUREXNWEZXXNYIWURUKVXQWUTYNWLAVWBXWPXPYDWUQAWX - BFGVWBJWDXWPRWXCXWQWXEWWSUWRWBWURVXQWUTUKVQVWBXWPYJVTZXXCWURVXRVXQXXPVCVA - ZWAZWUTVVSXWPVJZXXCXXRVVSWUSXWPWURVXQWVIVQVWBVQXXPVXRXWPWXGWURXXPYKXXAWUR - GXNWEYLYEWURXXSXXCXAXXQWURXXSVVSVVRXXCUWSUWTZVJZXXCWURVVSXWPXXTAXWPXXTXAW - UQAVVRGEUFVVPXXCVQXWPQXWDXXDXWQWWRXWRUXAWBYEWUQXYAXXCXAAVVRXXCVVSEXNUXEUX - BWQXMWBXMXXAYOYMWURXXMWAKEVWOXXLXXCOXWCXXDAWYMWUQXXMWXPVRWURXXMWFUXCXWIXW - GXXOYAUXFUXGWURVYQWVGEVNWURUKVXQVYPWVFWUQWWLVYPWVFXAAUMUNVVSVXRVVRVXQVYNW - VFVYOVXSVVSXAZVXTVXRXAZWAZVYIWVEVYMVWNVWOXYDVYBWUTVYHWVDVWOXYDVXSVVSVYAWU - SXYCVYAWUSXAXYBVXTVXRVWBYPWQXYBXYCUXHUXIXYDVYGWVCVWFVNXYDUOJVYFWVBXYDVYDW - VAVYEVWKXYCVYDWVAXAXYBVYCVXTVXRWJWQXDYQXFYRXYDVYLVWMVWFVNXYDUGVVPVYKVWLXY - DVYJVWHVWJVWKXYBVYJVWHXAXYCVWGVXSVVSWJWBXDYQXFYRVYOVPZWVEVWNVWOYGUXJUXNXG - XFUVPXGXFAWUPEWUOUMUNVVRVXQVXSVXTUXKZUUCZVIZVNVTEVYOVNVTVYTAVXAKVVRVXQUWT - ZWUOEXYGVQXXCOXXDAEWXPUWHZVXAVQVAAVWSUIVWTVBIVDYGYHZWLAUHVXAWUNKAVXBVXAVA - ZWAZKEVWOWUIWUMOXWCAWYMXYLWXPWBZXYMKEVWOWUDWUHOXWCXYNXYMVVRKWUAWUCXYMWVIV - VRGEUFVVPKWUCQOWWNXWDXYMVXQWVIWUBVWBAWXAXYLWXFWBXYMVXAULUIVXQVXBIJMVXAVPZ - WXDAIMVAZXYLTWBZAJIUXOZXYLUBWBZAXYLWFZUXLUXMVSXYMVXAUFUIVVRVXBIVVPMXYOXWD - XYQXYMIJUUEZXYTUXLUXMZXYMJKWUGVWFVQXVMWYJXVPAXXEXYLXXFWBZAWXKXYLWXLWBZXYM - UOJWUFKXYMWYGWAZKVWKVWFWUEVYEWYJWYKAWYLXYLWYGWYNVRXYMJVBVYCWUBXYMIVBJVXBX - YLIVBVXBWKAVXAUIVXBIXYOWPWQZXYSWRZWCAWYGXUFXYLAJKVYCVVTWYTWCUXPZWSXLXYMWU - BWUGYCVQVQXVMAWUGVQVAXYLAUOJWUFVQWXLUXQWBXYMVWFXNWEZWUGYIXYMUOJWUFYNWLXYM - VXBYSJYCXYLVXBYCXPYDAVXAUIVXBIXYOXRWQZXYMUYNZUXRXYMJWUFUOVQWUBYCYJVTZXVMX - YMVYCJYULVCVAZWAZWUFYCVYEVWKVTZXVMYUNWUEYCVYEVWKXYMJVBYSWUBVQYULVYCYCYUGX - YMYULYKYUDYUKYLXDYUMXYMWYGYUOXVMXAZVYCJYULUXSYUEXUFYUPYUHKVWKVWFVYEXVMWYJ - XVPWYKXTWNUXTXMYUDYOYMYBZWHXYMVVPKWULVWFVQXVMWYJXVPYUCAXUKXYLWWRWBZXYMUGV - VPWUKKXYMXXGWAZKVWKVWFWUJVWJWYJWYKAWYLXYLXXGWYNVRXYMVVPVBVWGWUAXYMIVBVVPV - XBYUFYUAWRZWCAXXGVWJKVAZXYLAVVPKVWGVWIXXJWCUXPZWSXLXYMWUAWULYCVQVQXVMXYMU - GVVPWUKVQYURUXQYUIWULYIXYMUGVVPWUKYNWLXYMVXBYSVVPYCYUJYUKUXRXYMVVPWUKUGVQ - WUAYCYJVTZXVMXYMVWGVVPYVCVCVAZWAZWUKYCVWJVWKVTZXVMYVEWUJYCVWJVWKXYMVVPVBY - SWUAVQYVCVWGYCYUTXYMYVCYKYURYUKYLXDYVEYVAYVFXVMXAYVDXYMXXGYVAVWGVVPYVCUXS - YVBUXTKVWKVWFVWJXVMWYJXVPWYKXTWNXMYURYOYMYBZWHXLAUHUQWUIWUMVXAKVWOVQVQXXC - XXCAUHUQWUDWUHVXAKVWOVQVQXXCXXCAUHVXAWUDVMUHVXAVXCVMZXXCXPAUHVXAWUDVXCXYM - CVXADEUIHIJVXBXYONPAXULXYLUAWBXYSAHCVAXYLUCWBXYTUYAZXGAHYVHXXCXPAUHVXAXVG - HACVXADEUIIXVGHNXVGVPPXYOUCVSXQACDEHIWDXXCNPXXDUCUAUWRXSUYBAXXMWAKEVWOXXL - XXCOXWCXXDAWYMXXMWXPWBAXXMWFUXCZXYMWUAWUCWEYUQAEXNWEZYAYVJXYMWUDWUHVWOUYC - YVGYVKYAZAVVRVXAUNUFULUIVXQXYGIJMUMXYOWXDXWDXYGVPTUBUYDZUYEAXYHVYOEVNAUMU - NUHVVRVXQVXAXYFWUNVYNXYGWUOAVXSVVRVAZVXTVXQVAZWAZWAZXYFVXAVAZIVBXYFWKZXYF - URVFUSUTVAZYVQVVPJUXKZVBXYFWKYVSYVQVVPJVBVXSVXTYVNVVPVBVXSWKAYVOVVRUFVXSV - VPXWDWPZUYFYVOJVBVXTWKAYVNVXQULVXTJWXDWPUYGZVVPJUYOUYHXAZYVQJIUYIWLZUYJYV - QYWAIVBXYFAYWAIXAZYVPAXYRYWFUBJIUYKUYLWBUYMUYPZYVQXYFYCXPYDZYVTYVQXYFVQYS - YCXYFVQVAZYVQVXSVXTUMUYQUNUYQUYRZWLZYVQUYNYVQIVBXYFYWGVUEYVQVXSVXTYCYVNVX - SYCXPYDAYVOVVRUFVXSVVPXWDXRUYFYVOVXTYCXPYDAYVNVXQULVXTJWXDXRUYGUYSUYTYVQY - WIYVSYWHYVTVUAYWKYWGXYFIVQVUBUVDUYPYVQXYPYVRYVSYVTWAVUAAXYPYVPTWBVXAUIXYF - IMXYOVUCWNVUDAXYGWIAWUOWIYVQUHXYFWUNVUFXYFVVPVHZXYFJVHZVWBVJZVJZVWFUOJVYC - YWMVJZVYEVWKVTZVMZVNVTZVWOVTZVWFUGVVPVWGYWLVJZVWJVWKVTZVMZVNVTZVWOVTZVYNU - HXYFWUNYXEYWJVXBXYFXAZWUIYWTWUMYXDVWOYXFWUDYWOWUHYWSVWOYXFWUAYWLWUCYWNYXF - WUBYWMVWBVXBXYFJVUGZXJVXBXYFVVPVUGZUXIYXFWUGYWRVWFVNYXFUOJWUFYWQYXFWUEYWP - VYEVWKYXFVYCWUBYWMYXGYEXDYQXFYRYXFWULYXCVWFVNYXFUGVVPWUKYXBYXFWUJYXAVWJVW - KYXFVWGWUAYWLYXHYEXDYQXFYRVUHYVQYWTVYIYXDVYMVWOYVQYWOVYBYWSVYHVWOYVQYWLVX - SYWNVYAYVQYWMVXTVWBYVQVXSVVPVUIZVXTJVUIZYWDYWMVXTXAYVNYXIAYVOYVNVVPVBVXSY - WBVUPUYFZYVQJVBVXTYWCVUPZYWEVVPJVXSVXTVUJXEZXJYVQYXIYXJYWDYWLVXSXAYXKYXLY - WEVVPJVXSVXTVUKXEZUXIYVQYWRVYGVWFVNYVQUOJYWQVYFYVQYWPVYDVYEVWKYVQVYCYWMVX - TYXMYEXDYQXFYRYVQYXCVYLVWFVNYVQUGVVPYXBVYKYVQYXAVYJVWJVWKYVQVWGYWLVXSYXNY - EXDYQXFYRXKVULZXFAVVRKVXQUEUKVYOEVQVQXXCOXXDXYJVVRVQVAAVVOUFVVQVBVVPVDYGY - HWLXWSAXWTWLAVYNKVAZUNVXQVUQUMVVRVUQXYIKVYOWKAYXPUMUNVVRVXQYVQKEVWOVYIVYM - OXWCAWYMYVPWXPWBZYVQKEVWOVYBVYHOXWCYXQAYVNYVOVYBKVAZAYVOYVNYXRAYVOWAZVVRK - VXSVYAYXSWVIVVRGEUFVVPKVYAQOWWNXWDAVXQWVIVXTVWBWXFWCVSWCUWEVUMYVQUOVVTVXT - VXQEULVWKJKVWFVQWXDOWYIWYKAWXKYVPWXLWBAXULYVPUAWBZAVVTKJVDVTVAYVPWXRWBAYV - NYVOVUNWGWHYVQUGVWIVXSVVREUFVWKVVPKVWFVQXWDOWYIWYKAXUKYVPWWRWBYXTAVWIKVVP - VDVTVAYVPABKIVVPUDWWQUUMZWBAYVNYVOVUOWGWHVURUMUNVVRVXQVYNKVYOXYEVUSUYLAXY - HVYOXXCXPYXOAWUOXYGVQVQXYIVXAXXCYVLAXYIVXAXYGVUTXYIVXAXYGVVAYVMXYIVXAXYGV - VBWNYVKWUOVQVAAUHVXAWUNXYKUXDWLVVCXSVVDVVGAWUOVXKEVNAUHVXAWUNVXJXYMWUNWUD - WUHWUMVWOVTZVWOVTVXJXYMKEVWOWUDWUHWUMOXWCXYNYUBYUQYVGVVEXYMWUDVXCYYBVXIVW - OYVIXYMVXIVWFVXHJVHZVNVTZVWFVXHVVPVHZVNVTZVWOVTYYBXYMIKJVVPVWOVXHVWFMXVMW - YJXVPEVWOVWFWYIXWCVVFYUCXYQXYMUJIVXGKXYMVXDIVAZWAKVWKVWFVXEVXFWYJWYKAWYLX - YLYYGWYNVRXYMIVBVXDVXBYUFWCZXYMIKVXDBAWYRXYLWYSWBWCZWSXLXYMUJUGVXEVXFIKVW - KVBVQYCXVMXYMVXBUJIVXEVMYCXPXYMUJIVBVXBYUFXQYUJXSXVNXVOXYMXVQWQYYHYYIYUIY - AJVVPUYOUYHXAXYMJIVVHWLAIJVVPUXKZXAXYLAYYJIAXYRYYJIXAUBJIVVIUYLXCWBVVJXYM - YYDWUHYYFWUMVWOXYMYYCWUGVWFVNXYMYYCUJJVXGVMZWUGXYMUJIJVXGXYSVVKXYMYYKUOJV - YCVXBVJZVYCBVJZVWKVTZVMWUGUJUOJVXGYYNVXDVYCXAVXEYYLVXFYYMVWKVXDVYCVXBYPVX - DVYCBYPYRVVLXYMUOJYYNWUFYUEWUFYYNYUEWUEYYLVYEYYMVWKYUEVYCJVXBXYMWYGWFZYTY - UEVYCJBYYOYTYRXCXGXKXMXFXYMYYEWULVWFVNXYMYYEUJVVPVXGVMZWULXYMUJIVVPVXGYUA - VVKXYMYYPUGVVPVWGVXBVJZVWGBVJZVWKVTZVMWULUJUGVVPVXGYYSVXDVWGXAVXEYYQVXFYY - RVWKVXDVWGVXBYPVXDVWGBYPYRVVLXYMUGVVPYYSWUKYUSWUKYYSYUSWUJYYQVWJYYRVWKYUS - VWGVVPVXBXYMXXGWFZYTYUSVWGVVPBYYTYTYRXCXGXKXMXFYRVVMYRXMXGXFVVNAVWIWVIVVR - GVXMEVWOUFUGVWKVWDVVPKVWFVQUEVXMVPQWWNXWDOWYIWYKXWCWWRUAXWOYYAYFABCVXADVX - NEVWOUIUJVWKHIKVWFMUHVXNVPNPXYOOWYIWYKXWCTUAUCUDYFUXG $. + BFGVWBJXWPRWXCXWQWXEUWRWBWURVXQWUTUKVQVWBXWPYJVTZXXCWURVXRVXQXXPVCVAZWAZW + UTVVSXWPVJZXXCXXRVVSWUSXWPWURVXQWVIVQVWBVQXXPVXRXWPWXGWURXXPYKXXAWURGXNWE + YLYEWURXXSXXCXAXXQWURXXSVVSVVRXXCUWSUWTZVJZXXCWURVVSXWPXXTAXWPXXTXAWUQAVV + RGEUFVVPXXCVQXWPQXWDXXDXWQWWRXWRUXAWBYEWUQXYAXXCXAAVVRXXCVVSEXNUXEUXBWQXM + WBXMXXAYOYMWURXXMWAKEVWOXXLXXCOXWCXXDAWYMWUQXXMWXPVRWURXXMWFUXCXWIXWGXXOY + AUXFUXGWURVYQWVGEVNWURUKVXQVYPWVFWUQWWLVYPWVFXAAUMUNVVSVXRVVRVXQVYNWVFVYO + VXSVVSXAZVXTVXRXAZWAZVYIWVEVYMVWNVWOXYDVYBWUTVYHWVDVWOXYDVXSVVSVYAWUSXYCV + YAWUSXAXYBVXTVXRVWBYPWQXYBXYCUXHUXIXYDVYGWVCVWFVNXYDUOJVYFWVBXYDVYDWVAVYE + VWKXYCVYDWVAXAXYBVYCVXTVXRWJWQXDYQXFYRXYDVYLVWMVWFVNXYDUGVVPVYKVWLXYDVYJV + WHVWJVWKXYBVYJVWHXAXYCVWGVXSVVSWJWBXDYQXFYRVYOVPZWVEVWNVWOYGUXJUXNXGXFUVP + XGXFAWUPEWUOUMUNVVRVXQVXSVXTUXKZUUCZVIZVNVTEVYOVNVTVYTAVXAKVVRVXQUWTZWUOE + XYGVQXXCOXXDAEWXPUWHZVXAVQVAAVWSUIVWTVBIVDYGYHZWLAUHVXAWUNKAVXBVXAVAZWAZK + EVWOWUIWUMOXWCAWYMXYLWXPWBZXYMKEVWOWUDWUHOXWCXYNXYMVVRKWUAWUCXYMWVIVVRGEU + FVVPKWUCQOWWNXWDXYMVXQWVIWUBVWBAWXAXYLWXFWBXYMVXAULUIVXQVXBIJMVXAVPZWXDAI + MVAZXYLTWBZAJIUXOZXYLUBWBZAXYLWFZUXLUXMVSXYMVXAUFUIVVRVXBIVVPMXYOXWDXYQXY + MIJUUEZXYTUXLUXMZXYMJKWUGVWFVQXVMWYJXVPAXXEXYLXXFWBZAWXKXYLWXLWBZXYMUOJWU + FKXYMWYGWAZKVWKVWFWUEVYEWYJWYKAWYLXYLWYGWYNVRXYMJVBVYCWUBXYMIVBJVXBXYLIVB + VXBWKAVXAUIVXBIXYOWPWQZXYSWRZWCAWYGXUFXYLAJKVYCVVTWYTWCUXPZWSXLXYMWUBWUGY + CVQVQXVMAWUGVQVAXYLAUOJWUFVQWXLUXQWBXYMVWFXNWEZWUGYIXYMUOJWUFYNWLXYMVXBYS + JYCXYLVXBYCXPYDAVXAUIVXBIXYOXRWQZXYMUYNZUXRXYMJWUFUOVQWUBYCYJVTZXVMXYMVYC + JYULVCVAZWAZWUFYCVYEVWKVTZXVMYUNWUEYCVYEVWKXYMJVBYSWUBVQYULVYCYCYUGXYMYUL + YKYUDYUKYLXDYUMXYMWYGYUOXVMXAZVYCJYULUXSYUEXUFYUPYUHKVWKVWFVYEXVMWYJXVPWY + KXTWNUXTXMYUDYOYMYBZWHXYMVVPKWULVWFVQXVMWYJXVPYUCAXUKXYLWWRWBZXYMUGVVPWUK + KXYMXXGWAZKVWKVWFWUJVWJWYJWYKAWYLXYLXXGWYNVRXYMVVPVBVWGWUAXYMIVBVVPVXBYUF + YUAWRZWCAXXGVWJKVAZXYLAVVPKVWGVWIXXJWCUXPZWSXLXYMWUAWULYCVQVQXVMXYMUGVVPW + UKVQYURUXQYUIWULYIXYMUGVVPWUKYNWLXYMVXBYSVVPYCYUJYUKUXRXYMVVPWUKUGVQWUAYC + YJVTZXVMXYMVWGVVPYVCVCVAZWAZWUKYCVWJVWKVTZXVMYVEWUJYCVWJVWKXYMVVPVBYSWUAV + QYVCVWGYCYUTXYMYVCYKYURYUKYLXDYVEYVAYVFXVMXAYVDXYMXXGYVAVWGVVPYVCUXSYVBUX + TKVWKVWFVWJXVMWYJXVPWYKXTWNXMYURYOYMYBZWHXLAUHUQWUIWUMVXAKVWOVQVQXXCXXCAU + HUQWUDWUHVXAKVWOVQVQXXCXXCAUHVXAWUDVMUHVXAVXCVMZXXCXPAUHVXAWUDVXCXYMCVXAD + EUIHIJVXBXYONPAXULXYLUAWBXYSAHCVAXYLUCWBXYTUYAZXGAHYVHXXCXPAUHVXAXVGHACVX + ADEUIIXVGHNXVGVPPXYOUCVSXQACDEHIXXCNPXXDUCUWRXSUYBAXXMWAKEVWOXXLXXCOXWCXX + DAWYMXXMWXPWBAXXMWFUXCZXYMWUAWUCWEYUQAEXNWEZYAYVJXYMWUDWUHVWOUYCYVGYVKYAZ + AVVRVXAUNUFULUIVXQXYGIJMUMXYOWXDXWDXYGVPTUBUYDZUYEAXYHVYOEVNAUMUNUHVVRVXQ + VXAXYFWUNVYNXYGWUOAVXSVVRVAZVXTVXQVAZWAZWAZXYFVXAVAZIVBXYFWKZXYFURVFUSUTV + AZYVQVVPJUXKZVBXYFWKYVSYVQVVPJVBVXSVXTYVNVVPVBVXSWKAYVOVVRUFVXSVVPXWDWPZU + YFYVOJVBVXTWKAYVNVXQULVXTJWXDWPUYGZVVPJUYOUYHXAZYVQJIUYIWLZUYJYVQYWAIVBXY + FAYWAIXAZYVPAXYRYWFUBJIUYKUYLWBUYMUYPZYVQXYFYCXPYDZYVTYVQXYFVQYSYCXYFVQVA + ZYVQVXSVXTUMUYQUNUYQUYRZWLZYVQUYNYVQIVBXYFYWGVUEYVQVXSVXTYCYVNVXSYCXPYDAY + VOVVRUFVXSVVPXWDXRUYFYVOVXTYCXPYDAYVNVXQULVXTJWXDXRUYGUYSUYTYVQYWIYVSYWHY + VTVUAYWKYWGXYFIVQVUBUVDUYPYVQXYPYVRYVSYVTWAVUAAXYPYVPTWBVXAUIXYFIMXYOVUCW + NVUDAXYGWIAWUOWIYVQUHXYFWUNVUFXYFVVPVHZXYFJVHZVWBVJZVJZVWFUOJVYCYWMVJZVYE + VWKVTZVMZVNVTZVWOVTZVWFUGVVPVWGYWLVJZVWJVWKVTZVMZVNVTZVWOVTZVYNUHXYFWUNYX + EYWJVXBXYFXAZWUIYWTWUMYXDVWOYXFWUDYWOWUHYWSVWOYXFWUAYWLWUCYWNYXFWUBYWMVWB + VXBXYFJVUGZXJVXBXYFVVPVUGZUXIYXFWUGYWRVWFVNYXFUOJWUFYWQYXFWUEYWPVYEVWKYXF + VYCWUBYWMYXGYEXDYQXFYRYXFWULYXCVWFVNYXFUGVVPWUKYXBYXFWUJYXAVWJVWKYXFVWGWU + AYWLYXHYEXDYQXFYRVUHYVQYWTVYIYXDVYMVWOYVQYWOVYBYWSVYHVWOYVQYWLVXSYWNVYAYV + QYWMVXTVWBYVQVXSVVPVUIZVXTJVUIZYWDYWMVXTXAYVNYXIAYVOYVNVVPVBVXSYWBVUPUYFZ + YVQJVBVXTYWCVUPZYWEVVPJVXSVXTVUJXEZXJYVQYXIYXJYWDYWLVXSXAYXKYXLYWEVVPJVXS + VXTVUKXEZUXIYVQYWRVYGVWFVNYVQUOJYWQVYFYVQYWPVYDVYEVWKYVQVYCYWMVXTYXMYEXDY + QXFYRYVQYXCVYLVWFVNYVQUGVVPYXBVYKYVQYXAVYJVWJVWKYVQVWGYWLVXSYXNYEXDYQXFYR + XKVULZXFAVVRKVXQUEUKVYOEVQVQXXCOXXDXYJVVRVQVAAVVOUFVVQVBVVPVDYGYHWLXWSAXW + TWLAVYNKVAZUNVXQVUQUMVVRVUQXYIKVYOWKAYXPUMUNVVRVXQYVQKEVWOVYIVYMOXWCAWYMY + VPWXPWBZYVQKEVWOVYBVYHOXWCYXQAYVNYVOVYBKVAZAYVOYVNYXRAYVOWAZVVRKVXSVYAYXS + WVIVVRGEUFVVPKVYAQOWWNXWDAVXQWVIVXTVWBWXFWCVSWCUWEVUMYVQUOVVTVXTVXQEULVWK + JKVWFVQWXDOWYIWYKAWXKYVPWXLWBAXULYVPUAWBZAVVTKJVDVTVAYVPWXRWBAYVNYVOVUNWG + WHYVQUGVWIVXSVVREUFVWKVVPKVWFVQXWDOWYIWYKAXUKYVPWWRWBYXTAVWIKVVPVDVTVAYVP + ABKIVVPUDWWQUUMZWBAYVNYVOVUOWGWHVURUMUNVVRVXQVYNKVYOXYEVUSUYLAXYHVYOXXCXP + YXOAWUOXYGVQVQXYIVXAXXCYVLAXYIVXAXYGVUTXYIVXAXYGVVAYVMXYIVXAXYGVVBWNYVKWU + OVQVAAUHVXAWUNXYKUXDWLVVCXSVVDVVGAWUOVXKEVNAUHVXAWUNVXJXYMWUNWUDWUHWUMVWO + VTZVWOVTVXJXYMKEVWOWUDWUHWUMOXWCXYNYUBYUQYVGVVEXYMWUDVXCYYBVXIVWOYVIXYMVX + IVWFVXHJVHZVNVTZVWFVXHVVPVHZVNVTZVWOVTYYBXYMIKJVVPVWOVXHVWFMXVMWYJXVPEVWO + VWFWYIXWCVVFYUCXYQXYMUJIVXGKXYMVXDIVAZWAKVWKVWFVXEVXFWYJWYKAWYLXYLYYGWYNV + RXYMIVBVXDVXBYUFWCZXYMIKVXDBAWYRXYLWYSWBWCZWSXLXYMUJUGVXEVXFIKVWKVBVQYCXV + MXYMVXBUJIVXEVMYCXPXYMUJIVBVXBYUFXQYUJXSXVNXVOXYMXVQWQYYHYYIYUIYAJVVPUYOU + YHXAXYMJIVVHWLAIJVVPUXKZXAXYLAYYJIAXYRYYJIXAUBJIVVIUYLXCWBVVJXYMYYDWUHYYF + WUMVWOXYMYYCWUGVWFVNXYMYYCUJJVXGVMZWUGXYMUJIJVXGXYSVVKXYMYYKUOJVYCVXBVJZV + YCBVJZVWKVTZVMWUGUJUOJVXGYYNVXDVYCXAVXEYYLVXFYYMVWKVXDVYCVXBYPVXDVYCBYPYR + VVLXYMUOJYYNWUFYUEWUFYYNYUEWUEYYLVYEYYMVWKYUEVYCJVXBXYMWYGWFZYTYUEVYCJBYY + OYTYRXCXGXKXMXFXYMYYEWULVWFVNXYMYYEUJVVPVXGVMZWULXYMUJIVVPVXGYUAVVKXYMYYP + UGVVPVWGVXBVJZVWGBVJZVWKVTZVMWULUJUGVVPVXGYYSVXDVWGXAVXEYYQVXFYYRVWKVXDVW + GVXBYPVXDVWGBYPYRVVLXYMUGVVPYYSWUKYUSWUKYYSYUSWUJYYQVWJYYRVWKYUSVWGVVPVXB + XYMXXGWFZYTYUSVWGVVPBYYTYTYRXCXGXKXMXFYRVVMYRXMXGXFVVNAVWIWVIVVRGVXMEVWOU + FUGVWKVWDVVPKVWFVQUEVXMVPQWWNXWDOWYIWYKXWCWWRUAXWOYYAYFABCVXADVXNEVWOUIUJ + VWKHIKVWFMUHVXNVPNPXYOOWYIWYKXWCTUAUCUDYFUXG $. $} ${ @@ -701424,28 +701433,28 @@ proof usage (see ~ mplelbas and ~ mpladd ). Note that hypothesis 0 is mhpind $p |- ( ph -> X e. G ) $= ( cfv cplusg ccnfld cn0 cress co cv cgsu wceq crab cin cvv eqid ccnv cima cn cfn wcel cmap ovexd rabexd wss ssrab2 a1i csn cxp cmhp reldmmhp mhprcl - elfvov1 mhp0cl weq cif cmpt eleq2i biimpri wa cbs cgrp adantr cmps cfsupp - elind wbr wf simplrr grpidcl ad2antrr ifcld fmpttd wb fvexi elmapd mpbird + elfvov1 mhp0cl elind weq cif cmpt eleq2i biimpri wa cbs adantr cfsupp wbr + cmps wf simplrr cgrp grpidcl ad2antrr ifcld fmpttd wb fvexi elmapd mpbird syl psrbas eleqtrrd c0g sniffsupp mplelbas sylanbrc csupp cdif wne necomd elneeldif adantll adantlrr neneqd iffalsed suppss2 ismhp2 sylanr1 elinel1 sseqtrdi cof ad2antrl mhpmpl ad2antll mpladd mhpaddcl eqeltrrd fsuppssind mplelf mplelsfi mhpdeg elin2d ) AOMUMZLPABCDHUNUMZUOUPUQURJUSUTUROVAZJEVB ZHYTLVCZEVDPQRSTUBUCUUAVEZUHAKUSVFVHVGVIVJKUPNVKUREVDUFAUPNVKVLVMZUUCEVNA - UUBJEVOVPAYTLEQVQVRAEHKMNOVDQUAUCUFAHMNVSPOVTUAUIWBZUHAHMNOPUAUIWAZWCUJWO - SUSZUUCVJZAUUIIVJZTUSZDVJZRERSWDZUULQWEZWFZUUDVJUUKUUJIUUCUUIUGWGWHAUUKUU - MWIZWIZYTLUUPUURFWJUMZEFHJKMNOVDWKUUPQUAUDUUSVEZUCUFANVDVJUUQUUGWLAHWKVJZ - UUQUHWLAOUPVJUUQUUHWLUURUUPNHWMURZWJUMZVJUUPQWNWPZUUPUUSVJUURUUPDEVKURZUV - CUURUUPUVEVJZEDUUPWQZUURREUUODUURRUSZEVJZWIUUNUULQDAUUKUUMUVIWRAQDVJZUUQU - VIAUVAUVJUHDHQUBUCWSXGWTXAXBAUVFUVGXCUUQADEUUPVDVDDVDVJADHWJUBXDVPUUFXEWL - XFAUVCUVEVAUUQAUVCEHUVBKNDVDUVBVEZUBUFUVCVEZUUGXHWLXIAUVDUUQARUULUUPEVDVD - UUIQUUFQVDVJAQHXJUCXDVPUUPVEXKWLUVCFHUVBUUSNUUPQUDUVKUVLUCUUTXLXMUURUUPQX - NURIUUCUUREUUORVDIQUURUVHEIXOVJZWIZUUNUULQUVNUVHUUIAUUKUVMUVHUUIXPZUUMUUK - UVMUVOAUUKUVMWIUUIUVHIEUUIUVHXRXQXSXTYAYBAEVDVJUUQUUFWLYCUGYGYDUKWOYEABUS - ZUUDVJZCUSZUUDVJZWIZWIZUVPUVRGURZUVPUVRUUAYHURUUDUWAUUSFUUAGHNUVPUVRUDUUT - UUEUEUWAUUSFHMNOUVPUAUDUUTUVQUVPYTVJAUVSUVPYTLYFYIZYJUWAUUSFHMNOUVRUAUDUU - TUVSUVRYTVJAUVQUVRYTLYFYKZYJYLUWAYTLUWBUWAFGHMNOUVPUVRUAUDUEAUVAUVTUHWLUW - CUWDYMULWOYNAUUSEFHKNDPUDUBUUTUFAUUSFHMNOPUAUDUUTUIYJZYPAUUSFHPNWKQUDUUTU - CUWEUHYQAEHJKMNOPQUAUCUFUIYRYOYS $. + UUBJEVOVPAYTLEQVQVRAEHKMNOVDQUAUCUFAHMNVSPOVTUAUIWBZUHAHMNOPUAUIWAZWCUJWD + SUSZUUCVJZAUUIIVJZTUSZDVJZRERSWEZUULQWFZWGZUUDVJUUKUUJIUUCUUIUGWHWIAUUKUU + MWJZWJZYTLUUPUURFWKUMZEFHJKMNOUUPQUAUDUUSVEZUCUFAOUPVJUUQUUHWLUURUUPNHWOU + RZWKUMZVJUUPQWMWNZUUPUUSVJUURUUPDEVKURZUVBUURUUPUVDVJZEDUUPWPZUURREUUODUU + RRUSZEVJZWJUUNUULQDAUUKUUMUVHWQAQDVJZUUQUVHAHWRVJZUVIUHDHQUBUCWSXGWTXAXBA + UVEUVFXCUUQADEUUPVDVDDVDVJADHWKUBXDVPUUFXEWLXFAUVBUVDVAUUQAUVBEHUVAKNDVDU + VAVEZUBUFUVBVEZUUGXHWLXIAUVCUUQARUULUUPEVDVDUUIQUUFQVDVJAQHXJUCXDVPUUPVEX + KWLUVBFHUVAUUSNUUPQUDUVKUVLUCUUTXLXMUURUUPQXNURIUUCUUREUUORVDIQUURUVGEIXO + VJZWJZUUNUULQUVNUVGUUIAUUKUVMUVGUUIXPZUUMUUKUVMUVOAUUKUVMWJUUIUVGIEUUIUVG + XRXQXSXTYAYBAEVDVJUUQUUFWLYCUGYGYDUKWDYEABUSZUUDVJZCUSZUUDVJZWJZWJZUVPUVR + GURZUVPUVRUUAYHURUUDUWAUUSFUUAGHNUVPUVRUDUUTUUEUEUWAUUSFHMNOUVPUAUDUUTUVQ + UVPYTVJAUVSUVPYTLYFYIZYJUWAUUSFHMNOUVRUAUDUUTUVSUVRYTVJAUVQUVRYTLYFYKZYJY + LUWAYTLUWBUWAFGHMNOUVPUVRUAUDUEAUVJUVTUHWLUWCUWDYMULWDYNAUUSEFHKNDPUDUBUU + TUFAUUSFHMNOPUAUDUUTUIYJZYPAUUSFHPNQUDUUTUCUWEYQAEHJKMNOPQUAUCUFUIYRYOYS + $. $} ${