[STATEMENT]
lemma tkt_thread_eq: 
    assumes R: "A.reachable (c,n,ts)"  
    assumes A: "t<N" "has_ticket (ts t) k"
    shows "tkt_thread ts k = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tkt_thread ts k = t
[PROOF STEP]
using has_ticket_unique[OF R]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; has_ticket (ts ?t) ?k; ?t' < N; has_ticket (ts ?t') ?k\<rbrakk> \<Longrightarrow> ?t' = ?t

goal (1 subgoal):
 1. tkt_thread ts k = t
[PROOF STEP]
unfolding tkt_thread_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; has_ticket (ts ?t) ?k; ?t' < N; has_ticket (ts ?t') ?k\<rbrakk> \<Longrightarrow> ?t' = ?t

goal (1 subgoal):
 1. (THE t. t < N \<and> has_ticket (ts t) k) = t
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t < N; has_ticket (ts ?t) ?k; ?t' < N; has_ticket (ts ?t') ?k\<rbrakk> \<Longrightarrow> ?t' = ?t
t < N
has_ticket (ts t) k

goal (1 subgoal):
 1. (THE t. t < N \<and> has_ticket (ts t) k) = t
[PROOF STEP]
by auto