YES Problem: not(x) -> if(x,false(),true()) and(x,y) -> if(x,y,false()) or(x,y) -> if(x,true(),y) implies(x,y) -> if(x,y,true()) =(x,x) -> true() =(x,y) -> if(x,y,not(y)) if(true(),x,y) -> x if(false(),x,y) -> y if(x,x,if(x,false(),true())) -> true() =(x,y) -> if(x,y,if(y,false(),true())) Proof: Matrix Interpretation Processor: dim=1 interpretation: [=](x0, x1) = 4x0 + 7x1 + 7, [implies](x0, x1) = 4x0 + 4x1 + 4, [or](x0, x1) = 4x0 + 7x1 + 1, [and](x0, x1) = 4x0 + 2x1 + 6, [if](x0, x1, x2) = x0 + x1 + 6x2, [true] = 0, [false] = 1, [not](x0) = x0 + 1 orientation: not(x) = x + 1 >= x + 1 = if(x,false(),true()) and(x,y) = 4x + 2y + 6 >= x + y + 6 = if(x,y,false()) or(x,y) = 4x + 7y + 1 >= x + 6y = if(x,true(),y) implies(x,y) = 4x + 4y + 4 >= x + y = if(x,y,true()) =(x,x) = 11x + 7 >= 0 = true() =(x,y) = 4x + 7y + 7 >= x + 7y + 6 = if(x,y,not(y)) if(true(),x,y) = x + 6y >= x = x if(false(),x,y) = x + 6y + 1 >= y = y if(x,x,if(x,false(),true())) = 8x + 6 >= 0 = true() =(x,y) = 4x + 7y + 7 >= x + 7y + 6 = if(x,y,if(y,false(),true())) problem: not(x) -> if(x,false(),true()) and(x,y) -> if(x,y,false()) if(true(),x,y) -> x Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1] [and](x0, x1) = [0 0 0]x0 + x1 + [0] [0 0 0] [0], [1 0 0] [1 0 0] [if](x0, x1, x2) = [0 0 0]x0 + x1 + [0 0 0]x2 [0 0 0] [0 0 0] , [0] [true] = [0] [0], [0] [false] = [0] [0], [1 0 0] [1] [not](x0) = [0 0 0]x0 + [0] [0 0 0] [0] orientation: [1 0 0] [1] [1 0 0] not(x) = [0 0 0]x + [0] >= [0 0 0]x = if(x,false(),true()) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] and(x,y) = [0 0 0]x + y + [0] >= [0 0 0]x + y = if(x,y,false()) [0 0 0] [0] [0 0 0] [1 0 0] if(true(),x,y) = x + [0 0 0]y >= x = x [0 0 0] problem: if(true(),x,y) -> x Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [1 1 1] [1 0 0] [0] [if](x0, x1, x2) = [0 0 0]x0 + [1 1 1]x1 + [0 0 0]x2 + [1] [0 0 0] [1 1 1] [0 0 0] [1], [0] [true] = [0] [1] orientation: [1 1 1] [1 0 0] [1] if(true(),x,y) = [1 1 1]x + [0 0 0]y + [1] >= x = x [1 1 1] [0 0 0] [1] problem: Qed