Just a different way to define
The definition of
Either definition is equivalent, as established by this theorem, which is ordinarily disabled.
Theorem:
(defthm 4v-sexpr-alist-<=-is-alt (iff (4v-sexpr-alist-<= a b) (4v-sexpr-alist-<=-alt a b)))
Theorem:
(defthm 4v-sexpr-alist-<=-alt-necc (implies (not (4v-alist-<= (4v-sexpr-eval-alist a env) (4v-sexpr-eval-alist b env))) (not (4v-sexpr-alist-<=-alt a b))))
Theorem:
(defthm 4v-sexpr-alist-<=-alt-witnessing-witness-rule-correct (implies (not ((lambda (env b a) (not (4v-alist-<= (4v-sexpr-eval-alist a env) (4v-sexpr-eval-alist b env)))) (4v-sexpr-alist-<=-alt-witness a b) b a)) (4v-sexpr-alist-<=-alt a b)) :rule-classes nil)
Theorem:
(defthm 4v-sexpr-alist-<=-alt-instancing-instance-rule-correct (implies (not (4v-alist-<= (4v-sexpr-eval-alist a env) (4v-sexpr-eval-alist b env))) (not (4v-sexpr-alist-<=-alt a b))) :rule-classes nil)
Theorem:
(defthm 4v-alist-<=-4v-sexpr-eval-alist (implies (4v-sexpr-alist-<= a b) (4v-alist-<= (4v-sexpr-eval-alist a env) (4v-sexpr-eval-alist b env))))
Theorem:
(defthm 4v-sexpr-alist-<=-is-alt (iff (4v-sexpr-alist-<= a b) (4v-sexpr-alist-<=-alt a b)))