Quickly add a free MyWikiBiz directory listing!

Propositional Equation Reasoning Systems

MyWikiBiz, Author Your Legacy — Saturday November 22, 2008

This article develops elementary facts about the formal calculi that we describe as propositional equation reasoning systems (PERS). This work follows up on the alpha graphs that Charles Sanders Peirce devised as a graphical syntax for propositional calculus and also on the calculus of indications that George Spencer Brown presented in his Laws of Form.

Formal development

The first order of business is to give the exact forms of the axioms that we use, devolving from Peirce's "Logical Graphs" via Spencer-Brown's Laws of Form (LOF). In formal proofs, we use a variation of the annotation scheme from LOF to mark each step of the proof according to which axiom, or initial, is being invoked to justify the corresponding step of syntactic transformation, whether it applies to graphs or to strings.

Axioms

The axioms are just four in number, divided into the arithmetic initials, $I_1\!$ and $I_2,\!$ and the algebraic initials, $J_1\!$ and $J_2.\!$

	(1)
	(2)
	(3)
	(4)

One way of assigning logical meaning to the initial equations is known as the entitative interpretation (EN). Under EN, the axioms read as follows:

$\begin{array}{ccccc} I_1 & : & \operatorname{true}\ \operatorname{or}\ \operatorname{true} & = & \operatorname{true} \\ I_2 & : & \operatorname{not}\ \operatorname{true}\ & = & \operatorname{false} \\ J_1 & : & a\ \operatorname{or}\ \operatorname{not}\ a & = & \operatorname{true} \\ J_2 & : & (a\ \operatorname{or}\ b)\ \operatorname{and}\ (a\ \operatorname{or}\ c) & = & a\ \operatorname{or}\ (b\ \operatorname{and}\ c) \\ \end{array}$

Another way of assigning logical meaning to the initial equations is known as the existential interpretation (EX). Under EX, the axioms read as follows:

$\begin{array}{ccccc} I_1 & : & \operatorname{false}\ \operatorname{and}\ \operatorname{false} & = & \operatorname{false} \\ I_2 & : & \operatorname{not}\ \operatorname{false} & = & \operatorname{true} \\ J_1 & : & a\ \operatorname{and}\ \operatorname{not}\ a & = & \operatorname{false} \\ J_2 & : & (a\ \operatorname{and}\ b)\ \operatorname{or}\ (a\ \operatorname{and}\ c) & = & a\ \operatorname{and}\ (b\ \operatorname{or}\ c) \\ \end{array}$

All of the axioms in this set have the form of equations. This means that all of the inference licensed by them are reversible. The proof annotation scheme employed below makes use of a double bar $\overline{\underline{~~~~~~}}$ to mark this fact, but it will often be left to the reader to decide which of the two possible ways of applying the axiom is the one that is called for in a particular case.

Peirce introduced these formal equations at a level of abstraction that is one step higher than their customary interpretations as propositional calculi, which two readings he called the Entitative and the Existential interpretations, here referred to as "EN" and "EX", respectively. The early CSP, as in his essay on "Qualitative Logic", and also GSB, emphasized the EN interpretation, while the later CSP developed mostly the EX interpretation.

Frequently used theorems

C₁. Double negation theorem

The first theorem goes under the names of Consequence 1 $(C_1)\!$ , the double negation theorem (DNT), or Reflection.

(5)

The proof that follows is adapted from the one that was given by George Spencer Brown in his book Laws of Form (LOF) and credited to two of his students, John Dawes and D.A. Utting.

(6)

(7)

C₂. Generation theorem

One theorem of frequent use goes under the nickname of the weed and seed theorem (WAST). The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader. What the WAST says is that a label can be freely distributed or freely erased anywhere in a subtree whose root is labeled with that label. The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem. In LOF, it goes by the names of Consequence 2 $(C_2)\!$ or Generation.

(8)

Here is a proof of the Generation Theorem.

(9)

C₃. Dominant form theorem

The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as Consequence 3 $(C_3)\!$ or Integration. A better mnemonic might be dominance and recession theorem (DART), but perhaps the brevity of dominant form theorem (DFT) is sufficient reminder of its double-edged role in proofs.

(10)

Here is a proof of the Dominant Form Theorem.

(11)

Exemplary proofs

Based on the axioms given at the outest, and aided by the theorems recorded so far, it is possible to prove a multitude of much more complex theorems. A couple of all-time favorites are given next.

Peirce's law

Main article : Peirce's law

Peirce's law is commonly written in the following form:

$((p \Rightarrow q) \Rightarrow p) \Rightarrow p$

The existential graph representation of Peirce's law is shown in Figure 12.

(12)

A graphical proof of Peirce's law is shown in Figure 13.

(13)

Praeclarum theorema

An illustrious example of a propositional theorem is the praeclarum theorema, the admirable, shining, or splendid theorem of Leibniz.

If a is b and d is c, then ad will be bc.

This is a fine theorem, which is proved in this way:

a is b, therefore ad is bd (by what precedes),

d is c, therefore bd is bc (again by what precedes),

ad is bd, and bd is bc, therefore ad is bc. Q.E.D.

(Leibniz, Logical Papers, p. 41).

Under the existential interpretation, the praeclarum theorema is represented by means of the following logical graph.

(14)

And here's a neat proof of that nice theorem.

(15)

Formal extension : Cactus calculus

Let us now extend the CSP–GSB calculus in the following way:

The first extension is the reflective extension of logical graphs, or what may be described as the cactus language, after its principal graph-theoretic data structure. It is generated by generalizing the negation operator $(\_)\!$ in a particular manner, treating $(\_)\!$ as the minimal negation operator of order 1, and adding another such operator for each integer parameter greater than 1. Taken in series, the minimal negation operators are symbolized by parenthesized argument lists of the following shapes: $(\_),\!$ $(\_, \_),\!$ $(\_, \_, \_),\!$ and so on, where the number of argument slots is the order of the reflective negation operator in question.

The formal rule of evaluation for a $k\!$ -lobe or $k\!$ -operator may be summarized as follows:

o-----------------------------------------------------------o
| Evaluation Rule ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` x_1 `x_2` `...` x_k ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `o----o-...-o----o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ( x_1, x_2, ..., x_k )` ` = ` ` ` ` ` <space> ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` IF AND ONLY IF` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` |
| ` Just one of the x_1, x_2, ..., x_k` `=` `|` `=` `( )` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

The interpretation of these operators, read as assertions about the values of their listed arguments, is as follows:

o-----------------------------------------------------------o
| Interpretation Rule ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` x_1 `x_2` `...` x_k ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o----o-...-o----o` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| A "k-lobe operator" of the form "(x_1, ..., x_k)" ` ` ` ` |
| enjoys two commonly employed interpretations for` ` ` ` ` |
| propositional logic, in other words, two ways of` ` ` ` ` |
| taking it as an assertion about, or a constraint` ` ` ` ` |
| upon, the logical values of the listed arguments, ` ` ` ` |
| the mentioned variables x_j, for j = 1 through k. ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| Existential Interpretation: ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` `"Just one of the k arguments is not true." ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| Entitative `Interpretation: ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` `"Not just one of the k arguments is true." ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

Case analysis-synthesis theorem

The task at hand is to lay out what I think of as the pontoon bridge between the model-theoretic and the proof-theoretic shores, and thus between their diverging perspectives on logical procedure, even if I can construct it at a point but so close to their common source that it may not seem like it's worth the candle.

The substance of this principle was known to Boole in the 1850's, tantamount to what we now call the boolean expansion of a propositional expression. The only novelty here resides in a certain manner of presentation, in which we will prove the basic principle from the axioms given before. One name for this rule is the Case Analysis-Synthesis Theorem (CAST).

I am going to revert to my customarily sloppy workshop manners and refer to propositions and proposition expressions on rough analogy with functions and function expressions, which implies that a proposition will be regarded as the chief formal object of discussion, enjoying many proposition expressions, formulas, or sentences that express it, but worst of all I will probably just go ahead and use any and all of these terms as loosely as I see fit, taking a bit of extra care only when I see the need.

Let $Q\!$ be a propositional expression with an unspecified, but context-appropriate number of variables, say, none, or $x,\!$ or $x_1, \ldots, x_k,\!$ as the case may be.

Strings and graphs that have no labels are called bare.
A bare terminal node, symbolized by a small circle $\circ$ in text, is known as a stone.
A bare terminal edge, symbolized by a vertical bar $\vert$ in text, is known as a stick.

Let the replacement expression of the form $Q[\circ /x]$ denote the proposition that results from $Q\!$ by replacing every token of the variable $x\!$ with a blank, that is to say, by erasing $x.\!$

Let the replacement expression of the form $Q[\,\vert /x]$ denote the proposition that results from $Q\!$ by replacing every token of the variable $x\!$ with a stick stemming from the site of $x.\!$

In the case of a propositional expression $Q\!$ that has no token of the designated variable $x,\!$ let it be stipulated that $Q[\circ /x] = Q = Q[\,\vert /x].$

I think that I am at long last ready to state the following:

o-----------------------------------------------------------o
| Case Analysis-Synthesis Theorem (CAST)` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `x` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `x` `|` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` Q[o/x] o---o Q[|/x] ` ` |
| ` ` ` ` ` ` `Q` ` ` ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `Q` ` ` ` ` ` ` = ` ( Q[o/x] x , Q[|/x] (x) ) |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

In order to think of tackling even the roughest sketch toward a proof of this theorem, we need to add a number of axioms and axiom schemata. Because I abandoned proof-theoretic purity somewhere in the middle of grinding this calculus into computational form, I never got around to finding the most elegant and minimal, or anything near a complete set of axioms for the cactus language, so what I list here are just the slimmest rudiments of the hodge-podge of rules of thumb that I have found over time to be necessary and useful in most working settings. Some of these special precepts are probably provable from genuine axioms, but I have yet to go looking for a more proper formulation.

o-----------------------------------------------------------o
| Precept L_1.` Indifference` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` a ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` a ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `(a, (a)) ` ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` Split <---- | ----> Merge ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

 
o-----------------------------------------------------------o
| Precept L_2.` Equality. `The Following Are Equivalent:` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` b ` ` ` ` ` ` ` a ` b ` ` ` ` ` ` ` a ` ` ` ` ` |
| ` ` ` ` ` o ` ` ` ` ` ` ` o---o ` ` ` ` ` ` ` o ` ` ` ` ` |
| ` ` ` a ` | ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` | ` b ` ` ` |
| ` ` ` o---o ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` o---o ` ` ` |
| ` ` ` `\ /` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` `\ /` ` ` ` |
| ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `(a, (b)) ` ` = ` ` ((a , b)) ` ` = ` ` ((a), b)` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

 
o-----------------------------------------------------------o
| Precept L_3.` Dispersion` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| For k > 1, the following equation holds:` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` y_1 ` `y_2` `...` ` y_k ` ` x y_1 `x y_2` `...` x y_k ` |
| ` `o------o-...-o------o` ` ` ` `o------o-...-o------o` ` |
| ` ` \ ` ` ` ` ` ` ` ` / ` ` ` ` ` \ ` ` ` ` ` ` ` ` / ` ` |
| ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` |
| ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` |
| ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` |
| ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` |
| ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` |
| ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` |
| ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` |
| ` ` ` ` ` `x @` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` x (y_1, ..., y_k) ` ` ` = ` ` (x y_1, ..., x y_k) ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` Distill ` ` <---- | ----> ` ` Disperse` ` ` ` ` |
o-----------------------------------------------------------o

To see why the Dispersion Rule holds, look at it this way: If $x\!$ is true, then the presence of $x\!$ makes no difference on either side of the equation, but if $x\!$ is false, then both sides of the equation are false.

Here is a proof sketch for the Case Analysis-Synthesis Theorem (CAST):

o-----------------------------------------------------------o
| Case Analysis-Synthesis Theorem.` Proof Sketch. ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `Q` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< L1. Split " " >=============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `o---o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `Q @` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< L3. Disperse "Q" >==========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `Q o---o Q` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< C1. Reflect "x" >===========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `Q o---o Q[((x))/x] ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< C2. Weed "x", "(x)" >=======o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x ` |` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` Q[o/x] o---o Q[|/x] ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< QES >=======================o

NB. QES = "Quod Erat Sketchiendum".

Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions. Once again, let us turn to the example of Leibniz's Praeclarum Theorema as a way of illustrating how.

o-----------------------------------------------------------o
| Praeclarum Theorema.` Proof by CAST.` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` a o ` o d ` ` o ad` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "a" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `bc ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` b o ` o c ` o o ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` | ` | ` ` |/` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` `o--o ` o d ` o d ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` o c ` ` o ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` | ` ` `/` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` `o--o ` o d ` o ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` o c ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` ` ` ` ` o d ` ` ` ` ` ` ` |
| ` ` ` `\ / ` ` `| ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "d" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` b ` c ` `bc ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` o ` o o ` o o ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` |/` ` |/` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` b ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` o ` ` o ` ` o ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` `/` ` `/` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` b ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "b" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` ` ` o ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` |
| ` ` o ` o c ` o c ` ` ` ` ` ` o ` o c ` o c ` ` ` ` ` ` ` |
| ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` |
| ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` |
| ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` ` o c ` o c ` ` ` ` ` ` ` ` o c ` o c ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` |
| ` ` ` `/` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o c ` o c ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` o ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `/` ` ` | ` ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o c ` o c ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `/` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "c" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` `/` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` c o-------------------------o---o c ` ` ` ` ` ` ` ` ` ` |
| ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` c o-------------------------o---o c ` ` ` ` ` ` ` ` ` ` |
| ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `c o---o---o c` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< QED >=======================o

What we have harvested is the succulent equivalent of a disjunctive normal form (DNF) for the proposition with which we started. Remembering that a blank node is the graphical equivalent of a logical value true, we can read this brand of DNF in the following manner:

o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `c o---o---o c` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| Either not 'a' and thus 'true'` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` Or ` ` 'a' and thus ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `Either not 'd' and thus 'true' ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `Or ` ` 'd' and thus` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` Either not 'b' and thus 'true'` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` Or ` ` 'b' and thus ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `Either not 'c' and thus 'true' ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` `Or ` ` 'c' and thus true.` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

That is tantamount to saying that the proposition being submitted for analysis is true in each case. Ergo we are justly entitled to title it a Theorem.

Logic as sign transformation

We have been looking at various ways of transforming propositional expressions, expressed in the parallel formats of character strings and graphical structures, all the while preserving certain aspects of their "meaning" — and here I risk using that vaguest of all possible words, but only as a promissory note, hopefully to be cached out in a more meaningful species of currency as the discussion develops.

I cannot pretend to be acquainted with or to comprehend every form of intension that others might find of interest in a given form of expression, nor can I speak for every form of meaning that another might find in a given form of syntax. The best that I can hope to do is to specify what my object is in using these expressions, and to say what aspects of their syntax are meant to serve this object, lending these properties the interest I have in preserving them as I put the expressions through the paces of their transformations.

On behalf of this object I have been spinning in the form of this thread a developing example base of propositional expressions, in the data structures of graphs and strings, along with many examples of step-wise transformations on these expressions that preserve something of significant logical import, something that might be referred to as their logical equivalence class (LEC), and that we could as well call the constraint information or the denotative object of the expression in view.

To focus still more, let us return to that Splendid Theorem noted by Leibniz, and let us look more carefully at the two distinct ways of transforming its initial expression that we just used to arrive at an equivalent expression, one that made its tautologous character or its theorematic nature as evident as it could be.

Just to remind you, here is the Splendid Theorem again:

o-----------------------------------------------------------o
| Praeclarum Theorema (PT)` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` a o ` o d ` ` o ad` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` @ ` ` ` ` ` ` ` ` ` = ` ` ` ` ` ` ` ` ` @ ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| `((a(b))(d(c))((ad(bc)))) ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

The first way of transforming the expression that appears on the left hand side of the equation can be described as proof-theoretic in character. That was given in Note 5.

PERS Note 5.

The other way of transforming the expression that appears on the left hand side of the equation can be described as model-theoretic in character. That was given in Note 9.

PERS Note 9.

What we have here amounts to a couple of different styles of communicational conduct, or conductive communication, if you prefer, that is to say, two sequences of signs of the form $e_1, e_2, \ldots, e_n,\!$ each one beginning with a problematic expression and eventually ending with a clear expression of the appropriate logical equivalence class (LEC) to which each and every sign or expression in the sequence belongs.

Ordinarily, any orbit through a locus of signs can be taken to reflect an underlying sign-process, a case of semiosis. So what we have here are two very special cases of semiosis, and what we might just find it useful to contemplate is how to characterize them as two species of a very general class.

We are starting to delve into some fairly picayune details of a particular sign system, non-trivial enough in its own right but still rather simple compared to the types of our ultimate interest, and though I believe that this exercise will be worth the effort in prospect of understanding more complicated sign systems, I feel that I ought to say a few words about the larger reasons for going through this work.

My broader interest lies in the theory of inquiry as a special application or a special case of the theory of signs. Another name for the theory of inquiry is logic and another name for the theory of signs is semiotics. So I might as well have said that I am interested in logic as a special application or a special case of semiotics. But what sort of a special application? What sort of a special case? Well, I think of logic as formal semiotics — though, of course, I am not the first to have said such a thing — and by formal we say, in our etymological way, that logic is concerned with the form, indeed, with the animate beauty and the very life force of signs and sign actions. Yes, perhaps that is far too Latin a way of understanding logic, but it's all I've got.

Now, if you think about these things just a little more, I know that you will find them just a little suspicious, for what besides logic would I use to do this theory of signs that I would apply to this theory of inquiry that I'm also calling logic? But that is precisely one of the things signified by the word formal, for what I'd be required to use would have to be some brand of logic, that is, some sort of innate or inured skill at inquiry, but a style of logic that is casual, catch-as-catch-can, formative, incipient, inchoate, unformalized, a work in progress, partially built into our natural language and partially more primitive than our most artless language. In so far as I use it more than mention it, mention it more than describe it, and describe it more than fully formalize it, then to that extent it must be consigned to the realm of unformalized and unreflective logic, where some say "there be oracles", but I don't know.

Still, one of the aims of formalizing what acts of reasoning that we can is to draw them into an arena where we can examine them more carefully, perhaps to get better at their performance than we can unreflectively, and thus to live, to formalize again another day. Formalization is not the be-all end-all of human life, not by a long shot, but it has its uses on that behalf.

This looks like a good place to pause and take stock. The question arises: What is really going on here? We have all these signs, but what is the object?

One object worth the candle is simply to study a non-trivial example of a syntactic system, simple in design but not entirely a toy, just to see how these systems tick.

More than that, we would like to understand how sign systems come to exist or can be placed in relation to object systems, in the likes of which we possess some compelling independent reason to take an interest.

What is the utility of setting up sets of strings and sets of graphs, and sorting them according to their semiotic equivalence class (SEC) based on this or that abstract notion of transformational equivalence?

Good questions.

I can but begin to address these questions in the present frame of work, but I can't hope to answer them in anything like a satisfactory fashion. Nevertheless, I will not mind one bit if you keep them in mind as we go.

Analysis of contingent propositions

For all of the reasons mentioned above, and for the sake of a more compact illustration of the in and outs of a typical propositional equation reasoning system (PERS), let's now take up a much simpler example of a contingent proposition:

o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` q o ` o r ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` p o ` o p ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `(p (q)) (p (r))` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

For the sake of simplicity in discussing this example, I will revert to the existential interpretation (Ex) of logical graphs and their corresponding parse strings.

Under Ex the expression $(p\ (q))(p\ (r))\!$ interprets as the vernacular expression $p\ \operatorname{implies}\ q\ \operatorname{and}\ p\ \operatorname{implies}\ r,$ in symbols, $\{ p \Rightarrow q \} \land \{ p \Rightarrow r \},$ so this is the reading that we'll want to keep in mind for the present.

Where brevity is required, and it occasionally is, we may invoke the propositional expression $(p\ (q))(p\ (r))\!$ under the name of $f\!$ by making use of the following definition: $f = (p\ (q))(p\ (r)).\!$

Since the expression $(p\ (q))(p\ (r))\!$ involves just three variables, it may be worth the trouble to draw a venn diagram of the situation. There are in fact a couple of different ways to execute the picture.

Figure 1 indicates the points of the universe of discourse X for which the proposition f : X → B has the value 1 (= true). In this paint by numbers style of picture, one simply paints over the cells of a generic template for the universe X, going according to some previously adopted convention, for instance: Let the cells that get the value 0 under f remain untinted, and let the cells that get the value 1 under f be painted or shaded. In doing this, it may be good to remind ourselves that the value of the picture as a whole is not in the paints, in other words, the 0, 1 in B, but in the pattern of regions that they indicate. NB. In this Ascii version, I use [```] for 0 and [^^^] for 1.

o-----------------------------------------------------------o
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^o-------------o^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^o` ` ` ` ` ` ` ` ` ` ` ` `o^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` P ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o--o----------o ` o----------o--o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^/^ ^ \ ` ` ` ` `\`/` ` ` ` ` / ^ ^\^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ / ^ ^ ^\` ` ` ` ` o ` ` ` ` `/^ ^ ^ \ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^/^ ^ ^ ^ \ ` ` ` `/^\` ` ` ` / ^ ^ ^ ^\^ ^ ^ ^ ^ |
| ^ ^ ^ ^ / ^ ^ ^ ^ ^\` ` ` / ^ \ ` ` `/^ ^ ^ ^ ^ \ ^ ^ ^ ^ |
| ^ ^ ^ ^/^ ^ ^ ^ ^ ^ \ ` `/^ ^ ^\` ` / ^ ^ ^ ^ ^ ^\^ ^ ^ ^ |
| ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^o--o-------o--o^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ Q ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ R ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^\^ ^ ^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ |
| ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ \ ^ / ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ |
| ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^\^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^/^\^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o-------------o ^ o-------------o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
o-----------------------------------------------------------o
Figure 1.  Venn Diagram for (p (q))(p (r))

There are a number of standard ways in mathematics and statistics for talking about "the subset W of the domain X that gets painted with the value z by the indicator function f : X → B". The subset W ⊆ X is called by a variety of names in different settings, for example, the antecedent, the fiber, the inverse image, the level set, or the pre-image in X of z under f. It is notated and defined as W = f^–1(z). Here, f^–1 is called the converse relation or the inverse relation — it is not in general an inverse function — corresponding to the function f. Whenever possible in simple examples, we use lower case letters for functions f : X → B, and its is sometimes useful to employ capital letters for subsets of X, if possible, in such a way that F is the fiber of 1 under f, in other words, F = f^–1(1).

The easiest way to see the sense of the venn diagram is to notice that the expression "(p (q))", read as "p ⇒ q", can also be read as "not p without q". Its assertion effectively excludes any tincture of truth from the region of P that lies outside the region Q.

Likewise for the expression "(p (r))", read as "p ⇒ r", and also readable as "not p without r". Asserting it effectively excludes any tincture of truth from the region of P that lies outside the region R.

Figure 2 shows the other standard way of drawing a venn diagram for such a proposition. In this punctured soap film style of picture — others may elect to give it the more dignified title of a logical quotient topology or some such thing — one goes on from the previous picture to collapse the fiber of 0 under X down to the point of vanishing utterly from the realm of active contemplation, thereby arriving at a degenre of picture like so:

o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` o-------------o ` o-------------o ` ` ` ` ` ` |
| ` ` ` ` ` `/` ` ` ` ` ` ` `\`/` ` ` ` ` ` ` `\` ` ` ` ` ` |
| ` ` ` ` ` / ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` \ ` ` ` ` ` |
| ` ` ` ` `/` ` ` ` ` ` ` ` `/`\` ` ` ` ` ` ` ` `\` ` ` ` ` |
| ` ` ` ` / ` ` ` ` ` ` ` ` / P \ ` ` ` ` ` ` ` ` \ ` ` ` ` |
| ` ` ` `/` ` ` ` ` ` ` ` `/` ` `\` ` ` ` ` ` ` ` `\` ` ` ` |
| ` ` ` o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` o ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` |
| ` ` ` | ` ` ` ` Q ` ` ` | ` ` ` | ` ` ` R ` ` ` ` | ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` | ` ` ` |
| ` ` ` o ` ` ` ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` o ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` `\ ` ` /` ` ` ` ` ` ` ` `/` ` ` ` |
| ` ` ` ` \ ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` / ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` `\`/` ` ` ` ` ` ` ` `/` ` ` ` ` |
| ` ` ` ` ` \ ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` / ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/`\` ` ` ` ` ` ` `/` ` ` ` ` ` |
| ` ` ` ` ` ` o-------------o ` o-------------o ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
Figure 2.  Venn Diagram for (p (q r))

This diagram indicates that the region where p is true is wholly contained in the region where both q and r are true. Since only the regions that are painted true in the previous figure show up at all in this one, it is no longer necessary to distinguish the fiber of 1 under f by means of any stipple.

In sum, it is immediately obvious from the venn diagram that in drawing a representation of the propositional expression:

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

in other words,

[p ⇒ q] ∧ [p ⇒ r],

we are also looking at a picture of:

(p (q r)),

in other words,

p ⇒ [q ∧ r].

Let us now examine the following propositional equation:

o-----------------------------------------------------------o
| Equation E_1` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` q r ` ` ` ` ` ` |
| ` ` ` ` `q o` `o r` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` |
| ` ` ` ` ` `|` `|` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` |
| ` ` ` ` `p o` `o p` ` ` ` ` ` ` ` ` ` ` `p o` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` (p (q)) (p (r)) ` ` ` = ` ` ` ` `(p `(q r)) ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` [p=>q] & [p=>r] ` ` ` = ` ` ` ` `[p=>[q&r]] ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

There are three distinct ways that I can think of right off as to how we might go about formally proving or systematically checking the proposed equivalence, the evidence of whose truth we already have before us clearly enough, and in a visually intuitive form, from the venn diagrams that we examined above.

While we go through each of these ways let us keep one eye out for the character and the conduct of each type of proceeding as a semiotic process, that is, as an orbit, in this case discrete, through a locus of signs, in this case propositional expressions, and as it happens in this case, a sequence of transformations that perseveres in the denotative objective of each expression, that is, in the abstract proposition that it expresses, while it preserves the informed constraint on the universe of discourse that gives us one viable candidate for the informational content of each expression in the interpretive chain of sign metamorphoses.

A sign relation L is a subset of a cartesian product O × S × I, where O, S, I are sets known as the object, sign, and interpretant sign domains, respectively. One writes L ⊆ O × S × I, where the symbol "⊆" indicates the subset relation, contained as a subset of. Accordingly, a sign relation L consists of ordered triples of the form (o, s, i), where o, s, i belong to the domains O, S, I, respectively.

The syntactic domain of a sign relation L ⊆ O × S × I is just the set-theoretic union S ∪ I of its sign domain S and its interpretant domain I.

It is not uncommon, especially in formal examples, for the sign domain and the interpretant domain to be equal as sets, in short, to have S = I.

Elsewhere I have discussed examples of sign relations that consist of a finite set of triples of the form (o, s, i), where o, s, i are the object, sign, interpretant sign, respectively, of what is called the sign triple or the elementary sign relation (o, s, i).

We will be taking a bit of a jump up from the finite case now, since most of the examples of sign relations that interest us in logic will have S and I being infinite sets, and usually O will be infinite, too, in the long run, at least, although we will frequently work up to the infinite object domains by way of various series of finite approximations and gradual stages.

With that preamble behind us, let us turn to consider the case of semiosis, or sign transformation process, that is generated by our first proof of the propositional equation E₁.

o-----------------------------------------------------------o
| Equation E_1. `Proof 1. ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `q o` `o r` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `|` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `p o` `o p` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` (p (q)) (p (r)) ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Double Negation >===========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `q o` `o r` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `|` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `p o` `o p` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` `(( (p (q)) (p (r)) ))` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Collection >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `q o` `o r` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `|` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `o` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `p o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` `(p ( ((q)) ((r)) ))` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Double Negation >===========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` q r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `p o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `(p (q r))` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< QED >=======================o

For some reason I always think of this as the way that our DNA would prove it.

We are in the process of examining various proofs of the propositional equation "(p (q))(p (r)) = (p (q r))", and viewing these proofs in the light of their character as semiotic processes, in essence, as sign-theoretic transformations.

Here is a reminder of the equation in question:

o-----------------------------------------------------------o
| Equation E_1` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` q r ` ` ` ` ` ` |
| ` ` ` ` `q o` `o r` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` |
| ` ` ` ` ` `|` `|` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` |
| ` ` ` ` `p o` `o p` ` ` ` ` ` ` ` ` ` ` `p o` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` (p (q)) (p (r)) ` ` ` = ` ` ` ` `(p `(q r)) ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` [p=>q] & [p=>r] ` ` ` = ` ` ` ` `[p=>[q&r]] ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

The second way of establishing the truth of this equation is one that I see, rather loosely, as model-theoretic, for no better reason than the sense of its ending with a pattern of expression, a variant of the disjunctive normal form (DNF), that is commonly recognized to be the form that one extracts from a truth table by pulling out the rows of the table that evaluate to true and constructing the disjunctive expression that sums up the senses of the corresponding interpretations.

In order to apply this model-theoretic method to an equation between a couple of contingent expressions, one must transform each expression into its associated DNF and then compare those to see if they are equal. In the current setting, these DNF's may indeed end up as identical expressions, but it is possible, also, for them to turn out slightly off-kilter from each other, and so the ultimate comparison may not be absolutely immediate. The explanation of this is that, for the sake of computational efficiency, it is useful to tailor the DNF that gets developed as the output of a DNF algorithm to the particular form of the propositional expression that is given as input.

o-----------------------------------------------------------o
| Equation E_1. `Proof 2, 1st Half. ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` q o ` o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` p o ` o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "p" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` q ` r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o ` o r ` o o ` o o ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` | ` ` `\| ` |/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` o ` ` ` o ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\ /` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` p o-----------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\`/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o ` o r ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` | ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` o ` ` ` o ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\ /` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` p o-----------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\`/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o ` o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` p o-----------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\`/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "q" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o r ` ` o ` o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` ` o ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` q o-----------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\`/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o r ` ` ` ` o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` ` ` o ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `/` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` q o-----------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\`/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `/` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` q o-----------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\`/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "r" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `/` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` r o-----------o---o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `\` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` / ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\`/` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` r o-------o---o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` / ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< DNF >=======================o

What we have harvested is the succulent equivalent of a disjunctive normal form (DNF) for the proposition with which we started. Remembering that a blank node is the graphical equivalent of a logical value true, we can read this brand of DNF in the following manner:

o-----------------------------------------------------------o
| DNF of "(p (q))(p (r))" ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` r o-------o---o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` / ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| Either not 'p' and thus 'true'` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` Or ` ` 'p' and thus ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `Either not 'q' and thus 'false'` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `Or ` ` 'q' and thus` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` Either not 'r' and thus 'false' ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` Or ` ` 'r' and thus 'true'. ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

Sorry, the half-time show was cancelled by the censors. But I'm guessing that the reader can probably finish off the second half of the proof with a few scribbles on paper faster than I can asciify it on my own, so at least there's that entertaiment to occupy the interval.

We are still in the middle of contemplating a particular example of a propositional equation, namely, "(p (q))(p (r)) = (p (q r))", and we are still considering the second of three formal methods that I intend to illustrate in the process of thrice-over establishing it.

o-----------------------------------------------------------o
| Equation E_1` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` q r ` ` ` ` ` ` |
| ` ` ` ` `q o` `o r` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` |
| ` ` ` ` ` `|` `|` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` |
| ` ` ` ` `p o` `o p` ` ` ` ` ` ` ` ` ` ` `p o` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` (p (q)) (p (r)) ` ` ` = ` ` ` ` `(p `(q r)) ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` [p=>q] & [p=>r] ` ` ` = ` ` ` ` `[p=>[q&r]] ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

I know that it must seem tedious, but I probably ought to go ahead and carry out the second half of this analogically model-theoretic strategy, just so that we will have the security of this concrete and shared experience on which to fall back at every later point in whatmay quickly become a rather abstruse discussion. Here then is the rest of the necessary chain of equations:

o-----------------------------------------------------------o
| Equation E_1. `Proof 2, 2nd Half. ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `q r` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` p o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "p" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `q r` ` ` q r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` o o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` `\| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `q r` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `q r` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "q" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o r ` ` o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o r ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "r" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` r o-------o---o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` / ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` r o-------o---o r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` / ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q o-------o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` p o-------o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< DNF >=======================o

This is not only a logically equivalent DNF, but exactly the same DNF expression that we obtained before, so we have established the given equation "(p (q))(p (r)) = (p (q r))".

Incidentally, one may wish to note that this DNF expression quickly folds into the following form:

o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` pqr o-------o---o p ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` (p q r, (p))` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

This can be read to say "either p q r, or not p", which gives us yet another expression equivalent to the sentences "(p (q))(p (r))" and "(p (q r))".

Still another way of writing the same thing would be like so:

o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` p o-------o pqr ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ((p , p q r)) ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

In other words, "p is equivalent to p and q and r".

Let's pause to refresh ourselves with a few morsels of lemmas bread. One lemma that I can see just far enough ahead to see our imminent need of is the principle that I canonize as the Emptiness Rule. It says that a bare lobe expression like "(… , …)", with any number of places for arguments but nothing but blanks as filler, is logically tantamount to the proto-typical expression of its type, namely, the constant expression "( )" that Ex interprets as denoting the logical value false. To depict the rule in graphical form, we have the continuing sequence of equations:

o-----------------------------------------------------------o
| Emptiness Rule` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` ` ` o---o ` ` ` o-o-o ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` `\ /` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` @ ` ` = ` ` @ ` ` = ` ` @ ` ` = ` `...` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

Yet another rule that we'll need is the following:

o-----------------------------------------------------------o
| Indistinctness Rule ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` a ` a ` ` ` a a a ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` ` ` o---o ` ` ` o-o-o ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` `\ /` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` @ ` ` = ` ` @ ` ` = ` ` @ ` ` = ` `...` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

This one is easy enough to derive from rules that are already known, but call it the Indistinctness Rule just on behalf of ready reference and employment.

Finally, let me introduce a rule-of-thumb that is a bit more suited to routine computation, and that will serve to replace the indistinctness rule in many of the cases where we actually have to call on it. This is actually just a special case of the evaluation rule listed above:

o-----------------------------------------------------------o
| Evaluation Rule ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | `x_2` `... x_k` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o---o-...-o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` x_2 ... x_k ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ((), x_2, ..., x_k) ` ` = ` ` ` ` x_2 ... x_k ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` `Setup` ` ` <---- | ----> ` ` `Spike` ` ` ` ` ` |
o-----------------------------------------------------------o

To continue with the beating of this still kicking horse that is known as the propositional equation "(p (q))(p (r)) = (p (q r))", let's now take up the third way that I mentioned for examining propositional equations, but I believe that you will be relieved to know that it is literally a third way only at the very outset, almost immediately breaking up according to whether one proceeds by way of the more "routine" model-theoretic path or else by way of the more "strategic" proof-theoretic path. I think that I'll take the low road today.

Let's convert the equation between propositions:

(p (q))(p (r)) = (p (q r)),

into the corresponding equational proposition:

(( (p (q))(p (r)) , (p (q r)) )).

If you're like me, you'd rather see it in pictures:

o-----------------------------------------------------------o
| Equation E_1, Written as an Equation in Cactus Language ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `q o` `o r` `q o r` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `|` `|` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `p o` `o p` `p o` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `o---------o` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` \ ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` \ ` / ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `(( `(p (q))` (p (r)) ` , ` (p` (q r))` ))` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` [[p=>q] & [p=>r]] `<=>` [p=>[q&r]]` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o

We may now interrogate the alleged equation for the third time, working by way of the case analysis-synthesis theorem (CAST).

o-----------------------------------------------------------o
| Equation E_1. `Proof 3. ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` q o ` o r ` q o r ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` p o ` o p ` p o ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\ ` ` ` /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \` ` `/ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\ ` /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o==================================< CAST "p" >=============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `q` `r` ` q r ` `q` `r` ` qr` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `o` `o` ` `o` ` `o o o o` `o o` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `|` `|` ` `|` ` `|/ `|/ ` `|/ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `o` `o` ` `o` ` `o` `o` ` `o` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ / ` ` `|` ` ` \ / ` ` `|` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `o-------o` ` ` `o-------o` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` ` / ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` `/` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` \ / ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `p o---------------o---o p` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o==================================< Domination >===========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `q` `r` ` q r ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `o` `o` ` `o` ` ` `o` `o` ` `o` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `|` `|` ` `|` ` ` / ` / ` ` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `o` `o` ` `o` ` `o` `o` ` `o` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ / ` ` `|` ` ` \ / ` ` `|` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `o-------o` ` ` `o-------o` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ ` ` / ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` `/` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` \ / ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `p o---------------o---o p` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o==================================< Cancellation >=========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `q` `r`