(VAR r x y )
(RULES 
        RAo(R) -> R
        RAn(R) -> R
        WAo(W) -> W
        WAn(W) -> W
        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))
)