let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b₁ -valued 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 with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for p being NAT -defined the InstructionsF of S -valued 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 InstructionsF of S -valued 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
A1: IC (Comput (p,s,i)) in dom p and
A2: CurInstr (p,(Comput (p,s,i))) = halt S ;
reconsider i = i as Nat ;
take i = i; :: thesis: p halts_at IC (Comput (p,s,i))
p . (IC (Comput (p,s,i))) = halt S by A1, A2, PARTFUN1:def 6;
hence p halts_at IC (Comput (p,s,i)) by A1; :: thesis: verum

end;

given i being Nat such that A3: p halts_at IC (Comput (p,s,i)) ; :: thesis: p halts_on s
A4: IC (Comput (p,s,i)) in dom p by A3;
A5: p . (IC (Comput (p,s,i))) = halt S by A3;
take i ; :: according to EXTPRO_1: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 A3; :: thesis: CurInstr (p,(Comput (p,s,i))) = halt S
thus CurInstr (p,(Comput (p,s,i))) = halt S by A4, A5, PARTFUN1:def 6; :: thesis: verum