; @author Jonas Schöpf
; @author Aart Middeldorp
; example 16
(format LCTRS)
(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))
(rule (g n) b :guard (= n 0))
(rule (f n) (f m) :guard (and (> n 0) (= (* 2 m) n)))
(rule (f n) (f m) :guard (and (> n 0) (= (+ (* 2 m) 1) n)))
(rule (g n) (g m) :guard (and (> n 0) (= (* 2 m) n)))
(rule (g n) (g m) :guard (and (> n 0) (= (+ (* 2 m) 1) n)))