Problem: a(a(y,0()),0()) -> y c(c(y)) -> y c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y) Proof: Bounds Processor: bound: 0 enrichment: match automaton: final states: {3,2} transitions: a0(1,1) -> 2* 00() -> 1* c0(1) -> 3* problem: Qed