The above way of rephrasing a counterfactual as a statement about state-vectors is insufficient in general. It does not specify how each step is to be done in other cases. There are three steps.
. We replace the terms t that are co-ordinates by their the
contents functions applied to the term, i.e. c(t,xi).
This gives the equation
11 above.
Our state vector does not have values for all terms, just those in our co-ordinate frame. Thus, for our numerical example, the set of co-ordinates is,
We need to distinguish between the value of a constant x and its
name 
. Here in bold font refers to the name x, while x in
plain font denotes the value of x.
Let the state vector assign these the terms
. The propositions
that the state vector encodes are thus the three propositions,
Here we have used x, in plain font, as the proposition states that
the value of is the value of the term 
.
We assign a co-ordinate a value using the a assignment function. We can determine the value of a co-ordinate in a state vector using c, the contents function.
We call the set of co-ordinates our frame, and we assume that they are exactly the names of terms that are true of the predicate f. Rather than assume that there is only a single frame, we can make the frame an argument of c and a. This gives the axioms,
However, for notational convenience we assume that the frame is recoverable from the state vector, so we keep the ternary a and the binary c whenever what frame we are using is clear from the context.
Our state vector thus uniquely determines the values of the co-ordinates in the frame. From these values, we can determine a theory, the set of sentences implied by the statements that the co-ordinates have the values in the state vector.
The propositions that our state vector gives us may not be all the facts about the world. In our numerical example, the extra fact,
was also the case.
We usually insist that our approximate theory is consistent with our frame. That is, the propositions true at every point in our frame are consistent with the approximate theory.
To reiterate, a co-ordinate frame, f, is a tuple of names of terms.
In the simplest case these are constants. A point p in a
co-ordinate frame f is a tuple of terms, equal in number to the
co-ordinates of f, and having the type/sort of the corresponding
term in f. In the simplest case, this is a tuple of values, the
denotation of the terms. The state vector that assigns the
co-ordinates f the terms p is denoted 
.
The relativization of a theory A to a state vector variable , written 
and
a set of co-ordinates X is the theory resulting from replacing each
co-ordinate x by , and replacing each function, predicate
and constant k not in X by a function from to the type/sort
of k.
We now consider our first example. We define our frame as follows.
It is important to note that 
are names of constants, not
variables themselves.
We now define our initial state vector 
.
We need unique names axioms for the names of terms. We use natural numbers as their own names, for simplicity.
We then have that
We can derive this from the second property of a
and c, and the fact that 
We have x = 1, y = 3, z = 1 
.
We have this set of sentences as our theory, as these are the formulas that result from the terms x,y etc. to their values, 1, etc. in the state vector.
We now prove that the first two counterfactuals that we considered in our skiing story are true and false respectively. To show this we need to introduce an axiomatization of skiing, which we do in the nest section. The axiomatization is only needed for proving the later theorems, and may be skipped by the un-interested reader.