; @origtpdbfilename ./TRS/relative/rtL-cbn5.trs
; @xtcfilename "./TRS_Relative/Relative_05/rtL-cbn5.xml"
(format TRS)
(fun car 2)
(fun left 2)
(fun bot 0)
(fun right 2)
(fun new 0)
(fun ok 1)
(fun old 0)
(fun check 1)
(fun top 1)
(rule (top (ok (left (car x y) z))) (top (check (right y z))))
(rule (top (ok (right x (car y z)))) (top (check (left x z))))
(rule (top (ok (left bot x))) (top (check (right bot x))))
(rule (top (ok (right x bot))) (top (check (left x bot))))
(rule (top (ok (left (car x y) z))) (top (check (left y z))) :cost 0)
(rule (top (ok (right x (car y z)))) (top (check (right x z))) :cost 0)
(rule bot (car new bot) :cost 0)
(rule (check old) (ok old) :cost 0)
(rule (check (car x y)) (car (check x) y) :cost 0)
(rule (check (car x y)) (car x (check y)) :cost 0)
(rule (check (left x y)) (left (check x) y) :cost 0)
(rule (check (left x y)) (left x (check y)) :cost 0)
(rule (check (right x y)) (right (check x) y) :cost 0)
(rule (check (right x y)) (right x (check y)) :cost 0)
(rule (car (ok x) y) (ok (car x y)) :cost 0)
(rule (car x (ok y)) (ok (car x y)) :cost 0)
(rule (left (ok x) y) (ok (left x y)) :cost 0)
(rule (left x (ok y)) (ok (left x y)) :cost 0)
(rule (right (ok x) y) (ok (right x y)) :cost 0)
(rule (right x (ok y)) (ok (right x y)) :cost 0)