Problem: c(b(a(X))) -> a(a(b(b(c(c(X)))))) a(X) -> e() b(X) -> e() c(X) -> e() Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {4,3,2} transitions: e1() -> 5* c0(1) -> 2* b0(1) -> 4* a0(1) -> 3* e0() -> 1* 5 -> 2,4,3 problem: Qed