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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {6,5,4,3}
   transitions:
    active1(15) -> 16*
    active1(13) -> 14*
    d1() -> 7*
    c1() -> 13*
    mark1(7) -> 8*
    active2(25) -> 26*
    d2() -> 21*
    mark2(21) -> 22*
    active0(2) -> 3*
    active0(1) -> 3*
    active3(29) -> 30*
    g0(2) -> 5*
    g0(1) -> 5*
    d3() -> 29*
    mark0(2) -> 4*
    mark0(1) -> 4*
    h0(2) -> 6*
    h0(1) -> 6*
    c0() -> 1*
    d0() -> 2*
    7 -> 15*
    8 -> 3*
    14 -> 4*
    16 -> 4*
    21 -> 25*
    22 -> 14,4
    26 -> 8,3
    30 -> 22,14
  problem:
   
  Qed