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

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

end;

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

then A6: LifeSpan s <= k by NAT_1:13;
thus IC (Computation s,(k + 1)) = IC (Following (Computation s,k)) by AMI_1:14
.= IC (Exec (halt SCM+FSA ),(Computation s,k)) by A1, A6, Th4
.= IC (Computation 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 (Computation s,k) = IC (Computation s,(LifeSpan s)) )
assume A7: LifeSpan s <= k ; :: thesis: IC (Computation s,k) = IC (Computation s,(LifeSpan s))
A8: S₁[ 0 ]

proof

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A2);
hence IC (Computation s,k) = IC (Computation s,(LifeSpan s)) by A7; :: thesis: verum