YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
    b: Int
    f: Int -> Int
    g: Int -> Int
  Rules
    a -> f(!n) [>=(!n, 0)]
    a -> g(!n) [>=(!n, 0)]
    f(!n) -> b [!n = 0]
    g(!n) -> b [!n = 0]
    f(!n) -> f(!m) [and(>(!n, 0), *(2, !m) = !n)]
    f(!n) -> f(!m) [and(>(!n, 0), +(*(2, !m), 1) = !n)]
    g(!n) -> g(!m) [and(>(!n, 0), *(2, !m) = !n)]
    g(!n) -> g(!m) [and(>(!n, 0), +(*(2, !m), 1) = !n)]
RPO with precedence:
  {a} > {g f} > {and = b >= > 2 1 0 + *}

Elapsed Time:  41.35 ms