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 (ProgramPart s),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 (ProgramPart s),s = k + 1 & ProgramPart s halts_on s ) )
TX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by AMI_1:123;
TY: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(k + 1)) by AMI_1:123;

hereby :: thesis: ( LifeSpan (ProgramPart s),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 (ProgramPart s),s = k + 1 & ProgramPart s halts_on s )
Y: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by TX, AMI_1:150;
A3: CurInstr (ProgramPart s),(Comput (ProgramPart s),s,k) <> halt SCM by A1, Y, AMI_1:54;

A4: now

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

end;

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

end;

assume A7: ( LifeSpan (ProgramPart s),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 s),(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 s) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by TX, AMI_1:150;
Y: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,(k + 1))) = (Comput (ProgramPart s),s,(k + 1)) . (IC (Comput (ProgramPart s),s,(k + 1))) by TY, AMI_1:150;
CurInstr (ProgramPart s),(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, Y, Z, AMI_1:54; :: thesis: verum