let s be State of SCMPDS ; :: thesis: for I being halt-free parahalting Program of SCMPDS st Initialize I c= s holds
IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I
let I be halt-free parahalting Program of SCMPDS ; :: thesis: ( Initialize I c= s implies IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I )
set ss = (Initialize s) +* (stop I);
set m = LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I));
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by SCMPDS_4:5;
I2: ((Initialize s) +* (stop I)) +* (Initialize (stop I)) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by SCMPDS_4:5;
A1: Initialize (stop I) c= (Initialize s) +* (stop I) by I1, FUNCT_4:26;
XX: ( (Initialize (stop I)) +* ((Initialize s) +* (stop I)) = (Initialize s) +* (stop I) & (Initialize ((Initialize s) +* (stop I))) +* (stop I) = (Initialize s) +* (stop I) ) by A1, I2, FUNCT_4:79;
assume Initialize I c= s ; :: thesis: IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I
hence IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by Th29, COMPOS_1:24
.= IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop I))),((Initialize ((Initialize s) +* (stop I))) +* (stop I)))) by XX
.= card I by Th27, I1, FUNCT_4:26 ;
:: thesis: verum