let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b₁ -valued ManySortedSet of NAT
for s being State of S
for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S
for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: for s being State of S
for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let s be State of S; :: thesis: for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let k be Element of NAT ; :: thesis: ( CurInstr (P,(Comput (P,s,k))) = halt S implies Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) )
assume A1: CurInstr (P,(Comput (P,s,k))) = halt S ; :: thesis: Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
X: dom P = NAT by PARTFUN1:def 4;
A2: P halts_on s by Def20, X, A1;
set Ls = LifeSpan (P,s);
A3: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by A2, Def46;
LifeSpan (P,s) <= k by A1, A2, Def46;
hence Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) by A3, Th6; :: thesis: verum