#base: inv1(init,i,j)

#inductive: istep1(i,j)

#successor: s'

#action: want(s,k)
#constants: k : -> Pid
#effective: pc(s,k) = l1
#case: i = k 
       (i = k) = false
#case: j = k 
       (j = k) = false

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

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