YES
LCTRS
  Theories
    Core, Ints
  Signature
    f: (Int, Int) -> Int
    g: (Int, Int) -> Int
    h: Int -> Int
  Rules
    f(?28, ?29) -> +(f(?30, ?29), 1) [and(>=(?28, 1), ?30 = -(?28, 1))]
    f(?31, ?32) -> g(1, ?31) [?32 = 0, <=(?31, 1)]
    g(?33, ?34) -> ?34 [?33 = 0, <=(?35, 0)]
    g(?36, ?37) -> +(g(1, 0), 1) [?36 = 1, ?37 = 1]
    h(?38) -> +(g(1, ?38), 1) [<=(?38, 1)]
    h(?39) -> +(+(f(?40, 0), 1), 1) [and(>(?39, 1), ?40 = -(?39, 1))]
Confluent by NewmansLemma with proof:
  Termination:
    DPGraph with indexed dependency pairs
      {1: f#(?28, ?29) -> f#(?30, ?29) [and(>=(?28, 1), =(?30, -(?28, 1)))]
      , 2: f#(?31, ?32) -> g#(1, ?31) [=(?32, 0), <=(?31, 1)]
      , 3: g#(?36, ?37) -> g#(1, 0) [=(?36, 1), =(?37, 1)]
      , 4: h#(?38) -> g#(1, ?38) [<=(?38, 1)]
      , 5: h#(?39) -> f#(?40, 0) [and(>(?39, 1), =(?40, -(?39, 1)))]}
    and edges
      1 -> {1, 2}
      2 -> {3}
      3 -> {}
      4 -> {3}
      5 -> {1, 2}
    with 1 SCC(s)
      SCC:
        {f#(?28, ?29) -> f#(?30, ?29) [and(>=(?28, 1), =(?30, -(?28, 1)))]}
    RPO with precedence:
      {h} > {f} > {f# and = g >= > <= 1 0 - +}
  Local Confluence:
      * Critical Pair
        Inner Rule
          f(?28', ?29') -> +(f(?30', ?29'), 1) [and(>=(?28', 1), ?30' = -(?28', 1))]
        Outer Rule
          f(?28", ?29") -> +(f(?30", ?29"), 1) [and(>=(?28", 1), ?30" = -(?28", 1))]
        Pair
          +(f(?30', ?29"), 1) ≈ +(f(?30", ?29"), 1) [and(>=(?28", 1), ?30' = -(?28", 1)), and(>=(?28", 1), ?30" = -(?28", 1))]
      which reaches the trivial constrained equation
        +(f(?30', ?29"), 1) ≈ +(f(?30", ?29"), 1) [and(>=(?28", 1), ?30' = -(?28", 1)), and(>=(?28", 1), ?30" = -(?28", 1))]
      * Critical Pair
        Inner Rule
          f(?31', ?32') -> g(1, ?31') [?32' = 0, <=(?31', 1)]
        Outer Rule
          f(?28", ?29") -> +(f(?30", ?29"), 1) [and(>=(?28", 1), ?30" = -(?28", 1))]
        Pair
          g(1, ?28") ≈ +(f(?30", ?29"), 1) [?29" = 0, <=(?28", 1), and(>=(?28", 1), ?30" = -(?28", 1))]
      which reaches the trivial constrained equation
        g(1, ?28") ≈ +(f(?30", ?29"), 1) [?29" = 0, <=(?28", 1), and(>=(?28", 1), ?30" = -(?28", 1))]
          ->^* +(g(1, 0), 1) ≈ +(f(?30", ?29"), 1) [?29" = 0, <=(?28", 1), and(>=(?28", 1), ?30" = -(?28", 1))]
          -> +(g(1, 0), 1) ≈ +(g(1, ?30"), 1) [?29" = 0, <=(?28", 1), and(>=(?28", 1), ?30" = -(?28", 1))]
      * Critical Pair
        Inner Rule
          f(?28', ?29') -> +(f(?30', ?29'), 1) [and(>=(?28', 1), ?30' = -(?28', 1))]
        Outer Rule
          f(?31", ?32") -> g(1, ?31") [?32" = 0, <=(?31", 1)]
        Pair
          +(f(?30', ?32"), 1) ≈ g(1, ?31") [and(>=(?31", 1), ?30' = -(?31", 1)), ?32" = 0, <=(?31", 1)]
      which reaches the trivial constrained equation
        +(f(?30', ?32"), 1) ≈ g(1, ?31") [and(>=(?31", 1), ?30' = -(?31", 1)), ?32" = 0, <=(?31", 1)]
          ->^* +(g(1, ?30'), 1) ≈ g(1, ?31") [and(>=(?31", 1), ?30' = -(?31", 1)), ?32" = 0, <=(?31", 1)]
          -> +(g(1, ?30'), 1) ≈ +(g(1, 0), 1) [and(>=(?31", 1), ?30' = -(?31", 1)), ?32" = 0, <=(?31", 1)]
      * Critical Pair
        Inner Rule
          h(?39') -> +(+(f(?40', 0), 1), 1) [and(>(?39', 1), ?40' = -(?39', 1))]
        Outer Rule
          h(?39") -> +(+(f(?40", 0), 1), 1) [and(>(?39", 1), ?40" = -(?39", 1))]
        Pair
          +(+(f(?40', 0), 1), 1) ≈ +(+(f(?40", 0), 1), 1) [and(>(?39", 1), ?40' = -(?39", 1)), and(>(?39", 1), ?40" = -(?39", 1))]
      which reaches the trivial constrained equation
        +(+(f(?40', 0), 1), 1) ≈ +(+(f(?40", 0), 1), 1) [and(>(?39", 1), ?40' = -(?39", 1)), and(>(?39", 1), ?40" = -(?39", 1))]

Elapsed Time: 325.37 ms