; @origtpdbfilename ./TRS/Cime/ternary.trs
; @xtcfilename "./TRS_Standard/CiME_04/ternary.xml"
(format TRS)
(fun |0| 1)
(fun |#| 0)
(fun + 2)
(fun |1| 1)
(fun j 1)
(fun opp 1)
(fun - 2)
(fun * 2)
(rule (|0| |#|) |#|)
(rule (+ |#| x) x)
(rule (+ x |#|) x)
(rule (+ (|0| x) (|0| y)) (|0| (+ x y)))
(rule (+ (|0| x) (|1| y)) (|1| (+ x y)))
(rule (+ (|1| x) (|0| y)) (|1| (+ x y)))
(rule (+ (|0| x) (j y)) (j (+ x y)))
(rule (+ (j x) (|0| y)) (j (+ x y)))
(rule (+ (|1| x) (|1| y)) (j (+ (+ x y) (|1| |#|))))
(rule (+ (j x) (j y)) (|1| (+ (+ x y) (j |#|))))
(rule (+ (|1| x) (j y)) (|0| (+ x y)))
(rule (+ (j x) (|1| y)) (|0| (+ x y)))
(rule (+ (+ x y) z) (+ x (+ y z)))
(rule (opp |#|) |#|)
(rule (opp (|0| x)) (|0| (opp x)))
(rule (opp (|1| x)) (j (opp x)))
(rule (opp (j x)) (|1| (opp x)))
(rule (- x y) (+ x (opp y)))
(rule (* |#| x) |#|)
(rule (* (|0| x) y) (|0| (* x y)))
(rule (* (|1| x) y) (+ (|0| (* x y)) y))
(rule (* (j x) y) (- (|0| (* x y)) y))
(rule (* (* x y) z) (* x (* y z)))