; @origtpdbfilename ./TRS/TRCSR/PEANO_nokinds_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/PEANO_nokinds_C.xml"
(format TRS)
(fun active 1)
(fun U11 2)
(fun tt 0)
(fun mark 1)
(fun U21 3)
(fun s 1)
(fun plus 2)
(fun and 2)
(fun isNat 1)
(fun |0| 0)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (U11 tt N)) (mark N))
(rule (active (U21 tt M N)) (mark (s (plus N M))))
(rule (active (and tt X)) (mark X))
(rule (active (isNat |0|)) (mark tt))
(rule (active (isNat (plus V1 V2))) (mark (and (isNat V1) (isNat V2))))
(rule (active (isNat (s V1))) (mark (isNat V1)))
(rule (active (plus N |0|)) (mark (U11 (isNat N) N)))
(rule (active (plus N (s M))) (mark (U21 (and (isNat M) (isNat N)) M N)))
(rule (active (U11 X1 X2)) (U11 (active X1) X2))
(rule (active (U21 X1 X2 X3)) (U21 (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 (and X1 X2)) (and (active X1) X2))
(rule (U11 (mark X1) X2) (mark (U11 X1 X2)))
(rule (U21 (mark X1) X2 X3) (mark (U21 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 (and (mark X1) X2) (mark (and X1 X2)))
(rule (proper (U11 X1 X2)) (U11 (proper X1) (proper X2)))
(rule (proper tt) (ok tt))
(rule (proper (U21 X1 X2 X3)) (U21 (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 (and X1 X2)) (and (proper X1) (proper X2)))
(rule (proper (isNat X)) (isNat (proper X)))
(rule (proper |0|) (ok |0|))
(rule (U11 (ok X1) (ok X2)) (ok (U11 X1 X2)))
(rule (U21 (ok X1) (ok X2) (ok X3)) (ok (U21 X1 X2 X3)))
(rule (s (ok X)) (ok (s X)))
(rule (plus (ok X1) (ok X2)) (ok (plus X1 X2)))
(rule (and (ok X1) (ok X2)) (ok (and X1 X2)))
(rule (isNat (ok X)) (ok (isNat X)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))