aig-vars

(in-package "ACL2")

(define aiglist-vars
  (x)
  (if (atom x)
    nil
    (union (aig-vars (car x)) (aiglist-vars (cdr x)))))

(defsection aig-vars-thms
  :parents (aig-vars)
  :short "Theorems about @(see aig-vars) from @('centaur/aig/aig-vars')."
  (defthm aig-vars-cons
    (implies (or x (not y))
      (equal (aig-vars (cons x y))
        (union (aig-vars x) (aig-vars y)))))
  (defthm member-aig-vars-alist-vals
    (implies (not (in v (aiglist-vars (alist-vals al))))
      (not (in v (aig-vars (cdr (hons-assoc-equal x al))))))
    :hints (("Goal" :in-theory (enable hons-assoc-equal aiglist-vars))))
  (defthm aig-vars-aig-not
    (equal (aig-vars (aig-not x)) (aig-vars x))
    :hints (("Goal" :in-theory (enable aig-not))))
  (local (defthm l1
      (b* (((mv ?hit ans) (aig-and-pass1 x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars ans))))))
      :hints (("Goal" :in-theory (enable aig-and-pass1)))))
  (local (defthm l2a
      (b* (((mv ?status arg1 arg2) (aig-and-pass2a x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass2a)))))
  (local (defthm l2
      (b* (((mv ?status arg1 arg2) (aig-and-pass2 x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass2)))))
  (local (defthm l3
      (b* (((mv ?status arg1 arg2) (aig-and-pass3 x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass3)))))
  (local (defthm l4a
      (b* (((mv ?status arg1 arg2) (aig-and-pass4a x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass4a)))))
  (local (defthm l4
      (b* (((mv ?status arg1 arg2) (aig-and-pass4 x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass4)))))
  (local (defthm l5
      (b* (((mv ?status arg1 arg2) (aig-and-pass5 x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass5)))))
  (local (defthm l6a
      (b* (((mv ?status arg1 arg2) (aig-and-pass6a x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass6a)))))
  (local (defthm l6
      (b* (((mv ?status arg1 arg2) (aig-and-pass6 x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-pass6)))))
  (local (defthm member-aig-vars-aig-and-main
      (b* (((mv ?status arg1 arg2) (aig-and-main x y)))
        (implies (and (not (in v (aig-vars x)))
            (not (in v (aig-vars y))))
          (and (not (in v (aig-vars arg1)))
            (not (in v (aig-vars arg2))))))
      :hints (("Goal" :in-theory (enable aig-and-main)))))
  (local (in-theory (enable aig-atom-p-of-cons-strong)))
  (defthm member-aig-vars-aig-and
    (implies (and (not (in v (aig-vars x)))
        (not (in v (aig-vars y))))
      (not (in v (aig-vars (aig-and x y)))))
    :hints (("Goal" :in-theory (enable aig-and))))
  (defthm member-aig-vars-aig-and-dumb
    (implies (and (not (in v (aig-vars x)))
        (not (in v (aig-vars y))))
      (not (in v (aig-vars (aig-and-dumb x y)))))
    :hints (("Goal" :in-theory (enable aig-and-dumb))))
  (defthm member-aig-vars-aig-restrict
    (implies (and (not (and (in v (aig-vars x))
            (not (member-equal v (alist-keys al)))))
        (not (in v (aiglist-vars (alist-vals al)))))
      (not (in v (aig-vars (aig-restrict x al)))))
    :hints (("Goal" :in-theory (enable aig-restrict))))
  (defthm member-aig-vars-aig-partial-eval
    (implies (not (and (in v (aig-vars x))
          (not (member-equal v (alist-keys al)))))
      (not (in v (aig-vars (aig-partial-eval x al)))))
    :hints (("Goal" :in-theory (enable aig-partial-eval)))))