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