; @origtpdbfilename ./TRS/various/13.trs
; @xtcfilename "./TRS_Standard/Various_04/13.xml"
(format TRS)
(fun O 1)
(fun |0| 0)
(fun + 2)
(fun I 1)
(fun * 2)
(fun - 2)
(fun |1| 0)
(rule (O |0|) |0|)
(rule (+ |0| x) x)
(rule (+ x |0|) x)
(rule (+ (O x) (O y)) (O (+ x y)))
(rule (+ (O x) (I y)) (I (+ x y)))
(rule (+ (I x) (O y)) (I (+ x y)))
(rule (+ (I x) (I y)) (O (+ (+ x y) (I |0|))))
(rule (* |0| x) |0|)
(rule (* x |0|) |0|)
(rule (* (O x) y) (O (* x y)))
(rule (* (I x) y) (+ (O (* x y)) y))
(rule (- x |0|) x)
(rule (- |0| x) |0|)
(rule (- (O x) (O y)) (O (- x y)))
(rule (- (O x) (I y)) (I (- (- x y) (I |1|))))
(rule (- (I x) (O y)) (I (- x y)))
(rule (- (I x) (I y)) (O (- x y)))