#base: inv2(init,i)

#inductive: istep2(i)

#successor: s'

#action: want(s,k)
#constants: k : -> Pid
#effective: pc(s,k) = l1
#lemma: inv3(s,i)
#case: i = k 
       (i = k) = false
#case: pc(s,i) = cs
       (pc(s,i) = cs) = false
#case: top(queue(s)) = i
       (top(queue(s)) = i) = false
#case: empty?(queue(s)) = true
       empty?(queue(s)) = false       

#action: try(s,k)
#constants: k : -> Pid 
#effective: pc(s,k) = l2 
            top(queue(s)) = k
#case: i = k 
       (i = k) = false

#action: exit(s,k)
#constants: k : -> Pid
#effective: pc(s,k) = cs
#lemma: inv1(s,i,k)
#case: i = k 
       (i = k) = false
#case: pc(s,i) = cs
       (pc(s,i) = cs) = false