:: deftheorem defines .Lifespan() GLIB_000:def 56 :
for F being ManySortedSet of NAT
for b₂ being Element of NAT holds
( ( F is halting implies ( b₂ = F .Lifespan() iff ( F . b₂ = F . (b₂ + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b₂ <= n ) ) ) ) & ( not F is halting implies ( b₂ = F .Lifespan() iff b₂ = 0 ) ) );