YES Problem: and(not(not(x)),y,not(z)) -> and(y,band(x,z),x) Proof: Matrix Interpretation Processor: dim=1 interpretation: [band](x0, x1) = 3x0 + x1 + 3, [and](x0, x1, x2) = 6x0 + 6x1 + 5x2, [not](x0) = 2x0 + 1 orientation: and(not(not(x)),y,not(z)) = 24x + 6y + 10z + 23 >= 23x + 6y + 6z + 18 = and(y,band(x,z),x) problem: Qed