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 holds
( p halts_on s iff ex i being Nat st p halts_at IC (Comput p,s,i) )
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 holds
( p halts_on s iff ex i being Nat st p halts_at IC (Comput p,s,i) )
let p be NAT -defined the Instructions of S -valued finite Function; :: thesis: for s being State of S holds
( p halts_on s iff ex i being Nat st p halts_at IC (Comput p,s,i) )
let s be State of S; :: thesis: ( p halts_on s iff ex i being Nat st p halts_at IC (Comput p,s,i) )

hereby :: thesis: ( ex i being Nat st p halts_at IC (Comput p,s,i) implies p halts_on s )

assume p halts_on s ; :: thesis: ex i being Nat st p halts_at IC (Comput p,s,i)
then consider i being Nat such that
A0: IC (Comput p,s,i) in dom p and
A1: CurInstr p,(Comput p,s,i) = halt S by Def8;
take i = i; :: thesis: p halts_at IC (Comput p,s,i)
p . (IC (Comput p,s,i)) = halt S by A0, A1, PARTFUN1:def 8;
hence p halts_at IC (Comput p,s,i) by A0, Def15; :: thesis: verum

end;

given i being Nat such that A0: p halts_at IC (Comput p,s,i) ; :: thesis: p halts_on s
A2: IC (Comput p,s,i) in dom p by A0, Def15;
A3: p . (IC (Comput p,s,i)) = halt S by A0, Def15;
take i ; :: according to SCMNORM:def 8 :: thesis: ( IC (Comput p,s,i) in dom p & CurInstr p,(Comput p,s,i) = halt S )
thus IC (Comput p,s,i) in dom p by A0, Def15; :: thesis: CurInstr p,(Comput p,s,i) = halt S
thus CurInstr p,(Comput p,s,i) = p /. (IC (Comput p,s,i))
.= halt S by A2, A3, PARTFUN1:def 8 ; :: thesis: verum