ACL2-pc::geneqv
(macro)
show the generated equivalence relation maintained at the current subterm
General Forms:
geneqv ; show list of equivalence relations being maintained
(geneqv t) ; as above, but pair each relation with a justifying rune
This is an advanced command, whose effect is to print the so-called
``generated equivalence relation'' (or ``geneqv'') that is maintained at the
current subterm of the conclusion. That structure is a list of equivalence
relations, representing the transitive closure E of the union of those
relations, such that it suffices to maintain E at the current subterm: if
that subterm, u, is replaced in the goal's conclusion, G, by another
term equivalent to u with respect to E, then the resulting
conclusion is Boolean equivalent to G. Also see defcong.
The command `geneqv' prints the above list of equivalence relations,
or more precisely, the list of function symbols for those relations. If
however geneqv is given a non-nil argument, then a list is printed
whose elements are each of the form (s r), where s is the symbol for
an equivalence relation and r is a :congruence rune
justifying the inclusion of s in the list of equivalence relations being
maintained at the current subterm.
