; @origtpdbfilename ./TRS/relative/rtL-rw5.trs
; @xtcfilename "./TRS_Relative/Relative_05/rtL-rw5.xml"
(format TRS)
(fun R 2)
(fun write 2)
(fun read 2)
(fun PR 0)
(fun New 0)
(fun Old 0)
(fun PW 0)
(fun RB 0)
(fun W 2)
(fun sys 3)
(fun ok 1)
(fun WB 0)
(fun check 1)
(fun RT 0)
(fun top 1)
(fun WT 0)
(rule (R x RT) RT)
(rule (W x WT) WT)
(rule RB (R New RB) :cost 0)
(rule WB (W New WB) :cost 0)
(rule (top (ok (sys (read r1 (R t r2)) (write WT WB) p))) (top (check (sys (read (R t r1) r2) (write WT WB) p))) :cost 0)
(rule (top (ok (sys (read RT RB) (write WT (W t w1)) p))) (top (check (sys (read RT RB) (write (W t WT) w1) p))) :cost 0)
(rule (top (ok (sys (read r1 (R t r2)) (write WT w1) PR))) (top (check (sys (read (R t r1) r2) (write WT w1) PW))) :cost 0)
(rule (top (ok (sys (read RT r2) (write WT (W t w1)) PW))) (top (check (sys (read RT r2) (write (W t WT) w1) PR))) :cost 0)
(rule (check Old) (ok Old) :cost 0)
(rule (check (R x y)) (R (check x) y) :cost 0)
(rule (check (R x y)) (R x (check y)) :cost 0)
(rule (check (W x y)) (W (check x) y) :cost 0)
(rule (check (W x y)) (W x (check y)) :cost 0)
(rule (check (read x y)) (read (check x) y) :cost 0)
(rule (check (read x y)) (read x (check y)) :cost 0)
(rule (check (write x y)) (write (check x) y) :cost 0)
(rule (check (write x y)) (write x (check y)) :cost 0)
(rule (check (sys x y z)) (sys (check x) y z) :cost 0)
(rule (check (sys x y z)) (sys x (check y) z) :cost 0)
(rule (check (sys x y z)) (sys x y (check z)) :cost 0)
(rule (R (ok x) y) (ok (R x y)) :cost 0)
(rule (R x (ok y)) (ok (R x y)) :cost 0)
(rule (W (ok x) y) (ok (W x y)) :cost 0)
(rule (W x (ok y)) (ok (W x y)) :cost 0)
(rule (read (ok x) y) (ok (read x y)) :cost 0)
(rule (read x (ok y)) (ok (read x y)) :cost 0)
(rule (write (ok x) y) (ok (write x y)) :cost 0)
(rule (write x (ok y)) (ok (write x y)) :cost 0)
(rule (sys (ok x) y z) (ok (sys x y z)) :cost 0)
(rule (sys x (ok y) z) (ok (sys x y z)) :cost 0)
(rule (sys x y (ok z)) (ok (sys x y z)) :cost 0)