; @origtpdbfilename ./TRS/TRCSR/MYNAT_complete_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_complete_C.xml"
(format TRS)
(fun active 1)
(fun U11 3)
(fun tt 0)
(fun mark 1)
(fun U12 2)
(fun isNat 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 isNatKind 1)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (U11 tt V1 V2)) (mark (U12 (isNat V1) V2)))
(rule (active (U12 tt V2)) (mark (U13 (isNat V2))))
(rule (active (U13 tt)) (mark tt))
(rule (active (U21 tt V1)) (mark (U22 (isNat V1))))
(rule (active (U22 tt)) (mark tt))
(rule (active (U31 tt V1 V2)) (mark (U32 (isNat V1) V2)))
(rule (active (U32 tt V2)) (mark (U33 (isNat V2))))
(rule (active (U33 tt)) (mark tt))
(rule (active (U41 tt N)) (mark N))
(rule (active (U51 tt M N)) (mark (s (plus N M))))
(rule (active (U61 tt)) (mark |0|))
(rule (active (U71 tt M N)) (mark (plus (x N M) N)))
(rule (active (and tt X)) (mark X))
(rule (active (isNat |0|)) (mark tt))
(rule (active (isNat (plus V1 V2))) (mark (U11 (and (isNatKind V1) (isNatKind V2)) V1 V2)))
(rule (active (isNat (s V1))) (mark (U21 (isNatKind V1) V1)))
(rule (active (isNat (x V1 V2))) (mark (U31 (and (isNatKind V1) (isNatKind V2)) V1 V2)))
(rule (active (isNatKind |0|)) (mark tt))
(rule (active (isNatKind (plus V1 V2))) (mark (and (isNatKind V1) (isNatKind V2))))
(rule (active (isNatKind (s V1))) (mark (isNatKind V1)))
(rule (active (isNatKind (x V1 V2))) (mark (and (isNatKind V1) (isNatKind V2))))
(rule (active (plus N |0|)) (mark (U41 (and (isNat N) (isNatKind N)) N)))
(rule (active (plus N (s M))) (mark (U51 (and (and (isNat M) (isNatKind M)) (and (isNat N) (isNatKind N))) M N)))
(rule (active (x N |0|)) (mark (U61 (and (isNat N) (isNatKind N)))))
(rule (active (x N (s M))) (mark (U71 (and (and (isNat M) (isNatKind M)) (and (isNat N) (isNatKind N))) M N)))
(rule (active (U11 X1 X2 X3)) (U11 (active X1) X2 X3))
(rule (active (U12 X1 X2)) (U12 (active X1) X2))
(rule (active (U13 X)) (U13 (active X)))
(rule (active (U21 X1 X2)) (U21 (active X1) X2))
(rule (active (U22 X)) (U22 (active X)))
(rule (active (U31 X1 X2 X3)) (U31 (active X1) X2 X3))
(rule (active (U32 X1 X2)) (U32 (active X1) X2))
(rule (active (U33 X)) (U33 (active X)))
(rule (active (U41 X1 X2)) (U41 (active X1) X2))
(rule (active (U51 X1 X2 X3)) (U51 (active X1) X2 X3))
(rule (active (s X)) (s (active X)))
(rule (active (plus X1 X2)) (plus (active X1) X2))
(rule (active (plus X1 X2)) (plus X1 (active X2)))
(rule (active (U61 X)) (U61 (active X)))
(rule (active (U71 X1 X2 X3)) (U71 (active X1) X2 X3))
(rule (active (x X1 X2)) (x (active X1) X2))
(rule (active (x X1 X2)) (x X1 (active X2)))
(rule (active (and X1 X2)) (and (active X1) X2))
(rule (U11 (mark X1) X2 X3) (mark (U11 X1 X2 X3)))
(rule (U12 (mark X1) X2) (mark (U12 X1 X2)))
(rule (U13 (mark X)) (mark (U13 X)))
(rule (U21 (mark X1) X2) (mark (U21 X1 X2)))
(rule (U22 (mark X)) (mark (U22 X)))
(rule (U31 (mark X1) X2 X3) (mark (U31 X1 X2 X3)))
(rule (U32 (mark X1) X2) (mark (U32 X1 X2)))
(rule (U33 (mark X)) (mark (U33 X)))
(rule (U41 (mark X1) X2) (mark (U41 X1 X2)))
(rule (U51 (mark X1) X2 X3) (mark (U51 X1 X2 X3)))
(rule (s (mark X)) (mark (s X)))
(rule (plus (mark X1) X2) (mark (plus X1 X2)))
(rule (plus X1 (mark X2)) (mark (plus X1 X2)))
(rule (U61 (mark X)) (mark (U61 X)))
(rule (U71 (mark X1) X2 X3) (mark (U71 X1 X2 X3)))
(rule (x (mark X1) X2) (mark (x X1 X2)))
(rule (x X1 (mark X2)) (mark (x X1 X2)))
(rule (and (mark X1) X2) (mark (and X1 X2)))
(rule (proper (U11 X1 X2 X3)) (U11 (proper X1) (proper X2) (proper X3)))
(rule (proper tt) (ok tt))
(rule (proper (U12 X1 X2)) (U12 (proper X1) (proper X2)))
(rule (proper (isNat X)) (isNat (proper X)))
(rule (proper (U13 X)) (U13 (proper X)))
(rule (proper (U21 X1 X2)) (U21 (proper X1) (proper X2)))
(rule (proper (U22 X)) (U22 (proper X)))
(rule (proper (U31 X1 X2 X3)) (U31 (proper X1) (proper X2) (proper X3)))
(rule (proper (U32 X1 X2)) (U32 (proper X1) (proper X2)))
(rule (proper (U33 X)) (U33 (proper X)))
(rule (proper (U41 X1 X2)) (U41 (proper X1) (proper X2)))
(rule (proper (U51 X1 X2 X3)) (U51 (proper X1) (proper X2) (proper X3)))
(rule (proper (s X)) (s (proper X)))
(rule (proper (plus X1 X2)) (plus (proper X1) (proper X2)))
(rule (proper (U61 X)) (U61 (proper X)))
(rule (proper |0|) (ok |0|))
(rule (proper (U71 X1 X2 X3)) (U71 (proper X1) (proper X2) (proper X3)))
(rule (proper (x X1 X2)) (x (proper X1) (proper X2)))
(rule (proper (and X1 X2)) (and (proper X1) (proper X2)))
(rule (proper (isNatKind X)) (isNatKind (proper X)))
(rule (U11 (ok X1) (ok X2) (ok X3)) (ok (U11 X1 X2 X3)))
(rule (U12 (ok X1) (ok X2)) (ok (U12 X1 X2)))
(rule (isNat (ok X)) (ok (isNat X)))
(rule (U13 (ok X)) (ok (U13 X)))
(rule (U21 (ok X1) (ok X2)) (ok (U21 X1 X2)))
(rule (U22 (ok X)) (ok (U22 X)))
(rule (U31 (ok X1) (ok X2) (ok X3)) (ok (U31 X1 X2 X3)))
(rule (U32 (ok X1) (ok X2)) (ok (U32 X1 X2)))
(rule (U33 (ok X)) (ok (U33 X)))
(rule (U41 (ok X1) (ok X2)) (ok (U41 X1 X2)))
(rule (U51 (ok X1) (ok X2) (ok X3)) (ok (U51 X1 X2 X3)))
(rule (s (ok X)) (ok (s X)))
(rule (plus (ok X1) (ok X2)) (ok (plus X1 X2)))
(rule (U61 (ok X)) (ok (U61 X)))
(rule (U71 (ok X1) (ok X2) (ok X3)) (ok (U71 X1 X2 X3)))
(rule (x (ok X1) (ok X2)) (ok (x X1 X2)))
(rule (and (ok X1) (ok X2)) (ok (and X1 X2)))
(rule (isNatKind (ok X)) (ok (isNatKind X)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))