in mcs



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


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

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

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

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

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

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

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

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

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

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

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


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

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

eq next(s,r) = p .
-- check
red   (inv15(s,p,q)) implies  inv15(stprd(s,r),p,q) .
close

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

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

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

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


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

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

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

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

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

eq pred(s,r) = nop .
eq pc(s,p) = l1 . red   inv15(s,p,q) implies   inv15(chprd(s,r),p,q) .
eq pc(s,p) = l12 . red  inv15(s,p,q) implies   inv15(chprd(s,r),p,q) .
eq pc(s,p) = rs . red   inv15(s,p,q) implies   inv15(chprd(s,r),p,q) .
close

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

eq pred(s,r) = nop .
eq (pc(s,p) = l1) = false .
eq (pc(s,p) = rs) = false .
eq (pc(s,p) = l12) = false .
-- check
red  (inv15(s,p,q)) implies   inv15(chprd(s,r),p,q) .
close

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

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

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

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

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

-- 5. stlck(s,r)
-- 5.2.1 pc(s,r) = l4, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l4 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(stlck(s,r),p,q) .
close

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

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

eq pc(s,p) = l1 . red   inv15(s,p,q) implies   inv15(stlck(s,r),p,q) .
eq pc(s,p) = l12 . red  inv15(s,p,q) implies   inv15(stlck(s,r),p,q) .
eq pc(s,p) = rs . red   inv15(s,p,q) implies   inv15(stlck(s,r),p,q) .
close

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

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

-- 6. stnpr(s,r)
-- 6.2.1 pc(s,r) = l5, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(stnpr(s,r),p,q) .
close

-- -- 6.2.2 pc(s,r) = l5, (p = r) = false, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .
eq pred(s,r) = p .
eq next(s,r) = r .
-- check
red  (inv18(s,r) and  inv15(s,p,q)) implies  inv15(stnpr(s,r),p,q) .
close

-- -- 6.2.2 pc(s,r) = l5, (p = r) = false, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .
eq pred(s,r) = p .
eq (next(s,r) = r) = false .
-- check
red  ( inv15(s,p,q)) implies  inv15(stnpr(s,r),p,q) .
close

-- -- 6.2.2 pc(s,r) = l5, (p = r) = false, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l5 .
eq (p = r) = false .
eq q = r .
eq (pred(s,r) = p) = false .
eq pred(s,r) = r .
-- check
red  (inv14(s,r) and inv15(s,p,q)) implies  inv15(stnpr(s,r),p,q) .
close

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

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

eq pc(s,q) = l1 . red   inv15(s,p,q) implies inv15(stnpr(s,r),p,q) .
eq pc(s,q) = l12 . red   inv15(s,p,q) implies inv15(stnpr(s,r),p,q) .
eq pc(s,q) = rs . red   inv15(s,p,q) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .

eq next(s,q) = r .
-- check
red   (inv10(s,r,q) and inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .

eq (next(s,q) = r) = false .
eq next(s,p) = r .
-- check
red   (inv10(s,r,p) and inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .

eq (next(s,q) = r) = false .
eq (next(s,p) = r) = false .

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

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .

eq (next(s,q) = r) = false .
eq (next(s,p) = r) = false .

eq pred(s,r) = q .
eq (q = p) = false .
-- check
red   ( inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .

eq (next(s,q) = r) = false .
eq (next(s,p) = r) = false .

eq (pred(s,r) = q) = false .
eq pred(s,r) = p .
eq q = p .
-- check
red   ( inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .

eq (next(s,q) = r) = false .
eq (next(s,p) = r) = false .

eq (pred(s,r) = q) = false .
eq pred(s,r) = p .
eq (q = p) = false .
-- check
red   ( inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

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

eq (pred(s,r) = q) = false .
eq (pred(s,r) = p) = false .
-- check
red   ( inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

eq pc(s,q) = l1 . red   inv15(s,p,q) implies inv15(stnpr(s,r),p,q) .
eq pc(s,q) = l12 . red   inv15(s,p,q) implies inv15(stnpr(s,r),p,q) .
eq pc(s,q) = rs . red   inv15(s,p,q) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .
eq pred(s,r) = r .
-- check
red   (inv14(s,r) and inv18(s,r) and  inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .
eq (pred(s,r) = r) = false .
eq pred(s,r) = q .
-- check
red   (inv18(s,r) and inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .
eq (pred(s,r) = r) = false .
eq (pred(s,r) = q) = false .
-- check
red   (inv18(s,r) and inv15(s,p,q)) implies inv15(stnpr(s,r),p,q) .
close

-- 7. chlck(s,r)
-- 7.2.1 pc(s,r) = l6, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l6 .
eq p = r .
eq q = r .
-- check
red  inv15(s,p,q) implies inv15(chlck(s,r),p,q) .
close

-- -- 7.2.2 pc(s,r) = l6, (p = r) = false, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l6 .
eq (p = r) = false .
eq q = r .
eq lock(s,r) = true . red   inv15(s,p,q) implies   inv15(chlck(s,r),p,q) .
eq lock(s,r) = false . red    inv15(s,p,q)  implies   inv15(chlck(s,r),p,q) .
close

-- -- 7.2.3 pc(s,r) = l6, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l6 .
eq (p = r) = false .
eq (q = r) = false .
eq pc(s,q) = l1 . red   inv15(s,p,q) implies inv15(chlck(s,r),p,q) .
eq pc(s,q) = l12 . red   inv15(s,p,q) implies inv15(chlck(s,r),p,q) .
eq pc(s,q) = rs . red   inv15(s,p,q) implies inv15(chlck(s,r),p,q) .
close

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

-- -- 7.2.4.1 pc(s,r) = l6,  p = r, (q = r) = false, lock(s,r) = true .
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l6 .
eq (q = r) = false .
eq p = r .
eq lock(s,r) = true . red   inv15(s,p,q) implies   inv15(chlck(s,r),p,q) .
eq lock(s,r) = false . red    inv15(s,p,q)  implies   inv15(chlck(s,r),p,q) .
close


-- 8. exit(s,r)
-- 8.2.1 pc(s,r) = cs, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = cs .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(exit(s,r),p,q) .
close

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

-- -- 8.2.3 pc(s,r) = cs, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = cs .
eq (p = r) = false .
eq (q = r) = false .
eq pc(s,q) = l1 . red   inv15(s,p,q) implies inv15(exit(s,r),p,q) .
eq pc(s,q) = l12 . red   inv15(s,p,q) implies inv15(exit(s,r),p,q) .
eq pc(s,q) = rs . red   inv15(s,p,q) implies inv15(exit(s,r),p,q) .
close

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

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

-- 9. chnxt(s,r)
-- 9.2.1 pc(s,r) = l7, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l7 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(chnxt(s,r),p,q) .
close

-- -- 9.2.2.1 pc(s,r) = l7, (p = r) = false, q = r,  next(s,r) = nop
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l7 .
eq (p = r) = false .
eq q = r .
eq next(s,r) = nop .
-- check
red   ( inv15(s,p,q)) implies   inv15(chnxt(s,r),p,q) .
close

-- -- 9.2.2.2 pc(s,r) = l7, (p = r) = false, q = r,  next(s,r) != nop
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l7 .
eq (p = r) = false .
eq q = r .
eq (next(s,r) = nop) = false .
-- check
red   (inv15(s,p,q)) implies   inv15(chnxt(s,r),p,q) .
close

-- -- 9.2.3 pc(s,r) = l7, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l7 .
eq (p = r) = false .
eq (q = r) = false .
eq pc(s,q) = l1 . red   inv15(s,p,q) implies inv15(chnxt(s,r),p,q) .
eq pc(s,q) = l12 . red   inv15(s,p,q) implies inv15(chnxt(s,r),p,q) .
eq pc(s,q) = rs . red   inv15(s,p,q) implies inv15(chnxt(s,r),p,q) .
close

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

-- -- 9.2.4.1 pc(s,r) = l7,  p = r, (q = r) = false, next(s,r) != nop
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l7 .
eq (q = r) = false .
eq p = r .
eq (next(s,r) = nop) = false  .
-- check
red   inv15(s,p,q) implies   inv15(chnxt(s,r),p,q) .
close

-- -- 9.2.4.2 pc(s,r) = l7,  p = r, (q = r) = false, next(s,r) = nop
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l7 .
eq (q = r) = false .
eq p = r .
eq next(s,r) = nop  .
-- check
red   inv15(s,p,q) implies   inv15(chnxt(s,r),p,q) .
close

-- 10. chglk(s,r)
-- 10.2.1 pc(s,r) = l8, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l8 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(chglk(s,r),p,q) .
close


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


-- -- 10.2.2.2 pc(s,r) = l8, (p = r) = false, q = r, glock(s) != r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l8 .
eq (p = r) = false .
eq q = r .
eq (glock(s) = r) = false .
-- check
red   inv15(s,p,q) implies   inv15(chglk(s,r),p,q) .
close

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

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

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

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


-- 11. go2rs(s,r)
-- 11.2.1 pc(s,r) = l9, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l9 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(go2rs(s,r),p,q) .
close

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

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

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

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

-- 12. chnxt2(s,r)
-- 12.2.1 pc(s,r) = l10, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l10 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(chnxt2(s,r),p,q) .
close

-- -- 12.2.2.1a pc(s,r) = l10, (p = r) = false, q = r,
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l10 .
eq (p = r) = false .
eq q = r .
eq next(s,r) = nop .
-- check
red   ( inv15(s,p,q))  implies   inv15(chnxt2(s,r),p,q) .
close

-- -- 12.2.2.1b pc(s,r) = l10, (p = r) = false, q = r,
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l10 .
eq (p = r) = false .
eq q = r .
eq (next(s,r) = nop) = false .
-- check
red   (inv15(s,p,q))  implies   inv15(chnxt2(s,r),p,q) .
close

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

-- -- 12.2.3 pc(s,r) = l10, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l10 .
eq (p = r) = false .
eq (q = r) = false .
eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .
red   inv15(s,p,q) implies   inv15(chnxt2(s,r),p,q) .
close

-- -- 12.2.4 pc(s,r) = l10,  p = r, (q = r) = false,
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l10 .
eq (q = r) = false .
eq p = r .
eq (next(s,r) = nop) = false .
-- check
red   inv15(s,p,q) implies   inv15(chnxt2(s,r),p,q) .
close

-- -- 12.2.4 pc(s,r) = l10,  p = r, (q = r) = false,
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l10 .
eq (q = r) = false .
eq p = r .
eq next(s,r) = nop .
-- check
red   inv15(s,p,q) implies   inv15(chnxt2(s,r),p,q) .
close

-- 13. stlnx(s,r)
-- 13.2.1 pc(s,r) = l11, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l11 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(stlnx(s,r),p,q) .
close

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

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

eq pc(s,q) = l1 . red   inv15(s,p,q) implies inv15(stlnx(s,r),p,q) .
eq pc(s,q) = l12 . red   inv15(s,p,q) implies inv15(stlnx(s,r),p,q) .
eq pc(s,q) = rs . red   inv15(s,p,q) implies inv15(stlnx(s,r),p,q) .
close

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

eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .
-- check
red   (inv15(s,p,q)) implies   inv15(stlnx(s,r),p,q) .
close

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


-- 14. go2rs2(s,r)
-- 14.2.1 pc(s,r) = l12, p = r, q = r
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l12 .
eq p = r .
eq q = r .
-- check
red   inv15(s,p,q) implies   inv15(go2rs2(s,r),p,q) .
close

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

-- -- 14.2.3 pc(s,r) = l11, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l12 .
eq (p = r) = false .
eq (q = r) = false .
eq pc(s,q) = l1 . red   inv15(s,p,q) implies inv15(go2rs2(s,r),p,q) .
eq pc(s,q) = l12 . red   inv15(s,p,q) implies inv15(go2rs2(s,r),p,q) .
eq pc(s,q) = rs . red   inv15(s,p,q) implies inv15(go2rs2(s,r),p,q) .
close

-- -- 14.2.3 pc(s,r) = l11, (p = r) = false, (q = r) = false
open INV .
-- fresh constants
op s : -> Sys .
ops p q r : -> Pid .
-- induction hypothesis
eq [:nonexec] :   inv15(s,P:Pid,Q:Pid) = true .
-- assumptions
eq pc(s,r) = l12 .
eq (p = r) = false .
eq (q = r) = false .
eq (pc(s,q) = l1) = false .
eq (pc(s,q) = rs) = false .
eq (pc(s,q) = l12) = false .
red   inv15(s,p,q) implies inv15(go2rs2(s,r),p,q) .
close

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