Problem:
 f(X,g(X)) -> f(1(),g(X))
 g(1()) -> g(0())

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    f0(1,2) -> 3*
    f0(2,1) -> 3*
    f0(1,1) -> 3*
    f0(2,2) -> 3*
    g0(1) -> 4*
    10() -> 1*
    g1(2) -> 4*
    01() -> 2*
  problem:
   
  Qed