; @origtpdbfilename ./TRS/TRCSR/PEANO_complete_noand_GM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/PEANO_complete_noand_GM.xml"
(format TRS)
(fun a__U11 3)
(fun tt 0)
(fun a__U12 3)
(fun a__isNatKind 1)
(fun a__U13 3)
(fun a__U14 3)
(fun a__U15 2)
(fun a__isNat 1)
(fun a__U16 1)
(fun a__U21 2)
(fun a__U22 2)
(fun a__U23 1)
(fun a__U31 2)
(fun a__U32 1)
(fun a__U41 1)
(fun a__U51 2)
(fun a__U52 2)
(fun mark 1)
(fun a__U61 3)
(fun a__U62 3)
(fun a__U63 3)
(fun a__U64 3)
(fun s 1)
(fun a__plus 2)
(fun |0| 0)
(fun plus 2)
(fun U11 3)
(fun U12 3)
(fun isNatKind 1)
(fun U13 3)
(fun U14 3)
(fun U15 2)
(fun isNat 1)
(fun U16 1)
(fun U21 2)
(fun U22 2)
(fun U23 1)
(fun U31 2)
(fun U32 1)
(fun U41 1)
(fun U51 2)
(fun U52 2)
(fun U61 3)
(fun U62 3)
(fun U63 3)
(fun U64 3)
(rule (a__U11 tt V1 V2) (a__U12 (a__isNatKind V1) V1 V2))
(rule (a__U12 tt V1 V2) (a__U13 (a__isNatKind V2) V1 V2))
(rule (a__U13 tt V1 V2) (a__U14 (a__isNatKind V2) V1 V2))
(rule (a__U14 tt V1 V2) (a__U15 (a__isNat V1) V2))
(rule (a__U15 tt V2) (a__U16 (a__isNat V2)))
(rule (a__U16 tt) tt)
(rule (a__U21 tt V1) (a__U22 (a__isNatKind V1) V1))
(rule (a__U22 tt V1) (a__U23 (a__isNat V1)))
(rule (a__U23 tt) tt)
(rule (a__U31 tt V2) (a__U32 (a__isNatKind V2)))
(rule (a__U32 tt) tt)
(rule (a__U41 tt) tt)
(rule (a__U51 tt N) (a__U52 (a__isNatKind N) N))
(rule (a__U52 tt N) (mark N))
(rule (a__U61 tt M N) (a__U62 (a__isNatKind M) M N))
(rule (a__U62 tt M N) (a__U63 (a__isNat N) M N))
(rule (a__U63 tt M N) (a__U64 (a__isNatKind N) M N))
(rule (a__U64 tt M N) (s (a__plus (mark N) (mark M))))
(rule (a__isNat |0|) tt)
(rule (a__isNat (plus V1 V2)) (a__U11 (a__isNatKind V1) V1 V2))
(rule (a__isNat (s V1)) (a__U21 (a__isNatKind V1) V1))
(rule (a__isNatKind |0|) tt)
(rule (a__isNatKind (plus V1 V2)) (a__U31 (a__isNatKind V1) V2))
(rule (a__isNatKind (s V1)) (a__U41 (a__isNatKind V1)))
(rule (a__plus N |0|) (a__U51 (a__isNat N) N))
(rule (a__plus N (s M)) (a__U61 (a__isNat M) M N))
(rule (mark (U11 X1 X2 X3)) (a__U11 (mark X1) X2 X3))
(rule (mark (U12 X1 X2 X3)) (a__U12 (mark X1) X2 X3))
(rule (mark (isNatKind X)) (a__isNatKind X))
(rule (mark (U13 X1 X2 X3)) (a__U13 (mark X1) X2 X3))
(rule (mark (U14 X1 X2 X3)) (a__U14 (mark X1) X2 X3))
(rule (mark (U15 X1 X2)) (a__U15 (mark X1) X2))
(rule (mark (isNat X)) (a__isNat X))
(rule (mark (U16 X)) (a__U16 (mark X)))
(rule (mark (U21 X1 X2)) (a__U21 (mark X1) X2))
(rule (mark (U22 X1 X2)) (a__U22 (mark X1) X2))
(rule (mark (U23 X)) (a__U23 (mark X)))
(rule (mark (U31 X1 X2)) (a__U31 (mark X1) X2))
(rule (mark (U32 X)) (a__U32 (mark X)))
(rule (mark (U41 X)) (a__U41 (mark X)))
(rule (mark (U51 X1 X2)) (a__U51 (mark X1) X2))
(rule (mark (U52 X1 X2)) (a__U52 (mark X1) X2))
(rule (mark (U61 X1 X2 X3)) (a__U61 (mark X1) X2 X3))
(rule (mark (U62 X1 X2 X3)) (a__U62 (mark X1) X2 X3))
(rule (mark (U63 X1 X2 X3)) (a__U63 (mark X1) X2 X3))
(rule (mark (U64 X1 X2 X3)) (a__U64 (mark X1) X2 X3))
(rule (mark (plus X1 X2)) (a__plus (mark X1) (mark X2)))
(rule (mark tt) tt)
(rule (mark (s X)) (s (mark X)))
(rule (mark |0|) |0|)
(rule (a__U11 X1 X2 X3) (U11 X1 X2 X3))
(rule (a__U12 X1 X2 X3) (U12 X1 X2 X3))
(rule (a__isNatKind X) (isNatKind X))
(rule (a__U13 X1 X2 X3) (U13 X1 X2 X3))
(rule (a__U14 X1 X2 X3) (U14 X1 X2 X3))
(rule (a__U15 X1 X2) (U15 X1 X2))
(rule (a__isNat X) (isNat X))
(rule (a__U16 X) (U16 X))
(rule (a__U21 X1 X2) (U21 X1 X2))
(rule (a__U22 X1 X2) (U22 X1 X2))
(rule (a__U23 X) (U23 X))
(rule (a__U31 X1 X2) (U31 X1 X2))
(rule (a__U32 X) (U32 X))
(rule (a__U41 X) (U41 X))
(rule (a__U51 X1 X2) (U51 X1 X2))
(rule (a__U52 X1 X2) (U52 X1 X2))
(rule (a__U61 X1 X2 X3) (U61 X1 X2 X3))
(rule (a__U62 X1 X2 X3) (U62 X1 X2 X3))
(rule (a__U63 X1 X2 X3) (U63 X1 X2 X3))
(rule (a__U64 X1 X2 X3) (U64 X1 X2 X3))
(rule (a__plus X1 X2) (plus X1 X2))