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