--> 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) *
**> 1-want(s,k), ~c-want(s,k) 
--> 1-try(s,k) *
--> 1-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)
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 .
-- |=
-- check if the predicate is true.
   red inv1(want(s,k),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)
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(try(s,k),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
--> Q.E.D