ws1s;
ex1 x1: ~ex1 x2: x1 < x2;