; @author Jonas Schöpf
; @author Aart Middeldorp
; @doi 10.1007/978-3-031-90643-5_7
; example 6
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun a Int)
(fun b Int)
(fun f (-> Int Int))
(fun g (-> Int Int))

(rule a (f n) :guard (>= n 0))
(rule a (g n) :guard (>= n 0))
(rule (f n) b :guard (= n 0) :var ((n Int)))
(rule (g n) b :guard (= n 0) :var ((n Int)))
(rule (f n) (f m) :guard (and (> n 0) (= (* 2 m) n)) :var ((n Int)))
(rule (f n) (f m) :guard (and (> n 0) (= (+ (* 2 m) 1) n)) :var ((n Int)))
(rule (g n) (g m) :guard (and (> n 0) (= (* 2 m) n)) :var ((n Int)))
(rule (g n) (g m) :guard (and (> n 0) (= (+ (* 2 m) 1) n)) :var ((n Int)))