let s be State of SCM ; :: thesis: for k being Element of NAT st IC (Comput (ProgramPart s),s,k) <> IC (Comput (ProgramPart s),s,(k + 1)) & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM holds
LifeSpan (ProgramPart s),s = k + 1
let k be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart s),s,k) <> IC (Comput (ProgramPart s),s,(k + 1)) & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM implies LifeSpan (ProgramPart s),s = k + 1 )
assume that
A1: IC (Comput (ProgramPart s),s,k) <> IC (Comput (ProgramPart s),s,(k + 1)) and
A2: s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM ; :: thesis: LifeSpan (ProgramPart s),s = k + 1
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 COMPOS_1:38;

now

T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by AMI_1:123;
assume s . (IC (Comput (ProgramPart s),s,k)) = halt SCM ; :: thesis: contradiction
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,k) = halt SCM by Y, T, AMI_1:54;
hence contradiction by A1, AMI_1:52, NAT_1:11; :: thesis: verum

end;

hence LifeSpan (ProgramPart s),s = k + 1 by A2, Th16; :: thesis: verum