Input TRS:
    1: R(x,RT()) -> RT()
    2: W(x,WT()) -> WT()
   e1: RB() ->= R(New(),RB())	[relative]
   e2: WB() ->= W(New(),WB())	[relative]
   e3: top(ok(sys(read(r1,R(t,r2)),write(WT(),WB()),p))) ->= top(check(sys(read(R(t,r1),r2),write(WT(),WB()),p)))	[relative]
   e4: top(ok(sys(read(RT(),RB()),write(WT(),W(t,w1)),p))) ->= top(check(sys(read(RT(),RB()),write(W(t,WT()),w1),p)))	[relative]
   e5: top(ok(sys(read(r1,R(t,r2)),write(WT(),w1),PR()))) ->= top(check(sys(read(R(t,r1),r2),write(WT(),w1),PW())))	[relative]
   e6: top(ok(sys(read(RT(),r2),write(WT(),W(t,w1)),PW()))) ->= top(check(sys(read(RT(),r2),write(W(t,WT()),w1),PR())))	[relative]
   e7: check(Old()) ->= ok(Old())	[relative]
   e8: check(R(x,y)) ->= R(check(x),y)	[relative]
   e9: check(R(x,y)) ->= R(x,check(y))	[relative]
   e10: check(W(x,y)) ->= W(check(x),y)	[relative]
   e11: check(W(x,y)) ->= W(x,check(y))	[relative]
   e12: check(read(x,y)) ->= read(check(x),y)	[relative]
   e13: check(read(x,y)) ->= read(x,check(y))	[relative]
   e14: check(write(x,y)) ->= write(check(x),y)	[relative]
   e15: check(write(x,y)) ->= write(x,check(y))	[relative]
   e16: check(sys(x,y,z)) ->= sys(check(x),y,z)	[relative]
   e17: check(sys(x,y,z)) ->= sys(x,check(y),z)	[relative]
   e18: check(sys(x,y,z)) ->= sys(x,y,check(z))	[relative]
   e19: R(ok(x),y) ->= ok(R(x,y))	[relative]
   e20: R(x,ok(y)) ->= ok(R(x,y))	[relative]
   e21: W(ok(x),y) ->= ok(W(x,y))	[relative]
   e22: W(x,ok(y)) ->= ok(W(x,y))	[relative]
   e23: read(ok(x),y) ->= ok(read(x,y))	[relative]
   e24: read(x,ok(y)) ->= ok(read(x,y))	[relative]
   e25: write(ok(x),y) ->= ok(write(x,y))	[relative]
   e26: write(x,ok(y)) ->= ok(write(x,y))	[relative]
   e27: sys(ok(x),y,z) ->= ok(sys(x,y,z))	[relative]
   e28: sys(x,ok(y),z) ->= ok(sys(x,y,z))	[relative]
   e29: sys(x,y,ok(z)) ->= ok(sys(x,y,z))	[relative]
Weak rule e20 calls a strict rule