[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Function domains in TLAPS

You seem to think that for any function f, you should be able to deduce

   (f[3] = 8) => (3 \in DOMAIN f)

That formula is equivalent to

    (3 \notin DOMAIN f)  =>  (f[3] # 8)

From what general properties of functions would you expect to be able
to deduce this?