[1 .. 3]([3 .. 5]p1 /\ [{1,2}]p2) /\ [{4}]([{3}]p2 /\ [{1,2}]p1)->[1 .. 5][1 .. 5] (p1 /\ p2)
