Changes

===Output===

===Output===

One component of the <math>\begin{smallmatrix}\operatorname{Theme~One}\end{smallmatrix}</math> program that I wrote some years ago finds all the satisfying interpretations of propositions expressed in cactus syntax.  It's not a polynomial time algorithm, as you may guess, but it was just barely efficient enough to do this example in the 500 K of spare memory that I had on an old 286 PC in about 1989, so I will give you the actual outputs from those trials.

One component of the Theme One program that I wrote some years ago

finds all the satisfying interpretations of propositions expressed

in cactus syntax.  It's not a polynomial time algorithm, as you may

guess, but it was just barely efficient enough to do this example

in the 500 K of spare memory that I had on an old 286 PC in about

1989, so I will give you the actual outputs from those trials.

Output Conditions for Tape Input "0"

====Output Conditions for Tape Input "0"====

Let P_0 be the proposition that we get by conjoining

Let P_0 be the proposition that we get by conjoining

the proposition that describes the initial conditions

the proposition that describes the initial conditions

the tape head H if and when the machine M reaches one of

the tape head H if and when the machine M reaches one of

its resting states, we get the result that Parity(0) = 0.

its resting states, we get the result that Parity(0) = 0.

Output Conditions for Tape Input "1"

====Output Conditions for Tape Input "1"====

Let P_1 be the proposition that we get by conjoining

Let P_1 be the proposition that we get by conjoining

the proposition that describes the initial conditions

the proposition that describes the initial conditions