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_{1} -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)) )

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

for p being NAT -defined the InstructionsF of b

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 )

given i being Nat such that A3:
p halts_at IC (Comput (p,s,i))
; :: thesis: p halts_on sassume
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;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

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