; @origtpdbfilename ./TRS/TRCSR/MYNAT_nokinds_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_iGM.xml"
(format TRS)
(fun active 1)
(fun U11 2)
(fun tt 0)
(fun mark 1)
(fun U21 3)
(fun s 1)
(fun plus 2)
(fun U31 1)
(fun |0| 0)
(fun U41 3)
(fun x 2)
(fun and 2)
(fun isNat 1)
(rule (active (U11 tt N)) (mark N))
(rule (active (U21 tt M N)) (mark (s (plus N M))))
(rule (active (U31 tt)) (mark |0|))
(rule (active (U41 tt M N)) (mark (plus (x N M) N)))
(rule (active (and tt X)) (mark X))
(rule (active (isNat |0|)) (mark tt))
(rule (active (isNat (plus V1 V2))) (mark (and (isNat V1) (isNat V2))))
(rule (active (isNat (s V1))) (mark (isNat V1)))
(rule (active (isNat (x V1 V2))) (mark (and (isNat V1) (isNat V2))))
(rule (active (plus N |0|)) (mark (U11 (isNat N) N)))
(rule (active (plus N (s M))) (mark (U21 (and (isNat M) (isNat N)) M N)))
(rule (active (x N |0|)) (mark (U31 (isNat N))))
(rule (active (x N (s M))) (mark (U41 (and (isNat M) (isNat N)) M N)))
(rule (mark (U11 X1 X2)) (active (U11 (mark X1) X2)))
(rule (mark tt) (active tt))
(rule (mark (U21 X1 X2 X3)) (active (U21 (mark X1) X2 X3)))
(rule (mark (s X)) (active (s (mark X))))
(rule (mark (plus X1 X2)) (active (plus (mark X1) (mark X2))))
(rule (mark (U31 X)) (active (U31 (mark X))))
(rule (mark |0|) (active |0|))
(rule (mark (U41 X1 X2 X3)) (active (U41 (mark X1) X2 X3)))
(rule (mark (x X1 X2)) (active (x (mark X1) (mark X2))))
(rule (mark (and X1 X2)) (active (and (mark X1) X2)))
(rule (mark (isNat X)) (active (isNat X)))
(rule (U11 (mark X1) X2) (U11 X1 X2))
(rule (U11 X1 (mark X2)) (U11 X1 X2))
(rule (U11 (active X1) X2) (U11 X1 X2))
(rule (U11 X1 (active X2)) (U11 X1 X2))
(rule (U21 (mark X1) X2 X3) (U21 X1 X2 X3))
(rule (U21 X1 (mark X2) X3) (U21 X1 X2 X3))
(rule (U21 X1 X2 (mark X3)) (U21 X1 X2 X3))
(rule (U21 (active X1) X2 X3) (U21 X1 X2 X3))
(rule (U21 X1 (active X2) X3) (U21 X1 X2 X3))
(rule (U21 X1 X2 (active X3)) (U21 X1 X2 X3))
(rule (s (mark X)) (s X))
(rule (s (active X)) (s 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 (U31 (mark X)) (U31 X))
(rule (U31 (active X)) (U31 X))
(rule (U41 (mark X1) X2 X3) (U41 X1 X2 X3))
(rule (U41 X1 (mark X2) X3) (U41 X1 X2 X3))
(rule (U41 X1 X2 (mark X3)) (U41 X1 X2 X3))
(rule (U41 (active X1) X2 X3) (U41 X1 X2 X3))
(rule (U41 X1 (active X2) X3) (U41 X1 X2 X3))
(rule (U41 X1 X2 (active X3)) (U41 X1 X2 X3))
(rule (x (mark X1) X2) (x X1 X2))
(rule (x X1 (mark X2)) (x X1 X2))
(rule (x (active X1) X2) (x X1 X2))
(rule (x X1 (active X2)) (x X1 X2))
(rule (and (mark X1) X2) (and X1 X2))
(rule (and X1 (mark X2)) (and X1 X2))
(rule (and (active X1) X2) (and X1 X2))
(rule (and X1 (active X2)) (and X1 X2))
(rule (isNat (mark X)) (isNat X))
(rule (isNat (active X)) (isNat X))