; @origtpdbfilename ./TRS/relative/rtL-evnz.trs
; @xtcfilename "./TRS_Relative/Relative_05/rtL-evnz.xml"
(format TRS)
(fun N 1)
(fun U 2)
(fun E 0)
(fun O 1)
(fun F 2)
(fun ok 1)
(fun check 1)
(fun B 0)
(fun top 1)
(fun D 2)
(rule (top (ok (U x y))) (top (check (D x y))))
(rule (D x B) (U x B))
(rule (F x (U (O y) z)) (U x (F y z)))
(rule (F x (U (N y) z)) (U x (F y z)))
(rule (D (O x) (F y z)) (F x (D y z)))
(rule (D (N x) (F y z)) (F x (D y z)))
(rule (F x (U E y)) (U x (F E y)))
(rule (D E (F x y)) (F E (D x y)))
(rule (U (O x) y) (U x y) :cost 0)
(rule (U (N x) y) (U x y) :cost 0)
(rule (D (O x) y) (D x y) :cost 0)
(rule (D (N x) y) (D x y) :cost 0)
(rule E (N E) :cost 0)
(rule (check (O x)) (ok (O x)) :cost 0)
(rule (check (U x y)) (U (check x) y) :cost 0)
(rule (check (U x y)) (U x (check y)) :cost 0)
(rule (check (D x y)) (D (check x) y) :cost 0)
(rule (check (D x y)) (D x (check y)) :cost 0)
(rule (check (F x y)) (F (check x) y) :cost 0)
(rule (check (F x y)) (F x (check y)) :cost 0)
(rule (check (O x)) (O (check x)) :cost 0)
(rule (check (N x)) (N (check x)) :cost 0)
(rule (U (ok x) y) (ok (U x y)) :cost 0)
(rule (U x (ok y)) (ok (U x y)) :cost 0)
(rule (D (ok x) y) (ok (D x y)) :cost 0)
(rule (D x (ok y)) (ok (D x y)) :cost 0)
(rule (F (ok x) y) (ok (F x y)) :cost 0)
(rule (F x (ok y)) (ok (F x y)) :cost 0)
(rule (O (ok x)) (ok (O x)) :cost 0)
(rule (N (ok x)) (ok (N x)) :cost 0)