; @author Jonas Schöpf
; @doi 10.4230/LIPIcs.FSCD.2018.30
; Example 37 (modified and corrected)
; we need a conversion toTree for type checking and to have a valid LCTRS
(format LCTRS :smtlib 2.6)
(theory Ints)

(sort List)
(sort Tree)
(fun add (-> Int List List))
(fun cons (-> Int List List))
(fun @ (-> List List List))
(fun sorting (-> List List))
(fun flatten (-> Tree List))
(fun tsorting (-> Tree Tree))
(fun N (-> Tree Tree Tree))
(fun L (-> Int Tree))
(fun Nil List)
(fun singleton (-> Int List))
(fun toTree (-> List Tree))

(rule (@ Nil xs) xs)
(rule (add x Nil) (singleton x))
(rule (add x (cons y ys)) (cons y (add x ys)) :guard (>= x y))
(rule (sorting (cons x xs)) (add x (sorting xs)))
(rule (flatten (N x y)) (@ (flatten x) (flatten y)))
(rule (tsorting t) (toTree (sorting (flatten t))))
(rule (@ (cons x xs) ys) (cons x (@ xs ys)))
(rule (add x (cons y ys)) (cons x (cons y ys)) :guard (< x y))
(rule (sorting Nil) Nil)
(rule (flatten (L x)) (singleton x))
(rule (N x y) (N y x))