; @author Jonas Schöpf
; @doi 10.48550/arXiv.1601.03206
; Example 1 (without restriction to 16-bit Ints)
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun A (-> Int Int Int))

(rule (A m n) (A (- m 1) (A m (- n 1))) :guard (and (not (= m 0)) (not (= n 0))))
(rule (A m 0) (A (- m 1) 1) :guard (not (= m 0)))
(rule (A 0 n) (+ n 1))