Problem:
 f(a(),x) -> g(a(),x)
 g(a(),x) -> f(b(),x)
 f(a(),x) -> f(b(),x)

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    f1(8,1) -> 3,4
    f1(8,2) -> 3,4
    b1() -> 8*
    g1(6,2) -> 3*
    g1(6,1) -> 3*
    a1() -> 6*
    f2(10,1) -> 3*
    f2(10,2) -> 3*
    f0(1,2) -> 3*
    f0(2,1) -> 3*
    f0(1,1) -> 3*
    f0(2,2) -> 3*
    b2() -> 10*
    a0() -> 1*
    g0(1,2) -> 4*
    g0(2,1) -> 4*
    g0(1,1) -> 4*
    g0(2,2) -> 4*
    b0() -> 2*
  problem:
   
  Qed