:: deftheorem Def15 defines LifeSpan EXTPRO_1:def 15 :
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b₂ -valued Function
for s being State of S st p halts_on s holds
for b₅ being Nat holds
( b₅ = LifeSpan (p,s) iff ( CurInstr (p,(Comput (p,s,b₅))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
b₅ <= k ) ) );