let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b₁ -valued finite 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 halting IC-Ins-separated definite AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued finite 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 finite 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 Def8;

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 Nat such that
W1: Result p,s = Comput p,s,i and
W2: CurInstr p,(Result p,s) = halt S by Z0, Def10;

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 Th7, W1, W2; :: 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 Th7, G2; :: 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 Def15, Y, G1, W1, Z; :: 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 SCMNORM:def 15 :: thesis: Result p,s = Comput p,s,k
X: CurInstr p,(Comput p,s,k) = halt S by Z1, Z2, PARTFUN1:def 8;

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 Th7, G2; :: 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 Th7, X; :: thesis: verum

end;

end;

end;

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