; @author Naoki Nishida
; Example 7 of IWC 2024 paper (Kojima and Nishida)
; secret problem 2024
; category: LCTRS
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Loc)
(sort State)
(fun state (-> Loc State))
(fun f (-> Int Loc))
(fun g (-> Int Int Loc))
(fun h (-> Int Int Loc))

(rule (state (f x)) (state (g x y)) :guard (>= y x) :var ((y Int)))
(rule (state (f x)) (state (h x y)) :guard (>= y x) :var ((y Int)))
(rule (state (g x y)) (state (f x)) :guard (<= y x))
(rule (state (g x y)) (state (g x y1)) :guard (and (> y x) (= y1 (+ y 1))) :var ((y1 Int)))
(rule (state (h x y)) (state (f x)) :guard (<= y x))
(rule (state (h x y)) (state (h x y1)) :guard (and (> y x) (= y1 (+ y 1))) :var ((y1 Int)))