Changes

We took up the Equation <math>E_1\!</math> that reads as follows:

We took up the Equation <math>E_1\!</math> that reads as follows:

: (p (q))(p (r)) = (p (q r)).

| <math>\texttt{(} p \texttt{~(} q \texttt{))(} p \texttt{~(} r \texttt{))} = \texttt{(} p \texttt{~(} q~r \texttt{))}.</math>

Each of our proofs is a finite sequence of signs, and thus, for a finite integer n, takes the form:

Each of our proofs is a finite sequence of signs, and thus, for a finite integer <math>n,\!</math> takes the form:

: ''s''₁, ''s''₂, ''s''₃, &hellip;, ''s''_''n''.

| <math>s_1, s_2, s_3, \ldots, s_n.</math>

Proof 1 proceeded by the ''straightforward approach'', starting with ''e''₂ as ''s''₁ and ending with ''e''₃ as ''s''_''n''.  That is, it commenced from the sign "(p (q))(p (r))" and ended up at the sign "(p (q r))" by legal moves.

Proof&nbsp;1 proceeded by the ''straightforward approach'', starting with ''e''₂ as ''s''₁ and ending with ''e''₃ as ''s''_''n''.  That is, it commenced from the sign "(p (q))(p (r))" and ended up at the sign "(p (q r))" by legal moves.

Proof 2 lit on by ''burning the candle at both ends'', changing ''e''₂ into a normal form that reduced to ''e''₄, and changing ''e''₃ into a normal form that also reduced to ''e''₄, in this way tethering ''e''₂ and ''e''₃ to a common stake.  In more detail, one route went from "(p (q))(p (r))" to "(p q r, (p))", and another went from "(p (q r))" to "(p q r, (p))", thus equating the two points of departure.

Proof&nbsp;2 lit on by ''burning the candle at both ends'', changing ''e''₂ into a normal form that reduced to ''e''₄, and changing ''e''₃ into a normal form that also reduced to ''e''₄, in this way tethering ''e''₂ and ''e''₃ to a common stake.  In more detail, one route went from "(p (q))(p (r))" to "(p q r, (p))", and another went from "(p (q r))" to "(p q r, (p))", thus equating the two points of departure.

Proof 3 took the path of reflection, expressing the met-equation between ''e''₂ and ''e''₃ in the naturalized equation ''e''₅, then taking ''e''₅ as ''s''₁ and exchanging it by dint of value preserving steps for ''e''₁ as ''s''_''n''.  Thus we went from "(( (p (q))(p (r)) , (p (q r)) ))" to the blank expression that <math>\operatorname{Ex}</math> recognizes as the value ''true''.

Proof&nbsp;3 took the path of reflection, expressing the met-equation between ''e''₂ and ''e''₃ in the naturalized equation ''e''₅, then taking ''e''₅ as ''s''₁ and exchanging it by dint of value preserving steps for ''e''₁ as ''s''_''n''.  Thus we went from "(( (p (q))(p (r)) , (p (q r)) ))" to the blank expression that <math>\operatorname{Ex}</math> recognizes as the value ''true''.

Review:

Review: