NO Problem: 0(x) -> 1(x) 0(0(x)) -> 0(x) 3(4(5(x))) -> 4(3(5(x))) 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2(2(2(2(2(2(2(2(2(2(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> 1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0(1(0(0(1(1(0( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0(1(1(1(1(0(0(0(1(1(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 0(0(1(1(0(0(1(0(0(1(0(1(1(1(0(1(0(1(1(0(1(1(0(0(1(0(0(1(1(0(0(1(0(1( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0(0(1(0(1(1(1(1(1(1(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2(2(2(2(2(2(2(2(2(2(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Proof: sorted: (order-sorted) 0:3(4(5(x))) -> 4(3(5(x))) 1:0(x) -> 1(x) 0(0(x)) -> 0(x) 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2(2(2(2(2(2(2(2(2(2(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> 1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0(1(0(0(1(1( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0(1(1(1(1(0(0(0(1(1(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 0(0(1(1(0(0(1(0(0(1(0(1(1(1(0(1(0(1(1(0(1(1(0(0(1(0(0(1(1(0(0(1(0( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0(0(1(0(1(1(1(1(1(1(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2(2(2(2(2(2(2(2(2(2(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ----- sorts [0>1, 1>2] sort attachment (non-strict) 0 : 3 -> 3 1 : 3 -> 3 3 : 0 -> 0 4 : 0 -> 0 5 : 2 -> 1 2 : 3 -> 3 ----- 0:3(4(5(x))) -> 4(3(5(x))) Church Rosser Transformation Processor: critical peaks: joinable Qed 1:0(x) -> 1(x) 0(0(x)) -> 0(x) 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2(2(2(2(2(2(2(2(2(2(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> 1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0(1(0(0(1(1( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0(1(1(1(1(0(0(0(1(1(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 0(0(1(1(0(0(1(0(0(1(0(1(1(1(0(1(0(1(1(0(1(1(0(0(1(0(0(1(1(0(0(1(0( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0(0(1(0(1(1(1(1(1(1(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2(2(2(2(2(2(2(2(2(2(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Nonconfluence Processor: terms: 2(1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1(1(1(0(0(0(1(1(x1679))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *<- 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2 ( 2(2(2(2(2(2(2(2(x1679)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* 1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0(1(0(0(1(1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 1 ( 1 ( 0 ( 0 ( 1 ( 0 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 1 ( 0 ( 1 ( 1 ( 1 ( 1 ( 0 ( 0 ( 0 ( 0 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 1 ( 0 ( 0 ( 0 ( 1 ( 1 ( 0 ( 1 ( 1 ( 0 ( 1 ( 0 ( 0 ( 0 ( 0 ( 1 ( 1 ( 1(1(0(0(0(1(1(2(x1679))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Qed