; @origtpdbfilename ./TRS/AProVE/JFP_Ex31.trs
; @xtcfilename "./TRS_Standard/AProVE_04/JFP_Ex31.xml"
(format TRS)
(fun active 1)
(fun f 3)
(fun b 0)
(fun c 0)
(fun mark 1)
(fun d 0)
(fun m 1)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (f b c x)) (mark (f x x x)))
(rule (active (f x y z)) (f x y (active z)))
(rule (active d) (m b))
(rule (f x y (mark z)) (mark (f x y z)))
(rule (active d) (mark c))
(rule (proper b) (ok b))
(rule (proper c) (ok c))
(rule (proper d) (ok d))
(rule (proper (f x y z)) (f (proper x) (proper y) (proper z)))
(rule (f (ok x) (ok y) (ok z)) (ok (f x y z)))
(rule (top (mark x)) (top (proper x)))
(rule (top (ok x)) (top (active x)))