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