156 is done (after 31.8 hours), starting 158. 160 is still running.
On Sat, Feb 15, 2020 at 7:18 PM Norman Megill <[email protected]> wrote:
> On Saturday, February 15, 2020 at 9:35:05 PM UTC-5, David A. Wheeler wrote:
> ...
>
>> Jobs 157-159 are unassigned. If they're still unassigned, I could take
>> one
>>
> (presumably 157) once 149 completes (presumably tomorrow AM).
>> Can I snag 157 as well?
>>
>
> OK, I'll assign 157 to you.
>
> Norm
>
> --
> 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/88673fc3-7d62-4ecb-8140-4e413c381476%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/88673fc3-7d62-4ecb-8140-4e413c381476%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAFXXJSvVON-FxEtcr8ND3WvBUqkm-XT_P4ERUQUCPmsqA-7WLA%40mail.gmail.com.
Metamath - Version 0.181 12-Feb-2020 Type HELP for help, EXIT to exit.
MM> read set.mm
Reading source file "set.mm"... 37327684 bytes
37327684 bytes were read into the source buffer.
The source has 174136 statements; 2483 are $a and 34733 are $p.
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
if you want to check them.
MM> submit 'metamathjobs/job156.cmd'
Taking command lines from file "metamathjobs/job156.cmd"...
MM> ! 3atlem4 is used as reference for CPU speed calibration
MM> prove 3atlem4
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT 3atlem4"):
155429 3at.l $e |- .<_ = ( le ` K ) $.
155430 3at.j $e |- .\/ = ( join ` K ) $.
155431 3at.a $e |- A = ( Atoms ` K ) $.
155435 3atlem4 $p |- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e.
A /\ T e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) /\ ( ( P .\/ Q )
.\/ R ) .<_ ( ( S .\/ T ) .\/ R ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/
T ) .\/ R ) ) $= ... $.
Note: The proof you are starting with is already complete.
MM-PA> minimize_with * /allow_new_axioms * /no_new_axioms_from ax-* /time
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
No shorter proof was found.
(Other mathboxes were not checked. Use / INCLUDE_MATHBOXES to include them.)
MINIMIZE_WITH run time = 45.31 sec for "3atlem4"
MM-PA> _exit_pa /force
Exiting the Proof Assistant. Type EXIT again to exit Metamath.
MM> ! start of main run
MM> prove fourierdlem81
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT fourierdlem81"):
$d A i m p $. $d x A i $. $d B i m p $. $d x B $. $d i F x $. $d x G $.
$d x L $. $d i M m p $. $d x M $. $d Q i p $. $d x Q $. $d x R $. $d S
i x $. $d T i x $. $d ph i x $.
137360 fourierdlem81.a $e |- ( ph -> A e. RR ) $.
137361 fourierdlem81.b $e |- ( ph -> B e. RR ) $.
137362 fourierdlem81.p $e |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | (
( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p
` ( i + 1 ) ) ) } ) $.
137363 fourierdlem81.m $e |- ( ph -> M e. NN ) $.
137364 fourierdlem81.t $e |- ( ph -> T e. RR+ ) $.
137365 fourierdlem81.q $e |- ( ph -> Q e. ( P ` M ) ) $.
137366 fourierdlem81.fper $e |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T )
) = ( F ` x ) ) $.
137367 fourierdlem81.s $e |- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) $.
137368 fourierdlem81.f $e |- ( ph -> F : RR --> CC ) $.
137369 fourierdlem81.cncf $e |- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q `
i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) )
-cn-> CC ) ) $.
137370 fourierdlem81.r $e |- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( (
Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) $.
137371 fourierdlem81.l $e |- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( (
Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) $.
137372 fourierdlem81.g $e |- G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |->
if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
$.
137373 fourierdlem81.h $e |- H = ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |->
( G ` ( x - T ) ) ) $.
137374 fourierdlem81 $p |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d
x = S. ( A [,] B ) ( F ` x ) _d x ) $= ... $.
Note: The proof you are starting with is already complete.
MM-PA> minimize_with * /allow_new_axioms * /no_new_axioms_from ax-* /time
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
Proof of "fourierdlem81" decreased from 15096 to 14047 bytes using "dummylink".
Proof of "fourierdlem81" decreased from 14047 to 14032 bytes using "idi".
Proof of "fourierdlem81" decreased from 14032 to 14029 bytes using "mp1i".
Proof of "fourierdlem81" decreased from 14029 to 13997 bytes using "sylib".
Proof of "fourierdlem81" decreased from 13997 to 13970 bytes using "syl5bir".
Proof of "fourierdlem81" decreased from 13970 to 13958 bytes using "syl6bb".
Proof of "fourierdlem81" decreased from 13958 to 13952 bytes using "adantl".
Proof of "fourierdlem81" decreased from 13952 to 13918 bytes using "syldan".
Proof of "fourierdlem81" decreased from 13918 to 13912 bytes using "ad2antrr".
Proof of "fourierdlem81" decreased from 13912 to 13898 bytes using "simpll".
Proof of "fourierdlem81" decreased from 13898 to 13887 bytes using "simplr".
Proof of "fourierdlem81" decreased from 13887 to 13865 bytes using "impbida".
Proof of "fourierdlem81" decreased from 13865 to 13831 bytes using "mpbir3and".
Proof of "fourierdlem81" decreased from 13831 to 13828 bytes using "thema1a".
Proof of "fourierdlem81" decreased from 13828 to 13823 bytes using "alrimiv".
Proof of "fourierdlem81" decreased from 13823 to 13812 bytes using "weq".
Proof of "fourierdlem81" decreased from 13812 to 13797 bytes using "chvarv".
Proof of "fourierdlem81" decreased from 13797 to 13739 bytes using "eqrdv".
Proof of "fourierdlem81" decreased from 13739 to 13719 bytes using "eqtr4i".
Proof of "fourierdlem81" decreased from 13719 to 13674 bytes using "eqtr2d".
Proof of "fourierdlem81" decreased from 13674 to 13653 bytes using "eqtr4d".
Proof of "fourierdlem81" decreased from 13653 to 13649 bytes using "3eqtrd".
Proof of "fourierdlem81" decreased from 13649 to 13647 bytes using "3eqtr3d".
Proof of "fourierdlem81" stayed at 13647 bytes using "3eqtr4d".
(Uncompressed steps decreased from 515842 to 515696).
Proof of "fourierdlem81" decreased from 13647 to 13646 bytes using "3eqtr4rd".
Proof of "fourierdlem81" decreased from 13646 to 13626 bytes using "eqeltrd".
Proof of "fourierdlem81" decreased from 13626 to 13618 bytes using "syl6eleq".
Proof of "fourierdlem81" decreased from 13618 to 13601 bytes using "3eltr3d".
Proof of "fourierdlem81" decreased from 13601 to 13588 bytes using "3eltr4d".
Proof of "fourierdlem81" decreased from 13588 to 13575 bytes using "cbvrexv".
Proof of "fourierdlem81" decreased from 13575 to 13552 bytes using "cbvrabv".
Proof of "fourierdlem81" decreased from 13552 to 13538 bytes using "vtoclg".
Proof of "fourierdlem81" decreased from 13538 to 13529 bytes using "sseli".
Proof of "fourierdlem81" decreased from 13529 to 13519 bytes using "sseldi".
Proof of "fourierdlem81" decreased from 13519 to 13498 bytes using "sselda".
Proof of "fourierdlem81" decreased from 13498 to 13497 bytes using "iftrued".
Proof of "fourierdlem81" decreased from 13497 to 13461 bytes using "iffalsed".
Proof of "fourierdlem81" decreased from 13461 to 13412 bytes using "ifbieq2d".
Proof of "fourierdlem81" decreased from 13412 to 13369 bytes using "3brtr4d".
Proof of "fourierdlem81" decreased from 13369 to 13320 bytes using "cbvmptv".
Proof of "fourierdlem81" decreased from 13320 to 13308 bytes using "feq2d".
Proof of "fourierdlem81" decreased from 13308 to 13300 bytes using "oveq1d".
Proof of "fourierdlem81" decreased from 13300 to 13254 bytes using "recnd".
Proof of "fourierdlem81" decreased from 13254 to 13202 bytes using "leltned".
Proof of "fourierdlem81" decreased from 13202 to 13157 bytes using "ltadd1dd".
Proof of "fourierdlem81" decreased from 13157 to 13122 bytes using "ltsub1dd".
Proof of "fourierdlem81" decreased from 13122 to 13045 bytes using "lesub1dd".
Proof of "fourierdlem81" decreased from 13045 to 13033 bytes using "0zd".
Proof of "fourierdlem81" decreased from 13033 to 13031 bytes using "elioore".
Proof of "fourierdlem81" decreased from 13031 to 13002 bytes using "adant423".
Proof of "fourierdlem81" decreased from 13002 to 12978 bytes using "neqne".
Proof of "fourierdlem81" decreased from 12978 to 12899 bytes using "leneltd".
Proof of "fourierdlem81" decreased from 12899 to 12791 bytes using "eliood".
Proof of "fourierdlem81" decreased from 12791 to 12706 bytes using "eliccd".
Proof of "fourierdlem81" decreased from 12706 to 12647 bytes using "iccssred".
Proof of "fourierdlem81" decreased from 12647 to 12584 bytes using "itgeq1d".
Scanning backward through statements...
Proof of "fourierdlem81" decreased from 15096 to 15034 bytes using "itgeq1d".
Proof of "fourierdlem81" decreased from 15034 to 14966 bytes using "iccssred".
Proof of "fourierdlem81" decreased from 14966 to 14860 bytes using "eliccd".
Proof of "fourierdlem81" decreased from 14860 to 14739 bytes using "eliood".
Proof of "fourierdlem81" decreased from 14739 to 14608 bytes using "leneltd".
Proof of "fourierdlem81" decreased from 14608 to 14590 bytes using "neqne".
Proof of "fourierdlem81" decreased from 14590 to 14561 bytes using "adant423".
Proof of "fourierdlem81" decreased from 14561 to 14559 bytes using "elioore".
Proof of "fourierdlem81" decreased from 14559 to 14547 bytes using "0zd".
Proof of "fourierdlem81" decreased from 14547 to 14470 bytes using "lesub1dd".
Proof of "fourierdlem81" decreased from 14470 to 14435 bytes using "ltsub1dd".
Proof of "fourierdlem81" decreased from 14435 to 14401 bytes using "ltadd1dd".
Proof of "fourierdlem81" decreased from 14401 to 14337 bytes using "recnd".
Proof of "fourierdlem81" decreased from 14337 to 14330 bytes using "oveq1d".
Proof of "fourierdlem81" decreased from 14330 to 14318 bytes using "feq2d".
Proof of "fourierdlem81" decreased from 14318 to 14303 bytes using "resmptd".
Proof of "fourierdlem81" decreased from 14303 to 14262 bytes using "cbvmptv".
Proof of "fourierdlem81" decreased from 14262 to 14208 bytes using "3brtr4d".
Proof of "fourierdlem81" decreased from 14208 to 14160 bytes using "ifbieq2d".
Proof of "fourierdlem81" decreased from 14160 to 14123 bytes using "iffalsed".
Proof of "fourierdlem81" stayed at 14123 bytes using "iftrued".
(Uncompressed steps decreased from 602607 to 602509).
Proof of "fourierdlem81" decreased from 14123 to 14099 bytes using "sselda".
Proof of "fourierdlem81" decreased from 14099 to 14086 bytes using "sseli".
Proof of "fourierdlem81" decreased from 14086 to 14072 bytes using "vtoclg".
Proof of "fourierdlem81" decreased from 14072 to 14040 bytes using "cbvrabv".
Proof of "fourierdlem81" decreased from 14040 to 14027 bytes using "cbvrexv".
Proof of "fourierdlem81" decreased from 14027 to 14022 bytes using "3eltr4d".
Proof of "fourierdlem81" decreased from 14022 to 14011 bytes using "3eltr3d".
Proof of "fourierdlem81" decreased from 14011 to 14003 bytes using "syl6eleq".
Proof of "fourierdlem81" decreased from 14003 to 14001 bytes using "eqeltrd".
Proof of "fourierdlem81" decreased from 14001 to 13989 bytes using "sylan9eq".
Proof of "fourierdlem81" decreased from 13989 to 13986 bytes using "syl6eq".
Proof of "fourierdlem81" decreased from 13986 to 13982 bytes using "syl5eq".
Proof of "fourierdlem81" decreased from 13982 to 13935 bytes using "3eqtr4rd".
Proof of "fourierdlem81" decreased from 13935 to 12914 bytes using "3eqtr3rd".
Proof of "fourierdlem81" decreased from 12914 to 12901 bytes using "3eqtr3d".
Proof of "fourierdlem81" decreased from 12901 to 12888 bytes using "3eqtrd".
Proof of "fourierdlem81" decreased from 12888 to 12865 bytes using "eqtr4d".
Proof of "fourierdlem81" decreased from 12865 to 12824 bytes using "eqtr2d".
Proof of "fourierdlem81" decreased from 12824 to 12803 bytes using "eqtr4i".
Proof of "fourierdlem81" decreased from 12803 to 12745 bytes using "eqrdv".
Proof of "fourierdlem81" decreased from 12745 to 12730 bytes using "chvarv".
Proof of "fourierdlem81" decreased from 12730 to 12719 bytes using "weq".
Proof of "fourierdlem81" decreased from 12719 to 12718 bytes using "thema1a".
Proof of "fourierdlem81" decreased from 12718 to 12695 bytes using "impbida".
Proof of "fourierdlem81" decreased from 12695 to 12684 bytes using "simplr".
Proof of "fourierdlem81" decreased from 12684 to 12677 bytes using "simpll".
Proof of "fourierdlem81" decreased from 12677 to 12667 bytes using "ad2antrr".
Proof of "fourierdlem81" decreased from 12667 to 12665 bytes using "sylanbrc".
Proof of "fourierdlem81" decreased from 12665 to 12652 bytes using "syl2anc".
Proof of "fourierdlem81" decreased from 12652 to 12623 bytes using "sylan2".
Proof of "fourierdlem81" decreased from 12623 to 12616 bytes using "adantl".
Proof of "fourierdlem81" decreased from 12616 to 12604 bytes using "syl6bb".
Proof of "fourierdlem81" decreased from 12604 to 12545 bytes using "syl5bir".
The backward scan results were used.
(Other mathboxes were not checked. Use / INCLUDE_MATHBOXES to include them.)
MINIMIZE_WITH run time = 114243.33 sec for "fourierdlem81"
MM-PA> _exit_pa /force
Warning: You have not saved changes to the proof of "fourierdlem81".
Do you want to EXIT anyway (Y, N) <N>? Y
Exiting the Proof Assistant. Type EXIT again to exit Metamath.
MM> [End of command file "metamathjobs/job156.cmd".]
MM> quit
114514.47user 1.39system 31:49:06elapsed 99%CPU (0avgtext+0avgdata 917612maxresident)k
16inputs+952outputs (0major+249418minor)pagefaults 0swaps
