; @origtpdbfilename ./TRS/TRCSR/MYNAT_complete_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_complete_L.xml"
(format TRS)
(fun U41 1)
(fun tt 0)
(fun U51 1)
(fun s 1)
(fun plus 2)
(fun U71 1)
(fun x 2)
(fun and 1)
(fun U11 1)
(fun U12 1)
(fun isNat 0)
(fun U13 1)
(fun U21 1)
(fun U22 1)
(fun U31 1)
(fun U32 1)
(fun U33 1)
(fun U61 1)
(fun |0| 0)
(fun isNatKind 0)
(rule (U41 tt) N)
(rule (U51 tt) (s (plus N M)))
(rule (U71 tt) (plus (x N M) N))
(rule (and tt) X)
(rule (U11 tt) (U12 isNat))
(rule (U12 tt) (U13 isNat))
(rule (U13 tt) tt)
(rule (U21 tt) (U22 isNat))
(rule (U22 tt) tt)
(rule (U31 tt) (U32 isNat))
(rule (U32 tt) (U33 isNat))
(rule (U33 tt) tt)
(rule (U61 tt) |0|)
(rule isNat tt)
(rule isNat (U11 (and isNatKind)))
(rule isNat (U21 isNatKind))
(rule isNat (U31 (and isNatKind)))
(rule isNatKind tt)
(rule isNatKind (and isNatKind))
(rule isNatKind isNatKind)
(rule (plus N |0|) (U41 (and isNat)))
(rule (plus N (s M)) (U51 (and (and isNat))))
(rule (x N |0|) (U61 (and isNat)))
(rule (x N (s M)) (U71 (and (and isNat))))