P<=>((=(x1,x2)&=(x3,x4)&P1(x1,x3))=>P1(x2,x4))?