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
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 ;
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 ; :: thesis: verum
end;
end;
end;
p . (IC (Comput (p,s,k))) = halt S by ;
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 ;
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
hence Result (p,s) = Comput (p,s,k) by A3, Def9, A1; :: thesis: verum