--
-- Claim 100 (**PROVED**) (Used Lemmas: 110)
--
--  invariant ((flag(s) implies mk(next(s)) = list(s)) and
--             (not flag(s) implies mk(next(s)) = (next(s) list(s))))
--

--
-- Claim 110 (**PROVED**) (Used Lemmas: 120)
--
--  invariant (not empty?(cell(s)) implies (next(s) = content(cell(s))))
--             
--

--
-- Claim 120 (**PROVED**) (Used Lemmas: Nonce)
--
--  invariant (flag(s) implies empty?(cell(s))) 
--             
--

mod INV {
  pr(SP)
-- declare invariants to prove
  op inv100 : System -> Bool
  op inv110 : System -> Bool
  op inv120 : System -> Bool
-- CafeOBJ variables
  var S : System
-- define invariants to prove
  eq inv100(S) = ((flag(S) implies mk(next(S)) = list(S)) and
                  (not flag(S) implies mk(next(S)) = (next(S) list(S)))) .
  eq inv110(S)
     = (not empty?(cell(S)) implies (next(S) = content(cell(S)))) .
  eq inv120(S) = (flag(S) implies empty?(cell(S))) .
}

mod ISTEP {
  pr(INV)
-- arbitrary objects
  ops s s' : -> System
-- declare predicates to prove in inductive step
  op istep100 : -> Bool
  op istep110 : -> Bool
  op istep120 : -> Bool
-- define predicates to prove in inductive step
  eq istep100 = inv100(s) implies inv100(s') .
  eq istep110 = inv110(s) implies inv110(s') .
  eq istep120 = inv120(s) implies inv120(s') .
}