YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
    b: Int
    f: (Int, Int) -> Int
    g: (Int, Int) -> Int
    h: Int -> Int
  Rules
    a -> b
    f(?12, ?13) -> g(a, +(?13, ?13)) [and(>=(?13, ?12), ?13 = 1)]
    g(?14, ?15) -> g(?15, ?14)
    h(f(?16, ?17)) -> h(g(b, 2)) [>=(?16, ?17)]
Confluent by Parallel Closedness with proof:
    * Critical Pair
      Inner Rule
        f(?12', ?13') -> g(a, +(?13', ?13')) [and(>=(?13', ?12'), ?13' = 1)]
      Outer Rule
        h(f(?16", ?17")) -> h(g(b, 2)) [>=(?16", ?17")]
      Pair
        h(g(a, +(?17", ?17"))) ≈ h(g(b, 2)) [and(>=(?17", ?16"), ?17" = 1), >=(?16", ?17")]
    which reaches the trivial constrained equation
      h(g(a, +(?17", ?17"))) ≈ h(g(b, 2)) [and(>=(?17", ?16"), ?17" = 1), >=(?16", ?17")]
        -||-> h(g(b, ?262')) ≈ h(g(b, 2)) [and(>=(?17", ?16"), ?17" = 1), >=(?16", ?17"), and(>=(?17", ?16"), ?17" = 1), >=(?16", ?17"), ?262' = +(?17", ?17")]

Elapsed Time:  86.74 ms