let s be State of SCM+FSA ; :: thesis: for I being InitHalting 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 InitHalting 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: ProgramPart s halts_on s by AMI_1:def 26;

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 )
set lk = IC (Comput (ProgramPart s),s,k);
A3: ( IC (Comput (ProgramPart s),s,k) in dom I & dom I = dom (loop I) ) by A1, Def1, FUNCT_4:105;
then A4: (loop I) . (IC (Comput (ProgramPart s),s,k)) in rng (loop I) by 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;
assume 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
then IC (Comput (ProgramPart s),s,k) = IC (Comput (ProgramPart (s +* (loop I))),(s +* (loop I)),k) by A1, A2, Th65, COMPOS_1:24;
then A5: CurInstr (ProgramPart (Comput (ProgramPart (s +* (loop I))),(s +* (loop I)),k)),(Comput (ProgramPart (s +* (loop I))),(s +* (loop I)),k) = (s +* (loop I)) . (IC (Comput (ProgramPart s),s,k)) by Y, AMI_1:54
.= (loop I) . (IC (Comput (ProgramPart s),s,k)) by A3, FUNCT_4:14 ;
assume 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
hence contradiction by A5, A4, SCMFSA8C:107; :: thesis: verum

end;