		Search-engine friendly clone of the ACL2 documentation.

Sexpr-equivs

Useful equivalence relations for reasoning about 4v-sexprs.

4v-sexpr-alist-equiv: X === Y in the sense of sexpr alists if X[k] === Y[k] in the sense of sexprs for all keys k.
4v-env-equiv: Equivalence of four-valued environments (alists).
4v-sexpr-list-equiv: X === Y in the sense of sexpr lists if they are equal lengths and Xi evaluates to the same thing as Yi for all i and for all environments.
4v-sexpr-equiv: X === Y in the sense of sexprs if they always evaluate to the same thing under any possible environment.
4v-alists-agree: See whether two four-valued alists agree on particular keys.
Key-and-env-equiv: (key-and-env-equiv x y) is an extension of 4v-env-equiv that additionally requires the keys match between the two alists.
4v-sexpr-alist-equiv-alt
4v-sexpr-alist-pair-equiv: Element equivalence for sexpr alists.
4v-cdr-consp-equiv: Stronger version of element equivalence for four-valued alists.
4v-cdr-equiv: Weaker version of element equivalence for four-valued alists.