--
-- inv1 can be deduced from inv10.
-- inv2 uses inv3.
-- inv3 can be proved independently.
-- inv4 uses inv5.
-- inv5 can be proved independently.
-- inv6 uses inv4, inv5, inv7.
-- inv7 can be proved independently.
-- inv8 uses inv2.
-- inv9 can be deduced from inv4, inv5, inv6, inv7, inv8.
-- inv10 uses inv9.

mod INV {
  pr(CROSSING)
-- arbitrary objects
-- declare operators denoting invariants to prove
  op inv0 : Sys -> Bool
  op inv1 : Sys -> Bool
  op inv2 : Sys -> Bool
  op inv3 : Sys -> Bool
  op inv4 : Sys -> Bool
  op inv5 : Sys -> Bool
  op inv6 : Sys -> Bool
  op inv7 : Sys -> Bool
  op inv8 : Sys -> Bool
  op inv9 : Sys -> Bool
  op inv10 : Sys -> Bool
-- CafeOBJ variables
  var S : Sys
-- define operators denoting invariants to prove
  eq inv1(S) = (t(S) = crossing implies g(S) = down) .
  eq inv2(S) = (t(S) = sect0 and c(S) = state0 implies g(S) = up) .
  eq inv3(S) = (g(S) = down and c(S) = state3 implies not(t(S) = sect0)) .
  eq inv4(S) 
     = (g(S) = up and c(S) = state1 implies cu(S) = cl(S) and tl(S) + d2 = cl(S) + d1) .
  eq inv5(S) = now(S) <= cu(S) .
  eq inv6(S) = (g(S) = lowering and c(S) = state2 implies gu(S) + d1 = tl(S) + d2 + d3) .
  eq inv7(S) = now(S) <= gu(S) .
  eq inv8(S) 
     = (t(S) = sect1 implies (g(S) = up and c(S) = state1) or
                             (g(S) = lowering and c(S) = state2) or
                             (g(S) = down and c(S) = state2)) .
  eq inv9(S) = (t(S) = sect1 and tl(S) <= now(S) implies g(S) = down and c(S) = state2) .
  eq inv10(S) = (t(S) = crossing implies g(S) = down and c(S) = state2) .
}

mod ISTEP {
  pr(INV)
-- arbitrary objects
  ops s s' : -> Sys
-- declare predicates to prove in each inductive case
  --
  op istep2 : -> Bool
  op istep3 : -> Bool
  op istep4 : -> Bool
  op istep5 : -> Bool
  op istep6 : -> Bool
  op istep7 : -> Bool
  op istep8 : -> Bool
  --
  op istep10 : -> Bool
-- CafeOBJ variables
  var S : Sys
-- define predicates to prove in each inductive case
  --
  eq istep2 = inv2(s) implies inv2(s') .
  eq istep3 = inv3(s) implies inv3(s') .
  eq istep4 = inv4(s) implies inv4(s') .
  eq istep5 = inv5(s) implies inv5(s') .
  eq istep6 = inv6(s) implies inv6(s') .
  eq istep7 = inv7(s) implies inv7(s') .
  eq istep8 = inv8(s) implies inv8(s') .
  --
  eq istep10 = inv10(s) implies inv10(s') .
}