` `

show the generated equivalence relation maintained at the current subterm
Major Section: PROOF-CHECKER-COMMANDS

General Forms: geneqv ; show list of equivalence relations being maintained (geneqv t) ; as above, but pair each relation with a justifying runeThis 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.