(VAR y x) (THEORY (C gcd)) (RULES le(0, y) -> true le(s(x), 0) -> false le(s(x), s(y)) -> le(x, y) minus(x, 0) -> x minus(s(x), s(y)) -> minus(x, y) gcd(0, y) -> y gcd(s(x), 0) -> s(x) gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)) if_gcd(true, s(x), s(y)) -> gcd(minus(x, y), s(y)) if_gcd(false, s(x), s(y)) -> gcd(minus(y, x), s(x)) )