always-equal-prep

(in-package "GL")

(include-book "symbolic-arithmetic")

(include-book "g-if")

(include-book "eval-g-base")

(include-book "gl-mbe")

(local (include-book "hyp-fix"))

(local (include-book "eval-g-base-help"))

(local (include-book "clause-processors/find-subterms" :dir :system))

(local (include-book "clause-processors/just-expand" :dir :system))

(local (include-book "centaur/bitops/ihsext-basics" :dir :system))

(defun ctrex-for-always-equal
  (x y)
  (declare (xargs :guard t
      :measure (+ (acl2-count x) (acl2-count y))))
  (if (and (atom x) (atom y))
    nil
    (b* (((mv xa xd) (if (consp x)
           (mv (car x) (cdr x))
           (mv x x))) ((mv ya yd) (if (consp y)
            (mv (car y) (cdr y))
            (mv y y))))
      (if (hqual xa ya)
        (cons nil (ctrex-for-always-equal xd yd))
        (cons t (ctrex-for-always-equal xa ya))))))

(defthmd ctrex-for-always-equal-correct
  (implies (and (ubddp x) (ubddp y) (not (equal x y)))
    (equal (eval-bdd x (ctrex-for-always-equal x y))
      (not (eval-bdd y (ctrex-for-always-equal x y)))))
  :hints (("goal" :induct (ctrex-for-always-equal x y)
     :in-theory (enable ubddp eval-bdd))))

(defun ctrex-for-always-equal-under-hyp1
  (x y hypbdd)
  (declare (xargs :guard t))
  (cond ((hqual x y) (mv nil nil))
    ((eq hypbdd nil) (mv nil nil))
    ((atom hypbdd) (mv (not (hqual x y))
        (ctrex-for-always-equal x y)))
    ((and (atom x) (atom y)) (mv (not (eq hypbdd nil))
        (ctrex-for-always-equal hypbdd nil)))
    ((eq (cdr hypbdd) nil) (mv-let (ok env)
        (ctrex-for-always-equal-under-hyp1 (if (consp x)
            (car x)
            x)
          (if (consp y)
            (car y)
            y)
          (car hypbdd))
        (mv ok (cons t env))))
    ((eq (car hypbdd) nil) (mv-let (ok env)
        (ctrex-for-always-equal-under-hyp1 (if (consp x)
            (cdr x)
            x)
          (if (consp y)
            (cdr y)
            y)
          (cdr hypbdd))
        (mv ok (cons nil env))))
    (t (let ((x1 (q-and hypbdd x)) (y1 (q-and hypbdd y)))
        (mv (not (hqual x1 y1))
          (ctrex-for-always-equal x1 y1))))))

(defun ctrex-for-always-equal-under-hyp1-ind
  (x y hypbdd env)
  (cond ((hqual x y) env)
    ((eq hypbdd nil) env)
    ((atom hypbdd) env)
    ((and (atom x) (atom y)) env)
    ((eq (cdr hypbdd) nil) (ctrex-for-always-equal-under-hyp1-ind (if (consp x)
          (car x)
          x)
        (if (consp y)
          (car y)
          y)
        (car hypbdd)
        (cdr env)))
    ((eq (car hypbdd) nil) (ctrex-for-always-equal-under-hyp1-ind (if (consp x)
          (cdr x)
          x)
        (if (consp y)
          (cdr y)
          y)
        (cdr hypbdd)
        (cdr env)))
    (t env)))

(local (in-theory (disable ctrex-for-always-equal-under-hyp1
      ctrex-for-always-equal
      qs-subset-when-booleans
      eval-bdd-when-qs-subset
      equal-of-booleans-rewrite)))

(defthm ctrex-for-always-equal-under-hyp1-correct
  (implies (and (ubddp x)
      (ubddp y)
      (ubddp hypbdd)
      (not (equal (eval-bdd x env) (eval-bdd y env)))
      (eval-bdd hypbdd env))
    (let ((env (mv-nth 1
           (ctrex-for-always-equal-under-hyp1 x
             y
             hypbdd))))
      (and (not (equal (eval-bdd x env) (eval-bdd y env)))
        (eval-bdd hypbdd env))))
  :hints ((just-induct-and-expand (ctrex-for-always-equal-under-hyp1-ind x
       y
       hypbdd
       env)
     :expand-others ((ctrex-for-always-equal-under-hyp1 x
        y
        hypbdd))) (and stable-under-simplificationp
      (let ((call (find-call-lst 'ctrex-for-always-equal clause)))
        (and call
          `(:use ((:instance ctrex-for-always-equal-correct
               (x ,(SECOND GL::CALL))
               (y ,(THIRD GL::CALL))))
            :in-theory (disable ctrex-for-always-equal-correct)))))
    (and (equal (car clause)
        '(not (equal (q-binary-and hypbdd x)
            (q-binary-and hypbdd y))))
      (bdd-reasoning))
    (and stable-under-simplificationp
      '(:expand ((:free (x a b)
           (eval-bdd x (cons a b))) (eval-bdd x env)
          (eval-bdd x nil)
          (eval-bdd y env)
          (eval-bdd y nil)
          (eval-bdd hypbdd env)
          (eval-bdd hypbdd nil))))))

(defthm ctrex-for-always-equal-under-hyp1-flag-correct
  (implies (and (ubddp x) (ubddp y) (ubddp hypbdd))
    (iff (mv-nth 0
        (ctrex-for-always-equal-under-hyp1 x
          y
          hypbdd))
      (let ((env (mv-nth 1
             (ctrex-for-always-equal-under-hyp1 x
               y
               hypbdd))))
        (and (not (equal (eval-bdd x env) (eval-bdd y env)))
          (eval-bdd hypbdd env)))))
  :hints ((just-induct-and-expand (ctrex-for-always-equal-under-hyp1-ind x
       y
       hypbdd
       env)
     :expand-others ((ctrex-for-always-equal-under-hyp1 x
        y
        hypbdd))) (and stable-under-simplificationp
      (let ((call (find-call-lst 'ctrex-for-always-equal clause)))
        (and call
          `(:use ((:instance ctrex-for-always-equal-correct
               (x ,(SECOND GL::CALL))
               (y ,(THIRD GL::CALL))))
            :in-theory (disable ctrex-for-always-equal-correct)))))
    (and stable-under-simplificationp
      (member-equal '(not (equal (q-binary-and hypbdd x)
            (q-binary-and hypbdd y)))
        clause)
      (bdd-reasoning))
    (and stable-under-simplificationp
      '(:expand ((:free (x a b)
           (eval-bdd x (cons a b))))))))

(defun ctrex-for-always-equal-under-hyp
  (x y hypbdd)
  (declare (xargs :guard t :measure (acl2-count hypbdd)))
  (cond ((hqual x y) (mv nil nil))
    ((eq hypbdd nil) (mv nil nil))
    ((atom hypbdd) (mv (not (hqual x y))
        (ctrex-for-always-equal x y)))
    ((eq (cdr hypbdd) nil) (mv-let (ok env)
        (ctrex-for-always-equal-under-hyp (if (consp x)
            (car x)
            x)
          (if (consp y)
            (car y)
            y)
          (car hypbdd))
        (mv ok (cons t env))))
    ((eq (car hypbdd) nil) (mv-let (ok env)
        (ctrex-for-always-equal-under-hyp (if (consp x)
            (cdr x)
            x)
          (if (consp y)
            (cdr y)
            y)
          (cdr hypbdd))
        (mv ok (cons nil env))))
    (t (b* (((mv ok env) (ctrex-for-always-equal-under-hyp (if (consp x)
               (car x)
               x)
             (if (consp y)
               (car y)
               y)
             (car hypbdd))) ((when ok) (mv t (cons t env)))
          ((mv ok env) (ctrex-for-always-equal-under-hyp1 (if (consp x)
                (cdr x)
                x)
              (if (consp y)
                (cdr y)
                y)
              (cdr hypbdd))))
        (mv ok (cons nil env))))))

(defun ctrex-for-always-equal-under-hyp-ind
  (x y hypbdd env)
  (declare (xargs :measure (acl2-count hypbdd)))
  (cond ((hqual x y) env)
    ((eq hypbdd nil) env)
    ((atom hypbdd) env)
    ((eq (cdr hypbdd) nil) (ctrex-for-always-equal-under-hyp-ind (if (consp x)
          (car x)
          x)
        (if (consp y)
          (car y)
          y)
        (car hypbdd)
        (cdr env)))
    ((eq (car hypbdd) nil) (ctrex-for-always-equal-under-hyp-ind (if (consp x)
          (cdr x)
          x)
        (if (consp y)
          (cdr y)
          y)
        (cdr hypbdd)
        (cdr env)))
    (t (ctrex-for-always-equal-under-hyp-ind (if (consp x)
          (car x)
          x)
        (if (consp y)
          (car y)
          y)
        (car hypbdd)
        (cdr env)))))

(local (in-theory (disable ctrex-for-always-equal-under-hyp
      double-containment)))

(defthm ctrex-for-always-equal-under-hyp-flag-correct
  (implies (and (ubddp x) (ubddp y) (ubddp hyp))
    (iff (mv-nth 0
        (ctrex-for-always-equal-under-hyp x y hyp))
      (let ((env (mv-nth 1
             (ctrex-for-always-equal-under-hyp x y hyp))))
        (and (not (equal (eval-bdd x env) (eval-bdd y env)))
          (eval-bdd hyp env)))))
  :hints ((just-induct-and-expand (ctrex-for-always-equal-under-hyp-ind x
       y
       hyp
       env)
     :expand-others ((ctrex-for-always-equal-under-hyp x y hyp))) (and stable-under-simplificationp
      (b* ((call (find-call-lst 'ctrex-for-always-equal clause)) ((when call) `(:use ((:instance ctrex-for-always-equal-correct
                 (x ,(SECOND GL::CALL))
                 (y ,(THIRD GL::CALL))))
              :in-theory (disable ctrex-for-always-equal-correct))))
        nil))
    (and stable-under-simplificationp
      '(:expand ((:free (x a b)
           (eval-bdd x (cons a b))) (eval-bdd x env)
          (eval-bdd x nil)
          (eval-bdd y env)
          (eval-bdd y nil)
          (eval-bdd hyp env)
          (eval-bdd hyp nil))))))

(defthm ctrex-for-always-equal-under-hyp-correct
  (implies (and (ubddp x)
      (ubddp y)
      (ubddp hyp)
      (not (equal (eval-bdd x env) (eval-bdd y env)))
      (eval-bdd hyp env))
    (let ((env (mv-nth 1
           (ctrex-for-always-equal-under-hyp x y hyp))))
      (and (not (equal (eval-bdd x env) (eval-bdd y env)))
        (eval-bdd hyp env))))
  :hints ((just-induct-and-expand (ctrex-for-always-equal-under-hyp-ind x
       y
       hyp
       env)
     :expand-others ((ctrex-for-always-equal-under-hyp x y hyp))) (and stable-under-simplificationp
      (b* ((call (find-call-lst 'ctrex-for-always-equal clause)) ((when call) `(:use ((:instance ctrex-for-always-equal-correct
                 (x ,(SECOND GL::CALL))
                 (y ,(THIRD GL::CALL))))
              :in-theory (disable ctrex-for-always-equal-correct)))
          (call (find-call-lst 'ctrex-for-always-equal-under-hyp1
              clause))
          ((when call) `(:use ((:instance ctrex-for-always-equal-under-hyp1-correct
                 (x ,(SECOND GL::CALL))
                 (y ,(THIRD GL::CALL))
                 (hypbdd ,(FOURTH GL::CALL))
                 (env (cdr env))))
              :in-theory (disable ctrex-for-always-equal-under-hyp1-correct))))
        nil))
    (and stable-under-simplificationp
      '(:expand ((:free (x a b)
           (eval-bdd x (cons a b))) (eval-bdd x env)
          (eval-bdd x nil)
          (eval-bdd y env)
          (eval-bdd y nil)
          (eval-bdd hyp env)
          (eval-bdd hyp nil))
        :do-not-induct t))))

(define always-equal-ss-under-hyp
  ((x true-listp) (y true-listp) hypbdd)
  :measure (+ (acl2-count x) (acl2-count y))
  (b* (((mv xa xd xend) (first/rest/end x)) ((mv ya yd yend) (first/rest/end y))
      ((when (hqual xa ya)) (if (and xend yend)
          (mv t nil)
          (always-equal-ss-under-hyp xd yd hypbdd)))
      (xa (ubdd-fix xa))
      (ya (ubdd-fix ya))
      ((mv diffp res) (ctrex-for-always-equal-under-hyp xa
          ya
          hypbdd)))
    (if diffp
      (mv nil res)
      (if (and xend yend)
        (mv t nil)
        (always-equal-ss-under-hyp xd yd hypbdd)))))

(local (encapsulate nil
    (local (progn (defthm equal-of-bool->bit
          (equal (equal (bool->bit x) (bool->bit y))
            (iff x y)))))
    (defthm always-equal-ss-under-hyp-correct
      (mv-let (always-equal ctrex)
        (always-equal-ss-under-hyp x y hyp)
        (and (implies (and always-equal
              (not (bfr-mode))
              (ubddp hyp)
              (bfr-eval hyp env))
            (equal (bfr-list->s x env)
              (bfr-list->s y env)))
          (implies (and (not (bfr-mode))
              (bfr-eval ctrex-bdd env)
              (ubddp hyp)
              (not always-equal))
            (and (bfr-eval hyp ctrex)
              (not (equal (bfr-list->s x ctrex)
                  (bfr-list->s y ctrex)))))))
      :hints (("Goal" :in-theory (e/d* (equal-logcons-strong always-equal-ss-under-hyp
             bfr-list->s
             bfr-eval
             scdr
             s-endp)
           (ctrex-for-always-equal-under-hyp logcons
             ctrex-for-always-equal-under-hyp-correct
             ctrex-for-always-equal-under-hyp-flag-correct
             default-cdr
             default-car
             default-+-1
             default-+-2
             (:definition always-equal-ss-under-hyp)
             (:rules-of-class :type-prescription :here))
           ((:type-prescription bfr-eval) (:type-prescription bool->bit$inline)
             (:type-prescription ash)
             (:type-prescription bfr-list->s)
             (:type-prescription eval-bdd)))
         :induct (always-equal-ss-under-hyp x y hyp)
         :expand ((always-equal-ss-under-hyp x y hyp) (always-equal-ss-under-hyp x nil hyp)
           (always-equal-ss-under-hyp nil y hyp)
           (always-equal-ss-under-hyp nil nil hyp)
           (:free (env) (bfr-list->s x env))
           (:free (env) (bfr-list->s y env)))) (and stable-under-simplificationp
          (b* ((call (find-call-lst 'ctrex-for-always-equal-under-hyp
                 clause)) ((when call) `(:use ((:instance ctrex-for-always-equal-under-hyp-correct
                     (x ,(SECOND GL::CALL))
                     (y ,(THIRD GL::CALL))
                     (hyp ,(FOURTH GL::CALL))) (:instance ctrex-for-always-equal-under-hyp-flag-correct
                      (x ,(SECOND GL::CALL))
                      (y ,(THIRD GL::CALL))
                      (hyp ,(FOURTH GL::CALL)))))))
            nil)))
      :rule-classes ((:rewrite :match-free :all)))))

(include-book "ctrex-utils")

(defun always-equal-of-integers
  (a b hyp config bvar-db state)
  (declare (xargs :guard (and (not (bfr-mode))
        (glcp-config-p config)
        (general-integerp a)
        (general-integerp b))
      :stobjs (hyp bvar-db state)))
  (b* ((abits (general-integer-bits a)) (bbits (general-integer-bits b))
      (uhyp (ubdd-fix (bfr-hyp->bfr hyp)))
      ((mv requal rctrex) (always-equal-ss-under-hyp abits bbits uhyp))
      ((unless requal) (ec-call (glcp-print-single-ctrex rctrex
            "Error:"
            "ALWAYS-EQUAL violation"
            config
            bvar-db
            state))
        (g-apply 'equal (gl-list a b))))
    t))

(defthm deps-of-always-equal-of-integers
  (implies (and (not (gobj-depends-on k p a))
      (not (gobj-depends-on k p b))
      (general-integerp a)
      (general-integerp b))
    (not (gobj-depends-on k
        p
        (always-equal-of-integers a
          b
          hyp
          config
          bvar-db
          state))))
  :hints (("Goal" :in-theory (enable always-equal-of-integers))))

(local (defthm eval-g-base-apply-of-equal
    (equal (eval-g-base-ev (list 'equal (list 'quote x) (list 'quote y))
        a)
      (equal x y))))

(local (defthm eval-g-base-apply-of-equal-kwote-lst
    (equal (eval-g-base-ev (cons 'equal (kwote-lst (list x y)))
        a)
      (equal x y))))

(local (defthm bfr-eval-of-ubdd-fix
    (implies (not (bfr-mode))
      (equal (bfr-eval (ubdd-fix x) env)
        (bfr-eval x env)))
    :hints (("Goal" :in-theory (enable bfr-eval)))))

(local (defthm always-equal-of-integers-correct
    (implies (and (not (bfr-mode))
        (general-integerp a)
        (general-integerp b)
        (bfr-hyp-eval hyp (car env)))
      (equal (eval-g-base (always-equal-of-integers a
            b
            hyp
            config
            bvar-db
            state)
          env)
        (equal (eval-g-base a env)
          (eval-g-base b env))))
    :hints (("Goal" :in-theory (e/d* ((:ruleset general-object-possibilities) ctrex-for-always-equal-correct
           boolean-list-bfr-eval-list)
         (bfr-sat-bdd-unsat bfr-list->s))))))

(in-theory (disable always-equal-of-integers))

(defun always-equal-of-booleans
  (a b hyp config bvar-db state)
  (declare (xargs :guard (and (not (bfr-mode))
        (glcp-config-p config)
        (general-booleanp a)
        (general-booleanp b))
      :stobjs (hyp bvar-db state)))
  (b* ((av (general-boolean-value a)) (bv (general-boolean-value b))
      ((when (hqual av bv)) t)
      (av (ubdd-fix av))
      (bv (ubdd-fix bv))
      ((when (hqual av bv)) t)
      ((mv unequal ctrex) (ctrex-for-always-equal-under-hyp av
          bv
          (ubdd-fix (bfr-hyp->bfr hyp))))
      ((unless unequal) t))
    (ec-call (glcp-print-single-ctrex ctrex
        "Error:"
        "ALWAYS-EQUAL violation"
        config
        bvar-db
        state))
    (g-apply 'equal (gl-list a b))))

(defthm deps-of-always-equal-of-booleans
  (implies (and (not (gobj-depends-on k p a))
      (not (gobj-depends-on k p b))
      (general-booleanp a)
      (general-booleanp b))
    (not (gobj-depends-on k
        p
        (always-equal-of-booleans a
          b
          hyp
          config
          bvar-db
          state))))
  :hints (("Goal" :in-theory (enable always-equal-of-booleans))))

(local (defthm ubdd-fixes-unequal
    (implies (not (equal (eval-bdd a env) (eval-bdd b env)))
      (not (equal (ubdd-fix a) (ubdd-fix b))))
    :hints (("goal" :in-theory (disable eval-bdd-ubdd-fix)
       :use ((:instance eval-bdd-ubdd-fix (x a) (env env)) (:instance eval-bdd-ubdd-fix (x b) (env env)))))))

(local (defthm eval-bdd-of-bfr-constr->bfr
    (implies (not (bfr-mode))
      (equal (eval-bdd (bfr-constr->bfr hyp) env)
        (bfr-hyp-eval hyp env)))
    :hints (("Goal" :in-theory (enable bfr-hyp-eval
         bfr-eval
         bfr-hyp-fix
         bfr-constr->bfr)))))

(local (defthm always-equal-of-booleans-correct
    (implies (and (not (bfr-mode))
        (general-booleanp a)
        (general-booleanp b)
        (bfr-hyp-eval hyp (car env)))
      (equal (eval-g-base (always-equal-of-booleans a
            b
            hyp
            config
            bvar-db
            state)
          env)
        (equal (eval-g-base a env)
          (eval-g-base b env))))
    :hints (("Goal" :in-theory (e/d (bfr-eval)
         (ctrex-for-always-equal-under-hyp-correct ctrex-for-always-equal-under-hyp-flag-correct))) (and stable-under-simplificationp
        (b* ((call (find-call-lst 'ctrex-for-always-equal-under-hyp
               clause)) ((when call) `(:use ((:instance ctrex-for-always-equal-under-hyp-correct
                   (x ,(SECOND GL::CALL))
                   (y ,(THIRD GL::CALL))
                   (hyp ,(FOURTH GL::CALL))
                   (env (car env))) (:instance ctrex-for-always-equal-under-hyp-flag-correct
                    (x ,(SECOND GL::CALL))
                    (y ,(THIRD GL::CALL))
                    (hyp ,(FOURTH GL::CALL)))))))
          nil)))))

(in-theory (disable always-equal-of-booleans))

(define g-always-equal-core
  (a b
    hyp
    clk
    config
    bvar-db
    state)
  :measure (+ (acl2-count a) (acl2-count b))
  :guard (and (not (bfr-mode))
    (natp clk)
    (glcp-config-p config))
  :verify-guards nil
  (let* ((hyp (lbfr-hyp-fix hyp)))
    (cond ((hqual a b) (gret t))
      ((and (general-concretep a)
         (general-concretep b)) (gret (hons-equal (general-concrete-obj a)
            (general-concrete-obj b))))
      ((zp clk) (gret (g-apply 'equal (gl-list a b))))
      ((mbe :logic (not (member-eq (tag a) '(:g-ite :g-var :g-apply)))
         :exec (or (atom a)
           (not (member-eq (tag a) '(:g-ite :g-var :g-apply))))) (cond ((mbe :logic (not (member-eq (tag b) '(:g-ite :g-var :g-apply)))
             :exec (or (atom b)
               (not (member-eq (tag b) '(:g-ite :g-var :g-apply))))) (cond ((general-booleanp a) (gret (and (general-booleanp b)
                    (always-equal-of-booleans a
                      b
                      hyp
                      config
                      bvar-db
                      state))))
              ((general-booleanp b) (gret nil))
              ((general-integerp a) (gret (and (general-integerp b)
                    (always-equal-of-integers a
                      b
                      hyp
                      config
                      bvar-db
                      state))))
              ((general-integerp b) (gret nil))
              ((general-consp a) (if (general-consp b)
                  (b* (((gret car-equal) (g-always-equal-core (general-consp-car a)
                         (general-consp-car b)
                         hyp
                         clk
                         config
                         bvar-db
                         state)))
                    (if (eq car-equal t)
                      (g-always-equal-core (general-consp-cdr a)
                        (general-consp-cdr b)
                        hyp
                        clk
                        config
                        bvar-db
                        state)
                      (g-if-mbe (gret car-equal)
                        (gret (g-apply 'equal (gl-list a b)))
                        (gret nil))))
                  (gret nil)))
              (t (mbe :logic (if (general-consp b)
                    (gret nil)
                    (gret nil))
                  :exec (gret nil)))))
          ((eq (tag b) :g-ite) (if (zp clk)
              (gret (g-apply 'equal (gl-list a b)))
              (let* ((test (g-ite->test b)) (then (g-ite->then b))
                  (else (g-ite->else b)))
                (g-if-mbe (gret test)
                  (g-always-equal-core a
                    then
                    hyp
                    clk
                    config
                    bvar-db
                    state)
                  (g-always-equal-core a
                    else
                    hyp
                    clk
                    config
                    bvar-db
                    state)))))
          (t (gret (g-apply 'equal (gl-list a b))))))
      ((eq (tag a) :g-ite) (if (zp clk)
          (gret (g-apply 'equal (gl-list a b)))
          (let* ((test (g-ite->test a)) (then (g-ite->then a))
              (else (g-ite->else a)))
            (g-if-mbe (gret test)
              (g-always-equal-core then
                b
                hyp
                clk
                config
                bvar-db
                state)
              (g-always-equal-core else
                b
                hyp
                clk
                config
                bvar-db
                state)))))
      (t (gret (g-apply 'equal (gl-list a b))))))
  ///
  (def-hyp-congruence g-always-equal-core
    :hints (("Goal" :in-theory (disable always-equal-of-integers
         always-equal-of-booleans
         (:d g-always-equal-core))
       :induct (g-always-equal-core a
         b
         hyp
         clk
         config
         bvar-db
         state)
       :expand ((:free (hyp)
          (g-always-equal-core a
            b
            hyp
            clk
            config
            bvar-db
            state)) (:free (hyp)
           (g-always-equal-core a
             a
             hyp
             clk
             config
             bvar-db
             state)))))))

(encapsulate nil
  (local (in-theory (e/d* (g-if-fn g-or-fn)
        (g-always-equal-core equal-of-booleans-rewrite
          iff-implies-equal-not
          (:type-prescription true-under-hyp)
          (:type-prescription false-under-hyp)
          (:type-prescription general-booleanp)
          (:type-prescription general-integerp)
          (:type-prescription ubddp)
          (:type-prescription general-concretep)
          (:meta mv-nth-cons-meta)
          zp-open
          default-<-2
          default-<-1
          (:type-prescription zp)
          (:type-prescription hyp-fix)
          default-car
          default-cdr
          general-concretep-def
          ctrex-for-always-equal
          hyp-fix
          (:rules-of-class :type-prescription :here)
          not))))
  (verify-guards g-always-equal-core))

(defthm deps-of-g-always-equal-core
  (implies (and (not (gobj-depends-on k p x))
      (not (gobj-depends-on k p y)))
    (not (gobj-depends-on k
        p
        (mv-nth 0
          (g-always-equal-core x
            y
            hyp
            clk
            config
            bvar-db
            state)))))
  :hints ('(:in-theory (e/d ((:i g-always-equal-core))
       (gobj-depends-on))) (just-induct-and-expand (g-always-equal-core x
        y
        hyp
        clk
        config
        bvar-db
        state))))

(local (include-book "std/util/termhints" :dir :system))

(encapsulate nil
  (local (include-book "clause-processors/just-expand" :dir :system))
  (local (in-theory (enable (:i g-always-equal-core))))
  (local (in-theory (enable possibilities-for-x-10-strong)))
  (local (include-book "tools/trivial-ancestors-check" :dir :system))
  (local (use-trivial-ancestors-check))
  (local (defthm general-consp-implies-general-consp
      (implies (general-consp x)
        (general-consp x))))
  (local (defthm equal-bfr-list->s-when-not-integerp
      (implies (not (integerp x))
        (not (equal x (bfr-list->s bits env))))))
  (local (defthm equal-bfr-eval-when-not-booleanp
      (implies (not (booleanp x))
        (not (equal x (bfr-eval bits env))))))
  (defthm g-always-equal-core-correct
    (implies (and (not (bfr-mode))
        (bfr-hyp-eval hyp (car env)))
      (equal (eval-g-base (mv-nth 0
            (g-always-equal-core x
              y
              hyp
              clk
              config
              bvar-db
              state))
          env)
        (always-equal (eval-g-base x env)
          (eval-g-base y env))))
    :hints ((just-induct-and-expand (g-always-equal-core x
         y
         hyp
         clk
         config
         bvar-db
         state)) (and stable-under-simplificationp
        '(:expand ((g-always-equal-core x
             y
             hyp
             clk
             config
             bvar-db
             state) (g-always-equal-core x
              x
              hyp
              clk
              config
              bvar-db
              state)
            (g-always-equal-core x
              y
              hyp
              clk
              config
              bvar-db
              state)
            (g-always-equal-core x
              x
              hyp
              clk
              config
              bvar-db
              state)
            (eval-g-base-list nil env))
          :do-not-induct t))
      (use-termhint (termhint-seq (if (equal (tag x) :g-ite)
            ''(:cases ((eval-g-base (g-ite->test x) env)))
            ''(:no-op t))
          (and (equal (tag y) :g-ite)
            ''(:cases ((eval-g-base (g-ite->test y) env)))))))))

(in-theory (disable g-always-equal-core))