; @origtpdbfilename ./TRS/TRCSR/Ex15_Luc98_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex15_Luc98_C.xml"
(format TRS)
(fun active 1)
(fun and 2)
(fun true 0)
(fun mark 1)
(fun false 0)
(fun if 3)
(fun add 2)
(fun |0| 0)
(fun s 1)
(fun first 2)
(fun nil 0)
(fun cons 2)
(fun from 1)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (and true X)) (mark X))
(rule (active (and false Y)) (mark false))
(rule (active (if true X Y)) (mark X))
(rule (active (if false X Y)) (mark Y))
(rule (active (add |0| X)) (mark X))
(rule (active (add (s X) Y)) (mark (s (add X Y))))
(rule (active (first |0| X)) (mark nil))
(rule (active (first (s X) (cons Y Z))) (mark (cons Y (first X Z))))
(rule (active (from X)) (mark (cons X (from (s X)))))
(rule (active (and X1 X2)) (and (active X1) X2))
(rule (active (if X1 X2 X3)) (if (active X1) X2 X3))
(rule (active (add X1 X2)) (add (active X1) X2))
(rule (active (first X1 X2)) (first (active X1) X2))
(rule (active (first X1 X2)) (first X1 (active X2)))
(rule (and (mark X1) X2) (mark (and X1 X2)))
(rule (if (mark X1) X2 X3) (mark (if X1 X2 X3)))
(rule (add (mark X1) X2) (mark (add X1 X2)))
(rule (first (mark X1) X2) (mark (first X1 X2)))
(rule (first X1 (mark X2)) (mark (first X1 X2)))
(rule (proper (and X1 X2)) (and (proper X1) (proper X2)))
(rule (proper true) (ok true))
(rule (proper false) (ok false))
(rule (proper (if X1 X2 X3)) (if (proper X1) (proper X2) (proper X3)))
(rule (proper (add X1 X2)) (add (proper X1) (proper X2)))
(rule (proper |0|) (ok |0|))
(rule (proper (s X)) (s (proper X)))
(rule (proper (first X1 X2)) (first (proper X1) (proper X2)))
(rule (proper nil) (ok nil))
(rule (proper (cons X1 X2)) (cons (proper X1) (proper X2)))
(rule (proper (from X)) (from (proper X)))
(rule (and (ok X1) (ok X2)) (ok (and X1 X2)))
(rule (if (ok X1) (ok X2) (ok X3)) (ok (if X1 X2 X3)))
(rule (add (ok X1) (ok X2)) (ok (add X1 X2)))
(rule (s (ok X)) (ok (s X)))
(rule (first (ok X1) (ok X2)) (ok (first X1 X2)))
(rule (cons (ok X1) (ok X2)) (ok (cons X1 X2)))
(rule (from (ok X)) (ok (from X)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))