<< >> = { }

[fl <freder...@xxxxxxxxxxx>]

 

 

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.

 

  (see http://us2.metamath.org:88/mpegif/funrel.html)

 

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

 

    ( see http://us2.metamath.org:88/mpegif/reldm0.html)

 

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

 

--

FL