Problem:
 active(f(f(X))) -> mark(c(f(g(f(X)))))
 active(c(X)) -> mark(d(X))
 active(h(X)) -> mark(c(d(X)))
 mark(f(X)) -> active(f(mark(X)))
 mark(c(X)) -> active(c(X))
 mark(g(X)) -> active(g(X))
 mark(d(X)) -> active(d(X))
 mark(h(X)) -> active(h(mark(X)))
 f(mark(X)) -> f(X)
 f(active(X)) -> f(X)
 c(mark(X)) -> c(X)
 c(active(X)) -> c(X)
 g(mark(X)) -> g(X)
 g(active(X)) -> g(X)
 d(mark(X)) -> d(X)
 d(active(X)) -> d(X)
 h(mark(X)) -> h(X)
 h(active(X)) -> h(X)

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {8,7,6,5,4,3,2}
   transitions:
    active0(1) -> 2*
    f0(1) -> 4*
    mark0(1) -> 3*
    c0(1) -> 5*
    g0(1) -> 6*
    d0(1) -> 7*
    h0(1) -> 8*
    f140() -> 1*
  problem:
   
  Qed