; @origtpdbfilename ./TRS/relative/rtL-rw2.trs
; @xtcfilename "./TRS_Relative/Relative_05/rtL-rw2.xml"
(format TRS)
(fun R 0)
(fun Rw 0)
(fun WAo 1)
(fun RIn 1)
(fun RIo 1)
(fun WIo 1)
(fun PR 0)
(fun PW 0)
(fun RAo 1)
(fun WAn 1)
(fun system 5)
(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 (system r W (RIo x) Ww p))) (top (check (system (RAo r) W x Ww p))) :cost 0)
(rule (top (ok (system r W (RIn x) Ww p))) (top (check (system (RAn r) W x Ww p))) :cost 0)
(rule (top (ok (system R W Rw (WIn y) p))) (top (check (system R (WAn W) Rw y p))) :cost 0)
(rule (top (ok (system R W Rw (WIo y) p))) (top (check (system R (WAo W) Rw y p))) :cost 0)
(rule (top (ok (system r W (RIo x) y PR))) (top (check (system (RAo r) W x y PW))) :cost 0)
(rule (top (ok (system r W (RIn x) y PR))) (top (check (system (RAn r) W x y PW))) :cost 0)
(rule (top (ok (system R W x (WIo y) PW))) (top (check (system R (WAo W) x y PR))) :cost 0)
(rule (top (ok (system R W x (WIn y) PW))) (top (check (system R (WAn W) x y PR))) :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 (system v1 v2 v3 v4 v5)) (system (check v1) v2 v3 v4 v5) :cost 0)
(rule (check (system v1 v2 v3 v4 v5)) (system v1 (check v2) v3 v4 v5) :cost 0)
(rule (check (system v1 v2 v3 v4 v5)) (system v1 v2 (check v3) v4 v5) :cost 0)
(rule (check (system v1 v2 v3 v4 v5)) (system v1 v2 v3 (check v4) v5) :cost 0)
(rule (check (system v1 v2 v3 v4 v5)) (system v1 v2 v3 v4 (check v5)) :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 (RIo (ok x)) (ok (RIo 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 (system (ok v1) v2 v3 v4 v5) (ok (system v1 v2 v3 v4 v5)) :cost 0)
(rule (system v1 (ok v2) v3 v4 v5) (ok (system v1 v2 v3 v4 v5)) :cost 0)
(rule (system v1 v2 (ok v3) v4 v5) (ok (system v1 v2 v3 v4 v5)) :cost 0)
(rule (system v1 v2 v3 (ok v4) v5) (ok (system v1 v2 v3 v4 v5)) :cost 0)
(rule (system v1 v2 v3 v4 (ok v5)) (ok (system v1 v2 v3 v4 v5)) :cost 0)