; @author Jonas Schöpf
; @author Aart Middeldorp
; @doi 10.1007/978-3-031-38499-8_27
; Example 6
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun ack (-> Int Int Int))

(rule (ack  0 n) (+  n 1) :guard (>= n 0))
(rule (ack  m 0) (ack  (-  m 1) 1) :guard (> m 0))
(rule (ack  m n) (ack  (-  m 1) (ack  m (-  n 1))) :guard (and (> m 0) (> n 0)))
(rule (ack  m n) 0 :guard (or (< m 0) (< n 0)))