YES Problem: h(a(),b()) -> a() f(c()) -> f(c()) c() -> h(a(),h(b(),b())) Proof: Church Rosser Transformation Processor (critical pair closing system, Thm 2.4): c() -> h(a(),h(b(),b())) critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b] = 0, [c] = 5, [a] = 0, [h](x0, x1) = 4x0 + x1 + 2 orientation: c() = 5 >= 4 = h(a(),h(b(),b())) problem: Qed