-- I) Eventually

open ESTEP
-- assumptions
  eq pc(s,i) = l2 .
  eq i \in queue(s) = true .
  eq where(queue(s),i) = s(n) .
  eq pc(s,top(queue(s))) = l2 .
-- successor state
  eq s' = try(s,top(queue(s))) .
-- check if the predicate holds
  red estep13(i,n) .
close

-- II) Unless

--> 1) want(s,k)
-- 1.1) pc(s,k) = l1
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq pc(s,k) = l1 .
--
  eq i = k .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = empty .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq l = k .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq (where((l q),i) = s(n)) = false .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq where((l q),i) = s(n) .
  eq i \in (l q) = false .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq where((l q),i) = s(n) .
  eq i \in (l q) = true .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
-- 1.2) not(pc(s,k) = l1)
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq not(pc(s,k) = l1) = true .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close

--> 2) try(s,k)
-- 2.1) pc(s,k) = l2 and top(queue(s)) = k 
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq pc(s,k) = l2 .
  eq top(queue(s)) = k .
--
  eq i = k .
  eq k \in queue(s) = false .
-- successor state
  eq s' = try(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq pc(s,k) = l2 .
  eq top(queue(s)) = k .
--
  eq i = k .
  eq k \in queue(s) = true .
-- successor state
  eq s' = try(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq pc(s,k) = l2 .
  eq top(queue(s)) = k .
--
  eq (i = k) = false .
-- successor state
  eq s' = try(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
-- 2.2) not(pc(s,k) = l2 and top(queue(s)) = k)
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq not(pc(s,k) = l2 and top(queue(s)) = k) = true .
-- successor state
  eq s' = try(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close

--> 3) exit(s,k)
-- 3.1) pc(s,k) = cs 
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq pc(s,k) = cs .
--
  eq i = k .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq pc(s,k) = cs .
--
  eq (i = k) = false .
  eq queue(s) = empty .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  eq pc(s,k) = cs .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq l = k .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close
--
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  eq pc(s,k) = cs .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate holds
  red inv2(s,k) implies ustep13(i,n) .
close
--
-- 3.2) not(pc(s,k) = cs)
open USTEP
-- arbitrary chosen objects
  op k : -> Pid .
-- assumptions
  eq not(pc(s,k) = cs) = true .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate holds
  red ustep13(i,n) .
close

-- Q.E.D.