# << >> = { }

Sometimes the mathematics behind TLA+ puzzle me.

For instance in TLA+ it is possible to prove that

ASSUME NEW A PROVE << >> = [ x \in { } |-> A ]

So DOMAIN << >> = { } and << >> is a function.

If << >> is a function then << >> is a relation.

But if << >> is a function and DOMAIN << >> = { } then << >> = { }

But I can't prove << >> = { } with TLA+. Why ?

--
FL