; @author Jonas Schöpf
; @cops 189
; transformed and modified TRS from COPS 189.trs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun dbl (-> Int Int))

(rule (dbl 0) 0)
(rule (dbl (+ x 1)) (+ (dbl x) 2))
(rule (dbl (+ x y)) (+ (dbl x) (dbl y)))