let s be State of SCMPDS ; :: thesis: ( ProgramPart s halts_on s implies for k being Element of NAT st LifeSpan s <= k holds
IC (Comput (ProgramPart s),s,k) = IC (Comput (ProgramPart s),s,(LifeSpan s)) )
defpred S₁[ Element of NAT ] means ( LifeSpan s <= $1 implies IC (Comput (ProgramPart s),s,$1) = IC (Comput (ProgramPart s),s,(LifeSpan s)) );
assume A1: ProgramPart s halts_on s ; :: thesis: for k being Element of NAT st LifeSpan s <= k holds
IC (Comput (ProgramPart s),s,k) = IC (Comput (ProgramPart s),s,(LifeSpan s))

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now

assume A4: LifeSpan s <= k + 1 ; :: thesis: IC (Comput (ProgramPart s),s,(k + 1)) = IC (Comput (ProgramPart s),s,(LifeSpan s))

per cases ( k + 1 = LifeSpan s or k + 1 > LifeSpan s ) by A4, XXREAL_0:1;

suppose k + 1 = LifeSpan s ; :: thesis: IC (Comput (ProgramPart s),s,(k + 1)) = IC (Comput (ProgramPart s),s,(LifeSpan s))

hence IC (Comput (ProgramPart s),s,(k + 1)) = IC (Comput (ProgramPart s),s,(LifeSpan s)) ; :: thesis: verum

end;

suppose A5: k + 1 > LifeSpan s ; :: thesis: IC (Comput (ProgramPart s),s,(k + 1)) = IC (Comput (ProgramPart s),s,(LifeSpan s))

then A6: LifeSpan s <= k by NAT_1:13;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by AMI_1:144;
thus IC (Comput (ProgramPart s),s,(k + 1)) = IC (Following (ProgramPart s),(Comput (ProgramPart s),s,k)) by AMI_1:14
.= IC (Exec (halt SCMPDS ),(Comput (ProgramPart s),s,k)) by A1, A6, Th2, T
.= IC (Comput (ProgramPart s),s,(LifeSpan s)) by A3, A5, AMI_1:def 8, NAT_1:13 ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

let k be Element of NAT ; :: thesis: ( LifeSpan s <= k implies IC (Comput (ProgramPart s),s,k) = IC (Comput (ProgramPart s),s,(LifeSpan s)) )
assume A7: LifeSpan s <= k ; :: thesis: IC (Comput (ProgramPart s),s,k) = IC (Comput (ProgramPart s),s,(LifeSpan s))
A8: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A2);
hence IC (Comput (ProgramPart s),s,k) = IC (Comput (ProgramPart s),s,(LifeSpan s)) by A7; :: thesis: verum