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

(format LCTRS :smtlib 2.6)
(theory Ints)

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

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

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