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

(format LCTRS :smtlib 2.6)
(theory Ints)

(define-fun max ((x Int) (y Int)) Int (ite (>= x y) x y))

(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 (minus x y) z :guard (and (>= y 0) (and (>= x y) (= z (max (- x y) 0)))))
(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)
;        minus(0,y) -> 0
;        minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
;        if_minus(true,s(x),y) -> 0
;        if_minus(false,s(x),y) -> s(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)
;
;)