let s be State of ; :: thesis: for k being Element of NAT holds
( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM iff ( LifeSpan s = k + 1 & ProgramPart s halts_on s ) )
let k be Element of NAT ; :: thesis: ( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation 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 (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM ) )

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

A4: now

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

end;

( ProgramPart s halts_on s & CurInstr (Computation s,(k + 1)) = halt SCM ) by A2, Th3, AMI_1:54;
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 (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM )

A8: now

assume CurInstr (Computation 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;

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