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


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