let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated halting AMI-Struct of N
for P being Instruction-Sequence of S
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 IC-Ins-separated halting AMI-Struct of N; :: thesis: for P being Instruction-Sequence of S
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 Instruction-Sequence of S; :: 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)))
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

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 Element of NAT by ORDINAL1:def 12;
A5: Comput (P,s,k) = Comput (P,(Comput (P,s,i)),j) by A4, Th5;
A6: P halts_on Comput (P,s,i) by A3, A5, Def7, A2;
thus Result (P,s) = Comput (P,s,k) by A1, Th8
.= Result (P,(Comput (P,s,i))) by A3, A5, A6, Def8 ; :: 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) by Th3;
A9: Comput (P,s,i) = Comput (P,s,k) by A3, A7, Th6;
A10: P halts_on Comput (P,s,i) by Def7, A2, A9, A3, A8;
thus Result (P,s) = Comput (P,s,k) by A1, Th8
.= Result (P,(Comput (P,s,i))) by A3, A9, A8, A10, Def8 ; :: thesis: verum

end;

end;

end;

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