revise exan + shorten equsb1v (#3263)

* expand hypothesis of exan

* shorten equsb1v

Author: icecream17

discouraged

@@ -15336,6 +15336,7 @@ New usage of "equs5aALT" is discouraged (0 uses).
 New usage of "equs5eALT" is discouraged (0 uses).
 New usage of "equsalhwOLD" is discouraged (0 uses).
 New usage of "equsb1vOLD" is discouraged (0 uses).
+New usage of "equsb1vOLDOLD" is discouraged (0 uses).
 New usage of "equsb3ALT" is discouraged (0 uses).
 New usage of "equsb3vOLD" is discouraged (0 uses).
 New usage of "equsexALT" is discouraged (0 uses).
@@ -15399,6 +15400,7 @@ New usage of "ex-natded9.20-2" is discouraged (0 uses).
 New usage of "ex-natded9.26" is discouraged (0 uses).
 New usage of "ex-natded9.26-2" is discouraged (0 uses).
 New usage of "exanOLD" is discouraged (0 uses).
+New usage of "exanOLDOLD" is discouraged (0 uses).
 New usage of "exatleN" is discouraged (1 uses).
 New usage of "exbirVD" is discouraged (0 uses).
 New usage of "exbiriVD" is discouraged (0 uses).
@@ -18932,7 +18934,8 @@ 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 "equsalhwOLD" is discouraged (39 steps).
-Proof modification of "equsb1vOLD" is discouraged (17 steps).
+Proof modification of "equsb1vOLD" is discouraged (32 steps).
+Proof modification of "equsb1vOLDOLD" is discouraged (17 steps).
 Proof modification of "equsb3ALT" is discouraged (44 steps).
 Proof modification of "equsb3vOLD" is discouraged (16 steps).
 Proof modification of "equsexALT" is discouraged (37 steps).
@@ -18978,7 +18981,8 @@ Proof modification of "ex-natded9.20" is discouraged (58 steps).
 Proof modification of "ex-natded9.20-2" is discouraged (44 steps).
 Proof modification of "ex-natded9.26" is discouraged (65 steps).
 Proof modification of "ex-natded9.26-2" is discouraged (22 steps).
-Proof modification of "exanOLD" is discouraged (29 steps).
+Proof modification of "exanOLD" is discouraged (19 steps).
+Proof modification of "exanOLDOLD" is discouraged (29 steps).
 Proof modification of "exbirVD" is discouraged (65 steps).
 Proof modification of "exbiriVD" is discouraged (70 steps).
 Proof modification of "exinst" is discouraged (12 steps).

set.mm

@@ -15328,13 +15328,27 @@ only postulated (that is, axiomatic) rule of inference of predicate
     ( wa ancom exbii ) ABDBADCABEF $.
 
   ${
-    exan.1 $e |- ( E. x ph /\ ps ) $.
+    exan.1 $e |- E. x ph $.
+    exan.2 $e |- ps $.
     $( Place a conjunct in the scope of an existential quantifier.
        (Contributed by NM, 18-Aug-1993.)  (Proof shortened by Andrew Salmon,
        25-May-2011.)  (Proof shortened by Wolf Lammen, 13-Jan-2018.)  Reduce
        axiom dependencies.  (Revised by BJ, 7-Jul-2021.)  (Proof shortened by
-       Wolf Lammen, 6-Nov-2022.) $)
+       Wolf Lammen, 6-Nov-2022.)  Expand hypothesis.  (Revised by Steven
+       Nguyen, 19-Jun-2023.) $)
     exan $p |- E. x ( ph /\ ps ) $=
+      ( wa jctr eximii ) AABFCDABEGH $.
+  $}
+
+  ${
+    exanOLD.1 $e |- ( E. x ph /\ ps ) $.
+    $( Obsolete proof of ~ exan as of 19-Jun-2023.  (Contributed by NM,
+       18-Aug-1993.)  (Proof shortened by Andrew Salmon, 25-May-2011.)  (Proof
+       shortened by Wolf Lammen, 13-Jan-2018.)  Reduce axiom dependencies.
+       (Revised by BJ, 7-Jul-2021.)  (Proof shortened by Wolf Lammen,
+       6-Nov-2022.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    exanOLD $p |- E. x ( ph /\ ps ) $=
       ( wa wex simpli simpri jctr eximii ) AABECACFZBDGABKBDHIJ $.
 
     $( Obsolete proof of ~ exan as of 6-Nov-2022.  (Contributed by NM,
@@ -15343,7 +15357,7 @@ only postulated (that is, axiomatic) rule of inference of predicate
        (Revised by BJ, 7-Jul-2021.)  (Proof shortened by Wolf Lammen,
        8-Oct-2021.)  (Proof modification is discouraged.)
        (New usage is discouraged.) $)
-    exanOLD $p |- E. x ( ph /\ ps ) $=
+    exanOLDOLD $p |- E. x ( ph /\ ps ) $=
       ( wex wa simpli wi simpri pm3.21 ax-mp eximi ) ACEZABFZCEMBDGANCBANHMBDIB
       AJKLK $.
   $}
@@ -16682,27 +16696,40 @@ modal logic (the other standard formulation being ~ extru ).  Note:  This
       ( weq wi wal wex ax6ev exim mpi exlimiv ) BCDZAEBFZABGZCMLBGNBCHLABIJK $.
   $}
 
+  ${
+    $d x y $.
+    sbtv.1 $e |- ph $.
+    $( A substitution into a theorem yields a theorem.  See ~ sbt when ` x ` ,
+       ` y ` need not be disjoint.  (Contributed by Steven Nguyen,
+       25-Apr-2023.) $)
+    sbtv $p |- [ x / y ] ph $=
+      ( wsb weq wi wa wex a1i ax6ev exan df-sb mpbir2an ) ACBECBFZAGOAHCIAODJOA
+      CCBKDLACBMN $.
+  $}
+
   ${
     $d x y $.
     $( Version of ~ equsb1 with a disjoint variable condition, which neither
        requires ~ ax-12 nor ~ ax-13 .  (Contributed by BJ, 11-Sep-2019.)
        Remove dependencies on axioms.  (Revised by Wolf Lammen, 30-May-2023.)
-       (Proof shortened by Steven Nguyen, 31-May-2023.) $)
+       (Proof shortened by Steven Nguyen, 19-Jun-2023.) $)
     equsb1v $p |- [ y / x ] x = y $=
-      ( weq wsb wi wa wex id ax6ev ancli eximii df-sb mpbir2an ) ABCZABDNNENNFZ
-      AGNHZNOAABINNPJKNABLM $.
+      ( weq wsb wi id sbtv sbequ8 mpbir ) ABCZABDJJEZABDKBAJFGJABHI $.
     $( $j usage 'equsb1v' avoids 'ax-12' 'ax-13'; $)
   $}
 
   ${
     $d x y $.
-    sbtv.1 $e |- ph $.
-    $( A substitution into a theorem yields a theorem.  See ~ sbt when ` x ` ,
-       ` y ` need not be disjoint.  (Contributed by Steven Nguyen,
-       25-Apr-2023.) $)
-    sbtv $p |- [ x / y ] ph $=
-      ( wsb weq wi wa wex a1i ax6ev pm3.2i exan df-sb mpbir2an ) ACBECBFZAGPAHC
-      IAPDJPACPCIACBKDLMACBNO $.
+    $( Obsolete version of ~ equsb1v as of 19-Jun-2023.  Version of ~ equsb1
+       with a disjoint variable condition, which neither requires ~ ax-12 nor
+       ~ ax-13 .  (Contributed by BJ, 11-Sep-2019.)  Remove dependencies on
+       axioms.  (Revised by Wolf Lammen, 30-May-2023.)  (Proof shortened by
+       Steven Nguyen, 31-May-2023.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    equsb1vOLD $p |- [ y / x ] x = y $=
+      ( weq wsb wi wa wex id ax6ev ancli eximii df-sb mpbir2an ) ABCZABDNNENNFZ
+      AGNHZNOAABINNPJKNABLM $.
+    $( $j usage 'equsb1vOLD' avoids 'ax-12' 'ax-13'; $)
   $}
 
   ${
@@ -18837,7 +18864,7 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
     $( Obsolete version of ~ equsb1v as of 30-May-2023.  (Contributed by BJ,
        11-Sep-2019.)  (Proof modification is discouraged.)
        (New usage is discouraged.) $)
-    equsb1vOLD $p |- [ y / x ] x = y $=
+    equsb1vOLDOLD $p |- [ y / x ] x = y $=
       ( weq wi wsb sb2v id mpg ) ABCZIDIABEAIABFIGH $.
   $}
 
@@ -45499,9 +45526,9 @@ conditioning it (with ` x e. z ` ) so that it asserts the existence of a
        p. 463.  (Contributed by NM, 21-Jun-1993.) $)
     bm1.3ii $p |- E. x A. y ( y e. x <-> ph ) $=
       ( vz wel wi wal wa wb wex 19.42v bimsc1 eximi sylbir elequ2 imbi2d albidv
-      alanimi weq cbvexvw mpbi ax-sep pm3.2i exan exlimiiv ) ACEFZGZCHZCBFZUGAI
-      JZCHZBKZIZUJAJZCHZBKZEUNUIULIZBKUQUIULBLURUPBUHUKUOCAUGUJMSNOUIUMEUIEKZUM
-      AUJGZCHZBKUSDVAUIBEBETZUTUHCVBUJUGABECPQRUAUBACBEUCUDUEUF $.
+      alanimi weq cbvexvw mpbi ax-sep exan exlimiiv ) ACEFZGZCHZCBFZUFAIJZCHZBK
+      ZIZUIAJZCHZBKZEUMUHUKIZBKUPUHUKBLUQUOBUGUJUNCAUFUIMSNOUHULEAUIGZCHZBKUHEK
+      DUSUHBEBETZURUGCUTUIUFABECPQRUAUBACBEUCUDUE $.
   $}
 
   ${
@@ -549385,10 +549412,10 @@ A collection of theorems for commuting equalities (or
        condition in the consequent.  (Contributed by Giovanni Mascellani,
        20-Aug-2018.) $)
     ac6s6f $p |- E. f A. x e. A ( E. y ph -> ps ) $=
-      ( vz cv wceq wex wi wral wa isseti vex ac6s6 pm3.2i exdistr raleqf biimpa
-      exan mpbir nfcv 2eximi ax5e mp2b ) KLZEMZADNBOZCUKPZQZFNKNZUMCEPZFNZKNURU
-      PULUNFNZQKNULUSKULKNUSKEGRABCDUKFHKSITUAUEULUNKFUBUFUOUQKFULUNUQUMCUKECUK
-      UGJUCUDUHURKUIUJ $.
+      ( vz cv wceq wex wi wral wa isseti vex ac6s6 exdistr raleqf biimpa 2eximi
+      exan mpbir nfcv ax5e mp2b ) KLZEMZADNBOZCUJPZQZFNKNZULCEPZFNZKNUQUOUKUMFN
+      ZQKNUKURKKEGRABCDUJFHKSITUEUKUMKFUAUFUNUPKFUKUMUPULCUJECUJUGJUBUCUDUQKUHU
+      I $.
   $}
 
 $( (End of Giovanni Mascellani's mathbox.) $)
@@ -652118,49 +652145,49 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
     fnchoice $p |- ( A e. Fin -> E. f ( f Fn A /\ A. x e. A ( x =/= (/) ->
                                   ( f ` x ) e. x ) ) ) $=
       ( vw cv wfn c0 wcel wral wa wex wceq anbi12d cvv a1i simplr adantr jca ex
-      syl vy vz vg vu wne cfv wi csn cun fneq2 raleq exbidv fn0 mpbir 0ex fneq1
-      eqid spcev ax-mp ral0 pm3.2i exan cfn wn cop wf dffn2 biimpi ad2antrl vex
-      simpllr fsnunf syl121anc sylibr simprr nfv nfra1 nfan simpr nelne2 necomd
-      fvunsn neeq1 fveq2 eleq1d bitrd imbi12d cbvralv rspcv syl5bir eqeltrd w3a
-      syl3c simp-4l elsni 3ad2ant2 simp1 eqtrd simp3 pm2.21ddne syl3anc wo elun
-      eleq2w sylib mpjaodan ralrimi eximdv snex unex fveq1 imbi2d ralbidv eximi
-      syl21anc syl6 ax5e imp an32s cbvexvw exdistrv simprrl simprrr simplrl cdm
-      neq0 simpl neleqtrrd fsnunfv 3eltr4d 2eximdv exlimiv pm2.61dan findcard2s
-      fndm ) CEZDEZFZAEZGUEZYSYPUFZYSHZUGZAYQIZJZCKYPGFZUUCAGIZJZCKYPUAEZFZUUCA
-      UUIIZJZCKZYPUUIUBEZUHZUIZFZUUCAUUPIZJZCKZYPBFZUUCABIZJZCKDUAUBBYQGLZUUEUU
-      HCUVDYRUUFUUDUUGYQGYPUJUUCAYQGUKMULYQUUILZUUEUULCUVEYRUUJUUDUUKYQUUIYPUJU
-      UCAYQUUIUKMULYQUUPLZUUEUUSCUVFYRUUQUUDUURYQUUPYPUJUUCAYQUUPUKMULYQBLZUUEU
-      VCCUVGYRUVAUUDUVBYQBYPUJUUCAYQBUKMULUUFUUGCUUFCKZUUGGGFZUVHUVIGGLGUQGUMUN
-      UUFUVICGUOGYPGUPURUSUUCAUTVAVBUUIVCHZUUNUUIHVDZJZUUMUUTUVLUUMJZUUNGLZUUTU
-      VMUVNJUCEZUUPFZYTYSUVOUFZYSHZUGZAUUPIZJZUCKZUUTUVLUVNUUMUWBUVLUVNJZUUMUWB
-      UWCUUMUWBCKZUWBUWCUUMYPUUNYQVEZUHZUIZUUPFZYTYSUWGUFZYSHZUGZAUUPIZJZCKUWDU
-      WCUULUWMCUWCUULUWMUWCUULJZUWHUWLUWNUUPNUWGVFZUWHUWNUUINYPVFZUUNNHZUVKYQNH
-      ZUWOUUJUWPUWCUUKUUJUWPUUIYPVGZVHVIUWQUWNUBVJZOUVJUVKUVNUULVKZUWRUWNDVJZOU
-      UINYPNUUNYQVLZVMUUPUWGVGZVNUWNUVNUVKUUKUWLUVLUVNUULPUXAUWCUUJUUKVOUVNUVKJ
-      ZUUKJZUWKAUUPUXEUUKAUXEAVPUUCAUUIVQZVRUXFYSUUPHZUWKUXFUXHJZYTUWJUXIYTJZYS
-      UUIHZUWJYSUUOHZUXJUXKJZUWIUUAYSUXMUUNYSUEZUWIUUALZUXMUXKUVKJZUXNUXMUXKUVK
-      UXJUXKVSZUXJUVKUXKUXIUVKYTUVNUVKUUKUXHVKQQRUXPYSUUNYSUUNUUIVTWAZTYPUUNYQY
-      SWBZTUXMUXKUUKYTUUBUXQUXJUUKUXKUXEUUKUXHYTVKQUXIYTUXKPUUKUDEZGUEZUXTYPUFZ
-      UXTHZUGZUDUUIIUXKUUCUYDUUCUDAUUIUXTYSLZUYAYTUYCUUBUXTYSGWCUYEUYCUUAUXTHUU
-      BUYEUYBUUAUXTUXTYSYPWDWEUDAUUAXDWFWGZWHUYDUUCUDYSUUIUYFWIWJZWMWKUXJUXLJUV
-      NUXLYTUWJUXJUVNUXLUVNUVKUUKUXHYTWNQUXJUXLVSUXIYTUXLPUVNUXLYTWLZUWJYSGUYHY
-      SUUNGUXLUVNYSUUNLZYTYSUUNWOZWPUVNUXLYTWQWRUVNUXLYTWSWTXAUXJUXHUXKUXLXBZUX
-      FUXHYTPYSUUIUUOXCZXEXFSSXGXORSXHUWMUWBCUWAUWMUCUWGYPUWFCVJUWEXIXJUVOUWGLZ
-      UVPUWHUVTUWLUUPUVOUWGUPUYMUVSUWKAUUPUYMUVRUWJYTUYMUVQUWIYSYSUVOUWGXKWEXLX
-      MMURZXNXPUWBCXQZXPXRXSUUSUWACUCYPUVOLZUUQUVPUURUVTUUPYPUVOUPUYPUUCUVSAUUP
-      UYPUUBUVRYTUYPUUAUVQYSYSYPUVOXKWEXLXMMXTZVNUVMUVNVDZJZUVKYQUUNHZDKZUUMJZJ
-      ZUUTUYSUVKVUBUVJUVKUUMUYRVKUYSVUAUUMUYSUYRVUAUVMUYRVSDUUNYFXEUVLUUMUYRPRR
-      VUCUWBUUTVUCUWDDKZUWBUVKVUBVUDVUBUYTUULJZCKDKUVKVUDUYTUULDCYAUVKVUEUWBDCU
-      VKVUEUWBUVKVUEJZUWMUWBVUFUWHUWLVUFUWOUWHVUFUWPUWQUVKUWRUWOVUFUUJUWPUVKUYT
-      UUJUUKYBZUWSXEUWQVUFUWTOUVKVUEYGUWRVUFUXBOUXCVMUXDVNVUFUWKAUUPUVKVUEAUVKA
-      VPUYTUULAUYTAVPUUJUUKAUUJAVPUXGVRVRVRVUFUXHUWKVUFUXHJZYTUWJVUHYTJZUXKUWJU
-      XLVUIUXKJZUWIUUAYSVUJUXPUXOVUJUXKUVKVUIUXKVSZUVKVUEUXHYTUXKWNRUXPUXNUXOUX
-      RUXSTTVUJUXKUUKYTUUBVUKVUIUUKUXKVUHUUKYTVUFUUKUXHUVKUYTUUJUUKYCQQQVUHYTUX
-      KPUYGWMWKVUIUXLJZYQUUNUWIYSVUIUYTUXLVUHUYTYTUVKUYTUULUXHYDQQVULUWIUUNUWGU
-      FZYQVULUYIUWIVUMLVULUXLUYIVUIUXLVSUYJTZYSUUNUWGWDTVULUWQUWRUUNYPYEZHVDVUM
-      YQLUWQVULUWTOUWRVULUXBOVULVUOUUIUUNUVKVUEUXHYTUXLWNVULUUJVUOUUILVUIUUJUXL
-      VUHUUJYTVUFUUJUXHVUGQQQUUIYPYOTYHYPNNUUNYQYIXAWRVUNYJVUIUXHUYKVUFUXHYTPUY
-      LXEXFSSXGRUYNTSYKWJXRUWDUWBDUYOYLTUYQVNTYMSYN $.
+      syl vy vz vg vu wne cfv wi csn cun fneq2 raleq exbidv 0ex fneq1 fn0 mpbir
+      eqid ceqsexv2d ral0 exan cfn wn cop wf biimpi ad2antrl vex simpllr fsnunf
+      dffn2 syl121anc sylibr simprr nfra1 nfan simpr nelne2 necomd fvunsn neeq1
+      nfv fveq2 eleq1d eleq2w bitrd imbi12d cbvralv rspcv syl5bir syl3c eqeltrd
+      simp-4l elsni 3ad2ant2 simp1 eqtrd simp3 pm2.21ddne syl3anc wo elun sylib
+      w3a mpjaodan ralrimi syl21anc eximdv snex unex fveq1 imbi2d ralbidv spcev
+      eximi syl6 ax5e imp an32s cbvexvw exdistrv simprrl simpl simprrr ad5ant12
+      neq0 simplrl fndmd neleqtrrd fsnunfv 3eltr4d 2eximdv pm2.61dan findcard2s
+      cdm exlimiv ) CEZDEZFZAEZGUEZYSYPUFZYSHZUGZAYQIZJZCKYPGFZUUCAGIZJZCKYPUAE
+      ZFZUUCAUUIIZJZCKZYPUUIUBEZUHZUIZFZUUCAUUPIZJZCKZYPBFZUUCABIZJZCKDUAUBBYQG
+      LZUUEUUHCUVDYRUUFUUDUUGYQGYPUJUUCAYQGUKMULYQUUILZUUEUULCUVEYRUUJUUDUUKYQU
+      UIYPUJUUCAYQUUIUKMULYQUUPLZUUEUUSCUVFYRUUQUUDUURYQUUPYPUJUUCAYQUUPUKMULYQ
+      BLZUUEUVCCUVGYRUVAUUDUVBYQBYPUJUUCAYQBUKMULUUFUUGCUUFGGFZCGUMGYPGUNUVHGGL
+      GUQGUOUPURUUCAUSUTUUIVAHZUUNUUIHVBZJZUUMUUTUVKUUMJZUUNGLZUUTUVLUVMJUCEZUU
+      PFZYTYSUVNUFZYSHZUGZAUUPIZJZUCKZUUTUVKUVMUUMUWAUVKUVMJZUUMUWAUWBUUMUWACKZ
+      UWAUWBUUMYPUUNYQVCZUHZUIZUUPFZYTYSUWFUFZYSHZUGZAUUPIZJZCKUWCUWBUULUWLCUWB
+      UULUWLUWBUULJZUWGUWKUWMUUPNUWFVDZUWGUWMUUINYPVDZUUNNHZUVJYQNHZUWNUUJUWOUW
+      BUUKUUJUWOUUIYPVJZVEVFUWPUWMUBVGZOUVIUVJUVMUULVHZUWQUWMDVGZOUUINYPNUUNYQV
+      IZVKUUPUWFVJZVLUWMUVMUVJUUKUWKUVKUVMUULPUWTUWBUUJUUKVMUVMUVJJZUUKJZUWJAUU
+      PUXDUUKAUXDAWAUUCAUUIVNZVOUXEYSUUPHZUWJUXEUXGJZYTUWIUXHYTJZYSUUIHZUWIYSUU
+      OHZUXIUXJJZUWHUUAYSUXLUUNYSUEZUWHUUALZUXLUXJUVJJZUXMUXLUXJUVJUXIUXJVPZUXI
+      UVJUXJUXHUVJYTUVMUVJUUKUXGVHQQRUXOYSUUNYSUUNUUIVQVRZTYPUUNYQYSVSZTUXLUXJU
+      UKYTUUBUXPUXIUUKUXJUXDUUKUXGYTVHQUXHYTUXJPUUKUDEZGUEZUXSYPUFZUXSHZUGZUDUU
+      IIUXJUUCUYCUUCUDAUUIUXSYSLZUXTYTUYBUUBUXSYSGVTUYDUYBUUAUXSHUUBUYDUYAUUAUX
+      SUXSYSYPWBWCUDAUUAWDWEWFZWGUYCUUCUDYSUUIUYEWHWIZWJWKUXIUXKJUVMUXKYTUWIUXI
+      UVMUXKUVMUVJUUKUXGYTWLQUXIUXKVPUXHYTUXKPUVMUXKYTXCZUWIYSGUYGYSUUNGUXKUVMY
+      SUUNLZYTYSUUNWMZWNUVMUXKYTWOWPUVMUXKYTWQWRWSUXIUXGUXJUXKWTZUXEUXGYTPYSUUI
+      UUOXAZXBXDSSXEXFRSXGUWLUWACUVTUWLUCUWFYPUWECVGUWDXHXIUVNUWFLZUVOUWGUVSUWK
+      UUPUVNUWFUNUYLUVRUWJAUUPUYLUVQUWIYTUYLUVPUWHYSYSUVNUWFXJWCXKXLMXMZXNXOUWA
+      CXPZXOXQXRUUSUVTCUCYPUVNLZUUQUVOUURUVSUUPYPUVNUNUYOUUCUVRAUUPUYOUUBUVQYTU
+      YOUUAUVPYSYSYPUVNXJWCXKXLMXSZVLUVLUVMVBZJZUVJYQUUNHZDKZUUMJZJZUUTUYRUVJVU
+      AUVIUVJUUMUYQVHUYRUYTUUMUYRUYQUYTUVLUYQVPDUUNYEXBUVKUUMUYQPRRVUBUWAUUTVUB
+      UWCDKZUWAUVJVUAVUCVUAUYSUULJZCKDKUVJVUCUYSUULDCXTUVJVUDUWADCUVJVUDUWAUVJV
+      UDJZUWLUWAVUEUWGUWKVUEUWNUWGVUEUWOUWPUVJUWQUWNVUEUUJUWOUVJUYSUUJUUKYAZUWR
+      XBUWPVUEUWSOUVJVUDYBUWQVUEUXAOUXBVKUXCVLVUEUWJAUUPUVJVUDAUVJAWAUYSUULAUYS
+      AWAUUJUUKAUUJAWAUXFVOVOVOVUEUXGUWJVUEUXGJZYTUWIVUGYTJZUXJUWIUXKVUHUXJJZUW
+      HUUAYSVUIUXOUXNVUIUXJUVJVUHUXJVPZUVJVUDUXGYTUXJWLRUXOUXMUXNUXQUXRTTVUIUXJ
+      UUKYTUUBVUJUVJVUDUUKUXGYTUXJUVJUYSUUJUUKYCYDVUGYTUXJPUYFWJWKVUHUXKJZYQUUN
+      UWHYSVUHUYSUXKVUGUYSYTUVJUYSUULUXGYFQQVUKUWHUUNUWFUFZYQVUKUYHUWHVULLVUKUX
+      KUYHVUHUXKVPUYITZYSUUNUWFWBTVUKUWPUWQUUNYPYNZHVBVULYQLUWPVUKUWSOUWQVUKUXA
+      OVUKVUNUUIUUNUVJVUDUXGYTUXKWLVUKUUIYPUVJVUDUUJUXGYTUXKVUFYDYGYHYPNNUUNYQY
+      IWSWPVUMYJVUHUXGUYJVUEUXGYTPUYKXBXDSSXERUYMTSYKWIXQUWCUWADUYNYOTUYPVLTYLS
+      YM $.
   $}
 
   ${