let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS

for I being halt-free parahalting Program of st I c= P holds

IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I

let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of st I c= P holds

IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I

let I be halt-free parahalting Program of ; :: thesis: ( I c= P implies IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )

set PP = P +* (stop I);

set m = LifeSpan ((P +* (stop I)),s);

A1: stop I c= P +* (stop I) by FUNCT_4:25;

A2: ( (stop I) +* (P +* (stop I)) = P +* (stop I) & (P +* (stop I)) +* (stop I) = P +* (stop I) ) by A1, FUNCT_4:97;

assume I c= P ; :: thesis: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I

hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by Th13

.= card I by Th11, A2, FUNCT_4:25 ;

:: thesis: verum

for I being halt-free parahalting Program of st I c= P holds

IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I

let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of st I c= P holds

IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I

let I be halt-free parahalting Program of ; :: thesis: ( I c= P implies IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )

set PP = P +* (stop I);

set m = LifeSpan ((P +* (stop I)),s);

A1: stop I c= P +* (stop I) by FUNCT_4:25;

A2: ( (stop I) +* (P +* (stop I)) = P +* (stop I) & (P +* (stop I)) +* (stop I) = P +* (stop I) ) by A1, FUNCT_4:97;

assume I c= P ; :: thesis: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I

hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by Th13

.= card I by Th11, A2, FUNCT_4:25 ;

:: thesis: verum