--
-- inv1(s) depends on inv2(s), inv3(s) and inv4(s).
-- inv2(s) depends on inv5(s).
-- inv3(s) can be proved independently.
-- inv4(s) can be proved independently.
-- inv5(s) can be proved independently.
--

mod INV {
  pr(ASEND)
-- arbitrary objects
-- declare operators denoting invariants
  op inv1 : Sys -> Bool
  op inv2 : Sys -> Bool
  op inv3 : Sys -> Bool
  op inv4 : Sys -> Bool
  op inv5 : Sys -> Bool
-- CafeOBJ variables
  var S : Sys
-- define operators denoting invariants
  eq inv1(S) = (empty(S) implies list(S) = (0 .. dec(data(S)))) and
               (not empty(S) implies list(S) = (0 .. dec(dec(data(S))))) .
  eq inv2(S) = l(S) <= now(S) implies empty(S) .
  eq inv3(S) = not empty(S) implies 0 < data(S) .
  eq inv4(S) = not empty(S) implies content(S) = dec(data(S)) .
  eq inv5(S) = not empty(S) implies u(S) < l(S) .
}

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