open INV
-- arbitrary objects
  op s : -> Sys .
  op k : -> Pid .
-- assumptions
  eq loc(s,i) = cs .
  eq loc(s,j) = cs .
  eq turn(s) = i .
-- check
  red inv4(s,i,k) and inv4(s,j,k) implies inv1(s,i,j) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
  op k : -> Pid .
-- assumptions
  eq loc(s,i) = cs .
  eq loc(s,j) = cs .
  eq (turn(s) = i) = false .
-- check
  red inv4(s,i,k) implies inv1(s,i,j) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
  op k : -> Pid .
-- assumptions
  eq (loc(s,i) = cs) = false .
-- check
  red inv1(s,i,j) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
  op k : -> Pid .
-- assumptions
  eq (loc(s,j) = cs) = false .
-- check
  red inv1(s,i,j) .
close

-- Q.E.D.