Problem: f(a()) -> f(f(a())) a() -> b() f(x) -> f(b()) Proof: Church Rosser Transformation Processor (no redundant rules): strict: f(x) -> f(b()) a() -> b() f(a()) -> f(f(a())) weak: critical peaks: 3 f(b()) <-0|[]- f(a()) -2|[]-> f(f(a())) f(b()) <-1|0[]- f(a()) -2|[]-> f(f(a())) f(f(a())) <-2|[]- f(a()) -0|[]-> f(b()) Closedness Processor (*strongly -- <=7 steps*): Qed