I wanted to group my vars roughly as follows
group1 == <<x, y, z>>
group2 == <<a, b, c>>
vars == group1 \o group2 \* small circle is tuple concatenation
then to write
Spec == Init /\ [][Next]_vars
as usual. It doesn't work unless I write
vars == <<x, y, z, a, b, c>>
manually concatenating the tuples and, worse, repeating myself. Of course, in my real code, as opposed to this toy question, there are many variables with long names and the value of grouping them will be painfully obvious. My question is about the proper way to use the groups in constructing a term I can use for subscripting formulas.
Did I misunderstand tuple concatenation?