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

for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

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

for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

let P be Instruction-Sequence of S; :: thesis: for s being State of S st ex k being Nat st P . (IC (Comput (P,s,k))) = halt S holds

for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

let s be State of S; :: thesis: ( ex k being Nat st P . (IC (Comput (P,s,k))) = halt S implies for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i))) )

given k being Nat such that A1: P . (IC (Comput (P,s,k))) = halt S ; :: thesis: for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

let i be Nat; :: thesis: Result (P,s) = Result (P,(Comput (P,s,i)))

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

set s9 = Comput (P,s,k);

A3: CurInstr (P,(Comput (P,s,k))) = halt S by A1, A2, PARTFUN1:def 6;

for P being Instruction-Sequence of S

for s being State of S st ex k being Nat st P . (IC (Comput (P,s,k))) = halt S holds

for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

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

for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

let P be Instruction-Sequence of S; :: thesis: for s being State of S st ex k being Nat st P . (IC (Comput (P,s,k))) = halt S holds

for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

let s be State of S; :: thesis: ( ex k being Nat st P . (IC (Comput (P,s,k))) = halt S implies for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i))) )

given k being Nat such that A1: P . (IC (Comput (P,s,k))) = halt S ; :: thesis: for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i)))

let i be Nat; :: thesis: Result (P,s) = Result (P,(Comput (P,s,i)))

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

set s9 = Comput (P,s,k);

A3: CurInstr (P,(Comput (P,s,k))) = halt S by A1, A2, PARTFUN1:def 6;

now :: thesis: Result (P,s) = Result (P,(Comput (P,s,i)))end;

hence
Result (P,s) = Result (P,(Comput (P,s,i)))
; :: thesis: verumper cases
( i <= k or i >= k )
;

end;

suppose
i <= k
; :: thesis: Result (P,s) = Result (P,(Comput (P,s,i)))

then consider j being Nat such that

A4: k = i + j by NAT_1:10;

reconsider j = j as Nat ;

A5: Comput (P,s,k) = Comput (P,(Comput (P,s,i)),j) by A4, Th4;

A6: P halts_on Comput (P,s,i) by A3, A5, A2;

thus Result (P,s) = Comput (P,s,k) by A1, Th7

.= Result (P,(Comput (P,s,i))) by A3, A5, A6, Def9 ; :: thesis: verum

end;A4: k = i + j by NAT_1:10;

reconsider j = j as Nat ;

A5: Comput (P,s,k) = Comput (P,(Comput (P,s,i)),j) by A4, Th4;

A6: P halts_on Comput (P,s,i) by A3, A5, A2;

thus Result (P,s) = Comput (P,s,k) by A1, Th7

.= Result (P,(Comput (P,s,i))) by A3, A5, A6, Def9 ; :: thesis: verum

suppose A7:
i >= k
; :: thesis: Result (P,s) = Result (P,(Comput (P,s,i)))

A8:
Comput (P,(Comput (P,s,k)),0) = Comput (P,s,k)
;

A9: Comput (P,s,i) = Comput (P,s,k) by A3, A7, Th5;

A10: P halts_on Comput (P,s,i) by A2, A9, A3, A8;

thus Result (P,s) = Comput (P,s,k) by A1, Th7

.= Result (P,(Comput (P,s,i))) by A3, A9, A8, A10, Def9 ; :: thesis: verum

end;A9: Comput (P,s,i) = Comput (P,s,k) by A3, A7, Th5;

A10: P halts_on Comput (P,s,i) by A2, A9, A3, A8;

thus Result (P,s) = Comput (P,s,k) by A1, Th7

.= Result (P,(Comput (P,s,i))) by A3, A9, A8, A10, Def9 ; :: thesis: verum