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