; @origtpdbfilename ./TRS/Koprowski/rt-rw4.trs
; @xtcfilename "./TRS_Relative/Mixed_relative_TRS/rt-rw4.xml"
(format TRS)
(fun write 2)
(fun R 0)
(fun Rw 0)
(fun WAo 1)
(fun read 2)
(fun RIn 1)
(fun sys_w 2)
(fun RIo 1)
(fun WIo 1)
(fun sys_r 2)
(fun RAo 1)
(fun WAn 1)
(fun RAn 1)
(fun W 0)
(fun Ww 0)
(fun WIn 1)
(fun ok 1)
(fun check 1)
(fun top 1)
(rule (RAo R) R)
(rule (RAn R) R)
(rule (WAo W) W)
(rule (WAn W) W)
(rule Rw (RIn Rw) :cost 0)
(rule Ww (WIn Ww) :cost 0)
(rule (top (ok (sys_r (read r (RIo x)) (write W Ww)))) (top (check (sys_r (read (RAo r) x) (write W Ww)))) :cost 0)
(rule (top (ok (sys_w (read r (RIo x)) (write W Ww)))) (top (check (sys_w (read (RAo r) x) (write W Ww)))) :cost 0)
(rule (top (ok (sys_r (read r (RIn x)) (write W Ww)))) (top (check (sys_r (read (RAn r) x) (write W Ww)))) :cost 0)
(rule (top (ok (sys_w (read r (RIn x)) (write W Ww)))) (top (check (sys_w (read (RAn r) x) (write W Ww)))) :cost 0)
(rule (top (ok (sys_r (read R Rw) (write W (WIn y))))) (top (check (sys_r (read R Rw) (write (WAn W) y)))) :cost 0)
(rule (top (ok (sys_w (read R Rw) (write W (WIn y))))) (top (check (sys_w (read R Rw) (write (WAn W) y)))) :cost 0)
(rule (top (ok (sys_r (read R Rw) (write W (WIo y))))) (top (check (sys_r (read R Rw) (write (WAo W) y)))) :cost 0)
(rule (top (ok (sys_w (read R Rw) (write W (WIo y))))) (top (check (sys_w (read R Rw) (write (WAo W) y)))) :cost 0)
(rule (top (ok (sys_r (read r (RIo x)) (write W y)))) (top (check (sys_w (read (RAo r) x) (write W y)))) :cost 0)
(rule (top (ok (sys_r (read r (RIn x)) (write W y)))) (top (check (sys_w (read (RAn r) x) (write W y)))) :cost 0)
(rule (top (ok (sys_w (read R x) (write W (WIo y))))) (top (check (sys_r (read R x) (write (WAo W) y)))) :cost 0)
(rule (top (ok (sys_w (read R x) (write W (WIn y))))) (top (check (sys_r (read R x) (write (WAn W) y)))) :cost 0)
(rule (check (RIo x)) (ok (RIo x)) :cost 0)
(rule (check (RAo x)) (RAo (check x)) :cost 0)
(rule (check (RAn x)) (RAn (check x)) :cost 0)
(rule (check (WAo x)) (WAo (check x)) :cost 0)
(rule (check (WAn x)) (WAn (check x)) :cost 0)
(rule (check (RIo x)) (RIo (check x)) :cost 0)
(rule (check (RIn x)) (RIn (check x)) :cost 0)
(rule (check (WIo x)) (WIo (check x)) :cost 0)
(rule (check (WIn x)) (WIn (check x)) :cost 0)
(rule (check (sys_r x y)) (sys_r (check x) y) :cost 0)
(rule (check (sys_r x y)) (sys_r x (check y)) :cost 0)
(rule (check (sys_w x y)) (sys_w (check x) y) :cost 0)
(rule (check (sys_w x y)) (sys_w x (check y)) :cost 0)
(rule (RAo (ok x)) (ok (RAo x)) :cost 0)
(rule (RAn (ok x)) (ok (RAn x)) :cost 0)
(rule (WAo (ok x)) (ok (WAo x)) :cost 0)
(rule (WAn (ok x)) (ok (WAn x)) :cost 0)
(rule (RIn (ok x)) (ok (RIn x)) :cost 0)
(rule (WIo (ok x)) (ok (WIo x)) :cost 0)
(rule (WIn (ok x)) (ok (WIn x)) :cost 0)
(rule (sys_r (ok x) y) (ok (sys_r x y)) :cost 0)
(rule (sys_r x (ok y)) (ok (sys_r x y)) :cost 0)
(rule (sys_w (ok x) y) (ok (sys_w x y)) :cost 0)
(rule (sys_w x (ok y)) (ok (sys_w x y)) :cost 0)