Skip to content

Commit d83acc2

Browse files
wlammenwlammen
authored
cbvabv reduce axiom footprint (#3165)
* cbvabv reduce axiom footprint * rewrap * attribute the revision to SN * prove drnfc1 without ax-11 * shorten drnfc2 * no OLD for dfnfc2, minimal change * prove nfabd without ax-ext * shorten nfabd * shorten nfabd again * shorten nfabd2 * prove nfcvf without ax-ext * prove cleqf without ax-13 * update comment of cbvabv --------- Co-authored-by: Wolf Lammen <[email protected]>
1 parent 88835c7 commit d83acc2

File tree

2 files changed

+92
-17
lines changed

2 files changed

+92
-17
lines changed

‎discouraged‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14238,6 +14238,7 @@ New usage of "cases2ALT" is discouraged (0 uses).
1423814238
New usage of "cayleyhamiltonALT" is discouraged (0 uses).
1423914239
New usage of "cba" is discouraged (86 uses).
1424014240
New usage of "cbncms" is discouraged (5 uses).
14241+
New usage of "cbvabvOLD" is discouraged (0 uses).
1424114242
New usage of "cbveuALT" is discouraged (0 uses).
1424214243
New usage of "cbvexsv" is discouraged (2 uses).
1424314244
New usage of "cbvmoOLD" is discouraged (0 uses).
@@ -14526,6 +14527,7 @@ New usage of "chunssji" is discouraged (0 uses).
1452614527
New usage of "cleljustALT" is discouraged (0 uses).
1452714528
New usage of "cleljustALT2" is discouraged (0 uses).
1452814529
New usage of "clelsb3fOLD" is discouraged (0 uses).
14530+
New usage of "cleqfOLD" is discouraged (0 uses).
1452914531
New usage of "clmgmOLD" is discouraged (1 uses).
1453014532
New usage of "clwlkclwwlk2OLD" is discouraged (0 uses).
1453114533
New usage of "clwlkclwwlkOLD" is discouraged (2 uses).
@@ -15073,6 +15075,7 @@ New usage of "dral1-o" is discouraged (4 uses).
1507315075
New usage of "dral1ALT" is discouraged (0 uses).
1507415076
New usage of "dral2-o" is discouraged (4 uses).
1507515077
New usage of "drhmsubcALTV" is discouraged (1 uses).
15078+
New usage of "drnfc1OLD" is discouraged (0 uses).
1507615079
New usage of "drngcatALTV" is discouraged (0 uses).
1507715080
New usage of "drngoi" is discouraged (2 uses).
1507815081
New usage of "dtruALT" is discouraged (0 uses).
@@ -16631,8 +16634,11 @@ New usage of "nexmoOLD" is discouraged (0 uses).
1663116634
New usage of "nf5dvOLD" is discouraged (0 uses).
1663216635
New usage of "nf5riOLD" is discouraged (0 uses).
1663316636
New usage of "nfa1-o" is discouraged (4 uses).
16637+
New usage of "nfabd2OLD" is discouraged (0 uses).
16638+
New usage of "nfabdOLD" is discouraged (0 uses).
1663416639
New usage of "nfan1OLDOLD" is discouraged (0 uses).
1663516640
New usage of "nfbii2OLD" is discouraged (0 uses).
16641+
New usage of "nfcvfOLD" is discouraged (0 uses).
1663616642
New usage of "nfeqf2OLD" is discouraged (0 uses).
1663716643
New usage of "nfeqf2OLDOLD" is discouraged (0 uses).
1663816644
New usage of "nfequid-o" is discouraged (0 uses).
@@ -18633,6 +18639,7 @@ Proof modification of "camestresOLD" is discouraged (23 steps).
1863318639
Proof modification of "camestrosOLD" is discouraged (28 steps).
1863418640
Proof modification of "cases2ALT" is discouraged (88 steps).
1863518641
Proof modification of "cayleyhamiltonALT" is discouraged (657 steps).
18642+
Proof modification of "cbvabvOLD" is discouraged (12 steps).
1863618643
Proof modification of "cbveuALT" is discouraged (48 steps).
1863718644
Proof modification of "cbvexsv" is discouraged (29 steps).
1863818645
Proof modification of "cbvmoOLD" is discouraged (48 steps).
@@ -18648,6 +18655,7 @@ Proof modification of "chordthmALT" is discouraged (440 steps).
1864818655
Proof modification of "cleljustALT" is discouraged (25 steps).
1864918656
Proof modification of "cleljustALT2" is discouraged (25 steps).
1865018657
Proof modification of "clelsb3fOLD" is discouraged (65 steps).
18658+
Proof modification of "cleqfOLD" is discouraged (15 steps).
1865118659
Proof modification of "clmgmOLD" is discouraged (50 steps).
1865218660
Proof modification of "clwlkclwwlk2OLD" is discouraged (302 steps).
1865318661
Proof modification of "clwlkclwwlkOLD" is discouraged (686 steps).
@@ -18771,6 +18779,7 @@ Proof modification of "dlwwlknondlwlknonf1oOLD" is discouraged (353 steps).
1877118779
Proof modification of "dmtrclfvRP" is discouraged (46 steps).
1877218780
Proof modification of "dral1ALT" is discouraged (34 steps).
1877318781
Proof modification of "dral2-o" is discouraged (14 steps).
18782+
Proof modification of "drnfc1OLD" is discouraged (52 steps).
1877418783
Proof modification of "dtruALT" is discouraged (79 steps).
1877518784
Proof modification of "dtruALT2" is discouraged (80 steps).
1877618785
Proof modification of "dummylink" is discouraged (1 steps).
@@ -19441,8 +19450,11 @@ Proof modification of "nexmoOLD" is discouraged (60 steps).
1944119450
Proof modification of "nf5dvOLD" is discouraged (20 steps).
1944219451
Proof modification of "nf5riOLD" is discouraged (13 steps).
1944319452
Proof modification of "nfa1-o" is discouraged (8 steps).
19453+
Proof modification of "nfabd2OLD" is discouraged (75 steps).
19454+
Proof modification of "nfabdOLD" is discouraged (18 steps).
1944419455
Proof modification of "nfan1OLDOLD" is discouraged (33 steps).
1944519456
Proof modification of "nfbii2OLD" is discouraged (15 steps).
19457+
Proof modification of "nfcvfOLD" is discouraged (18 steps).
1944619458
Proof modification of "nfeqf2OLD" is discouraged (65 steps).
1944719459
Proof modification of "nfeqf2OLDOLD" is discouraged (52 steps).
1944819460
Proof modification of "nfequid-o" is discouraged (8 steps).

‎set.mm‎

Lines changed: 80 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -25941,11 +25941,24 @@ choice between (what we call) a "definitional form" where the shorter
2594125941
$}
2594225942

2594325943
${
25944-
$d y ph $. $d x ps $.
25944+
$d y z ph $. $d x z ps $. $d x y $.
2594525945
cbvabv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
2594625946
$( Rule used to change bound variables, using implicit substitution.
25947-
(Contributed by NM, 26-May-1999.) $)
25947+
(Contributed by NM, 26-May-1999.) Require ` x ` , ` y ` be disjoint to
25948+
avoid ~ ax-11 and ~ ax-13 . (Revised by Steven Nguyen, 4-Dec-2022.) $)
2594825949
cbvabv $p |- { x | ph } = { y | ps } $=
25950+
( vz cab wsb cv wcel sbco2vv nfv sbiev sbbii bitr3i df-clab 3bitr4i eqriv
25951+
) FACGZBDGZACFHZBDFHZFIZSJUCTJUAACDHZDFHUBACFDKUDBDFABCDBCLEMNOAFCPBFDPQR
25952+
$.
25953+
$}
25954+
25955+
${
25956+
$d y ph $. $d x ps $.
25957+
cbvabvOLD.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
25958+
$( Obsolete version of ~ cbvabv as of 9-May-2023. (Contributed by NM,
25959+
26-May-1999.) (New usage is discouraged.)
25960+
(Proof modification is discouraged.) $)
25961+
cbvabvOLD $p |- { x | ph } = { y | ps } $=
2594925962
( nfv cbvab ) ABCDADFBCFEG $.
2595025963
$}
2595125964

@@ -26240,37 +26253,67 @@ choice between (what we call) a "definitional form" where the shorter
2624026253
$d w x $. $d w y $. $d w z $. $d w A $. $d w B $.
2624126254
drnfc1.1 $e |- ( A. x x = y -> A = B ) $.
2624226255
$( Formula-building lemma for use with the Distinctor Reduction Theorem.
26243-
(Contributed by Mario Carneiro, 8-Oct-2016.) $)
26256+
(Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ~ ax-11 . (Revised
26257+
by Wolf Lammen, 10-May-2023.) $)
2624426258
drnfc1 $p |- ( A. x x = y -> ( F/_ x A <-> F/_ y B ) ) $=
26259+
( vw weq wal cv wcel wnf wnfc eleq2d drnf1 albidv df-nfc 3bitr4g ) ABGAHZ
26260+
FIZCJZAKZFHSDJZBKZFHACLBDLRUAUCFTUBABRCDSEMNOAFCPBFDPQ $.
26261+
26262+
$( Obsolete version of ~ drnfc1 as of 10-May-2023. (Contributed by Mario
26263+
Carneiro, 8-Oct-2016.) (Proof modification is discouraged.)
26264+
(New usage is discouraged.) $)
26265+
drnfc1OLD $p |- ( A. x x = y -> ( F/_ x A <-> F/_ y B ) ) $=
2624526266
( vw weq wal cv wcel wnf wnfc eleq2d drnf1 dral2 df-nfc 3bitr4g ) ABGAHZF
2624626267
IZCJZAKZFHSDJZBKZFHACLBDLUAUCABFTUBABRCDSEMNOAFCPBFDPQ $.
2624726268

2624826269
$( Formula-building lemma for use with the Distinctor Reduction Theorem.
2624926270
(Contributed by Mario Carneiro, 8-Oct-2016.) $)
2625026271
drnfc2 $p |- ( A. x x = y -> ( F/_ z A <-> F/_ z B ) ) $=
26251-
( vw weq wal cv wcel wnf wnfc eleq2d drnf2 dral2 df-nfc 3bitr4g ) ABHAIZG
26252-
JZDKZCLZGITEKZCLZGICDMCEMUBUDABGUAUCABCSDETFNOPCGDQCGEQR $.
26272+
( vw weq wal cv wcel wnf wnfc eleq2d drnf2 albidv df-nfc 3bitr4g ) ABHAIZ
26273+
GJZDKZCLZGITEKZCLZGICDMCEMSUBUDGUAUCABCSDETFNOPCGDQCGEQR $.
2625326274
$}
2625426275

2625526276
${
2625626277
$d x z $. $d y z $. $d z ph $. $d z ps $.
26278+
nfabd.1 $e |- F/ y ph $.
26279+
nfabd.2 $e |- ( ph -> F/ x ps ) $.
26280+
$( Bound-variable hypothesis builder for a class abstraction. (Contributed
26281+
by Mario Carneiro, 8-Oct-2016.) Avoid ~ ax-9 and ~ ax-ext . (Revised
26282+
by Wolf Lammen, 23-May-2023.) $)
26283+
nfabd $p |- ( ph -> F/_ x { y | ps } ) $=
26284+
( vz cab nfv cv wcel wsb df-clab nfsbd nfxfrd nfcd ) ACGBDHZAGIGJQKBDGLAC
26285+
BGDMABDGCEFNOP $.
26286+
$}
26287+
26288+
${
2625726289
nfabd2.1 $e |- F/ y ph $.
2625826290
nfabd2.2 $e |- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) $.
2625926291
$( Bound-variable hypothesis builder for a class abstraction. (Contributed
26260-
by Mario Carneiro, 8-Oct-2016.) $)
26292+
by Mario Carneiro, 8-Oct-2016.) (Proof shortened by Wolf Lammen,
26293+
10-May-2023.) $)
2626126294
nfabd2 $p |- ( ph -> F/_ x { y | ps } ) $=
26295+
( weq wal cab wnfc wn wa nfnae nfan nfabd ex nfab1 eqidd drnfc1 mpbiri
26296+
pm2.61d2 ) ACDGCHZCBDIZJZAUBKZUDAUELBCDAUEDECDDMNFOPUBUDDUCJBDQCDUCUCUBUC
26297+
RSTUA $.
26298+
26299+
$d x z $. $d y z $. $d z ph $. $d z ps $.
26300+
$( Obsolete version of ~ nfabd2 as of 23-May-2023. (Contributed by Mario
26301+
Carneiro, 8-Oct-2016.) (Proof modification is discouraged.)
26302+
(New usage is discouraged.) $)
26303+
nfabd2OLD $p |- ( ph -> F/_ x { y | ps } ) $=
2626226304
( vz weq wal cab wnfc wn wa nfv cv wcel wsb df-clab nfnae nfan nfsbd nfcd
2626326305
nfxfrd ex nfab1 eqidd drnfc1 mpbiri pm2.61d2 ) ACDHCIZCBDJZKZAUJLZULAUMMZ
2626426306
CGUKUNGNGOUKPBDGQUNCBGDRUNBDGCAUMDECDDSTFUAUCUBUDUJULDUKKBDUECDUKUKUJUKUF
2626526307
UGUHUI $.
2626626308
$}
2626726309

2626826310
${
26269-
nfabd.1 $e |- F/ y ph $.
26270-
nfabd.2 $e |- ( ph -> F/ x ps ) $.
26271-
$( Bound-variable hypothesis builder for a class abstraction. (Contributed
26272-
by Mario Carneiro, 8-Oct-2016.) $)
26273-
nfabd $p |- ( ph -> F/_ x { y | ps } ) $=
26311+
nfabdOLD.1 $e |- F/ y ph $.
26312+
nfabdOLD.2 $e |- ( ph -> F/ x ps ) $.
26313+
$( Obsolete version of ~ nfabd as of 10-May-2023. (Contributed by Mario
26314+
Carneiro, 8-Oct-2016.) (Proof modification is discouraged.)
26315+
(New usage is discouraged.) $)
26316+
nfabdOLD $p |- ( ph -> F/_ x { y | ps } ) $=
2627426317
( wnf weq wal wn adantr nfabd2 ) ABCDEABCGCDHCIJFKL $.
2627526318
$}
2627626319

@@ -26301,27 +26344,47 @@ choice between (what we call) a "definitional form" where the shorter
2630126344
$}
2630226345

2630326346
${
26304-
$d x z $. $d y z $.
26347+
$d x w z $. $d y w z $.
2630526348
$( If ` x ` and ` y ` are distinct, then ` x ` is not free in ` y ` .
26306-
(Contributed by Mario Carneiro, 8-Oct-2016.) $)
26349+
(Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ~ ax-ext . (Revised
26350+
by Wolf Lammen, 10-May-2023.) $)
2630726351
nfcvf $p |- ( -. A. x x = y -> F/_ x y ) $=
26308-
( vz cv nfcv weq id dvelimc ) ABCCDZBDZAIECJECBFGH $.
26352+
( vw vz weq wal wn cv nfv wel elequ2 dvelimnf nfcd ) ABEAFGZACBHNCICDJZCB
26353+
JABDOAIDBCKLM $.
2630926354

2631026355
$( If ` x ` and ` y ` are distinct, then ` y ` is not free in ` x ` .
2631126356
(Contributed by Mario Carneiro, 5-Dec-2016.) $)
2631226357
nfcvf2 $p |- ( -. A. x x = y -> F/_ y x ) $=
2631326358
( cv wnfc nfcvf naecoms ) BACDBABAEF $.
2631426359
$}
2631526360

26361+
${
26362+
$d x z $. $d y z $.
26363+
$( Obsolete version of ~ nfcvf as of 10-May-2023. (Contributed by Mario
26364+
Carneiro, 8-Oct-2016.) (Proof modification is discouraged.)
26365+
(New usage is discouraged.) $)
26366+
nfcvfOLD $p |- ( -. A. x x = y -> F/_ x y ) $=
26367+
( vz cv nfcv weq id dvelimc ) ABCCDZBDZAIECJECBFGH $.
26368+
$}
26369+
2631626370
${
2631726371
$d y A $. $d y B $. $d x y $.
2631826372
cleqf.1 $e |- F/_ x A $.
2631926373
cleqf.2 $e |- F/_ x B $.
2632026374
$( Establish equality between classes, using bound-variable hypotheses
2632126375
instead of distinct variable conditions. See also ~ cleqh .
2632226376
(Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro,
26323-
7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) $)
26377+
7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) Avoid
26378+
~ ax-13 . (Revised by Wolf Lammen, 10-May-2023.) $)
2632426379
cleqf $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
26380+
( vy cv wcel wnfc wnf nfcr ax-mp nf5ri cleqh ) AFBCFGZBHZAABIPAJDAFBKLMOC
26381+
HZAACIQAJEAFCKLMN $.
26382+
26383+
$( Obsolete version of ~ cleqf as of 10-May-2023. (Contributed by NM,
26384+
26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof
26385+
shortened by Wolf Lammen, 17-Nov-2019.) (New usage is discouraged.)
26386+
(Proof modification is discouraged.) $)
26387+
cleqfOLD $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
2632526388
( vy nfcrii cleqh ) AFBCAFBDGAFCEGH $.
2632626389
$}
2632726390

@@ -32701,7 +32764,7 @@ something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy
3270132764
$( Distribute conditional equality over abstraction. (Contributed by
3270232765
Mario Carneiro, 11-Aug-2016.) $)
3270332766
cdeqab1 $p |- CondEq ( x = y -> { x | ph } = { y | ps } ) $=
32704-
( cab wceq wb cdeqri cbvabv cdeqth ) ACFBDFGCDABCDABHCDEIJK $.
32767+
( cab wceq nfv wb cdeqri cbvab cdeqth ) ACFBDFGCDABCDADHBCHABICDEJKL $.
3270532768
$}
3270632769

3270732770
cdeqim.1 $e |- CondEq ( x = y -> ( ch <-> th ) ) $.
@@ -413426,7 +413489,7 @@ symbols representing (not necessarily different) vertices connected by
413426413489
$( If there is only a finite number of vertices, the number of closed walks
413427413490
of fixed length (as words) is also finite. (Contributed by Alexander
413428413491
van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.) (Proof
413429-
shortened by AV, 22-Mar-2022.) $)
413492+
shortened by AV, 22-Mar-2022.) (Proof shortened by JJ, 18-Nov-2022.) $)
413430413493
clwwlknfi $p |- ( ( Vtx ` G ) e. Fin -> ( N ClWWalksN G ) e. Fin ) $=
413431413494
( vw cvtx cfv cfn wcel cclwwlkn co chash wceq cclwwlk crab clwwlkn wrdnfi
413432413495
cv cword wss clwwlksswrd rabss2 mp1i ssfid syl5eqel ) ADEZFGZBAHICPJEBKZC

0 commit comments

Comments
 (0)