; @origtpdbfilename ./TRS/TRCSR/MYNAT_complete_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_complete_FR.xml"
(format TRS)
(fun U11 3)
(fun tt 0)
(fun U12 2)
(fun isNat 1)
(fun activate 1)
(fun U13 1)
(fun U21 2)
(fun U22 1)
(fun U31 3)
(fun U32 2)
(fun U33 1)
(fun U41 2)
(fun U51 3)
(fun s 1)
(fun plus 2)
(fun U61 1)
(fun |0| 0)
(fun U71 3)
(fun x 2)
(fun and 2)
(fun n__0 0)
(fun n__plus 2)
(fun isNatKind 1)
(fun n__isNatKind 1)
(fun n__s 1)
(fun n__x 2)
(fun n__and 2)
(fun n__isNat 1)
(rule (U11 tt V1 V2) (U12 (isNat (activate V1)) (activate V2)))
(rule (U12 tt V2) (U13 (isNat (activate V2))))
(rule (U13 tt) tt)
(rule (U21 tt V1) (U22 (isNat (activate V1))))
(rule (U22 tt) tt)
(rule (U31 tt V1 V2) (U32 (isNat (activate V1)) (activate V2)))
(rule (U32 tt V2) (U33 (isNat (activate V2))))
(rule (U33 tt) tt)
(rule (U41 tt N) (activate N))
(rule (U51 tt M N) (s (plus (activate N) (activate M))))
(rule (U61 tt) |0|)
(rule (U71 tt M N) (plus (x (activate N) (activate M)) (activate N)))
(rule (and tt X) (activate X))
(rule (isNat n__0) tt)
(rule (isNat (n__plus V1 V2)) (U11 (and (isNatKind (activate V1)) (n__isNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isNat (n__s V1)) (U21 (isNatKind (activate V1)) (activate V1)))
(rule (isNat (n__x V1 V2)) (U31 (and (isNatKind (activate V1)) (n__isNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isNatKind n__0) tt)
(rule (isNatKind (n__plus V1 V2)) (and (isNatKind (activate V1)) (n__isNatKind (activate V2))))
(rule (isNatKind (n__s V1)) (isNatKind (activate V1)))
(rule (isNatKind (n__x V1 V2)) (and (isNatKind (activate V1)) (n__isNatKind (activate V2))))
(rule (plus N |0|) (U41 (and (isNat N) (n__isNatKind N)) N))
(rule (plus N (s M)) (U51 (and (and (isNat M) (n__isNatKind M)) (n__and (n__isNat N) (n__isNatKind N))) M N))
(rule (x N |0|) (U61 (and (isNat N) (n__isNatKind N))))
(rule (x N (s M)) (U71 (and (and (isNat M) (n__isNatKind M)) (n__and (n__isNat N) (n__isNatKind N))) M N))
(rule |0| n__0)
(rule (plus X1 X2) (n__plus X1 X2))
(rule (isNatKind X) (n__isNatKind X))
(rule (s X) (n__s X))
(rule (x X1 X2) (n__x X1 X2))
(rule (and X1 X2) (n__and X1 X2))
(rule (isNat X) (n__isNat X))
(rule (activate n__0) |0|)
(rule (activate (n__plus X1 X2)) (plus (activate X1) (activate X2)))
(rule (activate (n__isNatKind X)) (isNatKind X))
(rule (activate (n__s X)) (s (activate X)))
(rule (activate (n__x X1 X2)) (x (activate X1) (activate X2)))
(rule (activate (n__and X1 X2)) (and (activate X1) X2))
(rule (activate (n__isNat X)) (isNat X))
(rule (activate X) X)