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 NAT -defined the Instructions of b₁ -valued Function
for s being State of S
for k being Nat st p halts_on s holds
( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) )
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued Function
for s being State of S
for k being Nat st p halts_on s holds
( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) )
let p be NAT -defined the Instructions of S -valued Function; :: thesis: for s being State of S
for k being Nat st p halts_on s holds
( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) )
let s be State of S; :: thesis: for k being Nat st p halts_on s holds
( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) )
let k be Nat; :: thesis: ( p halts_on s implies ( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) ) )
assume Z0: p halts_on s ; :: thesis: ( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) )
then consider n being Nat such that
G1: IC (Comput p,s,n) in dom p and
G2: CurInstr p,(Comput p,s,n) = halt S by Def20;

hereby :: thesis: ( p halts_at IC (Comput p,s,k) implies Result p,s = Comput p,s,k )

assume Z: Result p,s = Comput p,s,k ; :: thesis: p halts_at IC (Comput p,s,k)
consider i being Element of NAT such that
W1: Result p,s = Comput p,s,i and
W2: CurInstr p,(Result p,s) = halt S by Z0, Def22;
reconsider i = i, n = n as Element of NAT by ORDINAL1:def 13;

Y: now

per cases ( i <= n or n <= i ) ;

suppose i <= n ; :: thesis: Comput p,s,i = Comput p,s,n

hence Comput p,s,i = Comput p,s,n by W1, W2, Th52; :: thesis: verum

end;

suppose n <= i ; :: thesis: Comput p,s,i = Comput p,s,n

hence Comput p,s,i = Comput p,s,n by G2, Th52; :: thesis: verum

end;

end;

end;

p . (IC (Comput p,s,k)) = halt S by Y, W2, Z, G1, W1, PARTFUN1:def 8;
hence p halts_at IC (Comput p,s,k) by Y, G1, W1, Z, COMPOS_1:def 19; :: thesis: verum

end;

assume that
Z1: IC (Comput p,s,k) in dom p and
Z2: p . (IC (Comput p,s,k)) = halt S ; :: according to COMPOS_1:def 19 :: thesis: Result p,s = Comput p,s,k
X: CurInstr p,(Comput p,s,k) = halt S by Z1, Z2, PARTFUN1:def 8;
reconsider k = k, n = n as Element of NAT by ORDINAL1:def 13;

now

per cases ( n <= k or k <= n ) ;

suppose n <= k ; :: thesis: Comput p,s,k = Comput p,s,n

hence Comput p,s,k = Comput p,s,n by G2, Th52; :: thesis: verum

end;

suppose k <= n ; :: thesis: Comput p,s,k = Comput p,s,n

hence Comput p,s,k = Comput p,s,n by X, Th52; :: thesis: verum

end;

end;

end;

hence Result p,s = Comput p,s,k by G2, Def22, Z0; :: thesis: verum