YES Input TRS: 1: a() -> b() 2: f(a()) -> b() 3: g(x) -> g(a()) | f(x) --> x Infeasibility test: f(x) --> x Co-Order(NegReal,≥,Sum) ... succeeded. a() weight: (- (/ 1 2)) b() weight: -1 f(x1) weight: (- (/ 1 2)) + x1 #(x1) weight: x1 g(x1) weight: x1