; @origtpdbfilename ./TRS/TRCSR/Ex1_GL02a_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex1_GL02a_iGM.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)
(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 (mark (eq X1 X2)) (active (eq X1 X2)))
(rule (mark |0|) (active |0|))
(rule (mark true) (active true))
(rule (mark (s X)) (active (s X)))
(rule (mark false) (active false))
(rule (mark (inf X)) (active (inf (mark X))))
(rule (mark (cons X1 X2)) (active (cons X1 X2)))
(rule (mark (take X1 X2)) (active (take (mark X1) (mark X2))))
(rule (mark nil) (active nil))
(rule (mark (length X)) (active (length (mark X))))
(rule (eq (mark X1) X2) (eq X1 X2))
(rule (eq X1 (mark X2)) (eq X1 X2))
(rule (eq (active X1) X2) (eq X1 X2))
(rule (eq X1 (active X2)) (eq X1 X2))
(rule (s (mark X)) (s X))
(rule (s (active X)) (s X))
(rule (inf (mark X)) (inf X))
(rule (inf (active X)) (inf X))
(rule (cons (mark X1) X2) (cons X1 X2))
(rule (cons X1 (mark X2)) (cons X1 X2))
(rule (cons (active X1) X2) (cons X1 X2))
(rule (cons X1 (active X2)) (cons X1 X2))
(rule (take (mark X1) X2) (take X1 X2))
(rule (take X1 (mark X2)) (take X1 X2))
(rule (take (active X1) X2) (take X1 X2))
(rule (take X1 (active X2)) (take X1 X2))
(rule (length (mark X)) (length X))
(rule (length (active X)) (length X))