Some Meta-Theory of Well Constructed Polish Meaningful Expressions:

For the following we'll use this definition.

1. All un-bolded small letters are meaningful expressions.

2. If x is a meaningful expression, then so is Nx.

3. If x is a meaningful expression, if y is a meaningful expression, then Cxy is meaningful expression.

From hereon, I'll abbreviate meaningful expression by MEXP.  The length of a MEXP we define as the number of symbols it has.

Meta-Theorem 1: Every MEXP which has a C in it, has one more small letter than C in it.

Meta-Proof: Consider an arbitrary MEXP of type Cab.

Case 1: Cab has two small letters in it, or one small letter in two distinct positions.  In either case it has one C and two small letters in it.

Case 2: Suppose that for any MEXP of length n it has type Ccd and it has one more small letter than C in it.  Now consider any MEXP of length (n +1).  It will either have type NCcd, CNcd, or type CcNd.  In any of those cases, it will have same number of small letters as type Ccd since we only adjoined an N to the sequence of letters.  Finally, consider any MEXP of length (n + 2).  It will have one of the following types: NNCcd, NCNcd, NCcNd, CNNcd, CNcNd, CcNNd, CxCcd, or CCxcd.  The cases which have N in them follow by our hypothesis of the MEXP having one more small letter than C in it.  Now consider the last two cases. Since the length of the MEXP is (n + 2), and has one more C in it than Ccd, x will consist of a small letter only.  And in every twenty-six of those subcases, CxCcd and CCxcd has one more small letter than C in it.  This completes the argument that every MEXP has one more small letter than C in it.

Meta-Claim 2: The following algorithm is sufficient to determine whether or not a sequence of letters is a MEXP.

Description: We first assign 1 to any small letter.  We also assign -1 to any C.  We assign 0 to all instances of N.

Step 1: We look at the last letter of the MEXP and check if it's a small letter.  If it is, then we continue.  Otherwise, we halt.  The sequence of letters is not a MEXP.

Step 2: We have a counter given a value of 1.  We now proceed from the right hand side to the left adding numbers according to whether it consists of a C or N.  If it at any point the counter equals 0, then we halt, and the sequence of letters it is not a MEXP.  If we get to the last letter and the value is greater than 1, then it is not a MEXP.  Otherwise, it is a MEXP.

Meta-Claim 3: The following algorithm is also sufficient to determine whether or not a sequence of letters is a MEXP.

Description: We assign -1 to any small letter.  We also assign 1 to any C.  We assign 0 to all instances of N.

Step 1: We first assign a value of 1 to a counter.

Step 2: Now we proceed from left to right changing the value of our counted by the above assignments.  If our counter equals 0 at any point which is not the last letter of the sequence of letters, then halt it is not a MEXP.  If the counter does not equal 0 at the last letter then it is not a MEXP.  If the counter does equal 0 at the last letter then it is a MEXP.

Meta-Claim 4: If we use the second algorithm, that described in meta-claim 3, and it has type Ckj, then the k MEXP can get found as follows. 

Step 1: We start with the letter in the sequence.  If it is a MEXP, then stop, that is the MEXP we wanted.

Step 2:  If it is not, then store that letter, and let's call it so_far.

Step 3: Adjoin the next letter in the sequence of letters to the end of so_far. 

Step 4: Check to see if so_far is now a MEXP.  If it is, then so_far is k.  If, not, then goto step 3.

Meta-Theorem 2: Every MEXP ends with a small letter.

Argument: If it does not end with a small letter, then it did not get constructed by the three clauses above.