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.
If the conc-equivs-thm component is not nil,
a positive integer indicating the kind of alternation
among the ones listed as supported in deftreeops:
1 for the first one, 2 for the second one.
This is 0 if conc-equivs-thm is nil.
The name of the <prefix>-<rulename>-conc? function
described in deftreeops.
This is nil if the function is not generated.
The information about the concatenations that form
the alternation that defines the rule name.
