let s be State of SCM+FSA; :: thesis: ( ProgramPart s halts_on s implies for k being Element of NAT st LifeSpan ((ProgramPart s),s) <= k holds
IC (Comput ((ProgramPart s),s,k)) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s)))) )
defpred S₁[ Nat] means ( LifeSpan ((ProgramPart s),s) <= $1 implies IC (Comput ((ProgramPart s),s,$1)) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s)))) );
assume A1: ProgramPart s halts_on s ; :: thesis: for k being Element of NAT st LifeSpan ((ProgramPart s),s) <= k holds
IC (Comput ((ProgramPart s),s,k)) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),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 ((ProgramPart s),s) <= k + 1 ; :: thesis: IC (Comput ((ProgramPart s),s,(k + 1))) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s))))

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

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

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

end;

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

then A6: LifeSpan ((ProgramPart s),s) <= k by NAT_1:13;
thus IC (Comput ((ProgramPart s),s,(k + 1))) = IC (Following ((ProgramPart s),(Comput ((ProgramPart s),s,k)))) by EXTPRO_1:4
.= IC (Exec ((halt SCM+FSA),(Comput ((ProgramPart s),s,k)))) by A1, A6, Th4
.= IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s)))) by A3, A5, EXTPRO_1:def 3, NAT_1:13 ; :: thesis: verum

end;

end;

end;

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

end;

let k be Element of NAT ; :: thesis: ( LifeSpan ((ProgramPart s),s) <= k implies IC (Comput ((ProgramPart s),s,k)) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s)))) )
assume A7: LifeSpan ((ProgramPart s),s) <= k ; :: thesis: IC (Comput ((ProgramPart s),s,k)) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s))))
A8: S₁[ 0 ]

proof

A9: 0 <= LifeSpan ((ProgramPart s),s) by NAT_1:2;
assume LifeSpan ((ProgramPart s),s) <= 0 ; :: thesis: IC (Comput ((ProgramPart s),s,0)) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s))))
hence IC (Comput ((ProgramPart s),s,0)) = IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s)))) by A9; :: thesis: verum

end;

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 ((ProgramPart s),s)))) by A7; :: thesis: verum