; @author Jonas Schöpf
; Ctrl example from examples/ackermann.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun ackermann (-> Int Int  Int))
(fun U2 (-> Int Int Int Int  Int))
(fun U7 (-> Int Int Int Int  Int))

(rule (ackermann  x y) (U2  x y x y))
(rule (U7  x y m n) (U7  x y (-  m 1) 1) :guard (and (<= n 0) (> m 0)))
(rule (U7  x y m n) (+  n 1) :guard (and (<= n 0) (not (> m 0))))
(rule (U7  x y m n) (U7  x y (-  m 1) (U2  m (-  n 1) m (-  n 1))) :guard (and (not (<= n 0)) (> m 0)))
(rule (U7  x y m n) (+  n 1) :guard (and (not (<= n 0)) (not (> m 0))))
(rule (U2  x y m n) 0 :guard (or (< y 0) (< x 0)))
(rule (U2  x y m n) (U7  x y m n) :guard (and (not (or (< y 0) (< x 0))) (> m 0)))
(rule (U2  x y m n) (+  n 1) :guard (and (not (or (< y 0) (< x 0))) (not (> m 0))))