diff --git a/discouraged b/discouraged
index c52e7d88e6..1e516e0352 100644
--- a/discouraged
+++ b/discouraged
@@ -15060,8 +15060,10 @@ New usage of "cbvmo" is discouraged (1 uses).
 New usage of "cbvmowOLD" is discouraged (0 uses).
 New usage of "cbvmptfg" is discouraged (1 uses).
 New usage of "cbvmptg" is discouraged (1 uses).
+New usage of "cbvmptvOLD" is discouraged (0 uses).
 New usage of "cbvmptvg" is discouraged (0 uses).
 New usage of "cbvopab1g" is discouraged (1 uses).
+New usage of "cbvopab1vOLD" is discouraged (0 uses).
 New usage of "cbvopabvOLD" is discouraged (0 uses).
 New usage of "cbvrab" is discouraged (0 uses).
 New usage of "cbvrabcsf" is discouraged (1 uses).
@@ -15927,12 +15929,14 @@ New usage of "domepOLD" is discouraged (0 uses).
 New usage of "dral1" is discouraged (10 uses).
 New usage of "dral1-o" is discouraged (4 uses).
 New usage of "dral1ALT" is discouraged (0 uses).
+New usage of "dral1vOLD" is discouraged (0 uses).
 New usage of "dral2" is discouraged (5 uses).
 New usage of "dral2-o" is discouraged (4 uses).
 New usage of "drex1" is discouraged (10 uses).
 New usage of "drex2" is discouraged (4 uses).
 New usage of "drhmsubcALTV" is discouraged (1 uses).
 New usage of "drnf1" is discouraged (4 uses).
+New usage of "drnf1vOLD" is discouraged (0 uses).
 New usage of "drnf2" is discouraged (3 uses).
 New usage of "drnfc1" is discouraged (4 uses).
 New usage of "drnfc1OLD" is discouraged (0 uses).
@@ -16297,6 +16301,7 @@ New usage of "equsb2" is discouraged (1 uses).
 New usage of "equsex" is discouraged (2 uses).
 New usage of "equsexALT" is discouraged (0 uses).
 New usage of "equsexh" is discouraged (0 uses).
+New usage of "equsexvOLD" is discouraged (0 uses).
 New usage of "equvel" is discouraged (0 uses).
 New usage of "equvini" is discouraged (1 uses).
 New usage of "erngbase-rN" is discouraged (4 uses).
@@ -19633,6 +19638,8 @@ Proof modification of "cbveuwOLD" is discouraged (29 steps).
 Proof modification of "cbvexsv" is discouraged (29 steps).
 Proof modification of "cbviotavwOLD" is discouraged (12 steps).
 Proof modification of "cbvmowOLD" is discouraged (62 steps).
+Proof modification of "cbvmptvOLD" is discouraged (13 steps).
+Proof modification of "cbvopab1vOLD" is discouraged (13 steps).
 Proof modification of "cbvopabvOLD" is discouraged (20 steps).
 Proof modification of "cbvralfwOLD" is discouraged (139 steps).
 Proof modification of "cbvreuvwOLD" is discouraged (13 steps).
@@ -19751,7 +19758,9 @@ Proof modification of "dmmpogaOLD" is discouraged (31 steps).
 Proof modification of "dmtrclfvRP" is discouraged (46 steps).
 Proof modification of "domepOLD" is discouraged (51 steps).
 Proof modification of "dral1ALT" is discouraged (34 steps).
+Proof modification of "dral1vOLD" is discouraged (36 steps).
 Proof modification of "dral2-o" is discouraged (14 steps).
+Proof modification of "drnf1vOLD" is discouraged (50 steps).
 Proof modification of "drnfc1OLD" is discouraged (51 steps).
 Proof modification of "drnfc2" is discouraged (59 steps).
 Proof modification of "drnfc2OLD" is discouraged (52 steps).
@@ -19998,6 +20007,7 @@ Proof modification of "equncomiVD" is discouraged (19 steps).
 Proof modification of "equs5aALT" is discouraged (25 steps).
 Proof modification of "equs5eALT" is discouraged (39 steps).
 Proof modification of "equsexALT" is discouraged (37 steps).
+Proof modification of "equsexvOLD" is discouraged (25 steps).
 Proof modification of "estrreslem1OLD" is discouraged (96 steps).
 Proof modification of "eubiOLD" is discouraged (15 steps).
 Proof modification of "eujustALT" is discouraged (188 steps).
diff --git a/set.mm b/set.mm
index 8c0c1d27a2..4944d9b170 100644
--- a/set.mm
+++ b/set.mm
@@ -19488,8 +19488,18 @@ disjoint variable condition if we allow more axioms (see ~ equs4 ).
        with a disjoint variable condition, which does not require ~ ax-13 .
        See ~ equsexvw for a version with two disjoint variable conditions
        requiring fewer axioms.  See also the dual form ~ equsalv .
-       (Contributed by NM, 5-Aug-1993.)  (Revised by BJ, 31-May-2019.) $)
+       (Contributed by NM, 5-Aug-1993.)  (Revised by BJ, 31-May-2019.)  Avoid
+       ~ ax-10 .  (Revised by Gino Giotto, 18-Nov-2024.) $)
     equsexv $p |- ( E. x ( x = y /\ ph ) <-> ps ) $=
+      ( weq wa wex wn wal df-ex wi wb nfn notbid equsalv bicom1 con1bid ax-mp
+      pm4.63 con1bii albii xchnxbir bitri ) CDGZAHZCIUGJZCKZJBUGCLUFAJZMZCKZBUI
+      ULBJZNZULJBNUJUMCDBCEOUFABFPQUNBULULUMRSTUHUKCUKUGUFAUAUBUCUDUE $.
+    $( $j usage 'equsexv' avoids 'ax-10'; $)
+
+    $( Obsolete version of ~ equsexv as of 18-Nov-2024.  (Contributed by NM,
+       5-Aug-1993.)  (Revised by BJ, 31-May-2019.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    equsexvOLD $p |- ( E. x ( x = y /\ ph ) <-> ps ) $=
       ( weq wa wex wi wal sbalex equsalv bitri ) CDGZAHCIOAJCKBACDLABCDEFMN $.
   $}
 
@@ -20507,8 +20517,22 @@ variables be distinct (cf. ~ cbvaev and ~ aecom , for example) in proofs.
        require ~ ax-13 .  Remark: the corresponding versions for ~ dral2 and
        ~ drex2 are instances of ~ albidv and ~ exbidv respectively.
        (Contributed by NM, 24-Nov-1994.)  (Revised by BJ, 17-Jun-2019.)  Base
-       the proof on ~ ax12v .  (Revised by Wolf Lammen, 30-Mar-2024.) $)
+       the proof on ~ ax12v .  (Revised by Wolf Lammen, 30-Mar-2024.)  Avoid
+       ~ ax-10 .  (Revised by Gino Giotto, 18-Nov-2024.) $)
     dral1v $p |- ( A. x x = y -> ( A. x ph <-> A. y ps ) ) $=
+      ( weq wal wi aev wb wa dfbi2 sp imim1i ax12v2 sps syl9 syl sylc alim syl6
+      equcoms adantr sylbi com23 simplbiim mpcom imp impancom anidms impbid ) C
+      DFZCGZACGZBDGZUMDCFZDGZUQUNUOHCDDCDIZURUQUNUQUOUQUNUPBHDGZUQUOHUQUMUMUNUS
+      HZDCCDCIZVAUMABJZUMUTHZEVBABHZBAHZKVCABLZVDVCVEVDUNBUMUSUNABACMNULBUSHZCV
+      GDCBDCOUBPQUCUDRSUPBDTUAUESUMUOUNHUMUOUMUNUMUOKULAHCGZUMUNHUMUOVHVBUMUOVH
+      HZEVBVDVEUMVIHVFVEUOAUMVHUOBABDMNULAVHHCACDOPQUFUGUHULACTRUIUJUK $.
+    $( $j usage 'dral1v' avoids 'ax-10'; $)
+
+    $( Obsolete version of ~ dral1v as of 18-Nov-2024.  (Contributed by NM,
+       24-Nov-1994.)  (Revised by BJ, 17-Jun-2019.)  Base the proof on
+       ~ ax12v .  (Revised by Wolf Lammen, 30-Mar-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    dral1vOLD $p |- ( A. x x = y -> ( A. x ph <-> A. y ps ) ) $=
       ( weq wal nfa1 albid axc11v axc11rv impbid bitrd ) CDFZCGZACGBCGZBDGZOABC
       NCHEIOPQBCDJBCDKLM $.
 
@@ -20523,8 +20547,17 @@ variables be distinct (cf. ~ cbvaev and ~ aecom , for example) in proofs.
     $( Formula-building lemma for use with the Distinctor Reduction Theorem.
        Version of ~ drnf1 with a disjoint variable condition, which does not
        require ~ ax-13 .  (Contributed by Mario Carneiro, 4-Oct-2016.)
-       (Revised by BJ, 17-Jun-2019.) $)
+       (Revised by BJ, 17-Jun-2019.)  Avoid ~ ax-10 .  (Revised by Gino Giotto,
+       18-Nov-2024.) $)
     drnf1v $p |- ( A. x x = y -> ( F/ x ph <-> F/ y ps ) ) $=
+      ( weq wal wex wi wnf drex1v dral1v imbi12d df-nf 3bitr4g ) CDFCGZACHZACGZ
+      IBDHZBDGZIACJBDJPQSRTABCDEKABCDELMACNBDNO $.
+    $( $j usage 'drnf1v' avoids 'ax-10'; $)
+
+    $( Obsolete version of ~ drnf1v as of 18-Nov-2024.  (Contributed by Mario
+       Carneiro, 4-Oct-2016.)  (Revised by BJ, 17-Jun-2019.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    drnf1vOLD $p |- ( A. x x = y -> ( F/ x ph <-> F/ y ps ) ) $=
       ( weq wal wi wnf dral1v imbi12d nf5 3bitr4g ) CDFCGZAACGZHZCGBBDGZHZDGACI
       BDIPRCDNABOQEABCDEJKJACLBDLM $.
   $}
@@ -48574,12 +48607,26 @@ although the definition does not require it (see ~ dfid2 for a case
   $}
 
   ${
-    $d x y z $.  $d z ph $.  $d x ps $.
+    $d x y z w $.  $d z w ph $.  $d x w ps $.
     cbvopab1v.1 $e |- ( x = z -> ( ph <-> ps ) ) $.
     $( Rule used to change the first bound variable in an ordered pair
        abstraction, using implicit substitution.  (Contributed by NM,
-       31-Jul-2003.)  (Proof shortened by Eric Schmidt, 4-Apr-2007.) $)
+       31-Jul-2003.)  (Proof shortened by Eric Schmidt, 4-Apr-2007.)  Reduce
+       axiom usage.  (Revised by Gino Giotto, 17-Nov-2024.) $)
     cbvopab1v $p |- { <. x , y >. | ph } = { <. z , y >. | ps } $=
+      ( vw cv cop wceq wa wex cab copab weq opeq1 eqeq2d anbi12d exbidv df-opab
+      cbvexvw abbii 3eqtr4i ) GHZCHZDHZIZJZAKZDLZCLZGMUDEHZUFIZJZBKZDLZELZGMACD
+      NBEDNUKUQGUJUPCECEOZUIUODURUHUNABURUGUMUDUEULUFPQFRSUAUBACDGTBEDGTUC $.
+    $( $j usage 'cbvopab1v' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d x y z $.  $d z ph $.  $d x ps $.
+    cbvopab1vOLD.1 $e |- ( x = z -> ( ph <-> ps ) ) $.
+    $( Obsolete version of ~ cbvopab1v as of 17-Nov-2024.  (Contributed by NM,
+       31-Jul-2003.)  (Proof shortened by Eric Schmidt, 4-Apr-2007.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    cbvopab1vOLD $p |- { <. x , y >. | ph } = { <. z , y >. | ps } $=
       ( nfv cbvopab1 ) ABCDEAEGBCGFH $.
   $}
 
@@ -48936,14 +48983,29 @@ although the definition does not require it (see ~ dfid2 for a case
   $}
 
   ${
-    $d A x y $.  $d B y $.  $d C x $.
+    $d A x y z $.  $d B y z $.  $d C x z $.
     cbvmptv.1 $e |- ( x = y -> B = C ) $.
     $( Rule to change the bound variable in a maps-to function, using implicit
        substitution.  (Contributed by Mario Carneiro, 19-Feb-2013.)  Add
-       disjoint variable condition to avoid ~ ax-13 .  See ~ cbvmptvg for a
-       less restrictive version requiring more axioms.  (Revised by Gino
-       Giotto, 17-Jan-2024.) $)
+       disjoint variable condition to avoid auxiliary axioms .  See ~ cbvmptvg
+       for a less restrictive version requiring more axioms.  (Revised by Gino
+       Giotto, 17-Nov-2024.) $)
     cbvmptv $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
+      ( vz cv wcel wceq wa copab eleq1w eqeq2d anbi12d cbvopab1v df-mpt 3eqtr4i
+      cmpt weq ) AHCIZGHZDJZKZAGLBHCIZUBEJZKZBGLACDSBCESUDUGAGBABTZUAUEUCUFABCM
+      UHDEUBFNOPAGCDQBGCEQR $.
+    $( $j usage 'cbvmptv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
+  ${
+    $d A x y $.  $d B y $.  $d C x $.
+    cbvmptvOLD.1 $e |- ( x = y -> B = C ) $.
+    $( Obsolete version of ~ cbvmptv as of 17-Nov-2024.  (Contributed by Mario
+       Carneiro, 19-Feb-2013.)  Add disjoint variable condition to avoid
+       ~ ax-13 .  See ~ cbvmptvg for a less restrictive version requiring more
+       axioms.  (Revised by Gino Giotto, 17-Jan-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    cbvmptvOLD $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( nfcv cbvmpt ) ABCDEBDGAEGFH $.
     $( $j usage 'cbvmptv' avoids 'ax-13'; $)
   $}
@@ -82544,20 +82606,6 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
       VJVMVFVGVH $.
   $}
 
-  ${
-    $d y A $.  $d y B $.  $d y C $.  $d y D $.  $d x E $.  $d x y $.
-    frsucmpt2w.1 $e |- F = ( rec ( ( x e. _V |-> C ) , A ) |` _om ) $.
-    frsucmpt2w.2 $e |- ( y = x -> E = C ) $.
-    frsucmpt2w.3 $e |- ( y = ( F ` B ) -> E = D ) $.
-    $( Version of ~ frsucmpt2 with a disjoint variable condition, which does
-       not require ~ ax-13 .  (Contributed by Gino Giotto, 26-Jan-2024.) $)
-    frsucmpt2w $p |- ( ( B e. _om /\ D e. V ) -> ( F ` suc B ) = D ) $=
-      ( nfcv cvv cmpt crdg com cres wceq cbvmptv rdgeq1 reseq1i eqtr4i frsucmpt
-      ax-mp ) BCDGFHIBCMBDMBFMHANEOZCPZQRBNGOZCPZQRJUIUGQUHUFSUIUGSBANGEKTCUHUF
-      UAUEUBUCLUD $.
-    $( $j usage 'frsucmpt2w' avoids 'ax-13'; $)
-  $}
-
   ${
     $d x y $.  $d y A $.  $d y B $.  $d y C $.  $d y D $.  $d x E $.
     frsucmpt2.1 $e |- F = ( rec ( ( x e. _V |-> C ) , A ) |` _om ) $.
@@ -82571,6 +82619,7 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
       ( nfcv cvv cmpt crdg com cres wceq cbvmptv rdgeq1 reseq1i eqtr4i frsucmpt
       ax-mp ) BCDGFHIBCMBDMBFMHANEOZCPZQRBNGOZCPZQRJUIUGQUHUFSUIUGSBANGEKTCUHUF
       UAUEUBUCLUD $.
+    $( $j usage 'frsucmpt2' avoids 'ax-13'; $)
   $}
 
   ${
@@ -99434,26 +99483,26 @@ a Cantor normal form (and injectivity, together with coherence
       ( vv vu wss cv com cfv wrex c0 wcel wceq fveq2 wtr wa wal ciun peano1 cvv
       wi cuni cun cmpt crdg cres fveq1i fr0g ax-mp eqtr2i eqimssi sseq2d rspcev
       mp2an ssiun sseqtrri dftr2 eliun anbi2i r19.42v bitr4i elunii ssun2 uniex
-      csuc fvex unex weq id unieq uneq12d frsucmpt2w mpan2 sseqtrrid sseld syl5
-      reximia sylbi peano2 eleq2d ex syl rexlimiv cbvrexvw sylibr ax-gen mpgbir
-      wb treq mpbir sseq1d eqtri sseq1i biimpri adantr uniss df-tr sstr2 syl5bi
-      wral anc2li unss syl6ib biimprd syl9r com23 adantld finds2 com12 ralrimiv
-      cbviunv iunss bitri 3pm3.2i ) DELEUAZDAMZLZYBUAZUBZEYBLZUGZAUCDBNBMZFOZUD
-      ZEDYILZBNPZDYJLQNRDQFOZLZYLUEDYMYMQCUFCMZYOUHZUIZUJZDUKNULZOZDQFYSHUMZDUF
-      RYTDSGDUFYRUNUOZUPUQYKYNBQNYHQSYIYMDYHQFTURUSUTBNYIDVAUOIVBYAYJUAZUUCJMZK
-      MZRZUUEYJRZUBZUUDYJRZUGZKUCJJKYJVCUUJKUUHUUDYHVKZFOZRZBNPZUUIUUHUUFUUEYIR
-      ZUBZBNPZUUNUUHUUFUUOBNPZUBUUQUUGUURUUFBUUENYIVDVEUUFUUOBNVFVGUUPUUMBNUUPU
-      UDYIUHZRYHNRZUUMUUDUUEYIVHUUTUUSUULUUDUUTYIUUSUIZUUSUULUUSYIVIUUTUVAUFRUU
-      LUVASYIUUSYHFVLZYIUVBVJVMCADYHYQUVAYBYBUHZUIFUFHACVNZYBYOUVCYPUVDVOYBYOVP
-      VQYBYISZYBYIUVCUUSUVEVOYBYIVPVQVRVSZVTWAWBWCWDUUNUUDYIRZBNPZUUIUUNUUDUUEF
-      OZRZKNPZUVHUUMUVKBNUUTUUKNRZUUMUVKUGYHWEUVLUUMUVKUVJUUMKUUKNUUEUUKSUVIUUL
-      UUDUUEUUKFTWFUSWGWHWIUVGUVJBKNBKVNYIUVIUUDYHUUEFTWFWJWKBUUDNYIVDWKWHWLWME
-      YJSYAUUCWNIEYJWOUOWPYGAYEUUDFOZYBLZJNXFZYFYEUVNJNUUDNRYEUVNUVNYMYBLZYIYBL
-      ZUULYBLZYEJBUUDQSUVMYMYBUUDQFTWQJBVNUVMYIYBUUDYHFTWQUUDUUKSUVMUULYBUUDUUK
-      FTWQYCUVPYDUVPYCYMDYBYMYTDUUAUUBWRWSWTXAUUTYDUVQUVRUGYCUUTUVQYDUVRUVQYDUV
-      AYBLZUUTUVRUVQYDUVQUUSYBLZUBUVSUVQYDUVTUVQUUSUVCLZYDUVTUGYIYBXBYDUVCYBLUW
-      AUVTYBXCUUSUVCYBXDXEWHXGYIUUSYBXHXIUUTUVRUVSUUTUULUVAYBUVFWQXJXKXLXMXNXOX
-      PYFJNUVMUDZYBLUVOEUWBYBEYJUWBIBJNYIUVMYHUUDFTXQWRWSJNUVMYBXRXSWKWLXT $.
+      csuc fvex unex unieq uneq12d frsucmpt2 mpan2 sseqtrrid sseld syl5 reximia
+      weq id sylbi peano2 eleq2d ex rexlimiv cbvrexvw sylibr ax-gen mpgbir treq
+      wb mpbir wral sseq1d eqtri sseq1i biimpri adantr uniss df-tr sstr2 syl5bi
+      syl anc2li unss syl6ib biimprd syl9r com23 adantld com12 ralrimiv cbviunv
+      finds2 iunss bitri 3pm3.2i ) DELEUAZDAMZLZYBUAZUBZEYBLZUGZAUCDBNBMZFOZUDZ
+      EDYILZBNPZDYJLQNRDQFOZLZYLUEDYMYMQCUFCMZYOUHZUIZUJZDUKNULZOZDQFYSHUMZDUFR
+      YTDSGDUFYRUNUOZUPUQYKYNBQNYHQSYIYMDYHQFTURUSUTBNYIDVAUOIVBYAYJUAZUUCJMZKM
+      ZRZUUEYJRZUBZUUDYJRZUGZKUCJJKYJVCUUJKUUHUUDYHVKZFOZRZBNPZUUIUUHUUFUUEYIRZ
+      UBZBNPZUUNUUHUUFUUOBNPZUBUUQUUGUURUUFBUUENYIVDVEUUFUUOBNVFVGUUPUUMBNUUPUU
+      DYIUHZRYHNRZUUMUUDUUEYIVHUUTUUSUULUUDUUTYIUUSUIZUUSUULUUSYIVIUUTUVAUFRUUL
+      UVASYIUUSYHFVLZYIUVBVJVMCADYHYQUVAYBYBUHZUIFUFHACWBZYBYOUVCYPUVDWCYBYOVNV
+      OYBYISZYBYIUVCUUSUVEWCYBYIVNVOVPVQZVRVSVTWAWDUUNUUDYIRZBNPZUUIUUNUUDUUEFO
+      ZRZKNPZUVHUUMUVKBNUUTUUKNRZUUMUVKUGYHWEUVLUUMUVKUVJUUMKUUKNUUEUUKSUVIUULU
+      UDUUEUUKFTWFUSWGXFWHUVGUVJBKNBKWBYIUVIUUDYHUUEFTWFWIWJBUUDNYIVDWJXFWKWLEY
+      JSYAUUCWNIEYJWMUOWOYGAYEUUDFOZYBLZJNWPZYFYEUVNJNUUDNRYEUVNUVNYMYBLZYIYBLZ
+      UULYBLZYEJBUUDQSUVMYMYBUUDQFTWQJBWBUVMYIYBUUDYHFTWQUUDUUKSUVMUULYBUUDUUKF
+      TWQYCUVPYDUVPYCYMDYBYMYTDUUAUUBWRWSWTXAUUTYDUVQUVRUGYCUUTUVQYDUVRUVQYDUVA
+      YBLZUUTUVRUVQYDUVQUUSYBLZUBUVSUVQYDUVTUVQUUSUVCLZYDUVTUGYIYBXBYDUVCYBLUWA
+      UVTYBXCUUSUVCYBXDXEXFXGYIUUSYBXHXIUUTUVRUVSUUTUULUVAYBUVFWQXJXKXLXMXQXNXO
+      YFJNUVMUDZYBLUVOEUWBYBEYJUWBIBJNYIUVMYHUUDFTXPWRWSJNUVMYBXRXSWJWKXT $.
   $}
 
   ${
@@ -115817,58 +115866,58 @@ prove that every set is contained in a weak universe in ZF (see
       fneq1i mpbir fnunirn ax-mp bitri csuc elssuni ad2antll ssun2 ssun1 sstrdi
       c1o sstri wceq simprl fvex uniex unex prex mptex rnex iunex unieq uneq12d
       weq pweq preq12d preq2 cbvmptv preq1 mpteq2dv eqtrid rneqd cbviunv mpteq1
-      uneq2d iuneq12d frsucmpt2w sylancl sseqtrrd fvssunirn sseqtrri rexlimdvaa
-      id syl5bi ralrimiv dftr3 sylibr con0 1on unexg mpan2 fveq1i syl eqsstrrdi
-      fr0g unssbd ssn0 ssiun2s sseqtrrid sstrd unssad vpwex vuniex simprd fveq2
-      1n0 prss sseq2d vtoclga findsg sseldd wi imbi12d eqeltri word ordom ssidd
-      simpld simplrl ordunel mp3an2i suceq fveq2d sseq12d sstr2 syl5com syl2anc
-      ad2antrr simplrr biantrud bicomd eleq1w anbi2d sseq1 anbi12d chvarvv expl
-      sseq1d sylc eqid elrnmpt1s 3jca wfun omex resfunexg mp2an iswun syl3anbrc
-      simprr rdgfun jca ) DGNZEUFNZDEOUVREUGZEUJUHZJPZUIZENZUWBUKZENZUWBUAPZULZ
-      ENZUAEUMZUNZJEUMZUVSUVRUWBEOZJEUMUVTUVRUWMJEUWBENZUWBKPZFUOZNZKQUPZUVRUWM
-      UWNUWBFUQZUIZNZUWREUWTUWBIURFQUSZUXAUWRUTUXBCRCPZUXCUIZSZAUXCAPZUKZUXFUIZ
-      ULZBUXCUXFBPZULZVAZUQZSZVBZSZVAZDVQSZVCZQVDZQUSUXRUXQVEQFUXTHVFVGZKUWBFQV
-      HVIVJZUVRUWQUWMKQUVRUWOQNZUWQTTZUWBUWOVKZFUOZEUYDUWBUWPUWPUIZSZLUWPLPZUKZ
-      UYIUIZULZMUWPUYIMPZULZVAZUQZSZVBZSZUYFUYDUWBUYGUYSUWQUWBUYGOUVRUYCUWBUWPV
-      LVMUYGUYHUYSUYGUWPVNUYHUYRVOZVRVPUYDUYCUYSRNZUYFUYSVSZUVRUYCUWQVTUYHUYRUW
-      PUYGUWOFWAZUWPVUCWBWCLUWPUYQVUCUYLUYPUYJUYKWDZUYOMUWPUYNVUCWEWFWCWGWCZCUB
-      UXRUWOUXPUYSUBPZVUFUIZSZLVUFUYLMVUFUYNVAZUQZSZVBZSZFRHUBCWJZVUHUXEVULUXOV
-      UNVUFUXCVUGUXDVUNXIZVUFUXCWHWIVUNVULAVUFUXIBVUFUXKVAZUQZSZVBUXOLAVUFVUKVU
-      RLAWJZUYLUXIVUJVUQVUSUYJUXGUYKUXHUYIUXFWKUYIUXFWHWLVUSVUIVUPVUSVUIBVUFUYI
-      UXJULZVAVUPMBVUFUYNVUTUYMUXJUYIWMWNVUSBVUFVUTUXKUYIUXFUXJWOWPWQWRWIWSVUNA
-      VUFUXCVURUXNVUOVUNVUQUXMUXIVUNVUPUXLBVUFUXCUXKWTWRXAXBWQWIZVUFUWPVSZVUHUY
-      HVULUYRVVBVUFUWPVUGUYGVVBXIZVUFUWPWHWIVVBLVUFUWPVUKUYQVVCVVBVUJUYPUYLVVBV
-      UIUYOMVUFUWPUYNWTWRXAXBWIXCZXDZXEUYFUWTEFUYEXFIXGZVPXHXJXKJEXLXMUVRVQEOVQ
-      UJUHUWAUVRDVQEUVRUXRUJFUOZEUVRUXRRNZVVGUXRVSUVRVQXNNVVHXODVQGXNXPXQVVHVVG
-      UJUXTUOUXRUJFUXTHXRUXRRUXQYAWQXSVVGUWTEFUJXFIXGXTZYBYLVQEYCXDUVRUWKJEUWNU
-      WRUVRUWKUYBUVRUWQUWKKQUYDUWDUWFUWJUYDUWFUWDUYDUWEUWCULZEOUWFUWDTUYDVVJMUW
-      PUWBUYMULZVAZUQZEUYDVVJVVMSZUYREUWQVVNUYROUVRUYCLUWPUYQUWBVVNLJWJZUYLVVJU
-      YPVVMVVOUYJUWEUYKUWCUYIUWBWKUYIUWBWHWLZVVOUYOVVLVVOMUWPUYNVVKUYIUWBUYMWOZ
-      WPWRWIYDVMUYDUYRUYFEUYDUYSUYRUYFUYRUYHVNVVEYEVVFVPYFYGUWEUWCEJYHJYIYMXMZY
-      JUYDUWFUWDVVRUUDUYDUWIUAEUWGENZUWGUCPZFUOZNZUCQUPZUYDUWIVVSUWGUWTNZVWCEUW
-      TUWGIURUXBVWDVWCUTUYAUCUWGFQVHVIVJUYDVWBUWIUCQUYDVVTQNZVWBTZTZMUWOVVTSZFU
-      OZVVKVAZUQZEUWHVWGVVJVWKEVWGVVJVWKSZLVWIUYLMVWIUYNVAZUQZSZVBZEVWGUWBVWINV
-      WLVWPOVWGUWPVWIUWBVWGVWHQNZUYCUWPVWIOZQUUAVWGUYCVWEVWQUUBUVRUYCUWQVWFUUEZ
-      UYDVWEVWBVTZQUWOVVTUUFUUGZVWSVWQUYCTUWOVWHOVWRUWOVVTVOUWPUDPZFUOZOZUWPUWP
-      OZUWPUEPZFUOZOZUWPVXFVKZFUOZOZVWRUDUEVWHUWOUDKWJVXCUWPUWPVXBUWOFYKYNZUDUE
-      WJVXCVXGUWPVXBVXFFYKYNZVXBVXIVSVXCVXJUWPVXBVXIFYKYNZVXBVWHVSVXCVWIUWPVXBV
-      WHFYKYNUYCUWPUUCZVXFQNZUYCTZUWOVXFOZTZVXGVXJOZVXHVXKVXPVXTUYCVXRUWPUYFOVX
-      TKVXFQKUEWJZUWPVXGUYFVXJUWOVXFFYKVYAUYEVXIFUWOVXFUUHUUIUUJUYCUYSUWPUYFUWP
-      UYHUYSUWPUYGVOUYTVRUYCVUAVUBVUEVVDXQYEYOUUNUWPVXGVXJUUKUULZYPXQUUMUVRUYCU
-      WQVWFUUOYQLVWIVWOUWBVWLVVOUYLVVJVWNVWKVVPVVOVWMVWJVVOMVWIUYNVVKVVQWPWRWIY
-      DXSVWGVWPVWHVKZFUOZEVWGVWIVWIUIZSZVWPSZVWPVYDVWPVYFVNVWGVWQVYGRNVYDVYGVSV
-      XAVYFVWPVWIVYEVWHFWAZVWIVYHWBWCLVWIVWOVYHUYLVWNVUDVWMMVWIUYNVYHWEWFWCWGWC
-      CUBUXRVWHUXPVYGVUMFRHVVAVUFVWIVSZVUHVYFVULVWPVYIVUFVWIVUGVYEVYIXIZVUFVWIW
-      HWIVYILVUFVWIVUKVWOVYJVYIVUJVWNUYLVYIVUIVWMMVUFVWIUYNWTWRXAXBWIXCXDYEVYDU
-      WTEFVYCXFIXGVPYFYBVWGUWGVWINUWHRNUWHVWKNVWGVWAVWIUWGVWGVWQVWEVWAVWIOZVXAV
-      WTVWEVVTVXFOZTZVWAVXGOZYRVWEVYKYRUEVWHQVXFVWHVSZVYMVWEVYNVYKVYOVWEVYMVYOV
-      YLVWEVYOVWHVVTVXFVVTUWOVNVYOXIYEUUPUUQVYOVXGVWIVWAVXFVWHFYKYNYSVXPVWEVYLV
-      YNVXSVXHYRVXPVWETZVYLTZVYNYRKUCKUCWJZVXSVYQVXHVYNVYRVXQVYPVXRVYLVYRUYCVWE
-      VXPKUCQUURUUSUWOVVTVXFUUTUVAVYRUWPVWAVXGUWOVVTFYKUVDYSVXDVXEVXHVXKVXHUDUE
-      VXFUWOVXLVXMVXNVXMVXOVYBYPUVBUVCYOUVEUYDVWEVWBUVOYQUWBUWGWDMVWIVVKUWHUWGV
-      WJRVWJUVFUYMUWGUWBWMUVGXDYQXHXJXKUVHXHXJXKERNUVSUVTUWAUWLUNUTEUWTRIUWSFFU
-      XTRHUXSUVIQRNUXTRNUXRUXQUVPUVJUXSQRUVKUVLYTWFWBYTJUAERUVMVIUVNUVRDVQEVVIY
-      GUVQ $.
+      id uneq2d iuneq12d frsucmpt2 sylancl sseqtrrd fvssunirn rexlimdvaa syl5bi
+      sseqtrri ralrimiv dftr3 sylibr con0 1on unexg mpan2 fveq1i fr0g eqsstrrdi
+      syl unssbd 1n0 ssn0 sseqtrrid sstrd unssad vpwex vuniex prss simprd fveq2
+      ssiun2s sseq2d vtoclga findsg sseldd wi imbi12d eqeltri simpld word ordom
+      simplrl ordunel mp3an2i ssidd suceq fveq2d sseq12d ad2antrr sstr2 syl5com
+      syl2anc simplrr biantrud bicomd eleq1w anbi2d anbi12d sseq1d chvarvv expl
+      sseq1 sylc simprr eqid elrnmpt1s 3jca wfun omex resfunexg mp2an syl3anbrc
+      rdgfun iswun jca ) DGNZEUFNZDEOUVREUGZEUJUHZJPZUIZENZUWBUKZENZUWBUAPZULZE
+      NZUAEUMZUNZJEUMZUVSUVRUWBEOZJEUMUVTUVRUWMJEUWBENZUWBKPZFUOZNZKQUPZUVRUWMU
+      WNUWBFUQZUIZNZUWREUWTUWBIURFQUSZUXAUWRUTUXBCRCPZUXCUIZSZAUXCAPZUKZUXFUIZU
+      LZBUXCUXFBPZULZVAZUQZSZVBZSZVAZDVQSZVCZQVDZQUSUXRUXQVEQFUXTHVFVGZKUWBFQVH
+      VIVJZUVRUWQUWMKQUVRUWOQNZUWQTTZUWBUWOVKZFUOZEUYDUWBUWPUWPUIZSZLUWPLPZUKZU
+      YIUIZULZMUWPUYIMPZULZVAZUQZSZVBZSZUYFUYDUWBUYGUYSUWQUWBUYGOUVRUYCUWBUWPVL
+      VMUYGUYHUYSUYGUWPVNUYHUYRVOZVRVPUYDUYCUYSRNZUYFUYSVSZUVRUYCUWQVTUYHUYRUWP
+      UYGUWOFWAZUWPVUCWBWCLUWPUYQVUCUYLUYPUYJUYKWDZUYOMUWPUYNVUCWEWFWCWGWCZCUBU
+      XRUWOUXPUYSUBPZVUFUIZSZLVUFUYLMVUFUYNVAZUQZSZVBZSZFRHUBCWJZVUHUXEVULUXOVU
+      NVUFUXCVUGUXDVUNXAZVUFUXCWHWIVUNVULAVUFUXIBVUFUXKVAZUQZSZVBUXOLAVUFVUKVUR
+      LAWJZUYLUXIVUJVUQVUSUYJUXGUYKUXHUYIUXFWKUYIUXFWHWLVUSVUIVUPVUSVUIBVUFUYIU
+      XJULZVAVUPMBVUFUYNVUTUYMUXJUYIWMWNVUSBVUFVUTUXKUYIUXFUXJWOWPWQWRWIWSVUNAV
+      UFUXCVURUXNVUOVUNVUQUXMUXIVUNVUPUXLBVUFUXCUXKWTWRXBXCWQWIZVUFUWPVSZVUHUYH
+      VULUYRVVBVUFUWPVUGUYGVVBXAZVUFUWPWHWIVVBLVUFUWPVUKUYQVVCVVBVUJUYPUYLVVBVU
+      IUYOMVUFUWPUYNWTWRXBXCWIXDZXEZXFUYFUWTEFUYEXGIXJZVPXHXIXKJEXLXMUVRVQEOVQU
+      JUHUWAUVRDVQEUVRUXRUJFUOZEUVRUXRRNZVVGUXRVSUVRVQXNNVVHXODVQGXNXPXQVVHVVGU
+      JUXTUOUXRUJFUXTHXRUXRRUXQXSWQYAVVGUWTEFUJXGIXJXTZYBYCVQEYDXEUVRUWKJEUWNUW
+      RUVRUWKUYBUVRUWQUWKKQUYDUWDUWFUWJUYDUWFUWDUYDUWEUWCULZEOUWFUWDTUYDVVJMUWP
+      UWBUYMULZVAZUQZEUYDVVJVVMSZUYREUWQVVNUYROUVRUYCLUWPUYQUWBVVNLJWJZUYLVVJUY
+      PVVMVVOUYJUWEUYKUWCUYIUWBWKUYIUWBWHWLZVVOUYOVVLVVOMUWPUYNVVKUYIUWBUYMWOZW
+      PWRWIYMVMUYDUYRUYFEUYDUYSUYRUYFUYRUYHVNVVEYEVVFVPYFYGUWEUWCEJYHJYIYJXMZYK
+      UYDUWFUWDVVRUUAUYDUWIUAEUWGENZUWGUCPZFUOZNZUCQUPZUYDUWIVVSUWGUWTNZVWCEUWT
+      UWGIURUXBVWDVWCUTUYAUCUWGFQVHVIVJUYDVWBUWIUCQUYDVVTQNZVWBTZTZMUWOVVTSZFUO
+      ZVVKVAZUQZEUWHVWGVVJVWKEVWGVVJVWKSZLVWIUYLMVWIUYNVAZUQZSZVBZEVWGUWBVWINVW
+      LVWPOVWGUWPVWIUWBVWGVWHQNZUYCUWPVWIOZQUUBVWGUYCVWEVWQUUCUVRUYCUWQVWFUUDZU
+      YDVWEVWBVTZQUWOVVTUUEUUFZVWSVWQUYCTUWOVWHOVWRUWOVVTVOUWPUDPZFUOZOZUWPUWPO
+      ZUWPUEPZFUOZOZUWPVXFVKZFUOZOZVWRUDUEVWHUWOUDKWJVXCUWPUWPVXBUWOFYLYNZUDUEW
+      JVXCVXGUWPVXBVXFFYLYNZVXBVXIVSVXCVXJUWPVXBVXIFYLYNZVXBVWHVSVXCVWIUWPVXBVW
+      HFYLYNUYCUWPUUGZVXFQNZUYCTZUWOVXFOZTZVXGVXJOZVXHVXKVXPVXTUYCVXRUWPUYFOVXT
+      KVXFQKUEWJZUWPVXGUYFVXJUWOVXFFYLVYAUYEVXIFUWOVXFUUHUUIUUJUYCUYSUWPUYFUWPU
+      YHUYSUWPUYGVOUYTVRUYCVUAVUBVUEVVDXQYEYOUUKUWPVXGVXJUULUUMZYPXQUUNUVRUYCUW
+      QVWFUUOYQLVWIVWOUWBVWLVVOUYLVVJVWNVWKVVPVVOVWMVWJVVOMVWIUYNVVKVVQWPWRWIYM
+      YAVWGVWPVWHVKZFUOZEVWGVWIVWIUIZSZVWPSZVWPVYDVWPVYFVNVWGVWQVYGRNVYDVYGVSVX
+      AVYFVWPVWIVYEVWHFWAZVWIVYHWBWCLVWIVWOVYHUYLVWNVUDVWMMVWIUYNVYHWEWFWCWGWCC
+      UBUXRVWHUXPVYGVUMFRHVVAVUFVWIVSZVUHVYFVULVWPVYIVUFVWIVUGVYEVYIXAZVUFVWIWH
+      WIVYILVUFVWIVUKVWOVYJVYIVUJVWNUYLVYIVUIVWMMVUFVWIUYNWTWRXBXCWIXDXEYEVYDUW
+      TEFVYCXGIXJVPYFYBVWGUWGVWINUWHRNUWHVWKNVWGVWAVWIUWGVWGVWQVWEVWAVWIOZVXAVW
+      TVWEVVTVXFOZTZVWAVXGOZYRVWEVYKYRUEVWHQVXFVWHVSZVYMVWEVYNVYKVYOVWEVYMVYOVY
+      LVWEVYOVWHVVTVXFVVTUWOVNVYOXAYEUUPUUQVYOVXGVWIVWAVXFVWHFYLYNYSVXPVWEVYLVY
+      NVXSVXHYRVXPVWETZVYLTZVYNYRKUCKUCWJZVXSVYQVXHVYNVYRVXQVYPVXRVYLVYRUYCVWEV
+      XPKUCQUURUUSUWOVVTVXFUVDUUTVYRUWPVWAVXGUWOVVTFYLUVAYSVXDVXEVXHVXKVXHUDUEV
+      XFUWOVXLVXMVXNVXMVXOVYBYPUVBUVCYOUVEUYDVWEVWBUVFYQUWBUWGWDMVWIVVKUWHUWGVW
+      JRVWJUVGUYMUWGUWBWMUVHXEYQXHXIXKUVIXHXIXKERNUVSUVTUWAUWLUNUTEUWTRIUWSFFUX
+      TRHUXSUVJQRNUXTRNUXRUXQUVOUVKUXSQRUVLUVMYTWFWBYTJUAERUVPVIUVNUVRDVQEVVIYG
+      UVQ $.
   $}
 
   ${