Skip to content

Commit 6504d82

Browse files
wlammenwlammen
authored
prove abbi2i without ax-11 (#3162)
* prove abbi2i without ax-11 * shorten abbi2i * shorten abbid * revert last commit * shorten abbid * prove abbidv without ax-12 * update comment of abbid * prove abbi2dv without ax-11 * shorten abbii * shorten clelsb3f * move common proof steps of abbid, abbidv to a lemma * shorten abbi2i --------- Co-authored-by: Wolf Lammen <[email protected]>
1 parent 5b85162 commit 6504d82

File tree

2 files changed

+158
-69
lines changed

2 files changed

+158
-69
lines changed

‎discouraged‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13392,8 +13392,12 @@ New usage of "7cnOLD" is discouraged (0 uses).
1339213392
New usage of "8cnOLD" is discouraged (0 uses).
1339313393
New usage of "9cnOLD" is discouraged (0 uses).
1339413394
New usage of "a1ii" is discouraged (0 uses).
13395+
New usage of "abbi2dvOLD" is discouraged (0 uses).
13396+
New usage of "abbi2iOLD" is discouraged (0 uses).
1339513397
New usage of "abbidOLD" is discouraged (0 uses).
13398+
New usage of "abbidvOLD" is discouraged (0 uses).
1339613399
New usage of "abbiiOLD" is discouraged (0 uses).
13400+
New usage of "abbiiOLDOLD" is discouraged (0 uses).
1339713401
New usage of "ablo32" is discouraged (4 uses).
1339813402
New usage of "ablo4" is discouraged (3 uses).
1339913403
New usage of "ablocom" is discouraged (6 uses).
@@ -14521,6 +14525,7 @@ New usage of "chub2i" is discouraged (24 uses).
1452114525
New usage of "chunssji" is discouraged (0 uses).
1452214526
New usage of "cleljustALT" is discouraged (0 uses).
1452314527
New usage of "cleljustALT2" is discouraged (0 uses).
14528+
New usage of "clelsb3fOLD" is discouraged (0 uses).
1452414529
New usage of "clmgmOLD" is discouraged (1 uses).
1452514530
New usage of "clwlkclwwlk2OLD" is discouraged (0 uses).
1452614531
New usage of "clwlkclwwlkOLD" is discouraged (2 uses).
@@ -18259,8 +18264,12 @@ Proof modification of "7cnOLD" is discouraged (3 steps).
1825918264
Proof modification of "8cnOLD" is discouraged (3 steps).
1826018265
Proof modification of "9cnOLD" is discouraged (3 steps).
1826118266
Proof modification of "a1ii" is discouraged (1 steps).
18267+
Proof modification of "abbi2dvOLD" is discouraged (24 steps).
18268+
Proof modification of "abbi2iOLD" is discouraged (18 steps).
1826218269
Proof modification of "abbidOLD" is discouraged (24 steps).
18263-
Proof modification of "abbiiOLD" is discouraged (17 steps).
18270+
Proof modification of "abbidvOLD" is discouraged (9 steps).
18271+
Proof modification of "abbiiOLD" is discouraged (38 steps).
18272+
Proof modification of "abbiiOLDOLD" is discouraged (17 steps).
1826418273
Proof modification of "abscncfALT" is discouraged (71 steps).
1826518274
Proof modification of "ackm" is discouraged (71 steps).
1826618275
Proof modification of "ad5ant123OLD" is discouraged (45 steps).
@@ -18637,6 +18646,7 @@ Proof modification of "cesaroOLD" is discouraged (28 steps).
1863718646
Proof modification of "chordthmALT" is discouraged (440 steps).
1863818647
Proof modification of "cleljustALT" is discouraged (25 steps).
1863918648
Proof modification of "cleljustALT2" is discouraged (25 steps).
18649+
Proof modification of "clelsb3fOLD" is discouraged (65 steps).
1864018650
Proof modification of "clmgmOLD" is discouraged (50 steps).
1864118651
Proof modification of "clwlkclwwlk2OLD" is discouraged (302 steps).
1864218652
Proof modification of "clwlkclwwlkOLD" is discouraged (686 steps).

‎set.mm‎

Lines changed: 147 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -16508,6 +16508,17 @@ requires either a disjoint variable condition ( ~ sb5 ) or a non-freeness
1650816508
HZCIZHQBGZQBHZCIZHACDJBCDJRUATUCABQEKSUBCABQELMNACDOBCDOP $.
1650916509
$}
1651016510

16511+
${
16512+
$d x ph $.
16513+
sbimdv.2 $e |- ( ph -> ( ps -> ch ) ) $.
16514+
$( Deduction substituting both sides of an implication, with ` ph ` and
16515+
` x ` disjoint. See also ~ sbimd . (Contributed by Wolf Lammen,
16516+
6-May-2023.) $)
16517+
sbimdv $p |- ( ph -> ( [ y / x ] ps -> [ y / x ] ch ) ) $=
16518+
( weq wi wa wex wsb imim2d anim2d eximdv anim12d df-sb 3imtr4g ) ADEGZBHZ
16519+
RBIZDJZIRCHZRCIZDJZIBDEKCDEKASUBUAUDABCRFLATUCDABCRFMNOBDEPCDEPQ $.
16520+
$}
16521+
1651116522
${
1651216523
sbbii.1 $e |- ( ph <-> ps ) $.
1651316524
$( Infer substitution into both sides of a logical equivalence.
@@ -16516,6 +16527,16 @@ requires either a disjoint variable condition ( ~ sb5 ) or a non-freeness
1651616527
( wsb biimpi sbimi biimpri impbii ) ACDFBCDFABCDABEGHBACDABEIHJ $.
1651716528
$}
1651816529

16530+
${
16531+
$d x ph $.
16532+
sbbidv.1 $e |- ( ph -> ( ps <-> ch ) ) $.
16533+
$( Deduction substituting both sides of a biconditional, with ` ph ` and
16534+
` x ` disjoint. See also ~ sbbid . (Contributed by Wolf Lammen,
16535+
6-May-2023.) $)
16536+
sbbidv $p |- ( ph -> ( [ y / x ] ps <-> [ y / x ] ch ) ) $=
16537+
( wsb biimpd sbimdv biimprd impbid ) ABDEGCDEGABCDEABCFHIACBDEABCFJIK $.
16538+
$}
16539+
1651916540

1652016541
$(
1652116542
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -25701,46 +25722,73 @@ replaced with setvar variables (see ~ cleljust ), so we don't include
2570125722
$}
2570225723

2570325724
${
25704-
$d ph y $. $d ps y $. $d x y $.
25705-
$( Equivalent wff's correspond to equal class abstractions. (Contributed
25706-
by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof
25707-
shortened by Wolf Lammen, 16-Nov-2019.) $)
25708-
abbi $p |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) $=
25709-
( vy cab wceq cv wcel wb wal hbab1 cleqh abid bibi12i albii bitr2i ) ACEZ
25710-
BCEZFCGZQHZSRHZIZCJABIZCJCDQRACDKBCDKLUBUCCTAUABACMBCMNOP $.
25725+
$d x y A $. $d ph x y $. $d ps y $.
25726+
abbi2dv.1 $e |- ( ph -> ( x e. A <-> ps ) ) $.
25727+
$( Deduction from a wff to a class abstraction. (Contributed by NM,
25728+
9-Jul-1994.) Avoid ~ ax-11 . (Revised by Wolf Lammen, 6-May-2023.) $)
25729+
abbi2dv $p |- ( ph -> A = { x | ps } ) $=
25730+
( vy cab cv wcel wsb sbbidv clelsb3v bicomi df-clab 3bitr4g eqrdv ) AFDBC
25731+
GZACHDIZCFJZBCFJFHZDIZTQIARBCFEKSUAFCDLMBFCNOP $.
2571125732
$}
2571225733

2571325734
${
25714-
$d x A $.
25735+
$d x A $. $d ph x $.
25736+
abbi2dvOLD.1 $e |- ( ph -> ( x e. A <-> ps ) ) $.
25737+
$( Obsolete version of ~ abbi2dv as of 6-May-2023. (Contributed by NM,
25738+
9-Jul-1994.) (Proof modification is discouraged.)
25739+
(New usage is discouraged.) $)
25740+
abbi2dvOLD $p |- ( ph -> A = { x | ps } ) $=
25741+
( cv wcel wb wal cab wceq alrimiv abeq2 sylibr ) ACFDGBHZCIDBCJKAOCELBCDM
25742+
N $.
25743+
$}
25744+
25745+
${
25746+
$d x A $. $d ph x $.
25747+
abbi1dv.1 $e |- ( ph -> ( ps <-> x e. A ) ) $.
25748+
$( Deduction from a wff to a class abstraction. (Contributed by NM,
25749+
9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) $)
25750+
abbi1dv $p |- ( ph -> { x | ps } = A ) $=
25751+
( cab cv wcel bicomd abbi2dv eqcomd ) ADBCFABCDABCGDHEIJK $.
25752+
$}
25753+
25754+
${
25755+
$d x y A $. $d y ph $.
2571525756
abbi2i.1 $e |- ( x e. A <-> ph ) $.
2571625757
$( Equality of a class variable and a class abstraction (inference form).
25717-
(Contributed by NM, 26-May-1993.) $)
25758+
(Contributed by NM, 26-May-1993.) Avoid ~ ax-11 . (Revised by Wolf
25759+
Lammen, 6-May-2023.) $)
2571825760
abbi2i $p |- A = { x | ph } $=
25761+
( cab wceq wtru cv wcel wb a1i abbi2dv mptru ) CABEFGABCBHCIAJGDKLM $.
25762+
$}
25763+
25764+
${
25765+
$d x A $.
25766+
abbi2iOLD.1 $e |- ( x e. A <-> ph ) $.
25767+
$( Obsolete version of ~ abbi2i as of 6-May-2023. (Contributed by NM,
25768+
26-May-1993.) (Proof modification is discouraged.)
25769+
(New usage is discouraged.) $)
25770+
abbi2iOLD $p |- A = { x | ph } $=
2571925771
( cab wceq cv wcel wb abeq2 mpgbir ) CABEFBGCHAIBABCJDK $.
2572025772
$}
2572125773

2572225774
${
2572325775
$d ph y $. $d ps y $. $d x y $.
25724-
abbii.1 $e |- ( ph <-> ps ) $.
25725-
$( Equivalent wff's yield equal class abstractions (inference form).
25726-
(Contributed by NM, 26-May-1993.) Remove dependency on ~ ax-10 ,
25727-
~ ax-11 , and ~ ax-12 . (Revised by Steven Nguyen, 3-May-2023.) $)
25728-
abbii $p |- { x | ph } = { x | ps } $=
25729-
( vy cab wsb cv wcel sbbii df-clab 3bitr4i eqriv ) EACFZBCFZACEGBCEGEHZNI
25730-
POIABCEDJAECKBECKLM $.
25731-
25732-
$( Theorem abbii is the congruence law for class abstraction. $)
25733-
$( $j congruence 'abbii'; $)
25776+
$( Equivalent wff's correspond to equal class abstractions. (Contributed
25777+
by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof
25778+
shortened by Wolf Lammen, 16-Nov-2019.) $)
25779+
abbi $p |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) $=
25780+
( vy cab wceq cv wcel wb wal hbab1 cleqh abid bibi12i albii bitr2i ) ACEZ
25781+
BCEZFCGZQHZSRHZIZCJABIZCJCDQRACDKBCDKLUBUCCTAUABACMBCMNOP $.
2573425782
$}
2573525783

2573625784
${
25737-
abbiiOLD.1 $e |- ( ph <-> ps ) $.
25738-
$( Obsolete version of ~ abbii as of 3-May-2023. Equivalent wff's yield
25739-
equal class abstractions (inference form). (Contributed by NM,
25740-
26-May-1993.) (Proof modification is discouraged.)
25741-
(New usage is discouraged.) $)
25742-
abbiiOLD $p |- { x | ph } = { x | ps } $=
25743-
( wb cab wceq abbi mpgbi ) ABEACFBCFGCABCHDI $.
25785+
$d x y $. $d y ph $. $d y ps $. $d y ch $.
25786+
abbilem.1 $e |- ( ph -> ( [ y / x ] ps <-> [ y / x ] ch ) ) $.
25787+
$( Replace substitution expressions with class abstractions. (Contributed
25788+
by Wolf Lammen, 8-May-2023.) $)
25789+
abbilem $p |- ( ph -> { x | ps } = { x | ch } ) $=
25790+
( cab wsb cv wcel df-clab 3bitr4g eqrdv ) AEBDGZCDGZABDEHCDEHEIZNJPOJFBED
25791+
KCEDKLM $.
2574425792
$}
2574525793

2574625794
${
@@ -25753,42 +25801,68 @@ equal class abstractions (inference form). (Contributed by NM,
2575325801
abbidOLD $p |- ( ph -> { x | ps } = { x | ch } ) $=
2575425802
( wb wal cab wceq alrimi abbi sylib ) ABCGZDHBDICDIJANDEFKBCDLM $.
2575525803

25756-
$d ps y $. $d ch y $. $d x y $.
25804+
$d ph y $. $d ps y $. $d ch y $. $d x y $.
2575725805
$( Equivalent wff's yield equal class abstractions (deduction form).
2575825806
(Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro,
25759-
7-Oct-2016.) Avoid ~ ax-11 . (Revised by Wolf Lammen, 4-May-2023.) $)
25807+
7-Oct-2016.) Avoid ~ ax-11 and ~ ax-10 . (Revised by Wolf Lammen,
25808+
6-May-2023.) $)
2576025809
abbid $p |- ( ph -> { x | ps } = { x | ch } ) $=
25761-
( vy wb wal cab wceq alrimi wsb wcel stdpc4v sbbiv sylib df-clab 3bitr4g
25762-
cv eqrdv syl ) ABCHZDIZBDJZCDJZKAUCDEFLUDGUEUFUDBDGMZCDGMZGTZUENUIUFNUDUC
25763-
DGMUGUHHUCDGOBCDGPQBGDRCGDRSUAUB $.
25810+
( vy sbbid abbilem ) ABCDGABCDGEFHI $.
2576425811
$}
2576525812

2576625813
${
25767-
$d x ph $.
25814+
$d x y ph $. $d y ps $. $d y ch $.
2576825815
abbidv.1 $e |- ( ph -> ( ps <-> ch ) ) $.
2576925816
$( Equivalent wff's yield equal class abstractions (deduction form).
25770-
(Contributed by NM, 10-Aug-1993.) $)
25817+
(Contributed by NM, 10-Aug-1993.) Avoid ~ ax-12 , based on an idea of
25818+
Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.) $)
2577125819
abbidv $p |- ( ph -> { x | ps } = { x | ch } ) $=
25820+
( vy sbbidv abbilem ) ABCDFABCDFEGH $.
25821+
$}
25822+
25823+
${
25824+
$d x ph $.
25825+
abbidvOLD.1 $e |- ( ph -> ( ps <-> ch ) ) $.
25826+
$( Obsolete version of ~ abbidv as of 6-May-2023. (Contributed by NM,
25827+
10-Aug-1993.) (Proof modification is discouraged.)
25828+
(New usage is discouraged.) $)
25829+
abbidvOLD $p |- ( ph -> { x | ps } = { x | ch } ) $=
2577225830
( nfv abbid ) ABCDADFEG $.
2577325831
$}
2577425832

2577525833
${
25776-
$d x A $. $d ph x $.
25777-
abbi2dv.1 $e |- ( ph -> ( x e. A <-> ps ) ) $.
25778-
$( Deduction from a wff to a class abstraction. (Contributed by NM,
25779-
9-Jul-1994.) $)
25780-
abbi2dv $p |- ( ph -> A = { x | ps } ) $=
25781-
( cv wcel wb wal cab wceq alrimiv abeq2 sylibr ) ACFDGBHZCIDBCJKAOCELBCDM
25782-
N $.
25834+
$d ph y $. $d ps y $. $d x y $.
25835+
abbii.1 $e |- ( ph <-> ps ) $.
25836+
$( Equivalent wff's yield equal class abstractions (inference form).
25837+
(Contributed by NM, 26-May-1993.) Remove dependency on ~ ax-10 ,
25838+
~ ax-11 , and ~ ax-12 . (Revised by Steven Nguyen, 3-May-2023.) $)
25839+
abbii $p |- { x | ph } = { x | ps } $=
25840+
( cab wceq wtru wb a1i abbidv mptru ) ACEBCEFGABCABHGDIJK $.
25841+
25842+
$( Theorem abbii is the congruence law for class abstraction. $)
25843+
$( $j congruence 'abbii'; $)
2578325844
$}
2578425845

2578525846
${
25786-
$d x A $. $d ph x $.
25787-
abbi1dv.1 $e |- ( ph -> ( ps <-> x e. A ) ) $.
25788-
$( Deduction from a wff to a class abstraction. (Contributed by NM,
25789-
9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) $)
25790-
abbi1dv $p |- ( ph -> { x | ps } = A ) $=
25791-
( cab cv wcel bicomd abbi2dv eqcomd ) ADBCFABCDABCGDHEIJK $.
25847+
$d ph y $. $d ps y $. $d x y $.
25848+
abbiiOLD.1 $e |- ( ph <-> ps ) $.
25849+
$( Obsolete version of ~ abbii as of 7-May-2023. (Contributed by NM,
25850+
26-May-1993.) Remove dependency on ~ ax-10 , ~ ax-11 , and ~ ax-12 .
25851+
(Revised by Steven Nguyen, 3-May-2023.) (New usage is discouraged.)
25852+
(Proof modification is discouraged.) $)
25853+
abbiiOLD $p |- { x | ph } = { x | ps } $=
25854+
( vy cab wsb cv wcel sbbii df-clab 3bitr4i eqriv ) EACFZBCFZACEGBCEGEHZNI
25855+
POIABCEDJAECKBECKLM $.
25856+
$}
25857+
25858+
${
25859+
abbiiOLDOLD.1 $e |- ( ph <-> ps ) $.
25860+
$( Obsolete version of ~ abbii as of 3-May-2023. Equivalent wff's yield
25861+
equal class abstractions (inference form). (Contributed by NM,
25862+
26-May-1993.) (Proof modification is discouraged.)
25863+
(New usage is discouraged.) $)
25864+
abbiiOLDOLD $p |- { x | ph } = { x | ps } $=
25865+
( wb cab wceq abbi mpgbi ) ABEACFBCFGCABCHDI $.
2579225866
$}
2579325867

2579425868
${
@@ -26039,9 +26113,17 @@ choice between (what we call) a "definitional form" where the shorter
2603926113
clelsb3f.1 $e |- F/_ y A $.
2604026114
$( Substitution applied to an atomic wff (class version of ~ elsb3 ).
2604126115
(Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by
26042-
Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux,
26043-
13-Mar-2017.) $)
26116+
Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
26117+
(Proof shortened by Wolf Lammen, 7-May-2023.) $)
2604426118
clelsb3f $p |- ( [ x / y ] y e. A <-> x e. A ) $=
26119+
( vw cv wcel wsb nfcri sbco2 clelsb3 sbbii 3bitr3i ) EFCGZEBHZBAHNEAHBFCG
26120+
ZBAHAFCGNEABBECDIJOPBABECKLAECKM $.
26121+
26122+
$( Obsolete version of ~ clelsb3f as of 7-May-2023. (Contributed by
26123+
Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon,
26124+
14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
26125+
(Proof modification is discouraged.) (New usage is discouraged.) $)
26126+
clelsb3fOLD $p |- ( [ x / y ] y e. A <-> x e. A ) $=
2604526127
( vw cv wcel wsb nfcri sbco2 nfv eleq1w sbie sbbii 3bitr3i ) EFCGZEBHZBAH
2604626128
PEAHBFCGZBAHAFCGZPEABBECDIJQRBAPREBREKEBCLMNPSEASEKEACLMO $.
2604726129
$}
@@ -151083,7 +151165,7 @@ Splicing words (substring replacement)
151083151165
UXJKYCUUMYBUVGUUOWDYBUUNYCUVGUUPWEYDUYSUVGYDUYRUVFUVBYDUUQYEUUSYGJUXGUVAX
151084151166
JVLWTAYKYLUVBXQVRWIXRXSXT $.
151085151167

151086-
$( Reversion is an involution on words. (Contributed by Mario Carneiro,
151168+
$( Reversal is an involution on words. (Contributed by Mario Carneiro,
151087151169
1-Oct-2015.) $)
151088151170
revrev $p |- ( W e. Word A -> ( reverse ` ( reverse ` W ) ) = W ) $=
151089151171
( vx wcel cc0 chash cfv cfzo co creverse wfn revcl wceq revlen syl oveq2d
@@ -152823,10 +152905,9 @@ the symbol at any position is repeated at multiples of L (modulo the
152823152905
$( The domain of a doubleton word is an unordered pair. (Contributed by AV,
152824152906
9-Jan-2020.) $)
152825152907
s2dm $p |- dom <" A B "> = { 0 , 1 } $=
152826-
( cc0 c1 cpr cvv cs2 wf chash cfv cfzo co cword wcel s2cli wrdf ax-mp s2len
152827-
c2 wceq oveq2 fzo0to2pr syl6eq eqcomi feq2i mpbir fdmi ) CDEZFABGZUHFUIHCUI
152828-
IJZKLZFUIHZUIFMNULABOFUIPQUHUKFUIUKUHUJSTZUKUHTABRUMUKCSKLUHUJSCKUAUBUCQUDU
152829-
EUFUG $.
152908+
( cc0 c1 cpr cvv cs2 chash cfv cfzo co wf cword wcel s2cli wrdf ax-mp s2len
152909+
c2 wceq oveq2 fzo0to2pr syl6eq feq2i mpbi fdmi ) CDEZFABGZCUHHIZJKZFUHLZUGF
152910+
UHLUHFMNUKABOFUHPQUJUGFUHUISTZUJUGTABRULUJCSJKUGUISCJUAUBUCQUDUEUF $.
152830152911

152831152912
$( Extract the first symbol from a length 3 string. (Contributed by Mario
152832152913
Carneiro, 13-Jan-2017.) $)
@@ -410161,22 +410242,20 @@ sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1)
410161410242
$d G i w $. $d N w $.
410162410243
$( The number of walks represented by words of fixed length is finite if
410163410244
the number of vertices is finite (in the graph). (Contributed by
410164-
Alexander van der Vekens, 30-Jul-2018.) (Revised by AV,
410165-
19-Apr-2021.) $)
410245+
Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.)
410246+
(Proof shortened by JJ, 18-Nov-2022.) $)
410166410247
wwlksnfi $p |- ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) $=
410167-
( vw vi cvv wcel cn0 wa cfv cfn co wi cv c0 c1 caddc wceq crab cab wn wne
410168-
cvtx cwwlksn cpr cedg cc0 chash cmin cfzo wral cword cwwlks wwlksn df-rab
410169-
syl6eq adantl w3a wb iswwlks a1i anbi1d abbidv 3anan12 anbi1i anass bitri
410170-
eqid abbii eqtr4i eqtrd adantr wss wrdnfi simpr rgenw ss2rab ssfi sylancl
410171-
mpbir eqeltrd ex wnel wo wwlksnndef ioran nnel anbi12i sylbb 0fin pm2.61i
410172-
nsyl4 a1d ) AEFZBGFZHZAUBIZJFZBAUCKZJFZLWOWQWSWOWQHZWRCMZNUAZDMZXAIXCOPKX
410173-
AIUDAUEIZFDUFXAUGIZOUHKUIKUJZHZXEBOPKZQZHZCWPUKZRZJWOWRXLQWQWOWRXAAULIZFZ
410174-
XIHZCSZXLWNWRXPQWMWNWRXICXMRXPCABUMXICXMUNUOUPWOXPXBXAXKFZXFUQZXIHZCSZXLW
410175-
OXOXSCWOXNXRXIXNXRURWODXDAWPXAWPVGXDVGUSUTVAVBXTXQXJHZCSXLXSYACXSXQXGHZXI
410176-
HYAXRYBXIXBXQXFVCVDXQXGXIVEVFVHXJCXKUNVIUOVJVKWTXICXKRZJFZXLYCVLZXLJFWQYD
410177-
WOCXHWPVMUPYEXJXILZCXKUJYFCXKXGXIVNVOXJXICXKVPVSYCXLVQVRVTWAWOTZWSWQYGWRN
410178-
JAEWBZBGWBZWCZWRNQWOABWDYJTYHTZYITZHWOYHYIWEYKWMYLWNAEWFBGWFWGWHWKNJFYGWI
410179-
UTVTWLWJ $.
410248+
( vw vi cn0 wcel cfv cfn co wi cv c0 c1 caddc wral wceq crab cab df-rab
410249+
wa cvtx cwwlksn wne cpr cedg cc0 chash cmin cfzo cword wrdnfi simpr rgenw
410250+
wss ss2rab mpbir a1i ssfid cwwlks wwlksn syl6eq 3anan12 anass bitri abbii
410251+
w3a anbi1i eqid iswwlks 3eqtr4i eleq1d syl5ibr wn cvv wnel df-nel biimpri
410252+
wo olcd wwlksnndef syl 0fin syl6eqel a1d pm2.61i ) BEFZAUAGZHFZBAUBIZHFZJ
410253+
WHWJWFCKZLUCZDKZWKGWMMNIWKGUDAUEGZFDUFWKUGGZMUHIUIIOZTZWOBMNIZPZTZCWGUJZQ
410254+
ZHFWHWSCXAQZXBCWRWGUKXBXCUNZWHXDWTWSJZCXAOXECXAWQWSULUMWTWSCXAUOUPUQURWFW
410255+
IXBHWFWIWKAUSGZFZWSTZCRZXBWFWIWSCXFQXICABUTWSCXFSVAWLWKXAFZWPVFZWSTZCRXJW
410256+
TTZCRXIXBXLXMCXLXJWQTZWSTXMXKXNWSWLXJWPVBVGXJWQWSVCVDVEXHXLCXGXKWSDWNAWGW
410257+
KWGVHWNVHVIVGVEWTCXASVJVAVKVLWFVMZWJWHXOWILHXOAVNVOZBEVOZVRWILPXOXQXPXQXO
410258+
BEVPVQVSABVTWAWBWCWDWE $.
410180410259

410181410260
$( Obsolete version of ~ wwlksnfiOLD as of 4-May-2023. (Contributed by
410182410261
Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.)

0 commit comments

Comments
 (0)