; @author Jonas Schöpf
; Ctrl example from completion/sort.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)

(sort List)
(fun insert (-> Int List List))
(fun sorting (-> List List))
(fun cons (-> Int List List))
(fun nil List)
(fun rev (-> List List))
(fun app (-> List List List))
(fun tsorting (-> List List))
(fun flatten (-> List List))
(fun leaf (-> Int List))
(fun node (-> List List List))

(rule (app nil xs) xs)
(rule (app (cons x xs) ys) (cons x (app xs ys)))
(rule (insert x nil) (cons x nil))
(rule (insert x (cons y nil)) (cons x (cons y nil)) :guard (< x y))
(rule (insert x (cons y ys)) (cons y (insert x ys)) :guard (>= x y))
(rule (sorting nil) nil)
(rule (sorting (cons x xs)) (insert x (sorting xs)))
(rule (flatten (leaf x)) (cons x nil))
(rule (flatten (node x y)) (app (flatten x) (flatten y)))
(rule (node x y) (node y x))
(rule (tsorting x) (sorting (flatten x)))