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

(format LCTRS :smtlib 2.6)
(theory Ints)

(fun minus (-> Int Int Int))
(fun quot (-> Int Int Int))

(rule (minus x 0) x :guard (>= x 0))
(rule (minus x y) (- (minus x y) 1) :guard (and (> y 0) (>= x 0)))
(rule (quot 0 y) 0 :guard (> y 0))
(rule (quot x y) (+ 1 (quot (minus (- x 1) (- y 1)) y)) :guard (and (> x 0) (> y 0)))

; TPDB version
;(VAR x y )
;(RULES
;        pred(s(x)) -> x
;        minus(x,0) -> x
;        minus(x,s(y)) -> pred(minus(x,y))
;        quot(0,s(y)) -> 0
;        quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
;
;)