Hi Ioannis,
as you noticed (and as stated on the Web site), the parser of the PM rejects any bindings involving tuples, such as
\E <<x,y>> \in S : ... or { ... : <<x,y>> \in S }
The next major release of TLAPS will be based on the SANY parser, so this limitation will disappear, but we don't know yet when the release will be ready.
Additionally, the backends currently have extremely poor support for functions that take more than one argument, such as in your example
If you look at the messages in the TLAPM console, you'll see that SMT, Zenon and Isabelle all complain about unsupported constructs. For the moment, I recommend as a workaround that you use "curried" functions instead and replace
[a,b \in S |-> TRUE] by [a \in S |-> [b \in S |-> TRUE]]
and similarly
[S \X T -> U] by [S -> [T -> U]]
Thanks for reminding us about this issue, which has been on our to-do list for too long already ...
Regards,
Stephan