Problem: F(x,y) -> c(y) G(x) -> x f(x) -> g(x) g(x) -> c(x) Proof: sorted: (order) 0:F(x,y) -> c(y) 1:G(x) -> x 2:f(x) -> g(x) g(x) -> c(x) ----- sorts [1>5, 1>10, 2>9, 3>4, 4>5, 5>6, 6>7, 6>11, 7>8] sort attachment (non-strict) F : 10 x 11 -> 1 c : 6 -> 5 G : 9 -> 2 f : 8 -> 3 g : 7 -> 4 ----- 0:F(x,y) -> c(y) Church Rosser Transformation Processor: strict: weak: critical peaks: 0 Qed 1:G(x) -> x Church Rosser Transformation Processor: strict: weak: critical peaks: 0 Qed 2:f(x) -> g(x) g(x) -> c(x) Church Rosser Transformation Processor: strict: weak: critical peaks: 0 Qed