--
-- inv1(s,i,j) can be deduced from inv4(s,i,j).
-- inv2(s,i,j) uses inv3(s,i).
-- inv3(s,i) can be proved independently.
-- inv4(s,i,j) uses inv2(s,i,j) and inv5(s,i).
-- inv5(s,i) can be proved independently.
--

mod INV {
  pr(FISCHER)
-- arbitrary objects
  ops i j : -> Pid 
-- declare operators denoting invariants
  op inv1 : Sys Pid Pid -> Bool
  op inv2 : Sys Pid Pid -> Bool
  op inv3 : Sys Pid -> Bool
  op inv4 : Sys Pid Pid -> Bool
  op inv5 : Sys Pid -> Bool
-- CafeOBJ variables
  var S : Sys
  vars I J : Pid
-- define operators denoting invariants
  eq inv1(S,I,J) = (loc(S,I) = cs and loc(S,J) = cs implies I = J) .
  eq inv2(S,I,J) 
     = (loc(S,I) = d and turn(S) = I and loc(S,J) = c and not(I = J)
        implies
        u(S,J) < l(S,I)) .
  eq inv3(S,I) = (loc(S,I) = c implies u(S,I) < now(S) + d2) .
  eq inv4(S,I,J) 
     = (loc(S,I) = cs or loc(S,I) = e and not(I = J) 
        implies
        turn(S) = I and not(loc(S,J) = c)) .
  eq inv5(S,I) = now(S) <= u(S,I) .
}

mod ISTEP {
  pr(INV)
-- arbitrary objects
  ops s s' : -> Sys
-- declare predicates to prove in each inductive step
  op istep1 : Pid Pid -> Bool
  op istep2 : Pid Pid -> Bool
  op istep3 : Pid -> Bool
  op istep4 : Pid Pid -> Bool
  op istep5 : Pid -> Bool
-- CafeOBJ variables
  vars I J : Pid
-- define predicates to prove in each inductive step
  eq istep1(I,J) = inv1(s,I,J) implies inv1(s',I,J) .
  eq istep2(I,J) = inv2(s,I,J) implies inv2(s',I,J) .
  eq istep3(I) = inv3(s,I) implies inv3(s',I) .
  eq istep4(I,J) = inv4(s,I,J) implies inv4(s',I,J) .
  eq istep5(I) = inv5(s,I) implies inv5(s',I) .
}