Сравнение элементов последовательности и набора в TLA+

Question

Дана последовательность S = <<1,2,3,4>> и множество S' = {1,2,3,4,5,6}. Как мы можем проверить, содержат ли они оба одинаковые значения в TLA+?

Answer 1

Определять Range(f) == {f[x]: x \in DOMAIN f}, Поскольку все последовательности являются функциями, Range(S) даст нам значения последовательности S. Затем мы проверим оба имеют одинаковые элементы с Range(S) = S_prime,

(Мы не можем назвать это S' потому что это означает "следующее значение состояния S".)