Problem: I(x) -> I(B(x)) F(E(x),x) -> G(x) E(x) -> x Proof: sorted: (order) 0:I(x) -> I(B(x)) 1:F(E(x),x) -> G(x) E(x) -> x ----- sorts [1>8, 2>3, 2>4, 3>6, 4>5, 5>7, 6>7] sort attachment (non-strict) I : 8 -> 1 B : 8 -> 8 F : 4 x 7 -> 2 E : 7 -> 5 G : 6 -> 3 ----- 0:I(x) -> I(B(x)) Church Rosser Transformation Processor: strict: I(x) -> I(B(x)) weak: critical peaks: 0 Closedness Processor (*parallel*): strict: weak: Qed 1:F(E(x),x) -> G(x) E(x) -> x Nonconfluence Processor: terms: F(x,x) *<- F(E(x),x) ->* G(x) Qed