in mcs

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


-- ------------------------------1.1: pc(s,r) = rs, p != r, q != r ----------------------
-- ----------------------------------1.1a.  -----------------
-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq z = r .
red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close


-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .
eq (z = r) = false .

eq q = r .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .
eq (z = r) = false .
eq (q = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .
eq (z = r) = false .

eq q = r .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- 1.1.1-(1) pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq (p = r) = false .
eq (z = r) = false .

eq (q = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

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

-- 1.2
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq p = r .
eq (z = r) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- -- 1.2 pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq p = r .
eq (z = r) = false .

eq q = r .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- -- -- 1.2 pc(s,r) = rs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = rs .
eq p = r .
eq (z = r) = false .

eq (q = r) = false .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(want(s,r),p,q,z) .
close

-- ------------------------------2.1: pc(s,r) = l1, p != r, q != r ----------------------
-- ----------------------------------2.1a.  -----------------
-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq z = r .
-- red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .
eq (z = r) = false .

eq q = r .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .
eq (z = r) = false .
eq (q = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .
eq (z = r) = false .

eq q = r .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- 2.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq (p = r) = false .
eq (z = r) = false .

eq (q = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

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

-- 2.2
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq p = r .
eq (z = r) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- -- 2.2 pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq p = r .
eq (z = r) = false .

eq q = r .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- -- -- 2.2 pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l1 .
eq p = r .
eq (z = r) = false .

eq (q = r) = false .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stnxt(s,r),p,q,z) .
close

-- ------------------------------3.1: pc(s,r) = l2, p != r, q != r ----------------------
-- ----------------------------------3.1a. -----------------
-- -- 3.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq glock(s) = nop .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
red (inv4(s,p) and inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq glock(s) = nop .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l1, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq (glock(s) = nop) = false .
red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l3 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,q) = l3 .

eq pc(s,z) = l11 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,q) = l4 .

eq pc(s,z) = l11 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,q) = l5 .

eq pc(s,z) = l11 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 . red (inv10(s,q,z) and inv10(s,r,q) and  inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pc(s,q) = l5) = false .
eq (pc(s,q) = l4) = false .
eq (pc(s,q) = l3) = false .

eq pred(s,q) = z .
eq pc(s,q) = l6 .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pc(s,q) = l5) = false .
eq (pc(s,q) = l4) = false .
eq (pc(s,q) = l3) = false .

eq pred(s,q) = z .
eq (pc(s,q) = l6) = false .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pc(s,q) = l5) = false .
eq (pc(s,q) = l4) = false .
eq (pc(s,q) = l3) = false .

eq (pred(s,q) = z) = false .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.1.1-(1) pc(s,r) = l2, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
-- check
red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

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

-- -- 3.2-1 pc(s,r) = l2, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq q = r .
eq p = r .
eq (z = r) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.2-1 pc(s,r) = l2, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq q = r .
eq p = r .
eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

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

-- -- 3.3-(1) pc(s,r) = l2, p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.3-(1) pc(s,r) = l2, p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
-- check
red   ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- ----------------------------3.4: pc(s,r) = l2, p != r, q = r --------------------------
-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .
eq z = r .

eq glock(s) = nop .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .
eq z = r .

eq glock(s) = nop .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
red (inv4(s,p) and inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .
eq z = r .

eq (glock(s) = nop) = false .
red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close


-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (glock(s) = z) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 . red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq glock(s) = z .

eq pc(s,z) = l11 . red (inv12(s,z) and   inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv12(s,z) and   inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv8(s,p,z) and inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv8(s,p,z) and inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv8(s,p,z) and inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv8(s,p,z) and inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq pc(s,z) = l6 .
eq lock(s,z) = false . red (inv8(s,p,z) and inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
eq lock(s,z) = true .  red (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- -- 3.4-(1) pc(s,r) = l2, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l2 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red   (inv19(s,p,q,z)) implies   inv19(stprd(s,r),p,q,z) .
close

-- ------------------------------4.1: pc(s,r) = l3, p != r, q != r ----------------------
-- ----------------------------------4.1a. z = r , p != z -----------------
-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pred(s,r) = nop .

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .

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

eq z = r .
eq pred(s,r) = nop .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .

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

eq z = r .
eq pred(s,r) = nop .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .

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

eq z = r .
eq pred(s,r) = nop .

eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .

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

eq z = r .
eq pred(s,r) = nop .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .

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

eq z = r .
eq pred(s,r) = nop .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .

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

eq z = r .
eq pred(s,r) = nop .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pred(s,r) = nop .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pred(s,r) = nop .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pred(s,r) = nop .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq (pred(s,r) = nop) = false .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq (pred(s,r) = nop) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close


-- -- 4.1.1-(1) pc(s,r) = l3, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .


eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
-- check
red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close


-- ------------------------------4.2: pc(s,r) = l3, p = r, q = r----------------------
-- -- 4.2-1 pc(s,r) = l3, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq q = r .
eq p = r .
eq z = r .
eq pred(s,r) = nop .
red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.2-1 pc(s,r) = l3, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq q = r .
eq p = r .
eq z = r .

eq (pred(s,r) = nop) = false .
red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.2-1 pc(s,r) = l3, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq q = r .
eq p = r .
eq (z = r) = false .

eq pred(s,r) = nop .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.2-1 pc(s,r) = l3, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq q = r .
eq p = r .
eq (z = r) = false .
eq pred(s,r) = nop .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.2-1 pc(s,r) = l3, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq q = r .
eq p = r .
eq (z = r) = false .

eq (pred(s,r) = nop) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.2-1 pc(s,r) = l3, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .

eq pc(s,r) = l3 .
eq q = r .
eq p = r .
eq (z = r) = false .
eq (pred(s,r) = nop) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- ------------------------------4.3: pc(s,r) = l3, p = r, q != r----------------------
-- -- 4.3-(1) pc(s,r) = l3, p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

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

-- -- 4.3-(1) pc(s,r) = l3, p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

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


-- -- 4.3-(1) pc(s,r) = l3, p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .
eq pred(s,r) = nop .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
-- check
red   ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.3-(1) pc(s,r) = l3, p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .
eq pred(s,r) = nop .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red   ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close


-- -- 4.3-(1) pc(s,r) = l3, p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .
eq (pred(s,r) = nop) = false .
eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.3-(1) pc(s,r) = l3, p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .

eq (pred(s,r) = nop) = false .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red   ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- ----------------------------4.4: pc(s,r) = l3, p != r, q = r --------------------------
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq z = r .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq z = r .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
-- check
red   (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .

eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq pred(s,r) = nop .
eq (z = r) = false .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red   (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq z = r .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq z = r .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red   (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .

eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close
-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- -- 4.4-(1) pc(s,r) = l3, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l3 .
eq (p = r) = false .
eq q = r .

eq (pred(s,r) = nop) = false .
eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
-- check
red   (inv19(s,p,q,z)) implies   inv19(chprd(s,r),p,q,z) .
close

-- ------------------------------5.1: pc(s,r) = l4, p != r, q != r ----------------------
-- ----------------------------------5.1a.  -----------------
-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close


-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close


-- -- 5.1.1-(1) pc(s,r) = l4, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

-- ------------------------------5.2: pc(s,r) = l4, p = r, q = r----------------------
-- 5.2
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq q = r .
eq p = r .
eq z = r .
-- check
red   (inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

-- 5.2
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l4 .
eq q = r .
eq p = r .
eq (z = r) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

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

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

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

eq z = r .
red   (inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

-- -- 5.3-(1) pc(s,r) = l4, p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .
eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

-- -- 5.3-(1) pc(s,r) = l4, p = r, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .
eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
-- check
red   (inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close


-- ----------------------------5.4: pc(s,r) = l4, p != r, q = r --------------------------
-- -- 5.4-(1) pc(s,r) = l4, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .

eq z = r .
-- check
red   (inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

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

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.4-(1) pc(s,r) = l4, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.4-(1) pc(s,r) = l4, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.4-(1) pc(s,r) = l4, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.4-(1) pc(s,r) = l4, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.4-(1) pc(s,r) = l4, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close
-- -- 5.4-(1) pc(s,r) = l4, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l4 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

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

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

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

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stlck(s,r),p,q,z) .
close

-- ------------------------------6.1: pc(s,r) = l5, p != r, q != r ----------------------
-- ----------------------------------6.1a. z = r , p != z -----------------
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq lock(s,r) = false .

eq pc(s,z) = l11 . red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq lock(s,r) = true .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close


-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .

eq lock(s,r) = false .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .

eq lock(s,r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq z = r .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .

eq lock(s,r) = true .
red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pc(s,q) = l5 .

eq pc(s,z) = l11 . red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
eq pc(s,q) = l4 .

eq pc(s,z) = l11 . red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .
eq pc(s,q) = l3 .

eq pc(s,z) = l11 . red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pc(s,q) = l5) = false .
eq (pc(s,q) = l4) = false .
eq (pc(s,q) = l3) = false .

eq pc(s,z) = l11 . red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.1.1-(1) pc(s,r) = l5, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq (q = r) = false .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
-- check
red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- ------------------------------6.2: pc(s,r) = l5, p = r, q = r----------------------
-- -- 6.2-1 pc(s,r) = l5, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq q = r .
eq p = r .
eq z = r .

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

-- -- 6.2-1 pc(s,r) = l5, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq q = r .
eq p = r .
eq (z = r) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.2-1 pc(s,r) = l5, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq q = r .
eq p = r .
eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- ------------------------------6.3: pc(s,r) = l5, p = r, q != r----------------------
-- -- 6.3-(1) pc(s,r) = l5, p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (q = r) = false .
eq p = r .

eq z = r .
-- check
red   (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.3-(1) pc(s,r) = l5, p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
-- check
red   ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.3-(1) pc(s,r) = l5, p = r, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
-- check
red   ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- ----------------------------6.4: pc(s,r) = l5, p != r, q = r --------------------------
-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq z = r .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq z = r .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq lock(s,r) = true .   red  (inv19(s,p,q,z)) implies  inv19(stnpr(s,r),p,q,z) .
eq lock(s,r) = false .  red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

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

eq (z = r) = false .
eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close
-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close


-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq pred(s,r) = z .

eq pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pred(s,r) = z) = false .

eq lock(s,r) = true .

eq pc(s,p) = l6 .
eq glock(s) = r .

eq pc(s,z) = l11 . red (inv10(s,r,z) and  inv19(s,p,q,z)) implies inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv10(s,r,z) and  inv19(s,p,q,z)) implies inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv10(s,r,z) and  inv19(s,p,q,z)) implies inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv10(s,r,z) and  inv19(s,p,q,z)) implies inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv10(s,r,z) and  inv19(s,p,q,z)) implies inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv10(s,r,z) and  inv19(s,p,q,z)) implies inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv10(s,r,z) and  inv19(s,p,q,z)) implies inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pred(s,r) = z) = false .
eq lock(s,r) = true .

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

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies  inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (   inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (   inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pred(s,r) = z) = false .
eq lock(s,r) = true .

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

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies  inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red (  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (   inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (   inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (pred(s,r) = z) = false .
eq lock(s,r) = false .

eq pc(s,z) = l11 . red (inv6(s,r) and inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv6(s,r) and  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv6(s,r) and  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv6(s,r) and  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv6(s,r) and  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv6(s,r) and  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv6(s,r) and  inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- -- 6.4-(1) pc(s,r) = l5, p != r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
-- check
red   (inv19(s,p,q,z)) implies   inv19(stnpr(s,r),p,q,z) .
close

-- ------------------------------7.1: pc(s,r) = l6, p != r, q != r ----------------------
-- ----------------------------------7.1a. z = r , p != z -----------------
-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq z = r .
eq lock(s,r) = false .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close
-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq z = r .
eq lock(s,r) = true .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq z = r .
eq q = r .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq lock(s,r) = false .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq lock(s,r) = true .   red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close


-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l6 .
eq (p = r) = false .

eq z = r .
eq (q = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq lock(s,r) = false .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq lock(s,r) = true .   red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l11 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close
-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l10 .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = cs .

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close
-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close
-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close
-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .
eq pc(s,z) = l3 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (q = r) = false .
eq pc(s,q) = l5 .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (q = r) = false .

eq pc(s,q) = l4 .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (q = r) = false .
eq pc(s,q) = l3 .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq (q = r) = false .
eq (pc(s,q) = l5) = false .
eq (pc(s,q) = l4) = false .
eq (pc(s,q) = l3) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq q = r .
eq lock(s,r) = true .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,p) = l1) =  false .
eq (pc(s,p) = l2) =  false .
eq (pc(s,p) = rs) =  false .
eq (pc(s,p) = l9) =  false .
eq (pc(s,p) = l12) =  false .

eq q = r .
eq lock(s,r) = false .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .

eq q = r .
red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.1.1-(1) pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq (p = r) = false .

eq (z = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .

eq (q = r) = false .
red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- ------------------------------7.2: pc(s,r) = l6, p = r, ----------------------
-- -- 7.2-1 pc(s,r) = l6, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq p = r .

eq z = r .
eq lock(s,r) = false .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq lock(s,r) = true .   red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close


-- -- 7.2-1 pc(s,r) = l6, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq p = r .

eq (z = r) = false .
eq q = r .

eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.2-1 pc(s,r) = l6, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l6 .
eq p = r .

eq (z = r) = false .
eq q = r .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.2-1 pc(s,r) = l6, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq p = r .

eq (z = r) = false .
eq (q = r) = false .

eq lock(s,r) = false .
eq pc(s,z) = l11 . red ( inv2(s,z,r) and inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv2(s,z,r) and inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv2(s,z,r) and inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv2(s,z,r) and inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv2(s,z,r) and inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv7(s,r,z) and inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv2(s,r,z) and  inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.2-1 pc(s,r) = l6, p = r, q = r
open INV .
op s : -> Sys .
ops p q r z : -> Pid .
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
eq pc(s,r) = l6 .
eq p = r .

eq (z = r) = false .
eq (q = r) = false .

eq lock(s,r) = true .
eq pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close

-- -- 7.2-1 pc(s,r) = l6, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r z : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv19(s,P:Pid,Q:Pid,Z:Pid) = true .
-- assumptions
eq pc(s,r) = l6 .
eq p = r .

eq (z = r) = false .
eq (q = r) = false .

eq (pc(s,z) = l11) =  false .
eq (pc(s,z) = l10) =  false .
eq (pc(s,z) = l8) =  false .
eq (pc(s,z) = l7) =  false .
eq (pc(s,z) = cs) =  false .
eq (pc(s,z) = l6) =  false .
eq (pc(s,z) = l3) =  false .
eq lock(s,r) = true .   red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
eq lock(s,r) = false .  red ( inv19(s,p,q,z)) implies   inv19(chlck(s,r),p,q,z) .
close