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

(fun f1 (-> Int Int  Int))
(fun u_14 (-> Int  Int))
(fun u_11 (-> Int Int  Int))
(fun u_7 (-> Int  Int))

(rule (u_14  w_5) w_5 :var ((w_5 Int)))
(rule (u_11  m w_4) (u_14  (f1  (-  m 1) w_4)) :var ((w_4 Int) (m Int)))
(rule (u_7  w_3) w_3 :var ((w_3 Int)))
(rule (f1  m n) (u_11  m (f1  m (-  n 1))) :guard (and (distinct m 0) (or (<= m 0) (distinct n 0))) :var ((n Int) (m Int)))
(rule (f1  m n) (u_7  (f1  (-  m 1) 1)) :guard (and (and (distinct m 0) (> m 0)) (= n 0)) :var ((n Int) (m Int)))
(rule (f1  m n) (+  n 1) :guard (= m 0) :var ((n Int) (m Int)))