; @origtpdbfilename ./TRS/TRCSR/PEANO_complete-noand_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/PEANO_complete-noand_FR.xml"
(format TRS)
(fun U11 3)
(fun tt 0)
(fun U12 3)
(fun isNatKind 1)
(fun activate 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)
(fun s 1)
(fun plus 2)
(fun n__0 0)
(fun n__plus 2)
(fun n__s 1)
(fun |0| 0)
(rule (U11 tt V1 V2) (U12 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (U12 tt V1 V2) (U13 (isNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U13 tt V1 V2) (U14 (isNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U14 tt V1 V2) (U15 (isNat (activate V1)) (activate V2)))
(rule (U15 tt V2) (U16 (isNat (activate V2))))
(rule (U16 tt) tt)
(rule (U21 tt V1) (U22 (isNatKind (activate V1)) (activate V1)))
(rule (U22 tt V1) (U23 (isNat (activate V1))))
(rule (U23 tt) tt)
(rule (U31 tt V2) (U32 (isNatKind (activate V2))))
(rule (U32 tt) tt)
(rule (U41 tt) tt)
(rule (U51 tt N) (U52 (isNatKind (activate N)) (activate N)))
(rule (U52 tt N) (activate N))
(rule (U61 tt M N) (U62 (isNatKind (activate M)) (activate M) (activate N)))
(rule (U62 tt M N) (U63 (isNat (activate N)) (activate M) (activate N)))
(rule (U63 tt M N) (U64 (isNatKind (activate N)) (activate M) (activate N)))
(rule (U64 tt M N) (s (plus (activate N) (activate M))))
(rule (isNat n__0) tt)
(rule (isNat (n__plus V1 V2)) (U11 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (isNat (n__s V1)) (U21 (isNatKind (activate V1)) (activate V1)))
(rule (isNatKind n__0) tt)
(rule (isNatKind (n__plus V1 V2)) (U31 (isNatKind (activate V1)) (activate V2)))
(rule (isNatKind (n__s V1)) (U41 (isNatKind (activate V1))))
(rule (plus N |0|) (U51 (isNat N) N))
(rule (plus N (s M)) (U61 (isNat M) M N))
(rule |0| n__0)
(rule (plus X1 X2) (n__plus X1 X2))
(rule (s X) (n__s X))
(rule (activate n__0) |0|)
(rule (activate (n__plus X1 X2)) (plus (activate X1) (activate X2)))
(rule (activate (n__s X)) (s (activate X)))
(rule (activate X) X)