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

(sort Unit)
(fun f (-> Int Int  Unit))
(fun g (-> Int  Unit))

(rule (f  x4 (+  x4 y4)) (g  y4) :guard (> x4 0))
(rule (f  x3 y3) (g  y3) :guard (< x3 y3))
(rule (f  x2 y2) (g  x2) :guard (<= x2 y2))
(rule (f  x1 y1) (g  (+  x1 y1)) :guard (>= x1 y1))