; @origtpdbfilename ./TRS/secret06/cime1.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/cime1.xml"
(format TRS)
(fun * 2)
(fun |0| 0)
(fun |1| 0)
(fun |2| 0)
(fun . 2)
(fun |3| 0)
(fun min 0)
(fun + 2)
(rule (* |0| x) |0|)
(rule (* |1| x) x)
(rule (* |2| |2|) (. |1| |0|))
(rule (* |3| x) (. x (* min x)))
(rule (* min min) |1|)
(rule (* |2| min) (. min |2|))
(rule (* (. x y) z) (. (* x z) (* y z)))
(rule (* (+ y z) x) (+ (* x y) (* x z)))
(rule (+ |0| x) x)
(rule (+ x x) (* |2| x))
(rule (+ |1| |2|) |3|)
(rule (+ |1| min) |0|)
(rule (+ |2| min) |1|)
(rule (+ |3| x) (. |1| (+ min x)))
(rule (+ (. x y) z) (. x (+ y z)))
(rule (+ (* |2| x) x) (* |3| x))
(rule (+ (* min x) x) |0|)
(rule (+ (* |2| v) (* min v)) v)
(rule (. min |3|) min)
(rule (. x min) (. (+ min x) |3|))
(rule (. |0| x) x)
(rule (. x (. y z)) (. (+ x y) z))