in mcs

-- used inv1, inv2, inv3



-- ---------- mutex property ------------

-- (I) Base case
open INV .
-- fresh constants
ops p q : -> Pid .
-- check
red mutex(init,p,q) .
close


-- (II) Induction case
-- 1. want(s,r)
-- -- 1.1 pc(s,r) != rs
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq (pc(s,r) = rs) = false .
-- check
red mutex(s,p,q) implies mutex(want(s,r),p,q) .
close

-- -- 1.2.1 pc(s,r) = rs, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq p = r .
eq q = r .
red mutex(s,p,q) implies mutex(want(s,r),p,q) .
close

-- -- 1.2.2 pc(s,r) = rs, (p = r) = false, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .
eq q = r .
-- check
red mutex(s,p,q) implies mutex(want(s,r),p,q) .
close

-- -- 1.2.3 pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .
eq (q = r) = false .
-- check
red mutex(s,p,q) implies mutex(want(s,r),p,q) .
close

-- -- 1.2.4 pc(s,r) = rs,  p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (q = r) = false .
eq p = r .
-- check
red mutex(s,p,q) implies mutex(want(s,r),p,q) .
close

-- ------------------------ 2. stnxt(s,r) - l1 ---------------------
-- 2.1 pc(s,r) != l1
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq (pc(s,r) = l1) = false .
-- check
red mutex(s,p,q) implies mutex(stnxt(s,r),p,q) .
close

-- 2.2.1 pc(s,r) = l1, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq p = r .
eq q = r .
-- check
red mutex(s,p,q) implies mutex(stnxt(s,r),p,q) .
close

-- 2.2.2 pc(s,r) = l1, (p = r) = false, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .
eq q = r .
-- check
red mutex(s,p,q) implies mutex(stnxt(s,r),p,q) .
close

-- 2.2.3 pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .
eq (q = r) = false .
-- check
red mutex(s,p,q) implies mutex(stnxt(s,r),p,q) .
close

-- 2.2.4 pc(s,r) = l1, p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq p = r .
eq (q = r) = false .
-- check
red mutex(s,p,q) implies mutex(stnxt(s,r),p,q) .
close

-- ------------------------- 3. stprd(S,P)  - l2 ---------------------.
-- -- 3.1 pc(s,r) != l2
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l2) = false .
-- check
red mutex(s,p,q) implies mutex(stprd(s,r),p,q) .
close

-- 3.2.1 pc(s,r) = l2, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq p = r .
eq q = r .
-- check
red mutex(s,p,q) implies mutex(stprd(s,r),p,q) .
close

-- 3.2.2 pc(s,r) = l2, (p = r) = false, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .
-- check
red mutex(s,p,q) implies mutex(stprd(s,r),p,q) .
close

-- 3.2.3 pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .
-- check
red mutex(s,p,q) implies mutex(stprd(s,r),p,q) .
close

-- 3.2.4 pc(s,r) = l2,  p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (q = r) = false .
eq p = r .
-- check
red mutex(s,p,q) implies mutex(stprd(s,r),p,q) .
close

-- ------------4. chprd(S,P) - pc(S,P) = l3 . --------------------
-- 4.1 pc(s,r) != l3
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq (pc(s,r) = l3) = false .
-- check
red mutex(s,p,q) implies mutex(chprd(s,r),p,q) .
close

-- -- 4.2.1 pc(s,r) = l3, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq p = r .
eq q = r .
-- check
red mutex(s,p,q) implies mutex(chprd(s,r),p,q) .
close

-- 4.2.2.1 pc(s,r) = l3, (p = r) = false, q = r, (pred(s,r) = nop), pc(s,p) = cs
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
-- check
red (inv1(s,p,r) and mutex(s,p,q)) implies mutex(chprd(s,r),p,q) .
close

-- -- 4.2.2.3 pc(s,r) = l3, (p = r) = false, q = r, (pred(s,r) != nop), pc(s,p) != cs
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
-- check
red (mutex(s,p,q)) implies mutex(chprd(s,r),p,q) .
close

-- 4.2.3 pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .
-- check
red mutex(s,p,q) implies mutex(chprd(s,r),p,q) .
close

-- -- 4.2.4.1 pc(s,r) = l3, (q = r) = false, p = r, (pred(s,r) = nop
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

eq pred(s,r) = nop .
-- check
red (inv1(s,q,r) and mutex(s,p,q)) implies mutex(chprd(s,r),p,q) .
close

-- -- 4.2.4.3 pc(s,r) = l3, (q = r) = false, p = r, (pred(s,r) != nop)
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

eq (pred(s,r) = nop) = false .
-- check
red (mutex(s,p,q)) implies mutex(chprd(s,r),p,q) .
close

-- ---------------------------- 5.stlck - l4 -------------------------------
-- 5. stlck(S,P) = S if not pc(S,P) = l4 .
-- 5.1 pc(s,r) != l4
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l4) = false .
red mutex(s,p,q) implies mutex(stlck(s,r),p,q) .
close

-- 5.2.1 pc(s,r) = l4,  p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l4 .
eq p = r .
eq q = r .

red mutex(s,p,q) implies mutex(stlck(s,r),p,q) .
close

-- 5.2.2 pc(s,r) = l4,  p != r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .
red mutex(s,p,q) implies mutex(stlck(s,r),p,q) .
close

-- 5.2.3 pc(s,r) = l4,  p = r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l4 .
eq (q = r) = false .
eq p = r .
red mutex(s,p,q) implies mutex(stlck(s,r),p,q) .
close

-- 5.2.4 pc(s,r) = l4,  p != r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l4 .
eq (q = r) = false .
eq (p = r) = false .

red mutex(s,p,q) implies mutex(stlck(s,r),p,q) .
close

-- ------------------- 6. stnpr(S,P) = S if not pc(S,P) = l5 . ---------------------------
-- 6.1 pc(s,r) != l5
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l5) = false .

red mutex(s,p,q) implies mutex(stnpr(s,r),p,q) .
close

-- 6.2.1 pc(s,r) = l5,  p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l5 .
eq p = r .
eq q = r .

red mutex(s,p,q) implies mutex(stnpr(s,r),p,q) .
close

-- 6.2.2 pc(s,r) = l5,  p != r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

red mutex(s,p,q) implies mutex(stnpr(s,r),p,q) .
close

-- 6.2.3 pc(s,r) = l5,  p = r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l5 .
eq (q = r) = false .
eq p = r .

red mutex(s,p,q) implies mutex(stnpr(s,r),p,q) .
close

-- 6.2.4 pc(s,r) = l5,  p != r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l5 .
eq (q = r) = false .
eq (p = r) = false .

red mutex(s,p,q) implies mutex(stnpr(s,r),p,q) .
close


-- -------------------------- 7. stnpr -  pc(S,P) = l6 -------------------------------.
-- 7.1 pc(s,r) != l6
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l6) = false .

red mutex(s,p,q) implies mutex(chlck(s,r),p,q) .
close

-- 7.2.1 pc(s,r) = l6,  p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l6 .
eq p = r .
eq q = r .

red mutex(s,p,q) implies mutex(chlck(s,r),p,q) .
close


-- 7.2.2.1 pc(s,r) = l6,  p != r, q = r, eq pc(s,p) != cs .
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .
eq q = r .

eq (pc(s,p) = cs) = false .
red (mutex(s,p,q)) implies mutex(chlck(s,r),p,q) .
close

-- 7.2.2.2 pc(s,r) = l6,  p != r, q = r, eq pc(s,p) = cs , lock(s,r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .

eq pc(s,r) = l6 .
eq (p = r) = false .
eq q = r .

eq pc(s,p) = cs .
eq lock(s,r) = false .
red (inv2(s,p,r) and mutex(s,p,q)) implies mutex(chlck(s,r),p,q) .
close

-- 7.2.2.2 pc(s,r) = l6,  p != r, q = r, eq pc(s,p) = cs , lock(s,r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .

eq pc(s,r) = l6 .
eq (p = r) = false .
eq q = r .

eq pc(s,p) = cs .
eq lock(s,r) = true .
red ( mutex(s,p,q)) implies mutex(chlck(s,r),p,q) .
close

-- 7.2.3.1 pc(s,r) = l6,  p = r, q != r, pc(s,q) != cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l6 .
eq (q = r) = false .
eq p = r .
eq (pc(s,q) = cs) = false .
red (mutex(s,p,q)) implies mutex(chlck(s,r),p,q) .
close

-- 7.2.3.2 pc(s,r) = l6,  q != r, p = r, eq pc(s,q) = cs , lock(s,r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l6 .
eq (q = r) = false .
eq p = r .

eq pc(s,q) = cs .
eq lock(s,r) = false .
red (inv2(s,q,r) and mutex(s,p,q)) implies mutex(chlck(s,r),p,q) .
close

-- 7.2.3.2 pc(s,r) = l6,  q != r, p = r, eq pc(s,q) = cs , lock(s,r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l6 .
eq (q = r) = false .
eq p = r .

eq pc(s,q) = cs .
eq lock(s,r) = true .
red (inv2(s,q,r) and mutex(s,p,q)) implies mutex(chlck(s,r),p,q) .
close

-- 7.2.4 pc(s,r) = l6,  p != r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l6 .
eq (q = r) = false .
eq (p = r) = false .

red mutex(s,p,q) implies mutex(chlck(s,r),p,q) .
close


-- ----------------------- 8. exit(S,P)  pc(S,P) = cs . ----------------
-- 8.1 pc(s,r) != cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = cs) = false .

red mutex(s,p,q) implies mutex(exit(s,r),p,q) .
close

-- 8.2.1 pc(s,r) = cs,  p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = cs .
eq p = r .
eq q = r .
red mutex(s,p,q) implies mutex(exit(s,r),p,q) .
close

-- 8.2.2 pc(s,r) = cs,  p != r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = cs .
eq (p = r) = false .
eq q = r .

red mutex(s,p,q) implies mutex(exit(s,r),p,q) .
close

-- 8.2.3 pc(s,r) = cs,  p = r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = cs .
eq (q = r) = false .
eq p = r .

red mutex(s,p,q) implies mutex(exit(s,r),p,q) .
close

-- 8.2.4 pc(s,r) = cs,  p != r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = cs .
eq (q = r) = false .
eq (p = r) = false .
red mutex(s,p,q) implies mutex(exit(s,r),p,q) .
close


-- -------------------------------------- 9. chnxt(S,P) - pc(S,P) = l7 ----------------
-- 9.1 pc(s,r) != l7
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l7) = false .

red mutex(s,p,q) implies mutex(chnxt(s,r),p,q) .
close

-- 9.2.1 pc(s,r) = l7,  p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l7 .
eq p = r .
eq q = r .
red mutex(s,p,q) implies mutex(chnxt(s,r),p,q) .
close

-- 9.2.2.1 pc(s,r) = l7,  p != r, q = r, pc(s,p) = cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l7 .
eq (p = r) = false .
eq q = r .
eq pc(s,p) = cs .

red (inv3(s,p,r) and mutex(s,p,q)) implies mutex(chnxt(s,r),p,q) .
close

-- 9.2.2.2 pc(s,r) = l7,  p != r, q = r, pc(s,p) != cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l7 .
eq (p = r) = false .
eq q = r .
eq (pc(s,p) = cs) = false .

red  mutex(s,p,q) implies mutex(chnxt(s,r),p,q) .
close


-- 9.2.3.1 pc(s,r) = l7,  p = r, q != r, pc(s,q) != cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l7 .
eq (q = r) = false .
eq p = r .
eq (pc(s,q) = cs) = false .

red mutex(s,p,q) implies mutex(chnxt(s,r),p,q) .
close

-- 9.2.3.2 pc(s,r) = l7,  p = r, q != r, pc(s,q) = cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l7 .
eq (q = r) = false .
eq p = r .
eq pc(s,q) = cs .

red (inv3(s,q,r) and mutex(s,p,q)) implies mutex(chnxt(s,r),p,q) .
close

-- 9.2.4 pc(s,r) = l7,  p != r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l7 .
eq (q = r) = false .
eq (p = r) = false .

red mutex(s,p,q) implies mutex(chnxt(s,r),p,q) .
close

-- ---------------------------------- 10. chglk(S,P) - pc(S,P) = l8 ------------------------
-- 10.1 pc(s,r) != l8
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l8) = false .

red mutex(s,p,q) implies mutex(chglk(s,r),p,q) .
close

-- 10.2.1 pc(s,r) = l8,  p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l8 .
eq p = r .
eq q = r .

red mutex(s,p,q) implies mutex(chglk(s,r),p,q) .
close


-- 10.2.2.1 pc(s,r) = l8,  p != r, q = r, pc(s,p) != cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l8 .
eq (p = r) = false .
eq q = r .

eq (pc(s,p) = cs) = false .
red (inv3(s,p,r) and mutex(s,p,q)) implies mutex(chglk(s,r),p,q) .
close

-- 10.2.2.2 pc(s,r) = l8,  p != r, q = r, pc(s,p) = cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l8 .
eq (p = r) = false .
eq q = r .

eq pc(s,p) = cs .
red (inv3(s,p,r) and mutex(s,p,q)) implies mutex(chglk(s,r),p,q) .
close

-- 10.2.3.2 pc(s,r) = l8,  p = r, q != r, pc(s,q) != cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l8 .
eq (q = r) = false .
eq p = r .

eq (pc(s,q) = cs) = false .
red (mutex(s,p,q))  implies mutex(chglk(s,r),p,q) .
close

-- 10.2.3.2 pc(s,r) = l8,  p = r, q != r, pc(s,q) = cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l8 .
eq (q = r) = false .
eq p = r .

eq pc(s,q) = cs .
red (inv3(s,q,r) and mutex(s,p,q))  implies mutex(chglk(s,r),p,q) .
close

-- 10.2.4 pc(s,r) = l8,  p != r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l8 .
eq (q = r) = false .
eq (p = r) = false .

red mutex(s,p,q) implies mutex(chglk(s,r),p,q) .
close

-- ---------------------------- 11. go2rs(S,P) = S if not pc(S,P) = l9 -------------------------
-- 11.1 pc(s,r) != l9
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l9) = false .

red mutex(s,p,q) implies mutex(go2rs(s,r),p,q) .
close

-- 11.2.1 pc(s,r) = l9,  p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l9 .
eq p = r .
eq q = r .

red mutex(s,p,q) implies mutex(go2rs(s,r),p,q) .
close


-- 11.2.2 pc(s,r) = l9,  p != r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l9 .
eq (p = r) = false .
eq q = r .
red (mutex(s,p,q)) implies mutex(go2rs(s,r),p,q) .
close

-- 11.2.3 pc(s,r) = l9,  p = r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l9 .
eq (q = r) = false .
eq p = r .
red (mutex(s,p,q))  implies mutex(go2rs(s,r),p,q) .
close

-- 11.2.4 pc(s,r) = l9,  p != r, q != r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l9 .
eq (q = r) = false .
eq (p = r) = false .
red (mutex(s,p,q))  implies mutex(go2rs(s,r),p,q) .
close

-- 12. chnxt2(s,r)
-- -- 12.1 pc(s,r) != l10
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l10) = false .
red mutex(s,p,q) implies mutex(chnxt2(s,r),p,q) .
close

-- 12.2.1 pc(s,r) = l10, p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l10 .
eq p = r .
eq q = r .
red mutex(s,p,q) implies mutex(chnxt2(s,r),p,q) .
close

-- -- 12.2.2.1 pc(s,r) = l10, (p = r) = false, q = r, pc(s,p) = cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l10 .
eq (p = r) = false .
eq q = r .

eq pc(s,p) = cs .

red (inv3(s,p,r) and mutex(s,p,q)) implies mutex(chnxt2(s,r),p,q) .
close


-- -- 12.2.2.2 pc(s,r) = l10, (p = r) = false, q = r, pc(s,p) != cs
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l10 .
eq (p = r) = false .
eq q = r .

eq (pc(s,p) = cs) = false .
red mutex(s,p,q) implies mutex(chnxt2(s,r),p,q) .
close


-- -- 12.2.3 pc(s,r) = l10, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l10 .
eq (p = r) = false .
eq (q = r) = false .
red mutex(s,p,q) implies mutex(chnxt2(s,r),p,q) .
close

-- 12.2.4.1 pc(s,r) = l10,  p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l10 .
eq (q = r) = false .
eq p = r .
eq (pc(s,q) = cs) = false .
red mutex(s,p,q) implies mutex(chnxt2(s,r),p,q) .
close

-- 12.2.4.2 pc(s,r) = l10,  p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l10 .
eq (q = r) = false .
eq p = r .
eq pc(s,q) = cs .
red (inv3(s,q,r) and mutex(s,p,q)) implies mutex(chnxt2(s,r),p,q) .
close


-- -------------------------- 13. stlnx(s,r) - l11 ---------------------------------
-- -- 13.1 pc(s,r) != l11
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l11) = false .
red mutex(s,p,q) implies mutex(stlnx(s,r),p,q) .
close


-- 13.2.1 pc(s,r) = l11, p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l11 .
eq p = r .
eq q = r .
red mutex(s,p,q) implies mutex(stlnx(s,r),p,q) .
close

-- 13.2.2 pc(s,r) = l11, (p = r) = false, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l11 .
eq (p = r) = false .
eq q = r .
red (mutex(s,p,q)) implies mutex(stlnx(s,r),p,q) .
close

-- -- 13.2.3 pc(s,r) = l11, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l11 .
eq (p = r) = false .
eq (q = r) = false .
red mutex(s,p,q) implies mutex(stlnx(s,r),p,q) .
close

-- 13.2.4 pc(s,r) = l11,  p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l11 .
eq (q = r) = false .
eq p = r .
red mutex(s,p,q) implies mutex(stlnx(s,r),p,q) .
close

-- -------------------------------------- 14. go2rs2(s,r) ---------------------------
-- -- 14.1 pc(s,r) != l12
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq (pc(s,r) = l12) = false .
red mutex(s,p,q) implies mutex(go2rs2(s,r),p,q) .
close


-- 14.2.1 pc(s,r) = l11, p = r, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l12 .
eq p = r .
eq q = r .
red mutex(s,p,q) implies mutex(go2rs2(s,r),p,q) .
close

-- 14.2.2 pc(s,r) = l10, (p = r) = false, q = r
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l12 .
eq (p = r) = false .
eq q = r .
red (mutex(s,p,q)) implies mutex(go2rs2(s,r),p,q) .
close

-- -- 14.2.3 pc(s,r) = l11, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l12 .
eq (p = r) = false .
eq (q = r) = false .
red mutex(s,p,q) implies mutex(go2rs2(s,r),p,q) .
close


-- 14.2.4 pc(s,r) = l12,  p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r : -> Pid .
eq [:nonexec] : mutex(s,P:Pid,Q:Pid) = true .
eq pc(s,r) = l12 .
eq (q = r) = false .
eq p = r .
red mutex(s,p,q) implies mutex(go2rs2(s,r),p,q) .
close