YES Problem: strict: RAo(R()) -> R() RAn(R()) -> R() WAo(W()) -> W() WAn(W()) -> W() weak: Rw() -> RIn(Rw()) Ww() -> WIn(Ww()) top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> top(check(sys_w(read(RAo(r),x),write(W(),y)))) top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> top(check(sys_w(read(RAn(r),x),write(W(),y)))) top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),x),write(WAo(W()),y)))) top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),x),write(WAn(W()),y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x,y)) -> sys_r(check(x),y) check(sys_r(x,y)) -> sys_r(x,check(y)) check(sys_w(x,y)) -> sys_w(check(x),y) check(sys_w(x,y)) -> sys_w(x,check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x),y) -> ok(sys_r(x,y)) sys_r(x,ok(y)) -> ok(sys_r(x,y)) sys_w(ok(x),y) -> ok(sys_w(x,y)) sys_w(x,ok(y)) -> ok(sys_w(x,y)) Proof: Bounds Processor: bound: 2 enrichment: match-rt automaton: final states: {2} transitions: R0() -> 2* read1(28,2) -> 29* read1(78,11) -> 29* read1(78,2) -> 29* read1(28,11) -> 29* top0(2) -> 2* Ww1() -> 26* check0(2) -> 2* check2(83) -> 83* check2(92) -> 92* W1() -> 10* WAo1(10) -> 77* sys_r1(29,108) -> 31* sys_r1(101,27) -> 31* sys_r1(29,27) -> 30* RIn0(2) -> 2* Ww2() -> 92* check1(29) -> 101* check1(26) -> 26* check1(30) -> 31* check1(11) -> 11* check1(27) -> 108* sys_w0(2,2) -> 2* WIo0(2) -> 2* RAn0(2) -> 2* RIo0(2) -> 2* WAn0(2) -> 2* write1(77,2) -> 27* write1(10,26) -> 27* write1(77,26) -> 27* sys_w1(29,108) -> 31* sys_w1(101,27) -> 31* sys_w1(29,27) -> 30* W0() -> 2* RIn1(11) -> 2* WIn0(2) -> 2* W2() -> 79* WAn1(10) -> 77* WAo0(2) -> 2* RAn1(2) -> 28* write0(2,2) -> 2* RIn2(83) -> 83,11 sys_r0(2,2) -> 2* WIn2(92) -> 92,26 R1() -> 28,78 Ww0() -> 2* Rw2() -> 83* ok0(2) -> 2* ok1(28) -> 28* RAo1(2) -> 28* WIn1(26) -> 2* top1(31) -> 2* Rw0() -> 2* Rw1() -> 11* RAo0(2) -> 2* read0(2,2) -> 2* 79 -> 77* 10 -> 2* problem: strict: RAo(R()) -> R() RAn(R()) -> R() WAo(W()) -> W() weak: Rw() -> RIn(Rw()) Ww() -> WIn(Ww()) top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> top(check(sys_w(read(RAo(r),x),write(W(),y)))) top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> top(check(sys_w(read(RAn(r),x),write(W(),y)))) top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),x),write(WAo(W()),y)))) top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),x),write(WAn(W()),y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x,y)) -> sys_r(check(x),y) check(sys_r(x,y)) -> sys_r(x,check(y)) check(sys_w(x,y)) -> sys_w(check(x),y) check(sys_w(x,y)) -> sys_w(x,check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x),y) -> ok(sys_r(x,y)) sys_r(x,ok(y)) -> ok(sys_r(x,y)) sys_w(ok(x),y) -> ok(sys_w(x,y)) sys_w(x,ok(y)) -> ok(sys_w(x,y)) Bounds Processor: bound: 2 enrichment: match-rt automaton: final states: {1} transitions: R0() -> 1* read1(56,10) -> 28* read1(27,10) -> 28* read1(27,1) -> 28* read1(56,1) -> 28* top0(1) -> 1* Ww1() -> 19* check0(1) -> 1* check2(63) -> 63* check2(66) -> 66* W1() -> 7* WAo1(7) -> 55* sys_r1(75,26) -> 30* sys_r1(28,78) -> 30* sys_r1(28,26) -> 29* RIn0(1) -> 1* Ww2() -> 66* check1(19) -> 19* check1(29) -> 30* check1(28) -> 75* check1(26) -> 78* check1(10) -> 10* sys_w0(1,1) -> 1* WIo0(1) -> 1* RAn0(1) -> 1* RIo0(1) -> 1* WAn0(1) -> 1* write1(55,19) -> 26* write1(7,1) -> 26* write1(55,1) -> 26* write1(7,19) -> 26* sys_w1(28,26) -> 29* sys_w1(75,26) -> 30* sys_w1(28,78) -> 30* W0() -> 1* RIn1(10) -> 1* WIn0(1) -> 1* W2() -> 59* WAn1(7) -> 55* WAo0(1) -> 1* RAn1(1) -> 27* write0(1,1) -> 1* RIn2(63) -> 63,10 sys_r0(1,1) -> 1* WIn2(66) -> 66,19 R1() -> 27,56 Ww0() -> 1* Rw2() -> 63* ok0(1) -> 1* ok1(27) -> 27* RAo1(1) -> 27* WIn1(19) -> 1* top1(30) -> 1* Rw0() -> 1* Rw1() -> 10* RAo0(1) -> 1* read0(1,1) -> 1* 7 -> 1* 59 -> 55* problem: strict: RAo(R()) -> R() RAn(R()) -> R() weak: Rw() -> RIn(Rw()) Ww() -> WIn(Ww()) top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> top(check(sys_w(read(RAo(r),x),write(W(),y)))) top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> top(check(sys_w(read(RAn(r),x),write(W(),y)))) top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),x),write(WAo(W()),y)))) top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),x),write(WAn(W()),y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x,y)) -> sys_r(check(x),y) check(sys_r(x,y)) -> sys_r(x,check(y)) check(sys_w(x,y)) -> sys_w(check(x),y) check(sys_w(x,y)) -> sys_w(x,check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x),y) -> ok(sys_r(x,y)) sys_r(x,ok(y)) -> ok(sys_r(x,y)) sys_w(ok(x),y) -> ok(sys_w(x,y)) sys_w(x,ok(y)) -> ok(sys_w(x,y)) Bounds Processor: bound: 2 enrichment: match-rt automaton: final states: {2} transitions: R0() -> 2* read1(6,2) -> 18* read1(6,7) -> 18* read1(2,2) -> 18* top0(2) -> 2* Ww1() -> 14* check0(2) -> 2* check2(52) -> 52* check2(49) -> 49* W1() -> 15* WAo1(15) -> 16* WAo1(2) -> 2* sys_r1(18,48) -> 20* sys_r1(43,17) -> 20* sys_r1(2,2) -> 2* sys_r1(18,17) -> 19* RIn0(2) -> 2* Ww2() -> 52* check1(7) -> 7* check1(18) -> 43* check1(19) -> 20* check1(14) -> 14* check1(17) -> 48* check1(2) -> 2* sys_w0(2,2) -> 2* WIo0(2) -> 2* RAn0(2) -> 2* RIo0(2) -> 2* WAn0(2) -> 2* write1(16,2) -> 17* write1(15,14) -> 17* write1(15,2) -> 17* write1(16,14) -> 17* sys_w1(18,17) -> 19* sys_w1(2,2) -> 2* sys_w1(18,48) -> 20* sys_w1(43,17) -> 20* W0() -> 2* RIn1(2) -> 2* RIn1(7) -> 7,2 WIn0(2) -> 2* WAn1(15) -> 16* WAn1(2) -> 2* WAo0(2) -> 2* RAn1(2) -> 6* write0(2,2) -> 2* RIn2(49) -> 49,7 sys_r0(2,2) -> 2* WIo1(2) -> 2* WIn2(52) -> 52,14 R1() -> 6* Ww0() -> 2* Rw2() -> 49* R2() -> 40* RIo1(2) -> 6* ok0(2) -> 2* ok1(2) -> 2* ok1(6) -> 6* RAo1(2) -> 2* WIn1(14) -> 14,2 WIn1(2) -> 2* top1(20) -> 2* Rw0() -> 2* Rw1() -> 7* RAo0(2) -> 2* read0(2,2) -> 2* 6 -> 2* 40 -> 6* problem: strict: RAo(R()) -> R() weak: Rw() -> RIn(Rw()) Ww() -> WIn(Ww()) top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> top(check(sys_w(read(RAo(r),x),write(W(),y)))) top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> top(check(sys_w(read(RAn(r),x),write(W(),y)))) top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),x),write(WAo(W()),y)))) top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),x),write(WAn(W()),y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x,y)) -> sys_r(check(x),y) check(sys_r(x,y)) -> sys_r(x,check(y)) check(sys_w(x,y)) -> sys_w(check(x),y) check(sys_w(x,y)) -> sys_w(x,check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x),y) -> ok(sys_r(x,y)) sys_r(x,ok(y)) -> ok(sys_r(x,y)) sys_w(ok(x),y) -> ok(sys_w(x,y)) sys_w(x,ok(y)) -> ok(sys_w(x,y)) Bounds Processor: bound: 1 enrichment: match-rt automaton: final states: {1} transitions: R0() -> 1* read1(3,6) -> 18* read1(22,6) -> 23* read1(3,1) -> 18* top0(1) -> 1* Ww1() -> 7* check0(1) -> 1* W1() -> 15* WAo1(15) -> 16* sys_r1(26,17) -> 20* sys_r1(23,29) -> 20* sys_r1(28,21) -> 20* sys_r1(23,21) -> 19* sys_r1(18,27) -> 20* sys_r1(18,17) -> 19* RIn0(1) -> 1* check1(7) -> 7* check1(18) -> 26* check1(19) -> 20* check1(21) -> 29* check1(17) -> 27* check1(6) -> 6* check1(23) -> 28* sys_w0(1,1) -> 1* RIo0(1) -> 1* RAn0(1) -> 1* WIo0(1) -> 1* WAn0(1) -> 1* write1(16,1) -> 17* write1(15,7) -> 21* write1(15,1) -> 21* write1(16,7) -> 17* sys_w1(18,17) -> 19* sys_w1(18,27) -> 20* sys_w1(28,21) -> 20* sys_w1(23,29) -> 20* sys_w1(23,21) -> 19* sys_w1(26,17) -> 20* W0() -> 1* RIn1(6) -> 6,1 WIn0(1) -> 1* WAn1(15) -> 16* WAo0(1) -> 1* RAn1(1) -> 22* write0(1,1) -> 1* sys_r0(1,1) -> 1* R1() -> 3* Ww0() -> 1* ok0(1) -> 1* ok1(22) -> 22* WIn1(7) -> 7,1 top1(20) -> 1* Rw0() -> 1* Rw1() -> 6* read0(1,1) -> 1* RAo0(1) -> 1* 3 -> 1* problem: strict: weak: Rw() -> RIn(Rw()) Ww() -> WIn(Ww()) top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAo(r),x),write(W(),Ww())))) top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_r(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> top(check(sys_w(read(RAn(r),x),write(W(),Ww())))) top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAn(W()),y)))) top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> top(check(sys_w(read(R(),Rw()),write(WAo(W()),y)))) top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> top(check(sys_w(read(RAo(r),x),write(W(),y)))) top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> top(check(sys_w(read(RAn(r),x),write(W(),y)))) top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> top(check(sys_r(read(R(),x),write(WAo(W()),y)))) top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> top(check(sys_r(read(R(),x),write(WAn(W()),y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x,y)) -> sys_r(check(x),y) check(sys_r(x,y)) -> sys_r(x,check(y)) check(sys_w(x,y)) -> sys_w(check(x),y) check(sys_w(x,y)) -> sys_w(x,check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x),y) -> ok(sys_r(x,y)) sys_r(x,ok(y)) -> ok(sys_r(x,y)) sys_w(ok(x),y) -> ok(sys_w(x,y)) sys_w(x,ok(y)) -> ok(sys_w(x,y)) Qed