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