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

A7: now :: thesis: Comput (p,s,i) = Comput (p,s,n)

per cases ( i <= n or n <= i ) ;

suppose i <= n ; :: thesis: Comput (p,s,i) = Comput (p,s,n)

hence Comput (p,s,i) = Comput (p,s,n) by A5, A6, Th5; :: thesis: verum

end;

suppose n <= i ; :: thesis: Comput (p,s,i) = Comput (p,s,n)

hence Comput (p,s,i) = Comput (p,s,n) by A3, Th5; :: thesis: verum

end;

end;

end;

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;

assume that
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 ;

now :: thesis: Comput (p,s,k) = Comput (p,s,n)

per cases ( n <= k or k <= n ) ;

suppose n <= k ; :: thesis: Comput (p,s,k) = Comput (p,s,n)

hence Comput (p,s,k) = Comput (p,s,n) by A3, Th5; :: thesis: verum

end;

suppose k <= n ; :: thesis: Comput (p,s,k) = Comput (p,s,n)

hence Comput (p,s,k) = Comput (p,s,n) by A10, Th5; :: thesis: verum

end;

end;

end;

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