In the CL-calculus, there is a 'brute force' way of telling whether two expressions
F and G are equivalent. We substitute values (mark or void) for the letters. Of course,
there are many ways of doing this. Suppose we call each way of assigning a value to
every one of the n letters appearing in the expressions, a 'valuation' (so the number
of such valuations is 2^{n}). In the section
Consequences of the Standard Form Lemma we established the
following

If V is a valuation, let F_{V} stand for the value
attained by F when values are substituted for the letters of F according to the scheme
laid down by V. If F_{V} = G_{V} for all possible valuations V, then F and G are CL-equivalent
(meaning that one can get from one to the other using the allowed steps of the
CL-calculus, namely wrap, delete, copy and their inverses).

As stated in 'Consequences' the theorem is a corollary of the following

If E_{V} = _ for all possible valuations V of E, then E is void-equivalent
(meaning that E can be reduced to the void using the allowed steps of the
CL-calculus).

The Test Theorem follows from this because F and G are CL-equivalent if and only if their equivalence expression

(F(G))((F)G)

is void-equivalent. Another easy corollary (just apply theorem 2.2 to the circled expression (E)) is the following:

If E_{V} = O for all possible valuations V of E then E is mark-equivalent.

We will give proofs of theorems 2.2 and 2.3 below.

Can we do the same sort of thing in the CLS-calculus? We must recognize at the outset
that we will need to tread rather carefully. For if E is mark-equivalent (meaning now
E≅O) we can no longer infer that (E) is void-equivalent. Also there is the question,
what is the appropriate definition of a valuation of a CLS-expression? For the subscripts
of the atoms (which are the equivalents, in CLS, of the letters in CL) are now liable to
be *changed* by substitutions: how will a valuation keep pace with that?

We begin our approach to these daunting questions by introducing the notion of a 'valuation string', restricting ourselves, to start with, to the CL-calculus. We will then establish the first of our criteria for mark-equivalence in CLS.

A valuation string in CL is an expression each of whose factors is either a letter or a letter in a circle, and in which no letter is repeated. Note that the void counts as a valuation string (it's just that the number of letters is zero), but the mark does not. A valuation string is 'complete' (with respect to a given expression) if it contains every letter that occurs in the expression. Thus the valuation string

p (q) (r)

is not complete with respect to the expression

((p)(q(r)(t))),

but

p(q)(r)t

is.

Let V be a valuation string, complete with respect to an expression E, then the expression VE is equivalent either to V or to the mark O.

In the presence of V, each letter (for example, x) that appears in E can be uncopied, leaving behind either a blank (in case x is a factor of V) or a mark (in case it is (x) that is a factor of V). By doing this with all the letters, we reduce E to a C-expression (circle-expression), which is C-equivalent either to _ or to O. Thus either

VE = V_ = V

or

VE = VO = O ◊

Consider the set of all complete valuation strings involving n letters. It is clear that the set has
N = 2^{n} elements (since each letter may appear in a string either as itself, or circled);
let those elements be denoted V_{i}, with i running from 1 to N. Now consider
the expression Ω_{n} formed as follows

Ω_{n} ≡ ( (V_{1})(V_{2})...(V_{N}) ).

Then

Ω_{n} = _ ,

that is, Ω_{n} is CL-equivalent to the void.

We make use of the lemma of the CL-calculus,

(A) = (Ax)(A(x))

where A is any expression and x is any letter. When the number of letters is zero, there is only one valuation string, _ , and

Ω_{0} ≡ ( ( ) ) = _

∴ (Ω_{0}) = ( ).

Applying our lemma with the void substituted for A and the first letter, a say, substituted for x:

(Ω_{0}) = ( ) = (a)((a)) ≡ (Ω_{1}).

Applying the lemma to each of the two factors in turn, and using the second letter, b say, for x, we obtain:

(Ω_{1}) = (a) ((a)) = (ab) (a(b)) ((a)b) ((a)(b))
≡ (Ω_{2}).

The step may be repeated as many times as necessary, until we obtain the expression (Ω_{n}),
which is necessarily equivalent to (Ω_{0}) = O. Therefore

Ω_{n} = Ω_{0} = _ ◊

a) Suppose that in the presence of any complete valuation string E is reduced to the void; in other words,

V E = V

for any V in the set of complete valuation strings (N in number). Then E = _ .

b) Suppose, on the contrary, that E is reduced by any valuation string to the mark. Then E = O.

Using Lemma 2.5,

E = E _ = E Ω_{n} = E ( (V_{1})(V_{2})...(V_{N}) )

= ( (E V_{1})(E V_{2})...(E V_{N}) ) ;

the last step uses the CL-move we have called 'distribute'
(see this page), extended from the usual 2 to N factors inside the outer circle.
Now, in case (a) each occurrence of E is reduced to _ , so each E V_{i} is equivalent
to just V_{i}, which converts the expression back into Ω_{n},
implying E = _ . In case (b), each factor of the form (E V_{i}) is equivalent to (O),
equivalent to the void; which means that the outer circle contains nothing, and is therefore a mark. Thus E = O ◊

Theorems 2.2 and 3.3 are comprehended in parts a) and b), respectively, of Theorem 2.6. Note that part b) does not really require to be proved separately, since if E is always reduced to O, then (E) is always reduced to _ .

We say that a CLS-expression, E, is 'mark-equivalent' if and only if

E ≅ O .

If A = B, and θ is any substitution, then

Aθ = Bθ.

A = B says that there is some sequence of CL-operations that converts A into B. This sequence may ultimately broken down into a sequence of (un)wraps, (un)deletes and (un)copies. But the very same sequence of operations cannot fail to convert Aθ into Bθ. This is because any substitution necessarily preserves the 'sameness' of atoms. That is, if two atoms are the same, and are therefore able to participate in a 'copy' or 'uncopy' operation, they will still be the same, and just as able to participate in 'copy', after the substitution θ has been applied◊

Under the same assumptions, A Aθ = B Bθ.

If an expression E is converted into K by some combination of theta-copies and CL-operations, the same effect can be achieved by performing all the theta-copies first, and keeping the CL-operations to the end.

For simplicity, let us assume that just three theta-copies are involved: it will be apparent that our reasoning can be extended to more complicated instances. Suppose then that E Eθ is CL-equivalent to F, that F Fφ is CL-equivalent to G, and that G Gψ is CL-equivalent to K. Let us introduce the abbreviation

E[1+θ]

for the expression

E Eθ.

What we want to show is that E[1+θ][1+φ][1+ψ] is CL-equivalent to K. It is given that E[1+θ] is CL-equivalent to F; then E[1+θ][1+φ] is CL-equivalent to F[1+φ] by Corollary 2.9. But it is given that F[1+φ] = G, therefore E[1+θ][1+φ] = G. By the same reasoning,

E[1+θ][1+φ][1+ψ] = F[1+φ][1+ψ] = G[1+ψ] = K ◊

A necessary and sufficient condition for E to be mark-equivalent, is that there should exist a set of
substitutions θ_{1}, θ_{2}.. θ_{n} such that

Eθ_{1} Eθ_{2} ... Eθ_{n} = O,

where = denotes CL-equivalence (not mere CLS-equivalence).

(i) We prove first sufficiency of the condition. O = Eθ_{1}Eθ_{2}..
Eθ_{n} implies (by the dominance of the mark O)

O =

E Eθ_{1} Eθ_{2} Eθ_{1}θ_{2}

Eθ_{3} Eθ_{1}θ_{3} Eθ_{2}θ_{3}
Eθ_{1}θ_{2}θ_{3} ...

= E [1+θ_{1}][1+θ_{2}] ... [1+θ_{n}] ,

where, as before, [1+θ] stands for the operation which converts an expression F into F Fθ. Thus E is transformed into an expression that is CL-equivalent to O by doing n of these operations in succession, therefore E is CLS-equivalent to O.

(ii) Necessity. Suppose it is given that E ≅ O. This means that some combination of theta-copies and CL-operations converts E into O. It is possible that some of the theta-copy steps might be reverse theta-copies (where F Fθ is converted to F). But such steps can be omitted. For the effect of such a step is simply to get rid of an unwanted sub-expression Fθ. If the step is omitted, the unwanted sub-expression remains as an appendage to the 'wanted' part of the expression. If many such steps are omitted, the wanted expression will end up accompanied by a whole lot of unwanted 'junk'. However, if the wanted expression is CL-equivalent to O, then so is the whole expression, including the junk (by repeated application of 'delete'). Therefore, without loss of generality, we may assume that all the theta-copy steps are positive (not reverse) theta-copies.

By the Delay Principle (Lemma 2.10), we may assume that the sequence of steps leading from E to the mark consists of a number of theta-copies, followed by a number of CL-steps. So the sequence of theta-copies turns E into an expression that is CL-equivalent to O. Thus

O =
E[1+φ_{1}][1+φ_{2}]...[1+φ_{m}]

= E Eφ_{1} Eφ_{2} Eφ_{1}φ_{2}
Eφ_{3} Eφ_{1}φ_{3} Eφ_{2}φ_{3}
Eφ_{1}φ_{2}φ_{3} ...

But each term in this last expression is actually of the form Eθ for some θ — where we use the facts a) that 'do nothing' may be regarded as a trivial sort of substitution, and b) that the effect of performing two substitutions in a row may be regarded as the effect of performing just one (more comprehensive) substitution. Thus the expression is of the form

Eθ_{1} Eθ_{2}.. Eθ_{n} = O,

as required to prove Lemma 2.11◊