Equality in set theory is defined as "same members" but while everything in TLA+ is a set, be it 1, "a", or [n ∈ Nat ↦ n + 1], the members of those sets aren't defined in the axioms of TLA+, and as we don't know what the members of 1 and "a" are, we cannot compare them. This is a good thing as it makes "nonsensical" propositions, such as 1 ∈ 3 undefined (indeterminable, really).We can compare objects on which equality is defined by the axioms of TLA+. In particular, if there is some set S such that a ∈ S and b ∈ S, then the truth of the proposition a = b is defined. And as Nat ⊆ Int ⊆ Real, all numbers can be compared. The rules for functions derived from that and from the fact that TLA+ defines the DOMAIN operator on all functions (so two functions are equal if their domains are equal and their mappings on the domain are equal), and that's how operators like Len work. Recursively, this means that sets with comparable members can be compared, and functions with comparable domains and ranges can be compared. This is why sequences with comparable elements can be compared, and why strings, which are also functions can be compared.-- RonOn Sunday, July 26, 2020 at 1:18:42 PM UTC+1 emanuel....@xxxxxxxxx wrote:Hi,This rises some more questions:* How is equality/unequality defined actually?** What about '1 = 2' and 1 /= 2?** What about '1.0 = 1' and 1.0 /= 1?** What about '3.14 = 1' and 3.14 /= 1?As far as I know, every value is a set in TLA+.We just don't care what the elmenets are in 1, 3.14 etc.Right?As far as I know, sets are equal if they have the same elements.This means, that we can't compare sets of unknown elements.* So what we can compare?* Why Len() from Sequences works as expected?Thanks,Emanuel