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 st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
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 st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let s be State of S; :: thesis: ( ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S implies for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) )
given k being Element of NAT such that A1: P . (IC (Comput (P,s,k))) = halt S ; :: thesis: for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let i be Element of NAT ; :: thesis: Result (P,s) = Result (P,(Comput (P,s,i)))
XX: dom P = NAT by PARTFUN1:def 4;
set s9 = Comput (P,s,k);
A2: CurInstr (P,(Comput (P,s,k))) = halt S by A1, XX, PARTFUN1:def 8;

now

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
A3: k = i + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A4: Comput (P,s,k) = Comput (P,(Comput (P,s,i)),j) by A3, Th5;
A5: P halts_on Comput (P,s,i) by A2, A4, Def20, XX;
thus Result (P,s) = Comput (P,s,k) by A1, Th56
.= Result (P,(Comput (P,s,i))) by A2, A4, A5, Def22 ; :: thesis: verum

end;

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

A7: Comput (P,(Comput (P,s,k)),0) = Comput (P,s,k) by Th3;
A8: Comput (P,s,i) = Comput (P,s,k) by A2, A6, Th6;
A9: P halts_on Comput (P,s,i) by Def20, XX, A8, A2, A7;
thus Result (P,s) = Comput (P,s,k) by A1, Th56
.= Result (P,(Comput (P,s,i))) by A2, A8, A7, A9, Def22 ; :: thesis: verum

end;

end;

end;

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