; @origtpdbfilename ./TRS/TRCSR/ExAppendixB_AEL03_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/ExAppendixB_AEL03_iGM.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 cons2 2)
(fun rcons 2)
(fun posrecip 1)
(fun |2ndsneg| 2)
(fun negrecip 1)
(fun pi 1)
(fun plus 2)
(fun times 2)
(fun square 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 Z))) (mark (|2ndspos| (s N) (cons2 X Z))))
(rule (active (|2ndspos| (s N) (cons2 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 Z))) (mark (|2ndsneg| (s N) (cons2 X Z))))
(rule (active (|2ndsneg| (s N) (cons2 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 (mark (from X)) (active (from (mark X))))
(rule (mark (cons X1 X2)) (active (cons (mark X1) X2)))
(rule (mark (s X)) (active (s (mark X))))
(rule (mark (|2ndspos| X1 X2)) (active (|2ndspos| (mark X1) (mark X2))))
(rule (mark |0|) (active |0|))
(rule (mark rnil) (active rnil))
(rule (mark (cons2 X1 X2)) (active (cons2 X1 (mark X2))))
(rule (mark (rcons X1 X2)) (active (rcons (mark X1) (mark X2))))
(rule (mark (posrecip X)) (active (posrecip (mark X))))
(rule (mark (|2ndsneg| X1 X2)) (active (|2ndsneg| (mark X1) (mark X2))))
(rule (mark (negrecip X)) (active (negrecip (mark X))))
(rule (mark (pi X)) (active (pi (mark X))))
(rule (mark (plus X1 X2)) (active (plus (mark X1) (mark X2))))
(rule (mark (times X1 X2)) (active (times (mark X1) (mark X2))))
(rule (mark (square X)) (active (square (mark X))))
(rule (from (mark X)) (from X))
(rule (from (active X)) (from 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 (s (mark X)) (s X))
(rule (s (active X)) (s X))
(rule (|2ndspos| (mark X1) X2) (|2ndspos| X1 X2))
(rule (|2ndspos| X1 (mark X2)) (|2ndspos| X1 X2))
(rule (|2ndspos| (active X1) X2) (|2ndspos| X1 X2))
(rule (|2ndspos| X1 (active X2)) (|2ndspos| X1 X2))
(rule (cons2 (mark X1) X2) (cons2 X1 X2))
(rule (cons2 X1 (mark X2)) (cons2 X1 X2))
(rule (cons2 (active X1) X2) (cons2 X1 X2))
(rule (cons2 X1 (active X2)) (cons2 X1 X2))
(rule (rcons (mark X1) X2) (rcons X1 X2))
(rule (rcons X1 (mark X2)) (rcons X1 X2))
(rule (rcons (active X1) X2) (rcons X1 X2))
(rule (rcons X1 (active X2)) (rcons X1 X2))
(rule (posrecip (mark X)) (posrecip X))
(rule (posrecip (active X)) (posrecip X))
(rule (|2ndsneg| (mark X1) X2) (|2ndsneg| X1 X2))
(rule (|2ndsneg| X1 (mark X2)) (|2ndsneg| X1 X2))
(rule (|2ndsneg| (active X1) X2) (|2ndsneg| X1 X2))
(rule (|2ndsneg| X1 (active X2)) (|2ndsneg| X1 X2))
(rule (negrecip (mark X)) (negrecip X))
(rule (negrecip (active X)) (negrecip X))
(rule (pi (mark X)) (pi X))
(rule (pi (active X)) (pi X))
(rule (plus (mark X1) X2) (plus X1 X2))
(rule (plus X1 (mark X2)) (plus X1 X2))
(rule (plus (active X1) X2) (plus X1 X2))
(rule (plus X1 (active X2)) (plus X1 X2))
(rule (times (mark X1) X2) (times X1 X2))
(rule (times X1 (mark X2)) (times X1 X2))
(rule (times (active X1) X2) (times X1 X2))
(rule (times X1 (active X2)) (times X1 X2))
(rule (square (mark X)) (square X))
(rule (square (active X)) (square X))