; @origtpdbfilename ./TRS/TRCSR/MYNAT_nokinds_GM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_GM.xml"
(format TRS)
(fun a__U11 2)
(fun tt 0)
(fun mark 1)
(fun a__U21 3)
(fun s 1)
(fun a__plus 2)
(fun a__U31 1)
(fun |0| 0)
(fun a__U41 3)
(fun a__x 2)
(fun a__and 2)
(fun a__isNat 1)
(fun plus 2)
(fun isNat 1)
(fun x 2)
(fun U11 2)
(fun U21 3)
(fun U31 1)
(fun U41 3)
(fun and 2)
(rule (a__U11 tt N) (mark N))
(rule (a__U21 tt M N) (s (a__plus (mark N) (mark M))))
(rule (a__U31 tt) |0|)
(rule (a__U41 tt M N) (a__plus (a__x (mark N) (mark M)) (mark N)))
(rule (a__and tt X) (mark X))
(rule (a__isNat |0|) tt)
(rule (a__isNat (plus V1 V2)) (a__and (a__isNat V1) (isNat V2)))
(rule (a__isNat (s V1)) (a__isNat V1))
(rule (a__isNat (x V1 V2)) (a__and (a__isNat V1) (isNat V2)))
(rule (a__plus N |0|) (a__U11 (a__isNat N) N))
(rule (a__plus N (s M)) (a__U21 (a__and (a__isNat M) (isNat N)) M N))
(rule (a__x N |0|) (a__U31 (a__isNat N)))
(rule (a__x N (s M)) (a__U41 (a__and (a__isNat M) (isNat N)) M N))
(rule (mark (U11 X1 X2)) (a__U11 (mark X1) X2))
(rule (mark (U21 X1 X2 X3)) (a__U21 (mark X1) X2 X3))
(rule (mark (plus X1 X2)) (a__plus (mark X1) (mark X2)))
(rule (mark (U31 X)) (a__U31 (mark X)))
(rule (mark (U41 X1 X2 X3)) (a__U41 (mark X1) X2 X3))
(rule (mark (x X1 X2)) (a__x (mark X1) (mark X2)))
(rule (mark (and X1 X2)) (a__and (mark X1) X2))
(rule (mark (isNat X)) (a__isNat X))
(rule (mark tt) tt)
(rule (mark (s X)) (s (mark X)))
(rule (mark |0|) |0|)
(rule (a__U11 X1 X2) (U11 X1 X2))
(rule (a__U21 X1 X2 X3) (U21 X1 X2 X3))
(rule (a__plus X1 X2) (plus X1 X2))
(rule (a__U31 X) (U31 X))
(rule (a__U41 X1 X2 X3) (U41 X1 X2 X3))
(rule (a__x X1 X2) (x X1 X2))
(rule (a__and X1 X2) (and X1 X2))
(rule (a__isNat X) (isNat X))