; @author Jonas Schöpf
; translated from TPDB AG01/#3.5a.trs

(format LCTRS :smtlib 2.6)
(theory Ints)

(fun minus (-> Int Int Int))
(fun cmod (-> Int Int Int))
(fun if_mod (-> Int Int Int))
(fun pred (-> Int Int))
(fun build (-> Int Int))

(rule (build 0) 0)
(rule (build x) (pred (build (- x 1))) :guard (> x 0))
(rule (minus x y) (- x y) :guard (and (>= y 0) (>= x y)))
(rule (minus x y) (build (- y x)) :guard (and (>= x 0) (> y x)))
(rule (cmod x y) 0 :guard (or (= x 0) (and (= y 0) (> x 0))))
(rule (cmod x y) (if_mod x y)  :guard (and (> x 0) (> y 0)))
(rule (if_mod x y) (cmod (minus (- x 1) (- y 1)) y) :guard (and (<= (- y 1) (- x 1)) (and (> x 1) (> y 1))))
(rule (if_mod x y) x :guard (and (not (<= (- y 1) (- x 1))) (and (> x 1) (> y 1))))

; TPDB version
;(VAR x y )
;(RULES
;        le(0,y) -> true
;        le(s(x),0) -> false
;        le(s(x),s(y)) -> le(x,y)
;        pred(s(x)) -> x
;        minus(x,0) -> x
;        minus(x,s(y)) -> pred(minus(x,y))
;        mod(0,y) -> 0
;        mod(s(x),0) -> 0
;        mod(s(x),s(y)) -> if_mod(le(y,x),s(x),s(y))
;        if_mod(true,s(x),s(y)) -> mod(minus(x,y),s(y))
;        if_mod(false,s(x),s(y)) -> s(x)
;
;)