; @author Jonas Schöpf
; Ctrl example from examples/student/sumfrom01.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Result)
(sort Result1)
(sort Result2)
(fun u3 (-> Int Int Int Int Result2 Int))
(fun return2 (-> Int Result2))
(fun max (-> Int Int Result2))
(fun return (-> Int Int))
(fun u2 (-> Int Int Int Int Result1 Int))
(fun return1 (-> Int Result1))
(fun u1 (-> Int Int Int Int Int))
(fun min (-> Int Int Result1))
(fun sum2 (-> Int Int Int))
(fun hikaku (-> Int Int Int))

(rule (u3 x y t i (return2 k)) (u3 x y (+ t i) (+ i 1) (max x y)) :guard (not (<= i k)) :var ((x Int) (y Int) (t Int) (i Int) (k Int)))
(rule (u3 x y t i (return2 k)) (return t) :guard (<= i k) :var ((x Int) (y Int) (t Int) (i Int) (k Int)))
(rule (u2 x y t i (return1 k)) (u3 x y t k (max x y)) :var ((x Int) (y Int) (t Int) (i Int) (k Int)))
(rule (u1 x y t i) (u2 x y 0 i (min x y)) :guard (not (> x y)) :var ((x Int) (y Int) (t Int) (i Int)))
(rule (u1 x y t i) (return 0) :guard (> x y) :var ((x Int) (y Int) (t Int) (i Int)))
(rule (sum2 x y) (u1 x y 0 rnd) :var ((x Int) (y Int) (rnd Int)))
(rule (min x y) (return1 y) :guard (not (> y x)) :var ((x Int) (y Int)))
(rule (min x y) (return1 x) :guard (> y x) :var ((x Int) (y Int)))
(rule (max x y) (return2 y) :guard (not (> x y)) :var ((x Int) (y Int)))
(rule (max x y) (return2 x) :guard (> x y) :var ((x Int) (y Int)))