Problem:
 f(X,X) -> f(a(),n__b())
 b() -> a()
 b() -> n__b()
 activate(n__b()) -> b()
 activate(X) -> X

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {13,12,11,5,4,3}
   transitions:
    f0(2,12) -> 3*
    f0(13,1) -> 3*
    f0(13,13) -> 3*
    f0(1,2) -> 3*
    f0(1,12) -> 3*
    f0(12,1) -> 3*
    f0(2,1) -> 3*
    f0(12,13) -> 3*
    f0(2,13) -> 3*
    f0(13,2) -> 3*
    f0(13,12) -> 3*
    f0(1,1) -> 3*
    f0(1,13) -> 3*
    f0(12,2) -> 3*
    f0(2,2) -> 3*
    f0(12,12) -> 3*
    activate0(12) -> 5*
    activate0(2) -> 5*
    activate0(1) -> 5*
    activate0(13) -> 5*
    b1() -> 11*,4,5
    f1(7,12) -> 3*
    f1(13,6) -> 3*
    f1(13,12) -> 3*
    f1(7,6) -> 3*
    n__b2() -> 11,6,4,2,5,12*
    a2() -> 11,7,4,1,5,13*
    1 -> 5*
    2 -> 5*
    12 -> 5*
    13 -> 5*
  problem:
   
  Qed