Minimization and Discouraged pass for August-October roll-up.

cgratie · Nov 2, 2020 · 4b249a6 · 4b249a6
1 parent 28696ed
commit 4b249a6
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 23 deletions.
diff --git a/discouraged b/discouraged
@@ -20619,6 +20619,7 @@ Proof modification of "toycom" is discouraged (142 steps).
 Proof modification of "tpid3gVD" is discouraged (116 steps).
 Proof modification of "tratrb" is discouraged (318 steps).
 Proof modification of "tratrbVD" is discouraged (395 steps).
+Proof modification of "trcleq2lemRP" is discouraged (32 steps).
 Proof modification of "trelded" is discouraged (27 steps).
 Proof modification of "trintALT" is discouraged (166 steps).
 Proof modification of "trintALTVD" is discouraged (211 steps).

diff --git a/set.mm b/set.mm
@@ -607173,13 +607173,13 @@ and the class of all sets ( ~ inex1g ) .
     $( If two classes have the finite intersection property, then so does their
        intersection.  (Contributed by Richard Penner, 1-Jan-2020.) $)
     fiinfi $p |- ( ph -> A. x e. C A. y e. C ( x i^i y ) e. C ) $=
-      ( cv cin wcel wral sseli imim1i ralimi2 imim12i syl ralbidv mpbird sylibr
-      wa inss1 inss2 r19.26-2 sylanbrc elin 2ralbii eleq2d raleqdv ) ABJZCJZKZF
-      LZCFMZBFMUOBDEKZMZAUQUNCUPMZBUPMZAUSUMUPLZCUPMZBUPMZAUMDLZUMELZUBZCUPMBUP
-      MZVBAVCCUPMZBUPMZVDCUPMZBUPMZVFAVCCDMZBDMVHGVKVGBDUPUKUPLZUKDLVKVGUPDUKDE
-      UCZNVCVCCDUPULUPLZULDLVCUPDULVMNOPQPRAVDCEMZBEMVJHVOVIBEUPVLUKELVOVIUPEUK
-      DEUDZNVDVDCEUPVNULELVDUPEULVPNOPQPRVCVDBCUPUPUEUFUTVEBCUPUPUMDEUGUHUAAURV
-      ABUPAUNUTCUPAFUPUMIUISSTAUOURBUPAUNCFUPIUJSTAUOBFUPIUJT $.
+      ( cv cin wcel wral elinel1 imim1i ralimi2 imim12i syl ralbidv mpbird elin
+      wa elinel2 r19.26-2 sylanbrc 2ralbii sylibr eleq2d raleqdv ) ABJZCJZKZFLZ
+      CFMZBFMUNBDEKZMZAUPUMCUOMZBUOMZAURULUOLZCUOMZBUOMZAULDLZULELZUBZCUOMBUOMZ
+      VAAVBCUOMZBUOMZVCCUOMZBUOMZVEAVBCDMZBDMVGGVJVFBDUOUJUOLZUJDLVJVFUJDENVBVB
+      CDUOUKUOLZUKDLVBUKDENOPQPRAVCCEMZBEMVIHVMVHBEUOVKUJELVMVHUJDEUCVCVCCEUOVL
+      UKELVCUKDEUCOPQPRVBVCBCUOUOUDUEUSVDBCUOUOULDEUAUFUGAUQUTBUOAUMUSCUOAFUOUL
+      IUHSSTAUNUQBUOAUMCFUOIUISTAUNBFUOIUIT $.
   $}
 
 $(
@@ -607624,21 +607624,21 @@ and the class of all sets ( ~ inex1g ) .
       ( vz cid wss wa wbr wi wal weq wex df-br bicomi 2albii bitri albii 3bitri
       wcel cdm crn cun cres cv resundi sseq1i unss cop wrel wb relres ssrel vex
       ax-mp ideq bitr3i eldm anbi12i opelres 19.42v 3bitr4i 19.23v alcom impexp
-      imbi12i ancomst 19.21v equcom imbi1i nfv breq2 equsal imbi2i elrn 3bitr2i
-      alrot3 19.26-2 pm4.76 ) FCUAZCUBZUCUDZDGFVTUDZFWAUDZUCZDGWCDGZWDDGZHZAUEZ
-      BUEZCIZWIWIDIZWJWJDIZHJZBKAKZWBWEDFVTWAUFUGWCWDDUHWHWKWLJZBKZAKZWKWMJZBKA
-      KZHWPWSHZBKAKWOWFWRWGWTWFWIEUEZUIZWCTZXCDTZJZEKAKZAELZWKHZBMZWIXBDIZJZEKA
-      KZWRWCUJWFXGUKFVTULAEWCDUMUOXFXLAEXDXJXEXKXCFTZWIVTTZHXHWKBMZHXDXJXNXHXOX
-      PXNWIXBFIXHWIXBFNWIXBEUNZUPUQBWICAUNURUSWIXBFVTXQUTXHWKBVAVBXKXEWIXBDNOVF
-      PXMXIXKJZBKZEKZAKWRXLXSAEXSXLXIXKBVCOPXTWQAXTXREKZBKWQXREBVDYAWPBYAWKXHXK
-      JZJZEKWKYBEKZJWPXRYCEXRWKXHHXKJYCXHWKXKVGWKXHXKVEQRWKYBEVHYDWLWKYDEALZXKJ
-      ZEKWLYBYFEXHYEXKAEVIVJRXKWLEAWLEVKXBWIWIDVLVMQVNSRQRQSWGWJXBUIZWDTZYGDTZJ
-      ZEKBKZBELZWKHZAMZWJXBDIZJZEKBKZWTWDUJWGYKUKFWAULBEWDDUMUOYJYPBEYHYNYIYOYG
-      FTZWJWATZHYLWKAMZHYHYNYRYLYSYTYRWJXBFIYLWJXBFNWJXBXQUPUQAWJCBUNVOUSWJXBFW
-      AXQUTYLWKAVAVBYOYIWJXBDNOVFPYQYMYOJZAKZEKBKUUAEKZBKAKWTYPUUBBEUUBYPYMYOAV
-      COPUUAABEVQUUCWSABUUCWKYLYOJZJZEKWKUUDEKZJWSUUAUUEEUUAWKYLHYOJUUEYLWKYOVG
-      WKYLYOVEQRWKUUDEVHUUFWMWKUUFEBLZYOJZEKWMUUDUUHEYLUUGYOBEVIVJRYOWMEBWMEVKX
-      BWJWJDVLVMQVNSPVPSUSWPWSABVRXAWNABWKWLWMVSPVPVP $.
+      imbi12i ancomst 19.21v equcom imbi1i breq2 equsalvw imbi2i alrot3 3bitr2i
+      elrn 19.26-2 pm4.76 ) FCUAZCUBZUCUDZDGFVSUDZFVTUDZUCZDGWBDGZWCDGZHZAUEZBU
+      EZCIZWHWHDIZWIWIDIZHJZBKAKZWAWDDFVSVTUFUGWBWCDUHWGWJWKJZBKZAKZWJWLJZBKAKZ
+      HWOWRHZBKAKWNWEWQWFWSWEWHEUEZUIZWBTZXBDTZJZEKAKZAELZWJHZBMZWHXADIZJZEKAKZ
+      WQWBUJWEXFUKFVSULAEWBDUMUOXEXKAEXCXIXDXJXBFTZWHVSTZHXGWJBMZHXCXIXMXGXNXOX
+      MWHXAFIXGWHXAFNWHXAEUNZUPUQBWHCAUNURUSWHXAFVSXPUTXGWJBVAVBXJXDWHXADNOVFPX
+      LXHXJJZBKZEKZAKWQXKXRAEXRXKXHXJBVCOPXSWPAXSXQEKZBKWPXQEBVDXTWOBXTWJXGXJJZ
+      JZEKWJYAEKZJWOXQYBEXQWJXGHXJJYBXGWJXJVGWJXGXJVEQRWJYAEVHYCWKWJYCEALZXJJZE
+      KWKYAYEEXGYDXJAEVIVJRXJWKEAXAWHWHDVKVLQVMSRQRQSWFWIXAUIZWCTZYFDTZJZEKBKZB
+      ELZWJHZAMZWIXADIZJZEKBKZWSWCUJWFYJUKFVTULBEWCDUMUOYIYOBEYGYMYHYNYFFTZWIVT
+      TZHYKWJAMZHYGYMYQYKYRYSYQWIXAFIYKWIXAFNWIXAXPUPUQAWICBUNVPUSWIXAFVTXPUTYK
+      WJAVAVBYNYHWIXADNOVFPYPYLYNJZAKZEKBKYTEKZBKAKWSYOUUABEUUAYOYLYNAVCOPYTABE
+      VNUUBWRABUUBWJYKYNJZJZEKWJUUCEKZJWRYTUUDEYTWJYKHYNJUUDYKWJYNVGWJYKYNVEQRW
+      JUUCEVHUUEWLWJUUEEBLZYNJZEKWLUUCUUGEYKUUFYNBEVIVJRYNWLEBXAWIWIDVKVLQVMSPV
+      OSUSWOWRABVQWTWMABWJWKWLVRPVOVO $.
   $}
 
   ${
@@ -608141,7 +608141,8 @@ and the class of all sets ( ~ inex1g ) .
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
 $)
 
-  $( Equality implies bijection.  (Contributed by RP, 5-May-2020.) $)
+  $( Equality implies bijection.  (Contributed by RP, 5-May-2020.)
+     (Proof modification is discouraged.) $)
   trcleq2lemRP $p |- ( A = B -> ( ( R C_ A /\ ( A o. A ) C_ A ) <->
                                 ( R C_ B /\ ( B o. B ) C_ B ) ) ) $=
     ( ccom wss wceq id coeq12d sseq12d cleq2lem ) AADZAEBBDZBEABCABFZKLABMABABM