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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {5,4,3,2}
   transitions:
    f3(41) -> 42*
    g3(47) -> 48*
    g3(53) -> 54*
    mark3(48) -> 49*
    active4(60) -> 61*
    g4(59) -> 60*
    active0(1) -> 2*
    c0() -> 1*
    mark0(1) -> 3*
    f0(1) -> 4*
    g0(1) -> 5*
    active1(14) -> 15*
    c1() -> 10*
    mark1(12) -> 13*
    f1(11) -> 12*
    g1(10) -> 11*
    active2(30) -> 31*
    f2(29) -> 30*
    f2(23) -> 24*
    mark2(24) -> 25*
    mark2(36) -> 37*
    g2(35) -> 36*
    g2(22) -> 23*
    c2() -> 22*
    active3(42) -> 43*
    active3(54) -> 55*
    10 -> 35,14
    11 -> 29*
    13 -> 2*
    15 -> 3*
    22 -> 47*
    23 -> 41*
    25 -> 15,3
    31 -> 13,2
    35 -> 53*
    37 -> 31,13
    43 -> 25,15
    47 -> 59*
    49 -> 43,25,15,3
    55 -> 37,31,13,2
    61 -> 49,43
  problem:
   
  Qed