The name of the <prefix>-<rulename>-nonleaf theorem
described in deftreeops.
The name of the <prefix>-<rulename>-rulename theorem
described in deftreeops.
The name of the <prefix>-<rulename>-branches-match-alt theorem
described in deftreeops.
The name of the <prefix>-<rulename>-concs theorem
described in deftreeops.
The name of the <prefix>-<rulename>-conc-equivs theorem
described in deftreeops.
This is nil if the theorem is not generated,
i.e. if some concatenation in the alternation that defines the rule name
is not a singleton concatenation
consisting of a singleton repetition of a rulename element.
The name of the <prefix>-<rulename>-conc? function
described in deftreeops.
This is nil if the function is not generated,
i.e. if the rule name is defined by
an alternation of just one concatenation.
The information about the concatenations that form
the alternation that defines the rule name.