let s be State of ; :: thesis: for I being InitHalting 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 InitHalting 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: ProgramPart s halts_on s by 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 )
set lk = IC (Computation s,k);
A3: ( IC (Computation s,k) in dom I & dom I = dom (loop I) ) by A1, Def1, FUNCT_4:105;
then A4: (loop I) . (IC (Computation s,k)) in rng (loop I) by FUNCT_1:def 5;
assume k <= LifeSpan s ; :: thesis: not CurInstr (Computation (s +* (loop I)),k) = halt SCM+FSA
then IC (Computation s,k) = IC (Computation (s +* (loop I)),k) by A1, A2, Th65, AMI_1:121;
then A5: CurInstr (Computation (s +* (loop I)),k) = (s +* (loop I)) . (IC (Computation s,k)) by AMI_1:54
.= (loop I) . (IC (Computation s,k)) by A3, FUNCT_4:14 ;
assume CurInstr (Computation (s +* (loop I)),k) = halt SCM+FSA ; :: thesis: contradiction
hence contradiction by A5, A4, SCMFSA8C:107; :: thesis: verum

end;