; @author Jonas Schöpf
; commutativity and associativity rules
(format LCTRS :smtlib 2.6)
(theory Core)

(sort Unit)
(fun + (-> Unit Unit Unit))

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