; @origtpdbfilename ./TRS/TRCSR/MYNAT_nokinds_noand_GM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_noand_GM.xml"
(format TRS)
(fun a__U11 2)
(fun tt 0)
(fun a__U12 1)
(fun a__isNat 1)
(fun a__U21 1)
(fun a__U31 2)
(fun a__U32 1)
(fun a__U41 2)
(fun mark 1)
(fun a__U51 3)
(fun a__U52 3)
(fun s 1)
(fun a__plus 2)
(fun a__U61 1)
(fun |0| 0)
(fun a__U71 3)
(fun a__U72 3)
(fun a__x 2)
(fun plus 2)
(fun x 2)
(fun U11 2)
(fun U12 1)
(fun isNat 1)
(fun U21 1)
(fun U31 2)
(fun U32 1)
(fun U41 2)
(fun U51 3)
(fun U52 3)
(fun U61 1)
(fun U71 3)
(fun U72 3)
(rule (a__U11 tt V2) (a__U12 (a__isNat V2)))
(rule (a__U12 tt) tt)
(rule (a__U21 tt) tt)
(rule (a__U31 tt V2) (a__U32 (a__isNat V2)))
(rule (a__U32 tt) tt)
(rule (a__U41 tt N) (mark N))
(rule (a__U51 tt M N) (a__U52 (a__isNat N) M N))
(rule (a__U52 tt M N) (s (a__plus (mark N) (mark M))))
(rule (a__U61 tt) |0|)
(rule (a__U71 tt M N) (a__U72 (a__isNat N) M N))
(rule (a__U72 tt M N) (a__plus (a__x (mark N) (mark M)) (mark N)))
(rule (a__isNat |0|) tt)
(rule (a__isNat (plus V1 V2)) (a__U11 (a__isNat V1) V2))
(rule (a__isNat (s V1)) (a__U21 (a__isNat V1)))
(rule (a__isNat (x V1 V2)) (a__U31 (a__isNat V1) V2))
(rule (a__plus N |0|) (a__U41 (a__isNat N) N))
(rule (a__plus N (s M)) (a__U51 (a__isNat M) M N))
(rule (a__x N |0|) (a__U61 (a__isNat N)))
(rule (a__x N (s M)) (a__U71 (a__isNat M) M N))
(rule (mark (U11 X1 X2)) (a__U11 (mark X1) X2))
(rule (mark (U12 X)) (a__U12 (mark X)))
(rule (mark (isNat X)) (a__isNat X))
(rule (mark (U21 X)) (a__U21 (mark X)))
(rule (mark (U31 X1 X2)) (a__U31 (mark X1) X2))
(rule (mark (U32 X)) (a__U32 (mark X)))
(rule (mark (U41 X1 X2)) (a__U41 (mark X1) X2))
(rule (mark (U51 X1 X2 X3)) (a__U51 (mark X1) X2 X3))
(rule (mark (U52 X1 X2 X3)) (a__U52 (mark X1) X2 X3))
(rule (mark (plus X1 X2)) (a__plus (mark X1) (mark X2)))
(rule (mark (U61 X)) (a__U61 (mark X)))
(rule (mark (U71 X1 X2 X3)) (a__U71 (mark X1) X2 X3))
(rule (mark (U72 X1 X2 X3)) (a__U72 (mark X1) X2 X3))
(rule (mark (x X1 X2)) (a__x (mark X1) (mark X2)))
(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__U12 X) (U12 X))
(rule (a__isNat X) (isNat X))
(rule (a__U21 X) (U21 X))
(rule (a__U31 X1 X2) (U31 X1 X2))
(rule (a__U32 X) (U32 X))
(rule (a__U41 X1 X2) (U41 X1 X2))
(rule (a__U51 X1 X2 X3) (U51 X1 X2 X3))
(rule (a__U52 X1 X2 X3) (U52 X1 X2 X3))
(rule (a__plus X1 X2) (plus X1 X2))
(rule (a__U61 X) (U61 X))
(rule (a__U71 X1 X2 X3) (U71 X1 X2 X3))
(rule (a__U72 X1 X2 X3) (U72 X1 X2 X3))
(rule (a__x X1 X2) (x X1 X2))