; @author Jonas Schöpf ; @author Aart Middeldorp ; example 19 (format LCTRS) (theory Ints) (fun f (-> Int Int)) (fun g (-> Int Int)) (fun h (-> Int Int)) (rule (f x) 2 :guard (and (<= 1 x) (<= x 3))) (rule (f x) (g x) :guard (and (<= 2 x) (<= x 4))) (rule (g x) (h x)) (rule (h x) y :guard (and (= x 2) (= y x))) (rule (h x) y :guard (and (= x 3) (= y 2)))