-- *** Mutual Exclusion
-- This claim guarantees that the program allows at most one process
-- to enter the critical section at the same time.
--
-- 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,130)
--
--  invariant (pc(s,p) = cs and pc(s,q) = l3 implies check(s,q))
--

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

--
-- Claim 130 (**PROVED**) (Used Lemmas: 150)
--
--  invariant (not(p = q) and pc(s,p) = l3 and pc(s,q) = l3 
--             implies check(s,p) or check(s,q))
--

--
-- Claim 140 (**PROVED**) (Used Lemmas: None)
--
--  invariant (pc(s,p) = l2 implies check(s,p)) .
--

--
-- Claim 150 (**PROVED**) (Used Lemmas: 140,170)
--
--  invariant (pc(s,p) = l3 and not check(s,p) implies locked(s)) 
--

--
-- Claim 160 (**PROVED**) (Used Lemmas: 170)
--
--  invariant (pc(s,p) = cs and pc(s,q) = l4 implies p = q) 
--

--
-- Claim 170 (**PROVED**) (Used Lemmas: 110,180)
--
--  invariant (pc(s,p) = l4 and pc(s,q) = l3 implies check(s,q))
--

--
-- Claim 180 (**PROVED**) (Used Lemmas: 120,140,190)
--
--  invariant (pc(s,p) = l4 implies locked(s))
--

--
-- Claim 190 (**PROVED**) (Used Lemmas: 160)
--
--  invariant (pc(s,p) = l4 and pc(s,q) = l4 implies p = q) 
--

mod INV {
  pr(MUTEX)
-- arbitrary objects
  ops p q : -> Process
-- declare invariants to prove
  op inv100 : System Process Process -> Bool
  op inv110 : System Process Process -> Bool
  op inv120 : System Process -> Bool
  op inv130 : System Process Process -> Bool
  op inv140 : System Process -> Bool
  op inv150 : System Process -> Bool
  op inv160 : System Process Process -> Bool
  op inv170 : System Process Process -> Bool
  op inv180 : System Process -> Bool
  op inv190 : 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,Q) = (pc(S,P) = cs and pc(S,Q) = l3) implies check(S,Q) .
  eq inv120(S,P) = (pc(S,P) = cs) implies locked(S) .
  eq inv130(S,P,Q) = (not(P = Q) and pc(S,P) = l3 and pc(S,Q) = l3) 
                      implies (check(S,P) or check(S,Q)) .
  eq inv140(S,P) = (pc(S,P) = l2) implies check(S,P) .
  eq inv150(S,P) = (pc(S,P) = l3 and not check(S,P)) implies locked(S) .
  eq inv160(S,P,Q) = (pc(S,P) = cs and pc(S,Q) = l4) implies (P = Q) .
  eq inv170(S,P,Q) = (pc(S,P) = l4 and pc(S,Q) = l3) implies check(S,Q) .
  eq inv180(S,P) = (pc(S,P) = l4) implies locked(S) .
  eq inv190(S,P,Q) = (pc(S,P) = l4 and pc(S,Q) = l4) implies (P = Q) .
}

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 Process -> Bool
  op istep120 : Process -> Bool
  op istep130 : Process Process -> Bool
  op istep140 : Process -> Bool
  op istep150 : Process -> Bool
  op istep160 : Process Process -> Bool
  op istep170 : Process Process -> Bool
  op istep180 : Process -> Bool
  op istep190 : 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,Q) = inv110(s,P,Q) implies inv110(s',P,Q) .
  eq istep120(P) = inv120(s,P) implies inv120(s',P) .
  eq istep130(P,Q) = inv130(s,P,Q) implies inv130(s',P,Q) .
  eq istep140(P) = inv140(s,P) implies inv140(s',P) .
  eq istep150(P) = inv150(s,P) implies inv150(s',P) .
  eq istep160(P,Q) = inv160(s,P,Q) implies inv160(s',P,Q) .
  eq istep170(P,Q) = inv170(s,P,Q) implies inv170(s',P,Q) .
  eq istep180(P) = inv180(s,P) implies inv180(s',P) .
  eq istep190(P,Q) = inv190(s,P,Q) implies inv190(s',P,Q) .
}