(VAR x y)
(RULES
min(x, 0) -> 0
min(0, y) -> 0
min(s(x), s(y)) -> s(min(x, y))

max(x, 0) -> x
max(0, y) -> y
max(s(x), s(y)) -> s(max(x, y))

minus(x, 0) -> x
minus(s(x), s(y)) -> s(minus(x, any(y)))

gcd(s(x), s(y)) -> gcd( minus(max(x, y), min(x, y)), s(min(x, y)))

any(s(x)) -> s(s(any(x)))
any(x) -> x
)