; @origtpdbfilename ./TRS/Koprowski/abp.trs
; @xtcfilename "./TRS_Relative/Mixed_relative_TRS/abp.xml"
(format TRS)
(fun f 1)
(fun |0| 0)
(fun sys 4)
(fun S 2)
(fun nils 0)
(fun old 0)
(fun p 2)
(fun r 1)
(fun c 2)
(fun T 1)
(fun bot 0)
(fun |1| 0)
(fun new 0)
(fun ok 1)
(fun check 1)
(rule (T (ok (sys x (p d |0|) (r |0|) y))) (T (check (sys x bot (r |1|) y))))
(rule (T (ok (sys x (p d |1|) (r |1|) y))) (T (check (sys x bot (r |0|) y))))
(rule (T (ok (sys (S |0| (c d ds)) bot y z))) (T (check (sys (S |0| (c d ds)) (p d |0|) y z))) :cost 0)
(rule (T (ok (sys (S |1| (c d ds)) bot y z))) (T (check (sys (S |0| (c d ds)) (p d |1|) y z))) :cost 0)
(rule (T (ok (sys (S |0| (c d ds)) x y (f |0|)))) (T (check (sys (S |1| ds) x y bot))) :cost 0)
(rule (T (ok (sys (S |1| (c d ds)) x y (f |1|)))) (T (check (sys (S |0| ds) x y bot))) :cost 0)
(rule (T (ok (sys x y (r |0|) bot))) (T (check (sys x y (r |0|) (f |1|)))) :cost 0)
(rule (T (ok (sys x y (r |1|) bot))) (T (check (sys x y (r |1|) (f |0|)))) :cost 0)
(rule nils (c new nils) :cost 0)
(rule (p d b) bot :cost 0)
(rule (f b) bot :cost 0)
(rule (check old) (ok old) :cost 0)
(rule (check (r v1)) (r (check v1)) :cost 0)
(rule (r (ok v1)) (ok (r v1)) :cost 0)
(rule (check (f v1)) (f (check v1)) :cost 0)
(rule (f (ok v1)) (ok (f v1)) :cost 0)
(rule (check (p v1 v2)) (p v1 (check v2)) :cost 0)
(rule (check (p v1 v2)) (p (check v1) v2) :cost 0)
(rule (p v1 (ok v2)) (ok (p v1 v2)) :cost 0)
(rule (p (ok v1) v2) (ok (p v1 v2)) :cost 0)
(rule (check (c v1 v2)) (c v1 (check v2)) :cost 0)
(rule (check (c v1 v2)) (c (check v1) v2) :cost 0)
(rule (c v1 (ok v2)) (ok (c v1 v2)) :cost 0)
(rule (c (ok v1) v2) (ok (c v1 v2)) :cost 0)
(rule (check (S v1 v2)) (S v1 (check v2)) :cost 0)
(rule (check (S v1 v2)) (S (check v1) v2) :cost 0)
(rule (S v1 (ok v2)) (ok (S v1 v2)) :cost 0)
(rule (S (ok v1) v2) (ok (S v1 v2)) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys v1 v2 v3 (check v4)) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys v1 v2 (check v3) v4) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys v1 (check v2) v3 v4) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys (check v1) v2 v3 v4) :cost 0)
(rule (sys v1 v2 v3 (ok v4)) (ok (sys v1 v2 v3 v4)) :cost 0)
(rule (sys v1 v2 (ok v3) v4) (ok (sys v1 v2 v3 v4)) :cost 0)
(rule (sys v1 (ok v2) v3 v4) (ok (sys v1 v2 v3 v4)) :cost 0)
(rule (sys (ok v1) v2 v3 v4) (ok (sys v1 v2 v3 v4)) :cost 0)