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 AMI_1:14
.= 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, 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 (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