#base: inv3(init,i)

#inductive: istep3(i)

#successor: s'

#action: want(s,k)
#constants: k : -> Pid
#effective: pc(s,k) = l1
#case: i = k 
       (i = k) = 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
            l : -> Pid
	    q : -> Queue
#effective: pc(s,k) = cs
#lemma: inv1(s,i,k) and inv2(s,k) and inv4(s,i)
#case: i = k 
       (i = k) = false
#case: pc(s,i) = l2
       (pc(s,i) = l2) = false
#case: queue(s) = empty
       queue(s) = l q
#case: l = k
       (l = k) = false
#case: empty?(q) = true
       empty?(q) = false
#case: pc(s,i) = cs
       (pc(s,i) = cs) = false