let Gs be ManySortedSet of NAT ; :: thesis: ( Gs is halting & Gs is iterative implies Gs is eventually-constant )

assume that

A1: Gs is halting and

A2: Gs is iterative ; :: thesis: Gs is eventually-constant

set GL = Gs .Lifespan() ;

defpred S_{1}[ Nat] means Gs . (Gs .Lifespan()) = Gs . ((Gs .Lifespan()) + $1);

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A5: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A3);

assume that

A1: Gs is halting and

A2: Gs is iterative ; :: thesis: Gs is eventually-constant

set GL = Gs .Lifespan() ;

defpred S

A3: for k being Nat st S

S

proof

A4:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then Gs . ((Gs .Lifespan()) + 1) = Gs . (((Gs .Lifespan()) + k) + 1) by A2;

hence S_{1}[k + 1]
by A1, GLIB_000:def 56; :: thesis: verum

end;assume S

then Gs . ((Gs .Lifespan()) + 1) = Gs . (((Gs .Lifespan()) + k) + 1) by A2;

hence S

A5: for k being Nat holds S

now :: thesis: for n being Nat st Gs .Lifespan() <= n holds

Gs . (Gs .Lifespan()) = Gs . n

hence
Gs is eventually-constant
; :: thesis: verumGs . (Gs .Lifespan()) = Gs . n

let n be Nat; :: thesis: ( Gs .Lifespan() <= n implies Gs . (Gs .Lifespan()) = Gs . n )

assume Gs .Lifespan() <= n ; :: thesis: Gs . (Gs .Lifespan()) = Gs . n

then ex i being Nat st (Gs .Lifespan()) + i = n by NAT_1:10;

hence Gs . (Gs .Lifespan()) = Gs . n by A5; :: thesis: verum

end;assume Gs .Lifespan() <= n ; :: thesis: Gs . (Gs .Lifespan()) = Gs . n

then ex i being Nat st (Gs .Lifespan()) + i = n by NAT_1:10;

hence Gs . (Gs .Lifespan()) = Gs . n by A5; :: thesis: verum