Completeness theorems for the parser of ABNF grammars.

For every terminated tree rooted at `parse-grammar` succeeds on the string at the leaves of the tree
and returns that tree:

**Theorem: **

(defthm parse-grammar-when-tree-match (implies (and (tree-match-element-p tree (element-rulename *rulelist*) *grammar*) (tree-terminatedp tree) (tree-rulelist-restriction-p tree)) (equal (parse-grammar (tree->string tree)) (tree-fix tree))))

This is proved by proving the following,
for each parsing function out of which `parse-grammar` is built:
if a (list of) terminated tree(s) matches a certain syntactic entity
and possibly satisfies certain disambiguating restrictions, then running the parsing function on the `append` of
(i) the string at the leaves of the tree(s) and
(ii) some remaining input
possibly satisfying certain hypotheses explained below,
succeeds and yields that (list of) tree(s) and that remaining input.
More precisely, the parsing function yields
the (list of) tree(s) fixed with `tree-fix` or `tree-list-fix`
and the remaining input fixed with `nat-list-fix`;
an alternative formulation is to avoid these fixing functions
but include the hypotheses
that the (list of) tree(s) satisfies `treep` or `tree-listp`
and that the remaining input satisfies `nat-listp`.

For example, the completeness theorem `parse-alpha-when-tree-match`
says that running `parse-alpha` on the `append` of
(i) the leaves of a terminated tree that matches `parse-alpha-when-tree-match` has no hypothesis
related to those disambiguating restrictions.
This theorem also has no hypothesis on the remaining input,
as explained below.

The completeness theorem of `parse-any`
does not involve trees but makes an analogous statement:
running `parse-any` on
the `cons` of a natural number and some remaining natural numbers,
returns (the fixing of) that natural number and
(the fixing of) the remaining natural numbers.

In all the completeness theorems,
the remaining input (following the string at the leaves of the tree(s))
is denoted by the variable

If a parsing function ignores the remaining input,
the corresponding completeness theorem
has no hypotheses on the remaining input.
This is the case for parsing functions that,
like `parse-alpha` mentioned above,
parse a fixed number of natural numbers from the input.
This is also the case for
parsing functions that parse a fixed number of natural numbers
after parsing a variable number of natural numbers:
for example,
`parse-prose-val` always parses the closing angle bracket
(which is a single character)
after parsing a variable number of characters
after parsing the opening angle bracket.

In contrast, if a parsing function ``examines'' (part of) the remaining input, the corresponding completeness theorem has hypotheses on the remaining input. If a parsing function examines part of the remaining input, but that part of the remaining input is absent from the returned tree(s) (by hypothesis of the function's completeness theorem), it means that the function attempts but fails to parse further into the remaining input, backtracking and returning a (list of) tree(s) only for the input that precedes the remaining input. Thus, the completeness theorem for the function must include hypotheses stating or implying such parsing failures. Without these hypotheses, parsing further into the remaining input might succeed, extending the tree(s) and rendering the theorem untrue. Some concrete examples are given below.

A parsing function for
a repetition of zero or more instances of some syntactic entity
always examines the remaining input to decide when to stop.
The function's completeness theorem has a hypothesis on the remaining input
stating or implying that
parsing another instance of the syntactic entity fails.
For example, `parse-*bit` stops when `parse-bit` fails;
this parsing failure occurs in the remaining input.
The completeness theorem `parse-*bit-when-tree-list-match`
has the hypothesis that `parse-bit` fails on the remaining input.
Without this hypothesis, the theorem would not hold because,
if another `parse-*bit` would return (at least) an additional tree
beyond the list of trees hypothesized in the theorem.

A parsing function for an optional occurrence of some syntactic entity
may examine the remaining input.
This happens when parsing the syntactic entity fails,
in which case the function returns a tree without leaves,
because the optional entity is absent.
The function's completeness theorem has a hypothesis on the remaining input
stating or implying that parsing the syntactic entity fails.
For example, `parse-?%i` may fail to parse `parse-?%i-when-tree-match`
has the hypothesis that `parse-ichar2`
(with arguments `parse-?%i` would return a tree with leaves instead.

The kind of hypothesis on the remaining input
described in the previous paragraph,
for the completeness theorems of parsing functions
that parse optional entities,
is stronger than needed.
If the parsing function succeeds in parsing the optional entity,
then it does not examine the remaining input, returning a tree with leaves.
So the hypothesis on the remaining input could be weakened
to require the parsing failure to happen only if the tree has no leaves.
However, in syntactically valid ABNF grammars,
the stronger hypothesis is always satisfied
(e.g.

If a parsing function calls, or may call, another parsing function
as its last action,
the former's completeness theorem ``inherits''
the hypotheses on the remaining input
from the latter's completeness theorem.
If the hypotheses were not inherited,
the called function may successfully parse some of the remaining input,
returning more or different subtrees
than hypothesized by the calling function's completeness theorem,
rendering the theorem untrue.
For example,
since `parse-1*bit` calls `parse-*bit` as its last action,
`parse-1*bit-when-tree-list-match` inherits from
`parse-*bit-when-tree-list-match`
the hypothesis that `parse-bit` fails on the remaining input;
otherwise, `parse-*bit` could return additional `parse-1*bit` could return additional `parse-dot-1*bit` calls `parse-1*bit` as its last action,
`parse-dot-1*bit-when-tree-match` inherits from
`parse-*bit-when-tree-list-match`
the hypothesis that `parse-bit` fails on the remaining input;
otherwise, `parse-1*bit` could return additional `parse-dot-1*bit` could return a tree
with additional `parse-bin/dec/hex-val` may call `parse-bin-val`
(and `parse-dec-val` and `parse-hex-val`)
as its last action,
`parse-bin/dec/hex-val-when-tree-match` inherits from
`parse-bin-val-when-tree-match`
(and `parse-dec-val-when-tree-match`
and `parse-hex-val-when-tree-match`)
various parsing failure hypotheses on the remaining input.

As a slight generalization of the situation
described in the previous paragraph,
a parsing function may call, as its last action,
another parsing function that may return a tree without leaves.
In this case, the calling parsing function's completeness theorem inherits
the hypotheses on the remaining input
also from the completeness theorem of
the parsing function that it calls just before the last one.
For example,
`parse-elements` calls `parse-*cwsp` as its last action,
and thus `parse-elements-when-tree-match` inherits
from `parse-*cwsp-when-tree-list-match`
the hypothesis that `parse-cwsp` fails on the remaining input,
as explained earlier.
But since `parse-*cwsp` may return a tree with no leaves
(if no instances of `parse-elements-when-tree-match` also inherits
the hypotheses on the remaining input
from `parse-alternation-when-tree-match`.

As illustrated by
the `parse-bin/dec/hex-val-when-tree-match` example above,
when a parsing function may call a set of different parsing functions
as its last action,
the calling function's completeness theorem inherits
from the called functions' completeness theorems
all the hypotheses on the remaining input.
The resulting hypotheses, in the calling function's completeness theorem,
are stronger than needed:
they could be weakened to require an inherited parsing failure hypothesis
only if the subtree(s) correspond(s) to the called function.
For example, in `parse-bin/dec/hex-val-when-tree-match`,
the failure of `parse-bit` could be required only if
the

In the rules in [RFC:4], certain repeated and optional syntactic entities
``nest to the right'',
e.g. `parse-1*-dot-1*bit-when-tree-list-match`
(and `parse-*-dot-1*bit-when-tree-list-match`)
includes not only the failure of `parse-dot-1*bit`
(actually, a stronger hypothesis, as explained below),
but also the failure of `parse-bit`.
As another example, `parse-bin-val-rest-when-tree-match`
includes the failure of `parse-bit` for the

Besides the cases already mentioned
of stronger hypotheses on the remaining input
(that keep the theorems simpler while not precluding the top-level proof),
there are other cases in which completeness theorems have
stronger parsing failure hypotheses than needed.
An example, as hinted above,
is `parse-1*-dot-1*bit-when-tree-list-match`:
instead of having a hypothesis
requiring the failure of `parse-1*-dot-1*bit`,
the theorem has the stronger hypothesis that
`parse-ichar` with argument

The two alternatives parsed by `parse-equal-/-equal-slash`
are one a prefix of the other.
Therefore, `parse-equal-/-equal-slash-when-tree-match`
has the hypothesis that `parse-ichar` with argument `parse-equal-/-equal-slash`
would return a tree matching

Since
(i) `parse-rule` calls `parse-cnl` as its last action,
(ii) `parse-cnl` always returns a tree with leaves, and
(iii) `parse-cnl-when-tree-match` has
no hypotheses on the remaining input,
it may seem that `parse-rule-when-tree-match`
needs no hypotheses on the remaining input.
However, before calling `parse-cnl`,
`parse-rule` calls `parse-elements`,
which may parse the ending `parse-rule` may actually examine part of the remaining input.
The needed hypothesis is that `parse-wsp`
fails on the remaining input:
if `parse-rule` would put that with the

An analogous discussion to the one in the previous paragraph
applies to `parse-*cwsp-cnl`.
Thus, `parse-*cwsp-cnl-when-tree-match` has the hypothesis that
`parse-wsp` fails on the remaining input.

Most completeness theorems include
hypotheses saying that the trees are terminated.
This ensures that the strings at the leaves of the trees
consist of natural numbers and not rule names,
since the parsing functions operate on natural numbers.
A few completeness theorems do not need those hypotheses
because the corresponding syntactic entities can only be matched
by trees whose leaves are natural numbers, e.g.
`parse-exact-when-tree-match`,
`parse-ichar-when-tree-match`, and
`parse-?%i-when-tree-match`.

The completeness theorems
`parse-*-rule-/-*cwsp-cnl-when-tree-list-match-and-restriction` and
`parse-rulelist-when-tree-match-and-restriction`,
as suggested by the ending of their names,
have hypotheses saying that the (list of) tree(s) satisfies the disambiguating restrictions. Without these hypotheses, the theorems would not hold
because there would be multiple choices of trees for certain inputs,
but the parser only produces one choice for each input.

The completeness theorems of the more ``basic'' parsing functions
`parse-any`,
`parse-exact`,
`parse-in-range`,
`parse-ichar`, and
`parse-ichar2`
are proved by expanding the necessary definitions.
The proofs for `parse-exact` and `parse-in-range`
use `parse-any-of-cons` as a rewrite rule,
obviating the need to expand `parse-any`.
The proofs for `parse-exact` and `parse-in-range`
also expand some tree-related functions, which seems odd
because it should be possible to treat trees as abstract data types;
there may be ways to avoid that, perhaps by adding some tree lemmas.

Each of the other completeness theorems is proved, generally speaking, by reducing the tree matching hypothesis to one or more subtree matching facts, reducing the call to the parsing function on the (list of) tree(s) to calls to other parsing functions on (lists of) subtrees, and using the already proved theorems for the called parsing functions to show that the calling parsing function returns the right results. The completeness theorems are used as rewrite rules (implicitly, since they are enabled). The subtree matching facts to which the tree matching hypothesis reduces are used to relieve the hypotheses of these rewrite rules.

For example, `parse-cr-when-tree-match` is proved as follows.
The hypothesis that the tree matches `parse-cr` in the conclusion is reduced
to a call to `parse-exact` with argument `append` of
(i) the string at the leaves of the subtree and
(ii) the remaining input.
The rewrite rule `parse-exact-when-tree-match` then applies
(whose hypothesis is relieved
via the aforementioned fact that the subtree matches `parse-exact` to the triple consisting of
`parse-cr`, by its definition,
returns the triple consisting of
`parse-cr-when-tree-match` is proved.

This reduction approach works also when there are multiple subtrees.
For example, `parse-crlf-when-tree-match` is proved as follows.
The hypothesis that the tree matches `parse-crlf` is reduced to
a call to `parse-cr`
on the string at the leaves of the first subtree
and a call to `parse-lf`
on the string at the leaves of the second subtree.
Then `parse-cr-when-tree-match` and `parse-lf-when-tree-match`
apply.

Since completeness theorems generally have hypotheses
about the trees being terminated,
in order to apply completeness theorems as rewrite rules to subtrees
(in the reduction approach outlined above),
the hypothesis that the trees are terminated
must be reduced to facts that subtrees are terminated
to relieve the hypotheses of the rewrite rules.
Thus,
we enable `tree-terminatedp` just before the completeness theorems
and we disable it just after.
The existing enabled rewrite rules take care of
`tree-list-terminatedp` and `tree-list-list-terminatedp`.

Similarly, when calls to parsing functions on trees
are reduced to calls to parsing functions on subtrees,
the strings at the leaves of the trees must be reduced to
strings at the leaves of the subtrees.
Thus, we enable
`tree->string`,
`tree-list->string`, and
`tree-list-list->string`
just before the completeness theorems
and we disable them just after.
The existing enabled rules about
`tree-list->string` and
`tree-list-list->string`
do not suffice:
if these two functions are not enabled,
the proofs of some completeness theorems fails.

The `tree-match-element-p` hypotheses of the completeness theorems
are expanded via explicit `tree-match-element-p` does not perform the expansion
(presumably due to ACL2's heuristics for expanding recursive functions).
Since many repetitions consist of one element,
the rewrite rule `tree-list-match-repetition-p-of-1-repetition`
is used in many completeness proofs:
we enable it just before the completeness theorems
and disabled it just after.
There is no direct use of the definitions of
`tree-list-list-match-alternation-p` and
`tree-list-list-match-concatenation-p`
because the alternations and concatenations in the completeness theorems
always have an explicit list structure and thus rewrite rules like
`tree-list-list-match-alternation-p-of-cons-alternation` suffice.
Repetition are handled via the rules
`tree-list-match-repetition-p-of-0+-reps-when-consp` and
`tree-list-match-repetition-p-of-1+-repetitions`
where needed, as explained below.

If a parsing function may backtrack,
its completeness theorem uses a disambiguation theorem as a rewrite rule,
by explicitly enabling it
(with just one exception:
`parse-alpha-when-tree-match` uses
`fail-1st-range-when-match-2nd-range` with a `parse-wsp-when-tree-match`,
the hypothesis that the tree matches `parse-sp-when-tree-match`
implies that `parse-sp` succeeds, so `parse-wsp` succeeds
and `parse-wsp-when-tree-match` is proved.
In the second case, in order to use, in a similar way,
the completeness theorem `parse-htab-when-tree-match`,
we need to show that `parse-sp` fails,
so that `parse-wsp` reduces to `parse-htab` by backtracking
and then `parse-wsp-when-tree-match` is proved
using `parse-htab-when-tree-match`.
The disambiguation theorem `fail-sp-when-match-htab`
serves to show that, in the second case above, `parse-sp` fails.

All the completeness theorems for parsing functions that may backtrack follow this proof pattern, which motivates the formulation of the disambiguation theorems. In particular, it motivates the ``asymmetric'' use of trees and parsing functions to show incompatibility (as opposed to showing incompatibility between parsing functions or between trees).

Some completeness theorems use some disambiguation theorems
not to show that the parsing function must backtrack,
but to relieve hypotheses of other completeness theorems.
For example,
in the completeness theorem
`parse-1*-dot-1*bit-when-tree-list-match`,
the disambiguation theorem `fail-bit-when-match-*-dot-1*bit`
serves to relieve the `parse-bit` failure hypothesis
of the `parse-dot-1*bit-when-tree-match` completeness theorem.

If a parsing function parses a repetition of one or more elements
(e.g. `parse-1*bit`),
its completeness theorem
(e.g. `parse-1*bit-when-tree-list-match`)
is proved by
using `tree-list-match-repetition-p-of-1+-repetitions`
to reduce the matching to
a single element and to a repetition of zero or more elements,
and then using the completeness theorems
for the element
(e.g. `parse-bit-when-tree-match`)
and for the repetition of zero or more elements
(e.g. `parse-*bit-when-tree-list-match`).

If a parsing function is singly recursive (e.g. `parse-*bit`),
i.e. it parses a repetition of zero or more elements,
its completeness theorem is proved by induction
on the length of the list of trees that matches the repetition;
induction on the parsing function does not work,
because the argument of the parsing function is not a variable
(it is `tree-list-match-repetition-p-of-0+-reps-when-consp`
to handle the induction step of the proof.
We also disable the rewrite rule `nat-list-fix` from being eliminated
via the rewrite rule that shows that the parsing function fixes the input
(e.g. the theorem

The proof of the mutually recursive parsing functions
(i.e. `parse-alternation`, `parse-concatenation`, etc.)
is more complex.
As with the singly recursive parsing functions,
a straightforward induction on the mutually recursive parsing functions
does not work because their arguments are not variables
(they are

Instead, we take the desired formulation of each completeness theorem
of the mutually recursive parsing functions,
we add a hypothesis that a new variable `define-sk` predicate with argument

The predicates are `pred-alternation`,
`pred-concatenation`, etc.
They are not guard-verified because they only serve
to prove the completeness of the mutually recursive parsing functions.
The consequents of the implications in their bodies
call the parsing functions on
`define-sk`
(e.g. `nat-listp`,
instead of using `nat-list-fix` in the consequent:
this is because the `nat-list-fix` approach causes the proofs to fail
(perhaps due to some interaction with the equality with `nat-listp` instead in the predicates.

We prove by induction on the mutually recursive parsing functions that
all the predicates hold for every `parse-alt/conc/rep/elem/group/option-when-tree-/-tree-list-match-lemmas`.
These are completeness lemmas,
from which the completeness theorems are proved with ease.
The completeness theorem have the same formulation as the ones
for the other, non-recursive or singly recursive parsing functions;
in particular, they use `nat-list-fix` instead of `nat-listp`
on the remaining input.

The induction proof of the conpleteness lemmas generates
5 base cases and 26 induction steps.
We prove each of them separately
(these are the theorems whose names end with
`parse-element-when-tree-match-base-case`
and `parse-alternation-when-tree-match-induction-step-2`.
Attempting to prove the completeness lemmas by induction in one shot fails,
perhaps due to interference between the different hints
used for the base cases and induction steps;
however,
it may be possible to find a way to prove the lemmas in one shot.

The formulation of each base case and induction step
is derived directly from the output
generated by
the

The proof of each local lemma for base cases and induction steps
is similar to the proofs of the completeness theorems
of the non-recursive and singly recursive parsing functions.
In addition, these local lemmas use (implicitly)
the rewrite rules generated by `define-sk`
(e.g. `define-sk` rewrite rules.
The induction steps that involve lists of trees
(as opposed to single trees)
use a

Earlier we explained that some completeness theorems have
stronger parsing failure hypotheses on the remaining input
than needed, in order to keep the theorems simpler.
These theorems enable certain parsing failure propagation theorems to turn the stronger hypotheses into
the facts needed to show the weaker parsing failures
within the parsing functions.
For example,
in the completeness theorem `parse-*-dot-1*bit-when-tree-list-match`,
the parsing failure propagation theorem
`fail-dot-1*bit-when-fail-dot`
is used to turn the hypothesis that
`parse-ichar` with argument `parse-dot-1*bit` fails,
needed to show that `parse-*-dot-1*bit` stops
before the remaining input.

At some point, the mutually recursive functions
`parse-alternation` and companions
were slightly changed to use *Seq*'s `mbt` check on the lengths:
see the `Termination' section in grammar-parser-implementation
for motivation.
Before the change, the code of those parsing functions
did not use any *Seq* macros,
and had explicit `mbt` tests.
After the change, the flag induction schema
generated from the mutually recursive functions changed slightly.
As a result, the lemmas for induction steps, described above,
no longer aligned exactly with the new induction schema.
However, the alignment could be easily restored
by combining some of the previous induction step lemmas into single ones:
these have names like

- Grammar-parser-disambiguation
- Disambiguation theorems for the parser of ABNF grammars.
- Grammar-parser-constraints-from-tree-matching
- Tree maching constraint theorems for the parser of ABNF grammars.
- Grammar-parser-constraints-from-parsing
- Parsing constraint theorems for the parser of ABNF grammars.
- Grammar-parser-disambiguating-restrictions
- Restrictions on parse trees that correspond to
how the parser of ABNF grammars resolves the
rulelist ambiguity. - Grammar-parser-parsing-failure-propagation
- Parsing failure propagation theorems for the parser of ABNF grammars.
- Parse-alt/conc/rep/elem/group/option-when-tree-/-tree-list-match-lemmas
- Completeness lemmas for the mutually recursive parsing functions.
- Parse-grammar-when-tree-match
- Top-level completeness theorem of the parser of ABNF grammars.
- Parse-*-in-either-range-when-tree-list-match
- Completeness theorem for
`parse-*-in-either-range`. - Parse-in-either-range-when-tree-match
- Completeness theorem for
`parse-in-either-range`. - Parse-element-when-tree-match-induction-step-1+2+3+4+5
- Combination of
`parse-element-when-tree-match-induction-step-1`,`parse-element-when-tree-match-induction-step-2`,`parse-element-when-tree-match-induction-step-3`,`parse-element-when-tree-match-induction-step-4`, and`parse-element-when-tree-match-induction-step-5`. - Pred-concatenation
- Completeness property for
`parse-concatenation`. - Pred-conc-rest
- Completeness property for
`parse-conc-rest`. - Pred-alternation
- Completeness property for
`parse-alternation`. - Pred-alt-rest
- Completeness property for
`parse-alt-rest`. - Pred-conc-rest-comp
- Completeness property for
`parse-conc-rest-comp`. - Pred-alt-rest-comp
- Completeness property for
`parse-alt-rest-comp`. - Parse-elements-when-tree-match
- Completeness theorem for
`parse-elements`. - Pred-repetition
- Completeness property for
`parse-repetition`. - Pred-element
- Completeness property for
`parse-element`. - Parse-*-rule-/-*cwsp-cnl-when-tree-list-match-and-restriction
- Completeness theorem for
`parse-*-rule-/-*cwsp-cnl`. - Parse-option-when-tree-match-induction-step-3
- Third induction step of
the completeness lemma for
`parse-option`. - Parse-option-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-option`. - Parse-option-when-tree-match-induction-step-1+2+3
- Combination of
`parse-option-when-tree-match-induction-step-1`,`parse-option-when-tree-match-induction-step-2`, and`parse-option-when-tree-match-induction-step-3`. - Parse-group-when-tree-match-induction-step-3
- Third induction step of
the completeness lemma for
`parse-group`. - Parse-group-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-group`. - Parse-group-when-tree-match-induction-step-1+2+3
- Combination of
`parse-group-when-tree-match-induction-step-1`,`parse-group-when-tree-match-induction-step-2`, and`parse-group-when-tree-match-induction-step-3`. - Parse-bin/dec/hex-val-when-tree-match
- Completeness theorem for
`parse-bin/dec/hex-val`. - Parse-alt-rest-when-tree-list-match
- Completeness theorem for
`parse-alt-rest`. - Parse-alt-rest-comp-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-alt-rest-comp`. - Parse-alt-rest-comp-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-alt-rest-comp`. - Parse-*bit-when-tree-list-match
- Completeness theorem for
`parse-*bit`. - Parse-*-dot-1*bit-when-tree-list-match
- Completeness theorem for
`parse-*-dot-1*bit`. - Parse-rulelist-when-tree-match-and-restriction
- Completeness theorem for
`parse-rulelist`. - Parse-exact-when-tree-match
- Completeness theorem for
`parse-exact`. - Parse-element-when-tree-match-induction-step-3
- Third induction step of
the completeness lemma for
`parse-element`. - Parse-element-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-element`. - Parse-element-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-element`. - Parse-conc-rest-when-tree-list-match
- Completeness theorem for
`parse-conc-rest`. - Parse-conc-rest-comp-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-conc-rest-comp`. - Parse-conc-rest-comp-when-tree-match-induction-step-1+2
- Combination of
`parse-conc-rest-comp-when-tree-match-induction-step-1`and`parse-conc-rest-comp-when-tree-match-induction-step-2`. - Parse-conc-rest-comp-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-conc-rest-comp`. - Parse-bin-val-rest-when-tree-match
- Completeness theorem for
`parse-bin-val-rest`. - Parse-alternation-when-tree-match
- Completeness theorem for
`parse-alternation`. - Parse-alt-rest-comp-when-tree-match-induction-step-1+2
- Combination of
`parse-alt-rest-comp-when-tree-match-induction-step-1`and`parse-alt-rest-comp-when-tree-match-induction-step-2`. - Parse-alt-rest-comp-when-tree-match
- Completeness theorem for
`parse-alt-rest-comp`. - Parse-1*-dot-1*bit-when-tree-list-match
- Completeness theorem for
`parse-1*-dot-1*bit`. - Pred-option
- Completeness property for
`parse-option`. - Pred-group
- Completeness property for
`parse-group`. - Parse-?%i-when-tree-match
- Completeness theorem for
`parse-?%i`. - Parse-*digit-when-tree-list-match
- Completeness theorem for
`parse-*digit`. - Parse-*cwsp-when-tree-list-match
- Completeness theorem for
`parse-*cwsp`. - Parse-wsp-when-tree-match
- Completeness theorem for
`parse-wsp`. - Parse-repetition-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-repetition`. - Parse-repetition-when-tree-match-induction-step-1+2
- Combination of
`parse-repetition-when-tree-match-induction-step-1`and`parse-repetition-when-tree-match-induction-step-2`. - Parse-repetition-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-repetition`. - Parse-repetition-when-tree-match
- Completeness theorem for
`parse-repetition`. - Parse-option-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-option`. - Parse-ichar-when-tree-match
- Completeness theorem for
`parse-ichar`. - Parse-htab-when-tree-match
- Completeness theorem for
`parse-htab`. - Parse-hex-val-when-tree-match
- Completeness theorem for
`parse-hex-val`. - Parse-group-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-group`. - Parse-equal-/-equal-slash-when-tree-match
- Completeness theorem for
`parse-equal-/-equal-slash`. - Parse-element-when-tree-match-induction-step-5
- Fifth induction step of
the completeness lemma for
`parse-element`. - Parse-element-when-tree-match-induction-step-4
- Fourth induction step of
the completeness lemma for
`parse-element`. - Parse-element-when-tree-match
- Completeness theorem for
`parse-element`. - Parse-dot-1*bit-when-tree-match
- Completeness theorem for
`parse-dot-1*bit`. - Parse-dec-val-when-tree-match
- Completeness theorem for
`parse-dec-val`. - Parse-cr-when-tree-match
- Completeness theorem for
`parse-cr`. - Parse-concatenation-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-concatenation`. - Parse-concatenation-when-tree-match
- Completeness theorem for
`parse-concatenation`. - Parse-conc-rest-comp-when-tree-match
- Completeness theorem for
`parse-conc-rest-comp`. - Parse-cnl-when-tree-match
- Completeness theorem for
`parse-cnl`. - Parse-bin-val-when-tree-match
- Completeness theorem for
`parse-bin-val`. - Parse-alternation-when-tree-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-alternation`. - Parse-alpha-when-tree-match
- Completeness theorem for
`parse-alpha`. - Parse-1*cwsp-when-tree-list-match
- Completeness theorem for
`parse-1*cwsp`. - Parse-1*bit-when-tree-list-match
- Completeness theorem for
`parse-1*bit`. - Parse-*wsp/vchar-when-tree-list-match
- Completeness theorem for
`parse-*wsp/vchar`. - Parse-*hexdig-when-tree-list-match
- Completeness theorem for
`parse-*hexdig`. - Parse-*digit-star-*digit-when-tree-match
- Completeness theorem for
`parse-*digit-star-*digit`. - Parse-*cwsp-cnl-when-tree-match
- Completeness theorem for
`parse-*cwsp-cnl`. - Parse-*-dot-1*hexdig-when-tree-list-match
- Completeness theorem for
`parse-*-dot-1*hexdig`. - Parse-*-dot-1*digit-when-tree-list-match
- Completeness theorem for
`parse-*-dot-1*digit`. - Parse-*-alpha/digit/dash-when-tree-list-match
- Completeness theorem for
`parse-*-alpha/digit/dash`. - Parse-sp-when-tree-match
- Completeness theorem for
`parse-sp`. - Parse-rule-/-*cwsp-cnl-when-tree-match
- Completeness theorem for
`parse-rule-/-*cwsp-cnl`. - Parse-rule-when-tree-match
- Completeness theorem for
`parse-rule`. - Parse-num-val-when-tree-match
- Completeness theorem for
`parse-num-val`. - Parse-lf-when-tree-match
- Completeness theorem for
`parse-lf`. - Parse-in-range-when-tree-match
- Completeness theorem for
`parse-in-range`. - Parse-ichar2-when-tree-match
- Completeness theorem for
`parse-ichar2`. - Parse-hex-val-rest-when-tree-match
- Completeness theorem for
`parse-hex-val-rest`. - Parse-defined-as-when-tree-match
- Completeness theorem for
`parse-defined-as`. - Parse-dec-val-rest-when-tree-match
- Completeness theorem for
`parse-dec-val-rest`. - Parse-crlf-when-tree-match
- Completeness theorem for
`parse-crlf`. - Parse-conc-rest-when-tree-list-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-conc-rest`. - Parse-case-sensitive-string-when-tree-match
- Completeness theorem for
`parse-case-sensitive-string`. - Parse-case-insensitive-string-when-tree-match
- Completeness theorem for
`parse-case-insensitive-string`. - Parse-bit-when-tree-match
- Completeness theorem for
`parse-bit`. - Parse-alt-rest-when-tree-list-match-induction-step-2
- Second induction step of
the completeness lemma for
`parse-alt-rest`. - Parse-1*hexdig-when-tree-list-match
- Completeness theorem for
`parse-1*hexdig`. - Parse-1*digit-when-tree-list-match
- Completeness theorem for
`parse-1*digit`. - Parse-1*-dot-1*hexdig-when-tree-list-match
- Completeness theorem for
`parse-1*-dot-1*hexdig`. - Parse-1*-dot-1*digit-when-tree-list-match
- Completeness theorem for
`parse-1*-dot-1*digit`. - Parse-?repeat-when-tree-match
- Completeness theorem for
`parse-?repeat`. - Parse-wsp/vchar-when-tree-match
- Completeness theorem for
`parse-wsp/vchar`. - Parse-vchar-when-tree-match
- Completeness theorem for
`parse-vchar`. - Parse-rulename-when-tree-match
- Completeness theorem for
`parse-rulename`. - Parse-repeat-when-tree-match
- Completeness theorem for
`parse-repeat`. - Parse-quoted-string-when-tree-match
- Completeness theorem for
`parse-quoted-string`. - Parse-prose-val-when-tree-match
- Completeness theorem for
`parse-prose-val`. - Parse-option-when-tree-match
- Completeness theorem for
`parse-option`. - Parse-hexdig-when-tree-match
- Completeness theorem for
`parse-hexdig`. - Parse-group-when-tree-match
- Completeness theorem for
`parse-group`. - Parse-element-when-tree-match-induction-step-6
- Sixth induction step of
the completeness lemma for
`parse-element`. - Parse-element-when-tree-match-base-case
- Base case of
the completeness lemma for
`parse-element`. - Parse-dquote-when-tree-match
- Completeness theorem for
`parse-dquote`. - Parse-dot-1*hexdig-when-tree-match
- Completeness theorem for
`parse-dot-1*hexdig`. - Parse-dot-1*digit-when-tree-match
- Completeness theorem for
`parse-dot-1*digit`. - Parse-digit-when-tree-match
- Completeness theorem for
`parse-digit`. - Parse-dash-1*hexdig-when-tree-match
- Completeness theorem for
`parse-dash-1*hexdig`. - Parse-dash-1*digit-when-tree-match
- Completeness theorem for
`parse-dash-1*digit`. - Parse-dash-1*bit-when-tree-match
- Completeness theorem for
`parse-dash-1*bit`. - Parse-cwsp-when-tree-match
- Completeness theorem for
`parse-cwsp`. - Parse-concatenation-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-concatenation`. - Parse-conc-rest-when-tree-list-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-conc-rest`. - Parse-conc-rest-comp-when-tree-match-base-case
- Base case of
the completeness lemma for
`parse-conc-rest-comp`. - Parse-comment-when-tree-match
- Completeness theorem for
`parse-comment`. - Parse-cnl-wsp-when-tree-match
- Completeness theorem for
`parse-cnl-wsp`. - Parse-char-val-when-tree-match
- Completeness theorem for
`parse-char-val`. - Parse-alternation-when-tree-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-alternation`. - Parse-alt-rest-when-tree-list-match-induction-step-1
- First induction step of
the completeness lemma for
`parse-alt-rest`. - Parse-alt-rest-comp-when-tree-match-base-case
- Base case of
the completeness lemma for
`parse-alt-rest-comp`. - Parse-alpha/digit/dash-when-tree-match
- Completeness theorem for
`parse-alpha/digit/dash`. - Parse-option-when-tree-match-base-case
- Base case of
the completeness lemma for
`parse-option`. - Parse-group-when-tree-match-base-case
- Base case of
the completeness lemma for
`parse-group`. - Parse-any-of-cons
- Completeness theorem for
`parse-any`.