Exhibit a new decoding for an ACL2 type-set

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description. Also see type-reasoning for basic background on type reasoning in ACL2.

Example Rule Class: (:type-set-inverter :corollary (equal (and (counting-number x) (not (equal x 0))) (and (integerp x) (< 0 x))) :type-set 2) General Forms of Rule Class: :type-set-inverter, or (:type-set-inverter :type-set n) General Form of Theorem or Corollary: (EQUAL new-expr old-expr)

where `type-set` (see type-set) and `type-set`

(convert-type-set-to-term 'x n (ens state) (w state) nil)].

If the `type-set` field of the rule-class is omitted, we
attempt to compute it from the right-hand side, `type-set` and an error is caused because `type-set` and
the

The rule generated will henceforth make `defthm` event named

Type-sets are inverted when forced assumptions are turned into formulas to
be proved. In their internal form, assumptions are essentially pairs
consisting of a context and a goal term, which was forced. Abstractly a
context is just a list of hypotheses which may be assumed while proving the
goal term. But actually contexts are alists which pair terms with type-sets,
encoding the current hypotheses. For example, if the original conjecture
contained the hypothesis