Hi Norm, I had a look at many entries of the third block. The remaining
entries should be revied by others. See my remarks/recommendations below.
Alexander
On Friday, February 21, 2020 at 4:28:24 AM UTC+1, Norman Megill wrote:
>
>
> $ grep 'to [1-3]. bytes' job*.log | uniq
> job101.log:Proof of "bj-bi3ant" decreased from 84 to 21 bytes using
> "bi3antOLD".
> job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using
> "eqeq1d".
>
"eqeq1dALT" should be tagged with "(Proof modification is discouraged.)"
job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf".
> job102.log:Proof of "frege53aid" decreased from 58 to 33 bytes using
> "com12".
> job102.log:Proof of "ifeq123d" decreased from 174 to 25 bytes using
> "ifbieq12d".
>
ifeq123d in GS's mathbox: usage should be replaced by ifbieq12d, and
ifeq123d should be
deleted afterwards (see my remark within the comment)
job102.log:Proof of "mplrcl" decreased from 170 to 38 bytes using
> "strov2rcl".
>
used 6 times, shortening OK, both should be kept
job103.log:Proof of "frege24" decreased from 55 to 19 bytes using
> "rp-frege24".
> job103.log:Proof of "hashssle" decreased from 447 to 19 bytes using
> "hashss".
>
hashssle in GS's mathbox: usage (2 times) should be replaced by hashss,
and hashssle should be deleted afterwards
job103.log:Proof of "tsor2" decreased from 55 to 39 bytes using "imori".
>
job104.log:Proof of "aevALT" decreased from 90 to 14 bytes using "aev".
>
"aevALT" should be tagged with "(Proof modification is discouraged.)"
job104.log:Proof of "frege25" decreased from 55 to 20 bytes using
> "rp-frege25".
> job104.log:Proof of "tsor3" decreased from 59 to 39 bytes using "imori".
>
job106.log:Proof of "gsumsndf" decreased from 351 to 29 bytes using
> "gsumsnfd".
>
gsumsndf in AV's mathbox: usage (only once) should be replaced by gsumsnfd,
and gsumsndf should be deleted afterwards
job107.log:Proof of "perpdrag" decreased from 420 to 36 bytes using
> "perpdragALT".
> job108.log:Proof of "leimnltd" decreased from 50 to 19 bytes using
> "lensymd".
>
leimnltd in GS's mathbox: not used, should be deleted
job108.log:Proof of "orcomdd" decreased from 60 to 31 bytes using "syl6".
>
orcomdd in GM's mathbox: usage (2 times) should be replaced by hashss
and hashssle should be deleted afterwards, or both should be kept,
shortening OK
job109.log:Proof of "bj-bisym" decreased from 39 to 18 bytes using
> "bisymOLD".
> job109.log:Proof of "fseq0hash" decreased from 88 to 16 bytes using
> "ffzohash".
>
Identical, one of them can be replaced by the other and removed afterwards
job109.log:Proof of "symgfixfvh" decreased from 116 to 32 bytes using
> "fvtresfn".
>
usage of symgfixfvh should be replaced by fvtresfn and removed afterwards
job110.log:Proof of "bj-hbsb3" decreased from 50 to 15 bytes using "hbsb3".
> job110.log:Proof of "bj-nfs1" decreased from 42 to 14 bytes using "nfs1".
> job110.log:Proof of "frege55aid" decreased from 30 to 14 bytes using
> "bicom1".
> job110.log:Proof of "sbequ8ALT" decreased from 72 to 15 bytes using
> "sbequ8".
>
"sbequ8ALT" should be tagged with "(Proof modification is discouraged.)"
job111.log:Proof of "frege55b" decreased from 138 to 15 bytes using
> "equcomi".
> job112.log:Proof of "equsb3ALT" decreased from 96 to 15 bytes using
> "equsb3".
>
"equsb3ALT" should be tagged with "(Proof modification is discouraged.)"
job112.log:Proof of "rp-simp2" decreased from 33 to 14 bytes using "simp2".
> job113.log:Proof of "rp-simp2-frege" decreased from 39 to 34 bytes using
> "rp-a1i".
> job114.log:Proof of "cleqf" decreased from 59 to 35 bytes using "nfcrii".
> job114.log:Proof of "vdgfrgra0" decreased from 495 to 17 bytes using
> "vdfrgra0".
>
Identical, vdgfrgra0 can be deleted (is not used anyway)
job115.log:Proof of "AnelBC" decreased from 61 to 32 bytes using "nelir".
> job115.log:Proof of "nfnfcALT" decreased from 89 to 15 bytes using "nfnfc".
>
"nfnfcALT" should be tagged with "(Proof modification is discouraged.)"
job116.log:Proof of "rexbidvaALT" decreased from 26 to 20 bytes using
> "rexbidva".
>
"nfnfcALT" should be tagged with "(Proof modification is discouraged.)"
("rexbida" in comment should be replaced by "rexbidva")
job116.log:Proof of "sbceq1ddi2" decreased from 105 to 38 bytes using
> "sbceq1ddi".
>
Identical, sbceq1ddi2 can be deleted (is not used anyway)
job116.log:Proof of "wl-equsal" decreased from 86 to 18 bytes using
> "equsal".
> job117.log:Proof of "adant423" decreased from 56 to 39 bytes using
> "sylancom".
> job117.log:Proof of "frege39" decreased from 56 to 34 bytes using
> "rp-frege2i".
> job117.log:Proof of "rexbidvALT" decreased from 25 to 19 bytes using
> "rexbidv".
>
"rexbidvALT" should be tagged with "(Proof modification is discouraged.)"
job118.log:Proof of "pirp2" decreased from 72 to 30 bytes using "elrpii".
> job119.log:Proof of "rp-frege2ii" decreased from 47 to 37 bytes using
> "rp-frege2i".
> job120.log:Proof of "eleq2dALT" decreased from 165 to 17 bytes using
> "eleq2d".
>
"eleq2dALT" should be tagged with "(Proof modification is discouraged.)"
job120.log:Proof of "frege57aid" decreased from 58 to 11 bytes using "bi2".
> job120.log:Proof of "impel" decreased from 61 to 35 bytes using "syl2anr".
> job120.log:Proof of "rp-frege2iii" decreased from 51 to 32 bytes using
> "rp-frege2ii".
> job122.log:Proof of "cbvald" decreased from 41 to 34 bytes using "nfvd".
>
used 15 times, shortening OK, both should be kept
job123.log:Proof of "ex3" decreased from 53 to 35 bytes using "3impa".
> job124.log:Proof of "3expc" decreased from 26 to 16 bytes using "exp31".
> job124.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using "dral1".
>
"dral1ALT" should be tagged with "(Proof modification is discouraged.)"
job124.log:Proof of "frege58bcor" decreased from 64 to 16 bytes using
> "spsbim".
> job125.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using
> "dveeq2".
>
"dveeq2ALT" should be tagged with "(Proof modification is discouraged.)"
job125.log:Proof of "tgiooss" decreased from 218 to 17 bytes using "rerest".
>
tgiooss in GS's mathbox: usage (3 times) should be replaced by rerest,
and tgiooss should be deleted afterwards
job125.log:Proof of "wl-sb6nae" decreased from 63 to 13 bytes using "sb4b".
> job126.log:Proof of "adantlllr" decreased from 47 to 21 bytes using
> "adantl3r".
> job126.log:Proof of "ax12a2" decreased from 55 to 26 bytes using "ax12v".
> job127.log:Proof of "absnpncand" decreased from 148 to 21 bytes using
> "abs3difd".
>
absnpncand in GS's mathbox: usage (2 times) should be replaced by abs3difd,
and absnpncand should be deleted afterwards
job127.log:Proof of "ad5ant1345" decreased from 54 to 21 bytes using
> "adantl3r".
> job127.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using
> "ax16nf".
> job130.log:Proof of "bf-frege55a" decreased from 73 to 23 bytes using
> "bj-frege55lem2a".
> job130.log:Proof of "bj-csbprc" decreased from 157 to 15 bytes using
> "csbprc".
> job130.log:Proof of "nn0ge2m1nnALT" decreased from 172 to 17 bytes using
> "nn0ge2m1nn".
>
"nn0ge2m1nnALT" should be tagged with "(Proof modification is discouraged.)"
job131.log:Proof of "bf-frege55cor1a" decreased from 74 to 14 bytes using
> "bicom1".
> job131.log:Proof of "ccat2s1fvwALT" decreased from 477 to 21 bytes using
> "ccat2s1fvw".
>
"ccat2s1fvwALT" should be tagged with "(Proof modification is discouraged.)"
job131.log:Proof of "wl-sbal1" decreased from 97 to 15 bytes using "sbal1".
> job132.log:Proof of "4an31" decreased from 67 to 37 bytes using "sylanb".
> job132.log:Proof of "frege52b" decreased from 42 to 16 bytes using
> "sbequi".
> job132.log:Proof of "wl-sbal2" decreased from 97 to 15 bytes using "sbal2".
>
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/282e52ee-bff5-43dd-855e-3e1642725441%40googlegroups.com.
