; @origtpdbfilename ./TRS/SchneiderKamp/trs/kabasci01.trs
; @xtcfilename "./TRS_Standard/AProVE_07/kabasci01.xml"
(format TRS)
(fun active 1)
(fun eq 2)
(fun |0| 0)
(fun mark 1)
(fun true 0)
(fun s 1)
(fun false 0)
(fun inf 1)
(fun cons 2)
(fun take 2)
(fun nil 0)
(fun length 1)
(fun proper 1)
(fun ok 1)
(fun any 1)
(fun top 1)
(rule (active (eq |0| |0|)) (mark true))
(rule (active (eq (s X) (s Y))) (mark (eq X Y)))
(rule (active (eq X Y)) (mark false))
(rule (active (inf X)) (mark (cons X (inf (s X)))))
(rule (active (take |0| X)) (mark nil))
(rule (active (take (s X) (cons Y L))) (mark (cons Y (take X L))))
(rule (active (length nil)) (mark |0|))
(rule (active (length (cons X L))) (mark (s (length L))))
(rule (active (inf X)) (inf (active X)))
(rule (active (take X1 X2)) (take (active X1) X2))
(rule (active (take X1 X2)) (take X1 (active X2)))
(rule (active (length X)) (length (active X)))
(rule (inf (mark X)) (mark (inf X)))
(rule (take (mark X1) X2) (mark (take X1 X2)))
(rule (take X1 (mark X2)) (mark (take X1 X2)))
(rule (length (mark X)) (mark (length X)))
(rule (proper (eq X1 X2)) (eq (proper X1) (proper X2)))
(rule (proper |0|) (ok |0|))
(rule (proper true) (ok true))
(rule (proper (s X)) (s (proper X)))
(rule (proper false) (ok false))
(rule (proper (inf X)) (inf (proper X)))
(rule (proper (cons (any X1) X2)) (cons (any (any (proper X1))) (any (proper X2))))
(rule (proper (take X1 X2)) (take (proper X1) (proper X2)))
(rule (proper nil) (ok nil))
(rule (proper (length X)) (length (proper X)))
(rule (eq (ok X1) (ok X2)) (ok (eq X1 X2)))
(rule (s (ok X)) (ok (s X)))
(rule (inf (ok X)) (ok (inf X)))
(rule (cons (ok X1) (ok X2)) (ok (cons X1 X2)))
(rule (take (ok X1) (ok X2)) (ok (take X1 X2)))
(rule (length (ok X)) (ok (length X)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))
(rule (any X) (s X))
(rule (any (proper X)) (any (any (any X))))