; @author Jonas Schöpf
(format LCTRS :smtlib 2.6)
(theory Ints)
(define-fun isEven ((x Int)) Bool (= (mod x 2) 0))
(sort NList)
(fun build (-> Int NList NList))
(fun nats NList)
(fun cons (-> Int NList NList))
(fun nil NList)
(rule nats (build 0 nil))
(rule (build n xs) (build (+ n 1) (cons n xs)) :guard (and (isEven n) (>= n 0)))
(rule (build n xs) (build (+ n 1) xs) :guard (and (not (isEven n)) (>= n 0)))