in mcs

-- ------------------------------8.1: pc(s,r) = cs, p != r, q != r ----------------------
-- ----------------------------------8.1a. z = r , p != z -----------------
-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
eq (p = r) = false .
eq (q = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close
-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
eq (p = r) = false .
eq (q = r) = false .

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

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

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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 .   red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq lock(s,r) = true .   red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.1.1-(1) pc(s,r) = cs, (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) = cs .
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(exit(s,r),p,q,z) .
close


-- ------------------------------8.2: pc(s,r) = cs, p = r, q = r----------------------
-- -- 8.2-1 pc(s,r) = cs, 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) = cs .
eq q = r .
eq p = r .

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

-- -- 8.2-1 pc(s,r) = cs, 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) = cs .
eq q = r .
eq p = r .

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

-- -- 8.2-1 pc(s,r) = cs, 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) = cs .
eq q = r .
eq p = r .

eq (z = r) = false .

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

-- -- 8.2-1 pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
close

-- ------------------------------8.3: pc(s,r) = cs, p = r, q != r----------------------
-- -- 8.3-(1) pc(s,r) = cs, 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) = cs .
eq (q = r) = false .
eq p = r .

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

-- -- 8.3-(1) pc(s,r) = cs, 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) = cs .
eq (q = r) = false .
eq p = r .

eq (z = r) = false .

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

-- -- 8.3-(1) pc(s,r) = cs, 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) = cs .
eq (q = r) = false .
eq p = r .

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

-- -- 8.3-(1) pc(s,r) = cs, 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) = cs .
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 .

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

-- ----------------------------8.4: pc(s,r) = cs, p != r, q = r --------------------------
-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
eq (p = r) = false .
eq q = r .

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

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
eq (p = r) = false .
eq q = r .

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

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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) = false . red   (inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq lock(s,r) = true . red   (inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4-(1) pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(exit(s,r),p,q,z) .
close

-- -- 8.4 pc(s,r) = cs, 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) = cs .
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(exit(s,r),p,q,z) .
close

-- ------------------------------9.1: pc(s,r) = l7, p != r ----------------------
-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

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

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close
-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close
-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close
-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close
-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close
-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close
-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

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

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .
eq z = r .

eq (next(s,r) = nop) = 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(chnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = 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(chnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq (next(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 .

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

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq (next(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 .

eq (q = r) = false  .

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

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq (next(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 .

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 .
red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq next(s,r) = nop .
eq q = r .
red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq next(s,r) = nop .
eq (q = r) = false .

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

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
eq (p = r) = false .

eq z = r .
eq next(s,r) = nop .
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 .
red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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 next(s,r) = nop .

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

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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 (next(s,r) = nop) = false .

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

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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(chnxt(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.1.1-(1) pc(s,r) = l7, (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) = l7 .
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 .
red ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close


-- ------------------------------9.2: pc(s,r) = l7, p = r----------------------
-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

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

-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

eq z = r .
eq next(s,r) = nop .
red   (inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

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

-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

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

-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

eq (z = r) = false .
eq (next(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 .
-- check
red   ( inv19(s,p,q,z)) implies   inv19(chnxt(s,r),p,q,z) .
close

-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

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

eq q = r .

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

-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

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

eq (q = r) = false .

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

-- -- 9.3-(1) pc(s,r) = l7, 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) = l7 .
eq p = r .

eq (z = r) = false .

eq next(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(chnxt(s,r),p,q,z) .
close

-- ------------------------------10.1: pc(s,r) = l8, p != r ----------------------
-- -- 10.1.1-(1) pc(s,r) = l8, (p = 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) = l8 .
eq (p = r) = false .

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

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close
-- -- 10.1.1-(1) pc(s,r) = l8, (p = 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) = l8 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close
-- -- 10.1.1-(1) pc(s,r) = l8, (p = 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) = l8 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close
-- -- 10.1.1-(1) pc(s,r) = l8, (p = 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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(s) = r) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close
-- -- 10.1.1-(1) pc(s,r) = l8, (p = 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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(s) = r) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close
-- -- 10.1.1-(1) pc(s,r) = l8, (p = 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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(s) = r) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close
-- -- 10.1.1-(1) pc(s,r) = l8, (p = 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) = l8 .
eq (p = r) = false .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(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 .

eq q = r .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(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 .

eq (q = r) = false .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(s) = 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(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(s) = 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 .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
eq (p = r) = false .

eq z = r .
eq (glock(s) = 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 .

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(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
eq (p = r) = false .

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

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
eq (p = r) = false .

eq z = r .
eq glock(s) = 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 .
red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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 glock(s) = r .

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


-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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 (glock(s) = r) = false .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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 (glock(s) = r) = false .

eq (q = r) = false .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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 (glock(s) = r) = false .

eq (q = r) = false .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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 (glock(s) = r) = false .

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

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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 (glock(s) = r) = 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(chglk(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
close

-- -- 10.1.1-(1) pc(s,r) = l8, (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) = l8 .
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(chglk(s,r),p,q,z) .
close

-- ------------------------------10.2: pc(s,r) = l8, p = r----------------------
-- -- 10.3-(1) pc(s,r) = l8, 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) = l8 .
eq p = r .

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

-- -- 10.3-(1) pc(s,r) = l8, 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) = l8 .
eq p = r .

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

-- -- 10.3-(1) pc(s,r) = l8, 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) = l8 .
eq p = r .

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

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

-- -- 10.3-(1) pc(s,r) = l8, 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) = l8 .
eq p = r .

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

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


-- -- 10.3-(1) pc(s,r) = l8, 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) = l8 .
eq p = r .

eq (z = r) = false .
eq (glock(s) = 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(chglk(s,r),p,q,z) .
close

-- -- 10.3-(1) pc(s,r) = l8, 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) = l8 .
eq p = r .

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

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

-- -- 10.3-(1) pc(s,r) = l8, 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) = l8 .
eq p = r .

eq (z = r) = false .

eq glock(s) = 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(chglk(s,r),p,q,z) .
close


-- ------------------------------11.1: pc(s,r) = l9, p != r ----------------------
-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = r) = false .

eq z = r .

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close
-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close
-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close
-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close
-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close
-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close
-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = r) = false .

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


-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = 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 pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
eq (p = 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 .
red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red (inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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 pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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(go2rs(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- -- 11.1.1-(1) pc(s,r) = l9, (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) = l9 .
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 .
red ( inv19(s,p,q,z)) implies   inv19(go2rs(s,r),p,q,z) .
close

-- ------------------------------11.2: pc(s,r) = l9, p = r----------------------
-- -- 11.3-(1) pc(s,r) = l9, 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) = l9 .
eq p = r .

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

-- -- 11.3-(1) pc(s,r) = l9, 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) = l9 .
eq p = r .

eq (z = r) = false .

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

-- -- 11.3-(1) pc(s,r) = l9, 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) = l9 .
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(go2rs(s,r),p,q,z) .
close

-- ------------------------------12.1: pc(s,r) = l10, p != r ----------------------
-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

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

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close
-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close
-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close
-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = false .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close
-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = false .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close
-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = false .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close
-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

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

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .
eq z = r .

eq (next(s,r) = nop) = 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(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq (next(s,r) = nop) = 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(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq (next(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 .

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

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq (next(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 .

eq (q = r) = false  .

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

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq (next(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 .

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 .
red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq next(s,r) = nop .
eq q = r .
red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq next(s,r) = nop .
eq (q = r) = false .

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

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
eq (p = r) = false .

eq z = r .
eq next(s,r) = nop .
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 .
red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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 next(s,r) = nop .

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

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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 (next(s,r) = nop) = false .

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

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.1.1-(1) pc(s,r) = l10, (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) = l10 .
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 .
red ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close


-- ------------------------------12.2: pc(s,r) = l10, p = r----------------------
-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

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

-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

eq z = r .
eq next(s,r) = nop .
red   (inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

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

-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

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

-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

eq (z = r) = false .
eq (next(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 .
-- check
red   ( inv19(s,p,q,z)) implies   inv19(chnxt2(s,r),p,q,z) .
close

-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

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

eq q = r .

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

-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

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

eq (q = r) = false .

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

-- -- 12.3-(1) pc(s,r) = l10, 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) = l10 .
eq p = r .

eq (z = r) = false .

eq next(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(chnxt2(s,r),p,q,z) .
close

-- ------------------------------13.1: pc(s,r) = l11, p != r ----------------------
-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close
-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close
-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close
-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close
-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close
-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close
-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = r) = false .

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

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = 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 pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = 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 p = q .
red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = 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 (p = q) = false .

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

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
eq (p = 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 (p = q) = 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(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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 pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close

-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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(stlnx(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(stlnx(s,r),p,q,z) .
close


-- -- 13.1.1-(1) pc(s,r) = l11, (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) = l11 .
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 .

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

-- ------------------------------13.2: pc(s,r) = l11, p = r----------------------
-- -- 13.3-(1) pc(s,r) = l11, 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) = l11 .
eq p = r .

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

-- -- 13.3-(1) pc(s,r) = l11, 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) = l11 .
eq p = r .

eq (z = r) = false .

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

-- -- 13.3-(1) pc(s,r) = l11, 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) = l11 .
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(stlnx(s,r),p,q,z) .
close

-- ------------------------------14.1: pc(s,r) = l12, p != r ----------------------
-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = r) = false .

eq z = r .

eq pc(s,z) = l11 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close
-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close
-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = r) = false .

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

eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close
-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l8 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close
-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l7 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close
-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = r) = false .

eq z = r .
eq pc(s,z) = l6 .
eq pc(s,p) = l1 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close
-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = r) = false .

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


-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = 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 pc(s,z) = l11 . red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l10 . red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = cs .  red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
eq (p = 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 .
red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red (inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l2 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = rs . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l9 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,p) = l12 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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 pc(s,z) = l11 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l10 . red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l8 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l7 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = cs .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l6 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
eq pc(s,z) = l3 .  red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- -- 14.1.1-(1) pc(s,r) = l12, (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) = l12 .
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 .
red ( inv19(s,p,q,z)) implies   inv19(go2rs2(s,r),p,q,z) .
close

-- ------------------------------14.2: pc(s,r) = l12, p = r----------------------
-- -- 14.3-(1) pc(s,r) = l12, 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) = l12 .
eq p = r .

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

-- -- 14.3-(1) pc(s,r) = l12, 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) = l12 .
eq p = r .

eq (z = r) = false .

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

-- -- 14.3-(1) pc(s,r) = l12, 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) = l12 .
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(go2rs2(s,r),p,q,z) .
close