let s be State of ; :: thesis: for I being parahalting Program of st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan s holds
CurInstr (Computation (s +* (loop I)),k) <> halt SCM+FSA
let I be parahalting Program of ; :: thesis: ( Initialized I c= s implies for k being Element of NAT st k <= LifeSpan s holds
CurInstr (Computation (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 s holds
CurInstr (Computation (s +* (loop I)),k) <> halt SCM+FSA
then A2: I +* (Start-At (insloc 0 )) c= s by SCMFSA6B:8;
A3: ProgramPart s halts_on s by A1, AMI_1:def 26;

hereby :: thesis: verum

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

end;