Re: Tagged formulas

   Basically I'm looking for a "lowering" operator where:

   Lower(x) == the level-0 _expression_ (constant value) which
               is equal to x in this state

I can't think of any way to define such an operator, but it may help
to observe that if Foo is defined by

Foo(a, b) == a' = e1 /\ b' = e2

Then \E t : (t=x) /\ Foo(t,y)' is equivalent to Foo(x, y').

TLC's requirement that x' be determined in a single _expression_ means
that I can't write:

\A t \in DOMAIN x : x'[t] = e \* e is some _expression_

   This is not a problem when only one variable is involved, as you can
   do:

x' = [t \in DOMAIN x |-> e]

This is exactly the kind of situation that I was talking about. Those
two formulas are not equivalent. The second determines the value of
x'. The first tells you very little about the value of x'. All it tells
you are the values of x'[t] for t \in DOMAIN x. It tells you nothing
about the domain of x'. It doesn't even tell you if x' is a function.
Hence, it's not a sensible formula--at least, not by itself. The following
formula is equivalent to the second one:

/\ x' = [t \in DOMAIN x |-> x'[t]]
/\ \A t \in DOMAIN x : x'[t] = e

but it's hardly simper than the second one.

So, as I wrote before, when TLC doesn't allow you to write something
you think it should, then it's often the case that what you wrote
isn't what you meant to write. You should learn to read what a
formula says rather than what you want it to say. This requires that
you stop thinking of TLA+ formula as a program and start thinking of
it as a mathematical assertion. Occasionally, this is difficult. For
example, if you write

f[n \in Nat] == IF n = 0 THEN x ELSE f[n-1]'

it's not easy to realize that if x is a variable, then f[2] is not
equal to the illegal _expression_ (x')'.

Leslie