YES
LCTRS
  Theories
    Core, Ints
  Signature
    g1: Int -> Int
    triangle1: Int -> Int
    u_2: Int -> Int
    u_9: (Int, Int) -> Int
  Rules
    u_9(!n, !w_4) -> +(!n, !w_4)
    g1(!n) -> u_9(!n, g1(-(!n, 1))) [>(!n, 0)]
    g1(!n) -> 0 [<=(!n, 0)]
    u_2(!w_2) -> !w_2
    triangle1(!n) -> u_2(g1(!n))
DPGraph with indexed dependency pairs
  {1: g1#(!n) -> u_9#(!n, g1(-(!n, 1))) [>(!n, 0)]
  , 2: g1#(!n) -> g1#(-(!n, 1)) [>(!n, 0)]
  , 3: triangle1#(!n) -> u_2#(g1(!n))
  , 4: triangle1#(!n) -> g1#(!n)}
and edges
  1 -> {}
  2 -> {1, 2}
  3 -> {}
  4 -> {1, 2}
with 1 SCC(s)
  SCC:
    {g1#(!n) -> g1#(-(!n, 1)) [>(!n, 0)]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(g1#) = 1
    removing the rule(s):
      {g1#(!n) -> g1#(-(!n, 1)) [>(!n, 0)]}

Elapsed Time:  32.45 ms