(meta-info (comment "Example 7 standard TRS taken from Nagele et al. 2016"))
(format LCTRS)

(fun + 2 :sort (Unit Unit Unit))
(fun * 2 :sort (Unit Unit Unit))

(rule (+ x y) (+ y x))
(rule (* (+ x y) z) (+ (* x z) (* y z)))
(rule (* (+ y x) z) (+ (* x z) (* y z)))