YES Problem: f(f(X)) -> c() c() -> d() h(X) -> c() Proof: Polynomial Interpretation Processor: dimension: 1 interpretation: [h](x0) = x0 + 7x0x0 + 4, [d] = 0, [c] = 2, [f](x0) = 2x0 + 1 orientation: f(f(X)) = 4X + 3 >= 2 = c() c() = 2 >= 0 = d() h(X) = X + 7X*X + 4 >= 2 = c() problem: Qed