; @origtpdbfilename ./TRS/AProVE/Liveness_WRS.trs
; @xtcfilename "./TRS_Standard/AProVE_04/Liveness_WRS.xml"
(format TRS)
(fun active 1)
(fun f 1)
(fun mark 1)
(fun chk 1)
(fun no 1)
(fun mat 2)
(fun X 0)
(fun y 0)
(fun c 0)
(fun tp 1)
(rule (active (f x)) (mark (f (f x))))
(rule (chk (no (f x))) (f (chk (mat (f (f (f (f (f (f (f (f (f (f X)))))))))) x))))
(rule (mat (f x) (f y)) (f (mat x y)))
(rule (chk (no c)) (active c))
(rule (mat (f x) c) (no c))
(rule (f (active x)) (active (f x)))
(rule (f (no x)) (no (f x)))
(rule (f (mark x)) (mark (f x)))
(rule (tp (mark x)) (tp (chk (mat (f (f (f (f (f (f (f (f (f (f X)))))))))) x))))