--
-- Claim 100 is the property (invariant) that we want to prove.
-- We need four more invariants to prove Claim 100.
--

-- *** Mutual Exclusion
-- Claim 100 (**PROVED**) (Used Lemmas: 110)
--
--  invariant (pc(s,p) = cs and pc(s,q) = cs implies p = q)
--

--
-- Claim 110 (**PROVED**) (Used Lemmas: 120)
--
--  invariant (pc(s,p) = cs implies locked(s))
--

--
-- Claim 120 (**PROVED**) (Used Lemmas: 100,110,130)
--
--  invariant (pc(s,p) = cs and pc(s,q) = l2 implies p = q)
--

--
-- Claim 130 (**PROVED**) (Used Lemmas: 110,140)
--
--  invariant (pc(s,p) = l2 implies locked(s))
--

--
-- Claim 140 (**PROVED**) (Used Lemmas: 120)
--
--  invariant (pc(s,p) = l2 and pc(s,q) = l2 implies p = q)
--

--
-- Invariants to prove are defined as CafeOBJ terms in module INV.
--
mod INV {
  pr(MUTEX)
-- arbitrary objects
  ops p q : -> Process
-- declare invariants to prove
  op inv100 : System Process Process -> Bool
  op inv110 : System Process -> Bool
  op inv120 : System Process Process -> Bool
  op inv130 : System Process -> Bool
  op inv140 : System Process Process -> Bool
-- CafeOBJ variables
  var S : System
  vars P Q : Process
-- define invariants to prove
  eq inv100(S,P,Q) = (pc(S,P) = cs and pc(S,Q) = cs) implies (P = Q) .
  eq inv110(S,P) = (pc(S,P) = cs) implies locked(S) .
  eq inv120(S,P,Q) = (pc(S,P) = cs and pc(S,Q) = l2) implies (P = Q) .
  eq inv130(S,P) = (pc(S,P) = l2) implies locked(S) .
  eq inv140(S,P,Q) = (pc(S,P) = l2 and pc(S,Q) = l2) implies (P = Q) .
}

--
-- Invariants are proved by INDUCTION on the numbers of transition 
-- rules applied or executed. 
--
-- If we prove that the system has invariant P by induction on the
-- number of transition rules applied, the proof structure looks as follows: 
--
--   I) Base case
--     P(init,x) for any x
--   II) Inductive cases
--     1. P(s,x) implies P(begin(s,p),x) for any s,x,p.
--     2. P(s,x) implies P(exit(s,p),x) for any s,x,p.
--     3. P(s,x) implies P(end(s,p),x) for any s,x,p.
--
-- Predicates to prove in each inductive step are defined as CafeOBJ
-- terms in module ISTEP.
--
mod ISTEP {
  pr(INV)
-- arbitrary objects
  ops s s' : -> System
-- declare predicates to prove in inductive step
  op istep100 : Process Process -> Bool
  op istep110 : Process -> Bool
  op istep120 : Process Process -> Bool
  op istep130 : Process -> Bool
  op istep140 : Process Process -> Bool
-- CafeOBJ variables
  vars P Q : Process
-- define predicates to prove in inductive step
  eq istep100(P,Q) = inv100(s,P,Q) implies inv100(s',P,Q) .
  eq istep110(P) = inv110(s,P) implies inv110(s',P) .
  eq istep120(P,Q) = inv120(s,P,Q) implies inv120(s',P,Q) .
  eq istep130(P) = inv130(s,P) implies inv130(s',P) .
  eq istep140(P,Q) = inv140(s,P,Q) implies inv140(s',P,Q) .
}