In the grammar , no logical formula is a proper initial segment of another. A recursive parser reads one variable, or a negation followed by one formula, or a parenthesized pair of formulas separated by implication. Structural induction shows that this parser consumes precisely one whole formula. Its deterministic stopping position proves prefix-freeness. Consequently any formula substring in a valid formula coincides with the formula of a syntax subtree.
Articles by others on the same topic
There are currently no matching articles.