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

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 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

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 InstructionsF of S -valued 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 A1: 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

A2: IC (Comput (p,s,n)) in dom p and

A3: CurInstr (p,(Comput (p,s,n))) = halt S ;

A8: IC (Comput (p,s,k)) in dom p and

A9: p . (IC (Comput (p,s,k))) = halt S ; :: according to COMPOS_1:def 12 :: thesis: Result (p,s) = Comput (p,s,k)

A10: CurInstr (p,(Comput (p,s,k))) = halt S by A8, A9, PARTFUN1:def 6;

reconsider k = k, n = n as Nat ;

hence Result (p,s) = Comput (p,s,k) by A3, Def9, A1; :: thesis: verum

for p being NAT -defined the InstructionsF of b

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 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

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 InstructionsF of S -valued 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 A1: 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

A2: IC (Comput (p,s,n)) in dom p and

A3: CurInstr (p,(Comput (p,s,n))) = halt S ;

hereby :: thesis: ( p halts_at IC (Comput (p,s,k)) implies Result (p,s) = Comput (p,s,k) )

assume that assume A4:
Result (p,s) = Comput (p,s,k)
; :: thesis: p halts_at IC (Comput (p,s,k))

consider i being Nat such that

A5: Result (p,s) = Comput (p,s,i) and

A6: CurInstr (p,(Result (p,s))) = halt S by A1, Def9;

reconsider i = i, n = n as Nat ;

p . (IC (Comput (p,s,k))) = halt S by A7, A6, A4, A2, A5, PARTFUN1:def 6;

hence p halts_at IC (Comput (p,s,k)) by A7, A2, A5, A4; :: thesis: verum

end;consider i being Nat such that

A5: Result (p,s) = Comput (p,s,i) and

A6: CurInstr (p,(Result (p,s))) = halt S by A1, Def9;

reconsider i = i, n = n as Nat ;

p . (IC (Comput (p,s,k))) = halt S by A7, A6, A4, A2, A5, PARTFUN1:def 6;

hence p halts_at IC (Comput (p,s,k)) by A7, A2, A5, A4; :: thesis: verum

A8: IC (Comput (p,s,k)) in dom p and

A9: p . (IC (Comput (p,s,k))) = halt S ; :: according to COMPOS_1:def 12 :: thesis: Result (p,s) = Comput (p,s,k)

A10: CurInstr (p,(Comput (p,s,k))) = halt S by A8, A9, PARTFUN1:def 6;

reconsider k = k, n = n as Nat ;

hence Result (p,s) = Comput (p,s,k) by A3, Def9, A1; :: thesis: verum