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 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 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 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 AMI_1:150;

now

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

end;

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