let s be State of SCM+FSA; :: thesis: for I being parahalting Program of SCM+FSA st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) <> halt SCM+FSA
let I be parahalting Program of SCM+FSA; :: thesis: ( Initialized I c= s implies for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) <> halt SCM+FSA )
set s2 = s +* (loop I);
assume A1: Initialized I c= s ; :: thesis: for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) <> halt SCM+FSA
then A2: I +* (Start-At (0,SCM+FSA)) c= s by SCMFSA6B:8;
A3: ProgramPart s halts_on s by A1, EXTPRO_1:def 10;

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((ProgramPart s),s) implies not CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = halt SCM+FSA )
assume A4: k <= LifeSpan ((ProgramPart s),s) ; :: thesis: not CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = halt SCM+FSA
set lk = IC (Comput ((ProgramPart s),s,k));
assume A5: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = halt SCM+FSA ; :: thesis: contradiction
A6: dom I = dom (loop I) by FUNCT_4:105;
A7: IC (Comput ((ProgramPart s),s,k)) in dom I by A2, SCMFSA6B:def 2;
then A8: (loop I) . (IC (Comput ((ProgramPart s),s,k))) in rng (loop I) by A6, FUNCT_1:def 5;
Y: (ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) /. (IC (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k)) . (IC (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) by COMPOS_1:38;
CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k)) . (IC (Comput ((ProgramPart s),s,k))) by A3, A2, A4, Th113, Y, COMPOS_1:24
.= (s +* (loop I)) . (IC (Comput ((ProgramPart s),s,k))) by AMI_1:54
.= (loop I) . (IC (Comput ((ProgramPart s),s,k))) by A7, A6, FUNCT_4:14 ;
hence contradiction by A5, A8, Th107; :: thesis: verum

end;