-- I) Base case

open INV
  red inv6(init,i) .
close

-- II) Inductive cases

--> 1) want(s,k)
-- 1.1) c-want(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
--
  eq i = k .
  eq queue(s) = empty .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
--
  eq i = k .
  eq queue(s) = l q .
  eq l = k .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red inv5(s,i) implies istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
--
  eq i = k .
  eq queue(s) = l q .
  eq (l = k) = false .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red istep6(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 queue(s) = empty .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq l = i .
  eq i \in q = true .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq l = i .
  eq i \in q = false .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  op l : -> Pid .
  op q : -> Queue .
-- assumptions
  -- eq c-want(s,k) = true .
  eq pc(s,k) = l1 .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq (l = i) = false .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red inv5(s,i) implies istep6(i) .
close
--
-- 1.2) not c-want(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-want(s,k) = false .
-- successor state
  eq s' = want(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close

--> 2) try(s,k)
-- 2.1) c-try(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-try(s,k) = true .
  eq pc(s,k) = l2 .
  eq top(queue(s)) = k .
-- successor state
  eq s' = try(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close
--
-- 2.2) not c-try(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-try(s,k) = false .
-- successor state
  eq s' = try(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close

--> 3) exit(s,k)
-- 3.1) c-exit(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
--
  eq i = k .
  eq queue(s) = empty .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(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 queue(s) = l q .
  eq l = k .
  eq k \in q = true .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(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 queue(s) = l q .
  eq l = k .
  eq k \in q = false .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(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 queue(s) = l q .
  eq (l = k) = false .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red inv2(s,i) implies istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
--
  eq (i = k) = false .
  eq queue(s) = empty .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(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 queue(s) = l q .
  eq l = k .
  eq q = empty .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  ops l l2 : -> Pid .
  ops q q2 : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq l = k .
  eq q = l2 q2 .
  eq l2 = i .
  eq i \in q2 = true .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red inv7(s,i) implies istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  ops l l2 : -> Pid .
  ops q q2 : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq l = k .
  eq q = l2 q2 .
  eq l2 = i .
  eq i \in q2 = false .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
  ops l l2 : -> Pid .
  ops q q2 : -> Queue .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
--
  eq (i = k) = false .
  eq queue(s) = l q .
  eq l = k .
  eq q = l2 q2 .
  eq (l2 = i) = false .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(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 queue(s) = l q .
  eq (l = k) = false .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red inv2(s,k) implies istep6(i) .
close
--
-- 3.2) not c-exit(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-exit(s,k) = false .
-- successor state
  eq s' = exit(s,k) .
-- check if the predicate is true.
  red istep6(i) .
close

--> Q.E.D