let s be State of SCM ; :: thesis: for k being Element of NAT holds
( s . (IC (Comput (ProgramPart s),s,k)) <> halt SCM & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM iff ( LifeSpan s = k + 1 & ProgramPart s halts_on s ) )
let k be Element of NAT ; :: thesis: ( s . (IC (Comput (ProgramPart s),s,k)) <> halt SCM & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM iff ( LifeSpan s = k + 1 & ProgramPart s halts_on s ) )

hereby :: thesis: ( LifeSpan s = k + 1 & ProgramPart s halts_on s implies ( s . (IC (Comput (ProgramPart s),s,k)) <> halt SCM & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM ) )

assume that
A1: s . (IC (Comput (ProgramPart s),s,k)) <> halt SCM and
A2: s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM ; :: thesis: ( LifeSpan s = k + 1 & ProgramPart s halts_on s )
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by AMI_1:150;
A3: CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCM by A1, AMI_1:54, Y;

A4: now

let i be Element of NAT ; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i) = halt SCM implies not k + 1 > i )
assume that
A5: CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i) = halt SCM and
A6: k + 1 > i ; :: thesis: contradiction
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,i) by AMI_1:144;
i <= k by A6, NAT_1:13;
then Comput (ProgramPart s),s,k = Comput (ProgramPart s),s,i by AMI_1:52, A5, T;
hence contradiction by A3, A5; :: thesis: verum

end;

Y: (ProgramPart (Comput (ProgramPart s),s,(k + 1))) /. (IC (Comput (ProgramPart s),s,(k + 1))) = (Comput (ProgramPart s),s,(k + 1)) . (IC (Comput (ProgramPart s),s,(k + 1))) by AMI_1:150;
( ProgramPart s halts_on s & CurInstr (ProgramPart (Comput (ProgramPart s),s,(k + 1))),(Comput (ProgramPart s),s,(k + 1)) = halt SCM ) by A2, Th3, AMI_1:54, Y;
hence ( LifeSpan s = k + 1 & ProgramPart s halts_on s ) by A4, AMI_1:def 46; :: thesis: verum

end;

assume A7: ( LifeSpan s = k + 1 & ProgramPart s halts_on s ) ; :: thesis: ( s . (IC (Comput (ProgramPart s),s,k)) <> halt SCM & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM )

A8: now

assume CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM ; :: thesis: contradiction
then k + 1 <= k by A7, AMI_1:def 46;
hence contradiction by NAT_1:13; :: thesis: verum

end;

Z: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by AMI_1:150;
Y: (ProgramPart (Comput (ProgramPart s),s,(k + 1))) /. (IC (Comput (ProgramPart s),s,(k + 1))) = (Comput (ProgramPart s),s,(k + 1)) . (IC (Comput (ProgramPart s),s,(k + 1))) by AMI_1:150;
CurInstr (ProgramPart (Comput (ProgramPart s),s,(k + 1))),(Comput (ProgramPart s),s,(k + 1)) = halt SCM by A7, AMI_1:def 46;
hence ( s . (IC (Comput (ProgramPart s),s,k)) <> halt SCM & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM ) by A8, AMI_1:54, Y, Z; :: thesis: verum