equal-by-g - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "records")

local

(local (include-book "equal-by-g-help"))

equal-by-g-constraintencapsulate

(encapsulate (((equal-by-g-hyp) => *) ((equal-by-g-lhs) => *)
    ((equal-by-g-rhs) => *))
  (local (defun equal-by-g-hyp nil nil))
  (local (defun equal-by-g-lhs nil nil))
  (local (defun equal-by-g-rhs nil nil))
  (defthm equal-by-g-constraint
    (implies (equal-by-g-hyp)
      (equal (g arbitrary-key (equal-by-g-lhs))
        (g arbitrary-key (equal-by-g-rhs))))))

equal-by-gtheorem

(defthm equal-by-g
  (implies (equal-by-g-hyp)
    (equal (equal-by-g-lhs) (equal-by-g-rhs)))
  :hints (("Goal" :in-theory (disable g-worseguy-finds-counterexample g-worseguy)
     :use ((:instance g-worseguy-finds-counterexample
        (x (equal-by-g-lhs))
        (y (equal-by-g-rhs)))))))