Let M be an NTM.  Then, we can encode all configurations of M as binary
strings.  Let <x> be the binary encoding of a configuration x.
We will need to insist that <x> always ends with 1: this will allow
us to "pad" with zeros later in the proof.  (See "Padding" below.)

We can make sure that there are constants A and B such that:
If the length of x is m, the length of <x> is no more than A + Bm.

The values of A and B depend on M, but for each M, they are constant.

Theorem: Given an NTM M, there exist constants A,B,C such that:

For any input string w, and for any t-step computation of M with input w
resulting in configuration x, the length of <x> is no more than
A + B|w| + Ct.

Again, the values of A, B, and C depend on M, but for each M, they are
constant.

Remark: Given a configuration x whose encoding <x> has length p, we
represent x as an assignment of the Boolean variables b_1, b_2, ... b_p.
That is: b_i is true if and only if the i^{th} bit of <x> is 1.

Padding: Given a configuration x whose encoding <x> has length q, where
q < p, we can represent x as an assignment of the Boolean variables b_1,
b_2, ... b_p, where b_{q+1} ... b_p are all false.  Because b_q = true,
we can tell the actual length of <x>.