; @origtpdbfilename ./TRS/TRCSR/Ex1_2_AEL03_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex1_2_AEL03_C.xml"
(format TRS)
(fun active 1)
(fun from 1)
(fun mark 1)
(fun cons 2)
(fun s 1)
(fun |2ndspos| 2)
(fun |0| 0)
(fun rnil 0)
(fun rcons 2)
(fun posrecip 1)
(fun |2ndsneg| 2)
(fun negrecip 1)
(fun pi 1)
(fun plus 2)
(fun times 2)
(fun square 1)
(fun proper 1)
(fun ok 1)
(fun nil 0)
(fun top 1)
(rule (active (from X)) (mark (cons X (from (s X)))))
(rule (active (|2ndspos| |0| Z)) (mark rnil))
(rule (active (|2ndspos| (s N) (cons X (cons Y Z)))) (mark (rcons (posrecip Y) (|2ndsneg| N Z))))
(rule (active (|2ndsneg| |0| Z)) (mark rnil))
(rule (active (|2ndsneg| (s N) (cons X (cons Y Z)))) (mark (rcons (negrecip Y) (|2ndspos| N Z))))
(rule (active (pi X)) (mark (|2ndspos| X (from |0|))))
(rule (active (plus |0| Y)) (mark Y))
(rule (active (plus (s X) Y)) (mark (s (plus X Y))))
(rule (active (times |0| Y)) (mark |0|))
(rule (active (times (s X) Y)) (mark (plus Y (times X Y))))
(rule (active (square X)) (mark (times X X)))
(rule (active (s X)) (s (active X)))
(rule (active (posrecip X)) (posrecip (active X)))
(rule (active (negrecip X)) (negrecip (active X)))
(rule (active (cons X1 X2)) (cons (active X1) X2))
(rule (active (rcons X1 X2)) (rcons (active X1) X2))
(rule (active (rcons X1 X2)) (rcons X1 (active X2)))
(rule (active (from X)) (from (active X)))
(rule (active (|2ndspos| X1 X2)) (|2ndspos| (active X1) X2))
(rule (active (|2ndspos| X1 X2)) (|2ndspos| X1 (active X2)))
(rule (active (|2ndsneg| X1 X2)) (|2ndsneg| (active X1) X2))
(rule (active (|2ndsneg| X1 X2)) (|2ndsneg| X1 (active X2)))
(rule (active (pi X)) (pi (active X)))
(rule (active (plus X1 X2)) (plus (active X1) X2))
(rule (active (plus X1 X2)) (plus X1 (active X2)))
(rule (active (times X1 X2)) (times (active X1) X2))
(rule (active (times X1 X2)) (times X1 (active X2)))
(rule (active (square X)) (square (active X)))
(rule (s (mark X)) (mark (s X)))
(rule (posrecip (mark X)) (mark (posrecip X)))
(rule (negrecip (mark X)) (mark (negrecip X)))
(rule (cons (mark X1) X2) (mark (cons X1 X2)))
(rule (rcons (mark X1) X2) (mark (rcons X1 X2)))
(rule (rcons X1 (mark X2)) (mark (rcons X1 X2)))
(rule (from (mark X)) (mark (from X)))
(rule (|2ndspos| (mark X1) X2) (mark (|2ndspos| X1 X2)))
(rule (|2ndspos| X1 (mark X2)) (mark (|2ndspos| X1 X2)))
(rule (|2ndsneg| (mark X1) X2) (mark (|2ndsneg| X1 X2)))
(rule (|2ndsneg| X1 (mark X2)) (mark (|2ndsneg| X1 X2)))
(rule (pi (mark X)) (mark (pi X)))
(rule (plus (mark X1) X2) (mark (plus X1 X2)))
(rule (plus X1 (mark X2)) (mark (plus X1 X2)))
(rule (times (mark X1) X2) (mark (times X1 X2)))
(rule (times X1 (mark X2)) (mark (times X1 X2)))
(rule (square (mark X)) (mark (square X)))
(rule (proper |0|) (ok |0|))
(rule (proper (s X)) (s (proper X)))
(rule (proper (posrecip X)) (posrecip (proper X)))
(rule (proper (negrecip X)) (negrecip (proper X)))
(rule (proper nil) (ok nil))
(rule (proper (cons X1 X2)) (cons (proper X1) (proper X2)))
(rule (proper rnil) (ok rnil))
(rule (proper (rcons X1 X2)) (rcons (proper X1) (proper X2)))
(rule (proper (from X)) (from (proper X)))
(rule (proper (|2ndspos| X1 X2)) (|2ndspos| (proper X1) (proper X2)))
(rule (proper (|2ndsneg| X1 X2)) (|2ndsneg| (proper X1) (proper X2)))
(rule (proper (pi X)) (pi (proper X)))
(rule (proper (plus X1 X2)) (plus (proper X1) (proper X2)))
(rule (proper (times X1 X2)) (times (proper X1) (proper X2)))
(rule (proper (square X)) (square (proper X)))
(rule (s (ok X)) (ok (s X)))
(rule (posrecip (ok X)) (ok (posrecip X)))
(rule (negrecip (ok X)) (ok (negrecip X)))
(rule (cons (ok X1) (ok X2)) (ok (cons X1 X2)))
(rule (rcons (ok X1) (ok X2)) (ok (rcons X1 X2)))
(rule (from (ok X)) (ok (from X)))
(rule (|2ndspos| (ok X1) (ok X2)) (ok (|2ndspos| X1 X2)))
(rule (|2ndsneg| (ok X1) (ok X2)) (ok (|2ndsneg| X1 X2)))
(rule (pi (ok X)) (ok (pi X)))
(rule (plus (ok X1) (ok X2)) (ok (plus X1 X2)))
(rule (times (ok X1) (ok X2)) (ok (times X1 X2)))
(rule (square (ok X)) (ok (square X)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))