let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N

for P being Instruction-Sequence of S

for s being State of S

for k being 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 with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for P being Instruction-Sequence of S

for s being State of S

for k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S holds

Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)

let P be Instruction-Sequence of S; :: thesis: for s being State of S

for k being 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 Nat st CurInstr (P,(Comput (P,s,k))) = halt S holds

Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)

let k be 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)

A2: dom P = NAT by PARTFUN1:def 2;

A3: P halts_on s by A2, A1;

set Ls = LifeSpan (P,s);

A4: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by A3, Def15;

LifeSpan (P,s) <= k by A1, A3, Def15;

hence Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) by A4, Th5; :: thesis: verum

for P being Instruction-Sequence of S

for s being State of S

for k being 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 with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for P being Instruction-Sequence of S

for s being State of S

for k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S holds

Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)

let P be Instruction-Sequence of S; :: thesis: for s being State of S

for k being 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 Nat st CurInstr (P,(Comput (P,s,k))) = halt S holds

Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)

let k be 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)

A2: dom P = NAT by PARTFUN1:def 2;

A3: P halts_on s by A2, A1;

set Ls = LifeSpan (P,s);

A4: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by A3, Def15;

LifeSpan (P,s) <= k by A1, A3, Def15;

hence Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) by A4, Th5; :: thesis: verum