Problem: W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) F(H(x),y) -> F(H(x),G(y)) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x Proof: sorted: (order) 0:F(H(x),y) -> F(H(x),G(y)) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x 1:W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) ----- sorts [1>4, 2>3, 3>5, 4>5, 4>7, 5>6, 7>8] sort attachment (non-strict) W : 2 -> 2 B : 3 -> 2 I : 6 -> 5 F : 4 x 4 -> 1 H : 8 -> 7 G : 4 -> 4 ----- 0:F(H(x),y) -> F(H(x),G(y)) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x Church Rosser Transformation Processor: strict: F(H(x),y) -> F(H(x),G(y)) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x weak: critical peaks: 2 F(H(x27),G(I(y))) <-0|[]- F(H(x27),I(y)) -1|[]-> F(G(H(x27)),I(y)) F(G(H(x)),I(x30)) <-1|[]- F(H(x),I(x30)) -0|[]-> F(H(x),G(I(x30))) Closedness Processor (*parallel*): strict: weak: Qed 1:W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) Church Rosser Transformation Processor (kb): W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [B](x0) = x0, [I](x0) = x0 + 4, [W](x0) = x0 orientation: W(W(x)) = x >= x = W(x) B(I(x)) = x + 4 >= x = W(x) W(B(x)) = x >= x = B(x) problem: W(W(x)) -> W(x) W(B(x)) -> B(x) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [0] [B](x0) = [0 0 0]x0 + [1] [0 0 0] [0], [1 1 0] [0] [W](x0) = [0 0 0]x0 + [1] [0 0 0] [0] orientation: [1 1 0] [1] [1 1 0] [0] W(W(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = W(x) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] [0] W(B(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = B(x) [0 0 0] [0] [0 0 0] [0] problem: Qed