--> a line starting with **> indicates a added/changed proof passage
--> a line ending with * indicates a non-effective proof passage
--
--> 1-init
--> 1-want(s,k), c-want(s,k), i = k
--> 1-want(s,k), c-want(s,k), ~(i = k), j = k
--> 1-want(s,k), c-want(s,k), ~(i = k), ~(j = k), istep1
--> 1-want(s,k), ~c-want(s,k)
--> 1-try(s,k), c-try(s,k), i = k, j = k
--> 1-2-try(s,k), c-try(s,k), i = k, ~(j = k), inv2
**> 1-2-try(s,k), c-try(s,k), ~(i = k), j = k *
**> 1-2-try(s,k), c-try(s,k), ~(i = k), ~(j = k)
--> 1-try(s,k), ~c-try(s,k)
--> 1-exit(s,k) *
--> 2-init
--> 2-2-want(s,k) *
--> 2-2-try(s,k) *
--> 2-2-exit(s,k) *
--> Q.E.D

--> 1-init
open INV1
  ops i j : -> Pid .
-- |=  
  red inv1(init,i,j) .
close
--> 1-want(s,k), c-want(s,k), i = k
open INV1
-- arbitrary objects
   op s : -> Sys .
   ops i j k : -> Pid .
-- assumptions
   eq inv1(s,I:Pid,J:Pid) = true .
--
   -- eq c-want(s,k) = true .
   eq pc(s,k) = rm .
--
   eq i = k .
-- |=
-- check if the predicate is true.
   red inv1(want(s,k),i,j) .
close
--> 1-want(s,k), c-want(s,k), ~(i = k), j = k
open INV1
-- arbitrary objects
   op s : -> Sys .
   ops i j k : -> Pid .
-- assumptions
   eq inv1(s,I:Pid,J:Pid) = true .
--
   -- eq c-want(s,k) = true .
   eq pc(s,k) = rm .
-- 
   eq (i = k) = false .
   eq j = k .
-- |=
-- check if the predicate is true.
   red inv1(want(s,k),i,j) .
close
--> 1-want(s,k), c-want(s,k), ~(i = k), ~(j = k), istep1
open ISTEP1
-- arbitrary objects
   ops i j k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
--
   -- eq c-want(s,k) = true .
   eq pc(s,k) = rm .
-- 
   eq (i = k) = false .
   eq (j = k) = false .
** successor state
   eq s' = want(s,k) . 
-- |=
** check if the predicate is true.
   red istep1(i,j) .
close
--> 1-want(s,k), ~c-want(s,k)
open INV1
-- arbitrary objects
   op s : -> Sys .
   ops i j k : -> Pid .
-- assumptions
   eq inv1(s,I:Pid,J:Pid) = true .
--
   eq c-want(s,k) = false .
-- |=
-- check if the predicate is true.
   red inv1(want(s,k),i,j) .
close
--> 1-try(s,k), c-try(s,k), i = k, j = k
open ISTEP1
-- arbitrary objects
   ops i j k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
--
   -- eq c-try(s,k) = true .
   eq pc(s,k) = wt .
   eq top(queue(s)) = k .
--
   eq i = k .
   eq j = k .
-- successor state
   eq s' = try(s,k) . 
-- |=
-- check if the predicate is true.
  red istep1(i,j) .
close
--> 1-2-try(s,k),c-try(s,k), i = k, ~(j = k), inv2
open INV2
-- arbitrary objects
   ops i j k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,J:Pid) = true .
--
   -- eq c-try(s,k) = true .
   eq pc(s,k) = wt .
   eq top(queue(s)) = k .
--
   eq i = k .
   eq (j = k) = false .
-- successor state
   eq s' = try(s,k) . 
-- |=
-- check if the predicate is true.
   red inv2(s,j) implies istep1(i,j) .
close
--> 1-2-try(s,k), c-try(s,k), ~(i = k), j = k
open INV2
-- arbitrary objects
   ops i j k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,J:Pid) = true .
--
   -- eq c-try(s,k) = true .
   eq pc(s,k) = wt .
   eq top(queue(s)) = k .
--
   eq (i = k) = false .
   eq j = k .
-- successor state
   eq s' = try(s,k) . 
-- |=
-- check if the predicate is true.
  red istep1(i,j) .
close
--> 1-2-try(s,k), c-try(s,k), ~(i = k), ~(j = k)
open INV2
-- arbitrary objects
   ops i j k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,J:Pid) = true .
--
   -- eq c-try(s,k) = true .
   eq pc(s,k) = wt .
   eq top(queue(s)) = k .
--
   eq (i = k) = false .
   eq (j = k) = false .
-- successor state
   eq s' = try(s,k) . 
-- |=
-- check if the predicate is true.
  red istep1(i,j) .
close
--> 1-try(s,k), ~c-try(s,k)
open ISTEP1
-- arbitrary objects
   ops i j k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,J:Pid) = true .
--
   eq c-try(s,k) = false .
-- successor state
   eq s' = try(s,k) . 
-- |=
-- check if the predicate is true.
  red istep1(i,j) .
close
--> 1-exit(s,k)
open INV1
-- arbitrary objects
   op s : -> Sys .
   ops i j k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
-- |=
-- check if the predicate is true.
   red inv1(exit(s,k),i,j) .
close
--> 2-init
open INV2
  ops i : -> Pid .
-- |=  
  red inv2(init,i) .
close
--> 2-2-want(s,k)
open ISTEP2
-- arbitrary objects
   ops i k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
-- successor state
   eq s' = want(s,k) .
-- |=
-- check if the predicate is true.
   red istep2(i) .
close
--> 2-2-try(s,k)
open ISTEP2
-- arbitrary objects
   ops i k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
-- successor state
   eq s' = try(s,k) .
-- |=
-- check if the predicate is true.
   red istep2(i) .
close
--> 2-2-exit(s,k)
open ISTEP2
-- arbitrary objects
   ops i k : -> Pid .
-- assumptions
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
-- successor state
   eq s' = exit(s,k) .
-- |=
-- check if the predicate is true.
   red istep2(i) .
close
--> Q.E.D