in mcs



--
-- ------------------- proof inv16 -------------------
--


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


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

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

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

-- 2. stnxt(s,r)
-- -- 1.1 pc(s,r) != l1
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P ) = true .
eq (pc(s,r) = l1) = false .
-- check
red inv16(s,p) implies inv16(stnxt(s,r),p) .
close


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

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

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

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

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

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

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

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

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

-- 5. stlck(s,r)
-- -- 5.1 pc(s,r) != l4
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = l4) = false .
-- check
red inv16(s,p ) implies inv16(stlck(s,r),p ) .
close

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

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

-- 6. stnpr(s,r)
-- -- 6.1 pc(s,r) != l5
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = l5) = false .
-- check
red inv16(s,p ) implies inv16(stnpr(s,r),p ) .
close

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

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

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

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

-- 7. chlck(s,r)
-- -- 7.1 pc(s,r) != l6
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = l6) = false .
-- check
red inv16(s,p ) implies inv16(chlck(s,r),p ) .
close

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

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

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


-- 8. exit(s,r)
-- -- 8.1 pc(s,r) != cs
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = cs) = false .
-- check
red inv16(s,p ) implies inv16(exit(s,r),p ) .
close

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

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

-- 9. chnxt(s,r)
-- -- 9.1 pc(s,r) != l7
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = l7) = false .
-- check
red inv16(s,p ) implies inv16(chnxt(s,r),p ) .
close

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

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

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

-- 10. chglk(s,r)
-- -- 10.1 pc(s,r) != l8
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = l8) = false .
-- check
red inv16(s,p ) implies inv16(chglk(s,r),p ) .
close


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

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

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

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

-- 11. go2rs(s,r)
-- -- 11.1 pc(s,r) != l9
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = l9) = false .
-- check
red inv16(s,p ) implies inv16(go2rs(s,r),p ) .
close

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

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


-- 12. chnxt2(s,r)
-- -- 10.1 pc(s,r) != l10
open INV .
op s : -> Sys .
ops p r  : -> Pid .
-- induction hypothesis
eq [:nonexec] : inv16(s,P:Pid  ) = true .
eq (pc(s,r) = l10) = false .
-- check
red inv16(s,p ) implies inv16(chnxt2(s,r),p ) .
close

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

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

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

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

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

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

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

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

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


eof .