TRS:
 {   a__f(X) -> g(h(f(X))),
  mark(f(X)) -> a__f(mark(X)),
  mark(g(X)) -> g(X),
  mark(h(X)) -> h(mark(X)),
     a__f(X) -> f(X)}
 RPO Product:
  Quasi-Precedence:
  mark > a__f
  empty
  
  Qed


TRS:
 {   a__f(X) -> g(h(f(X))),
  mark(f(X)) -> a__f(mark(X)),
  mark(g(X)) -> g(X),
  mark(h(X)) -> h(mark(X)),
     a__f(X) -> f(X)}
 Cdiprover:
  Interpretation class: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  mark(X4) = + 0*X4^2 + 0 + 3*X4
  a__f(X3) = + 0*X3^2 + 3 + 1*X3
  f(X2) = + 1*X2 + 1
  h(X1) = + 1*X1 + 1
  g(X0) = + 1*X0 + 1
  
  Qed