--> I) Base cases
open INV
  red inv4(init,i) .
close

--> II) Inductive cases
--> 1 want(s,k)
-- 1.1 c-want(s,k) = true
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq i = k  .
  eq pc(s,i) = l2  .
  eq i \in queue(s) = true .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2  .
  eq i \in queue(s) = true .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq i \in queue(s) = true .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq i \in queue(s) = true .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq i = k  .
  eq pc(s,i) = l2  .
  eq i \in queue(s) = false .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2  .
  eq i \in queue(s) = false .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq i \in queue(s) = false .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq i \in queue(s) = false .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close
--
-- 1.2 c-want(s,k) = false
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-want(s,k) = false .
-- successor
  eq s' = want(s,k) .
-- checking
  red istep4(i) .
close

--> 2 try(s,k)
-- 2.1 c-try(s,k) = true
open ISTEP
-- arbitrary objects
  op k : -> Pid  .
-- assumptions
  -- eq c-try(s,k) = true .
  eq pc(s,k) = l2  .
  eq top(queue(s)) = k .
  --
  eq i = k  .
-- successor
  eq s' = try(s,k) .
-- checking
  red istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid  .
-- assumptions
  -- eq c-try(s,k) = true .
  eq pc(s,k) = l2  .
  eq top(queue(s)) = k .
  --
  eq (i = k) = false .
-- successor
  eq s' = try(s,k) .
-- checking
  red istep4(i) .
close
--
-- 2.2 c-try(s,k) = false
open ISTEP
-- arbitrary objects
  op k : -> Pid  .
-- assumptions
  eq c-try(s,k) = false .
-- successor
  eq s' = try(s,k) .
-- checking
  red istep4(i) .
close

--> 3 exit(s,k)
-- 3.1 c-exit(s,k) = true
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = true .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq l = k .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = empty .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq pc(s,i) = l2 .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq i = k  .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (pc(s,i) = l2) = false .
  eq queue(s) = l q .
  eq (l = k) = false .
  eq empty?(q) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red inv2(s,k) implies istep4(i) .
close
--
-- 3.2 c-exit(s,k) = false
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  eq c-exit(s,k) = false .
-- successor
  eq s' = exit(s,k) .
-- checking
  red istep4(i) .
close

--> Q.E.D.