; @origtpdbfilename ./TRS/TRCSR/PEANO_complete-noand_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/PEANO_complete-noand_L.xml"
(format TRS)
(fun U52 1)
(fun tt 0)
(fun U64 1)
(fun s 1)
(fun plus 2)
(fun U11 1)
(fun U12 1)
(fun isNatKind 0)
(fun U13 1)
(fun U14 1)
(fun U15 1)
(fun isNat 0)
(fun U16 1)
(fun U21 1)
(fun U22 1)
(fun U23 1)
(fun U31 1)
(fun U32 1)
(fun U41 1)
(fun U51 1)
(fun U61 1)
(fun U62 1)
(fun U63 1)
(fun |0| 0)
(rule (U52 tt) N)
(rule (U64 tt) (s (plus N M)))
(rule (U11 tt) (U12 isNatKind))
(rule (U12 tt) (U13 isNatKind))
(rule (U13 tt) (U14 isNatKind))
(rule (U14 tt) (U15 isNat))
(rule (U15 tt) (U16 isNat))
(rule (U16 tt) tt)
(rule (U21 tt) (U22 isNatKind))
(rule (U22 tt) (U23 isNat))
(rule (U23 tt) tt)
(rule (U31 tt) (U32 isNatKind))
(rule (U32 tt) tt)
(rule (U41 tt) tt)
(rule (U51 tt) (U52 isNatKind))
(rule (U61 tt) (U62 isNatKind))
(rule (U62 tt) (U63 isNat))
(rule (U63 tt) (U64 isNatKind))
(rule isNat tt)
(rule isNat (U11 isNatKind))
(rule isNat (U21 isNatKind))
(rule isNatKind tt)
(rule isNatKind (U31 isNatKind))
(rule isNatKind (U41 isNatKind))
(rule (plus N |0|) (U51 isNat))
(rule (plus N (s M)) (U61 isNat))