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;

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

per cases ( i <= k or i >= k ) ;

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;

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;

end;

end;

hence Result (P,s) = Result (P,(Comput (P,s,i))) ; :: thesis: verum