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, Th6; :: 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, Th6; :: 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, Th6; :: 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, Th6; :: thesis: verum

end;

end;

end;

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