let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of SCMPDS
for k being Element of NAT st I c= s & k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) holds
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCMPDS
let I be halt-free parahalting Program of SCMPDS; :: thesis: for k being Element of NAT st I c= s & k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) holds
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCMPDS
let k be Element of NAT ; :: thesis: ( I c= s & k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) implies CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCMPDS )
set sI = s +* (stop I);
set s1 = Comput ((ProgramPart s),s,k);
set s2 = Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k);
assume that
A1: I c= s and
A2: k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) ; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCMPDS
A3: I c= Comput ((ProgramPart s),s,k) by A1, AMI_1:81;
A4: IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) in dom I by A2, Th28;
TT: ProgramPart (Comput ((ProgramPart s),s,k)) = ProgramPart s by AMI_1:123;
Y: (ProgramPart s) /. (IC (Comput ((ProgramPart s),s,k))) = (Comput ((ProgramPart s),s,k)) . (IC (Comput ((ProgramPart s),s,k))) by TT, COMPOS_1:38;
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = (Comput ((ProgramPart s),s,k)) . (IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k))) by A1, A2, Th29, Y, COMPOS_1:24
.= I . (IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k))) by A3, A4, GRFUNC_1:8 ;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCMPDS by A4, Def3, TT; :: thesis: verum