accumulate-nodes-vars

Included Books

other

(in-package "ACL2")

include-book

(include-book "aig-vars-ext")

include-book

(include-book "aig-vars")

include-book

(include-book "centaur/misc/alist-equiv" :dir :system)

local

(local (in-theory (disable double-containment)))

collect-nodesfunction

(defun collect-nodes
  (a)
  (b* (((when (aig-atom-p a)) (if (booleanp a)
         nil
         (list a))) ((when (eq (cdr a) nil)) (collect-nodes (car a))))
    (cons a
      (append (collect-nodes (car a)) (collect-nodes (cdr a))))))

accumulate-nodes-postfunction

(defun accumulate-nodes-post
  (a lst)
  (b* (((when (aig-atom-p a)) (if (or (booleanp a) (member a lst))
         lst
         (cons a lst))) ((when (eq (cdr a) nil)) (accumulate-nodes-post (car a) lst))
      ((when (member a lst)) lst)
      (lst (accumulate-nodes-post (car a) lst))
      (lst (accumulate-nodes-post (cdr a) lst)))
    (cons a lst)))

accumulate-nodes-prefunction

(defun accumulate-nodes-pre
  (a lst)
  (b* (((when (aig-atom-p a)) (if (or (booleanp a) (member a lst))
         lst
         (cons a lst))) ((when (eq (cdr a) nil)) (accumulate-nodes-pre (car a) lst))
      ((when (member a lst)) lst)
      (lst (cons a lst))
      (lst (accumulate-nodes-pre (car a) lst)))
    (accumulate-nodes-pre (cdr a) lst)))

subnode-lst-completefunction

(defun-sk subnode-lst-complete
  (lst)
  (forall (x y)
    (implies (and (member x lst) (member y (collect-nodes x)))
      (member y lst))))

subnode-lst-complete-rewritetheorem

(defthm subnode-lst-complete-rewrite
  (implies (and (subnode-lst-complete lst)
      (member x lst)
      (not (member y lst)))
    (not (member y (collect-nodes x))))
  :hints (("goal" :use subnode-lst-complete-necc)))

in-theory

(in-theory (disable subnode-lst-complete-necc))

subnode-is-transitivetheorem

(defthm subnode-is-transitive
  (implies (and (member x (collect-nodes y))
      (member y (collect-nodes z)))
    (member x (collect-nodes z)))
  :hints (("goal" :induct (collect-nodes z)))
  :rule-classes ((:rewrite :match-free :all)))

subnode-lst-complete-of-collect-nodestheorem

(defthm subnode-lst-complete-of-collect-nodes
  (subnode-lst-complete (collect-nodes a)))

in-theory

(in-theory (disable subnode-lst-complete))

accumulate-nodes-post-member-indmutual-recursion

(mutual-recursion (defun-nx accumulate-nodes-post-member-ind
    (a lst x)
    (declare (ignorable x)
      (xargs :measure (* 2 (acl2-count a))))
    (b* (((when (aig-atom-p a)) lst) ((when (eq (cdr a) nil)) (accumulate-nodes-post-member-ind (car a) lst x))
        ((when (member a lst)) lst)
        (lst2 (accumulate-nodes-post (car a) lst)))
      (list (accumulate-nodes-post-member-ind (car a) lst x)
        (accumulate-nodes-post-member-ind (cdr a) lst2 x)
        (accumulate-nodes-post-complete-ind (car a) lst))))
  (defun-nx accumulate-nodes-post-complete-ind
    (a lst)
    (declare (xargs :measure (+ 1 (* 2 (acl2-count a)))))
    (mv-let (ax ay)
      (subnode-lst-complete-witness (accumulate-nodes-post a lst))
      (list (accumulate-nodes-post-member-ind a lst ax)
        (accumulate-nodes-post-member-ind a lst ay)))))

other

(make-flag accumulate-nodes-post-flg
  accumulate-nodes-post-member-ind)

other

(defthm-accumulate-nodes-post-flg (defthm member-of-accumulate-nodes-post
    (implies (subnode-lst-complete lst)
      (let ((lst2 (accumulate-nodes-post a lst)))
        (iff (member x lst2)
          (or (member x lst) (member x (collect-nodes a))))))
    :flag accumulate-nodes-post-member-ind)
  (defthm accumulate-nodes-post-complete
    (implies (subnode-lst-complete lst)
      (let ((lst2 (accumulate-nodes-post a lst)))
        (subnode-lst-complete lst2)))
    :hints ((and stable-under-simplificationp
       `(:expand (,(CAR (LAST CLAUSE))))))
    :flag accumulate-nodes-post-complete-ind))

subnode-lst-complete-of-emptytheorem

(defthm subnode-lst-complete-of-empty
  (subnode-lst-complete nil)
  :hints (("goal" :in-theory (enable subnode-lst-complete))))

accumulate-nodes-post-under-set-equivtheorem

(defthm accumulate-nodes-post-under-set-equiv
  (implies (subnode-lst-complete lst)
    (set-equiv (accumulate-nodes-post a lst)
      (append (collect-nodes a) lst)))
  :hints ((set-reasoning)))

accumulate-nodes-post-reduces-to-collect-nodestheorem

(defthm accumulate-nodes-post-reduces-to-collect-nodes
  (set-equiv (accumulate-nodes-post a nil) (collect-nodes a)))

in-theory

(in-theory (disable accumulate-nodes-post))

subnode-lst-complete-for-subnodesfunction

(defun-sk subnode-lst-complete-for-subnodes
  (a lst)
  (forall (x y)
    (implies (and (member x (collect-nodes a))
        (member x lst)
        (member y (collect-nodes x)))
      (member y lst))))

subnode-lst-complete-for-subnodes-rewritetheorem

(defthm subnode-lst-complete-for-subnodes-rewrite
  (implies (and (subnode-lst-complete-for-subnodes a lst)
      (member x (collect-nodes a))
      (member x lst)
      (not (member y lst)))
    (not (member y (collect-nodes x))))
  :hints (("goal" :use subnode-lst-complete-for-subnodes-necc)))

in-theory

(in-theory (disable subnode-lst-complete-for-subnodes-necc))

subnode-lst-complete-for-subnodes-of-collect-nodestheorem

(defthm subnode-lst-complete-for-subnodes-of-collect-nodes
  (subnode-lst-complete-for-subnodes b (collect-nodes a)))

in-theory

(in-theory (disable subnode-lst-complete-for-subnodes))

accumulate-nodes-pre-member-indmutual-recursion

(mutual-recursion (defun-nx accumulate-nodes-pre-member-ind
    (a lst x)
    (declare (ignorable x)
      (xargs :measure (* 2 (acl2-count a))))
    (b* (((when (aig-atom-p a)) lst) ((when (eq (cdr a) nil)) (accumulate-nodes-pre-member-ind (car a) lst x))
        ((when (member a lst)) lst)
        (lst2 (cons a lst))
        (lst3 (accumulate-nodes-pre (car a) lst2)))
      (list (accumulate-nodes-pre-member-ind (car a) lst2 x)
        (accumulate-nodes-pre-member-ind (cdr a) lst3 x)
        (accumulate-nodes-pre-complete-ind (car a) (cdr a) lst2))))
  (defun-nx accumulate-nodes-pre-complete-ind
    (a b lst)
    (declare (xargs :measure (+ 1 (* 2 (acl2-count a)))))
    (mv-let (ax ay)
      (subnode-lst-complete-for-subnodes-witness b
        (accumulate-nodes-pre a lst))
      (list (accumulate-nodes-pre-member-ind a lst ax)
        (accumulate-nodes-pre-member-ind a lst ay)))))

other

(make-flag accumulate-nodes-pre-flg
  accumulate-nodes-pre-member-ind)

local

(local (defthmd car-of-aig-atom
    (implies (aig-atom-p x) (equal (car x) nil))
    :hints (("Goal" :in-theory (enable aig-atom-p)))))

subnode-lst-complete-for-subnodes-of-niltheorem

(defthm subnode-lst-complete-for-subnodes-of-nil
  (subnode-lst-complete-for-subnodes nil lst)
  :hints (("Goal" :in-theory (enable subnode-lst-complete-for-subnodes))))

subnode-lst-complete-for-subnodes-of-car-atheorem

(defthm subnode-lst-complete-for-subnodes-of-car-a
  (implies (subnode-lst-complete-for-subnodes a lst)
    (subnode-lst-complete-for-subnodes (car a) lst))
  :hints (("goal" :expand ((subnode-lst-complete-for-subnodes (car a) lst))
     :use ((:instance subnode-lst-complete-for-subnodes-necc
        (x (mv-nth 0
            (subnode-lst-complete-for-subnodes-witness (car a) lst)))
        (y (mv-nth 1
            (subnode-lst-complete-for-subnodes-witness (car a) lst)))))
     :cases ((aig-atom-p a))
     :in-theory (e/d (car-of-aig-atom)
       (subnode-lst-complete-for-subnodes-rewrite)))))

subnode-lst-complete-for-subnodes-of-cdr-atheorem

(defthm subnode-lst-complete-for-subnodes-of-cdr-a
  (implies (and (subnode-lst-complete-for-subnodes a lst)
      (not (aig-atom-p a)))
    (subnode-lst-complete-for-subnodes (cdr a) lst))
  :hints (("goal" :expand ((subnode-lst-complete-for-subnodes (cdr a) lst))
     :use ((:instance subnode-lst-complete-for-subnodes-necc
        (x (mv-nth 0
            (subnode-lst-complete-for-subnodes-witness (cdr a) lst)))
        (y (mv-nth 1
            (subnode-lst-complete-for-subnodes-witness (cdr a) lst)))))
     :cases ((aig-atom-p a))
     :in-theory (disable subnode-lst-complete-for-subnodes-rewrite))))

subnode-lst-complete-for-subnodes-cons-non-subnodetheorem

(defthm subnode-lst-complete-for-subnodes-cons-non-subnode
  (implies (and (subnode-lst-complete-for-subnodes a lst)
      (not (member k (collect-nodes a))))
    (subnode-lst-complete-for-subnodes a (cons k lst)))
  :hints ((and stable-under-simplificationp
     `(:expand (,(CAR (LAST CLAUSE)))))))

subnodes-smaller-or-equaltheorem

(defthm subnodes-smaller-or-equal
  (implies (and (<= (acl2-count x) (acl2-count y)) (not (equal x y)))
    (not (member y (collect-nodes x)))))

a-is-not-a-subnode-of-car-atheorem

(defthm a-is-not-a-subnode-of-car-a
  (not (member a (collect-nodes (car a)))))

a-is-not-a-subnode-of-cdr-atheorem

(defthm a-is-not-a-subnode-of-cdr-a
  (not (member a (collect-nodes (cdr a)))))

in-theory

(in-theory (disable subnodes-smaller-or-equal))

subnode-of-and-node-when-in-lsttheorem

(defthm subnode-of-and-node-when-in-lst
  (implies (and (subnode-lst-complete-for-subnodes a lst)
      (not (aig-atom-p a))
      (cdr a)
      (member a lst)
      (not (member x lst)))
    (not (member x (collect-nodes a))))
  :hints (("goal" :use ((:instance subnode-lst-complete-for-subnodes-necc
        (x a)
        (y x)))
     :in-theory (disable subnode-lst-complete-for-subnodes-rewrite))))

other

(defthm-accumulate-nodes-pre-flg (defthm member-of-accumulate-nodes-pre
    (implies (subnode-lst-complete-for-subnodes a lst)
      (let ((lst2 (accumulate-nodes-pre a lst)))
        (iff (member x lst2)
          (or (member x lst) (member x (collect-nodes a))))))
    :flag accumulate-nodes-pre-member-ind)
  (defthm accumulate-nodes-pre-complete
    (implies (and (subnode-lst-complete-for-subnodes a lst)
        (subnode-lst-complete-for-subnodes b lst))
      (let ((lst2 (accumulate-nodes-pre a lst)))
        (subnode-lst-complete-for-subnodes b lst2)))
    :hints ((and stable-under-simplificationp
       `(:expand (,(CAR (LAST CLAUSE))))))
    :flag accumulate-nodes-pre-complete-ind))

subnode-lst-complete-for-subnodes-of-emptytheorem

(defthm subnode-lst-complete-for-subnodes-of-empty
  (subnode-lst-complete-for-subnodes a nil)
  :hints (("goal" :in-theory (enable subnode-lst-complete-for-subnodes))))

accumulate-nodes-pre-under-set-equivtheorem

(defthm accumulate-nodes-pre-under-set-equiv
  (implies (subnode-lst-complete-for-subnodes a lst)
    (set-equiv (accumulate-nodes-pre a lst)
      (append (collect-nodes a) lst)))
  :hints ((set-reasoning)))

accumulate-nodes-pre-reduces-to-collect-nodestheorem

(defthm accumulate-nodes-pre-reduces-to-collect-nodes
  (set-equiv (accumulate-nodes-pre a nil) (collect-nodes a)))

in-theory

(in-theory (disable accumulate-nodes-pre))

accumulate-aig-vars-nodetable-is-accumulate-nodes-pretheorem

(defthm accumulate-aig-vars-nodetable-is-accumulate-nodes-pre
  (equal (alist-keys (mv-nth 0 (accumulate-aig-vars a nodetable acc)))
    (accumulate-nodes-pre a (alist-keys nodetable)))
  :hints (("Goal" :in-theory (enable accumulate-nodes-pre accumulate-aig-vars))))

lookup-in-nodetable-is-subnodetheorem

(defthm lookup-in-nodetable-is-subnode
  (implies (subnode-lst-complete-for-subnodes a (alist-keys nodetable))
    (iff (hons-assoc-equal x
        (mv-nth 0 (accumulate-aig-vars a nodetable acc)))
      (or (member x (collect-nodes a))
        (hons-assoc-equal x nodetable))))
  :hints (("goal" :use accumulate-aig-vars-nodetable-is-accumulate-nodes-pre
     :in-theory (e/d (hons-assoc-equal-iff-member-alist-keys)
       (alist-keys-member-hons-assoc-equal accumulate-aig-vars-nodetable-is-accumulate-nodes-pre)))))

var-lst-complete-for-subnodesfunction

(defun-sk var-lst-complete-for-subnodes
  (a nodes vars)
  (forall (v n)
    (implies (and (member n (collect-nodes a))
        (member n nodes)
        (member v (aig-vars n)))
      (member v vars))))

in-theory

(in-theory (disable var-lst-complete-for-subnodes
    var-lst-complete-for-subnodes-necc))

var-lst-complete-for-subnodes-rwtheorem

(defthm var-lst-complete-for-subnodes-rw
  (implies (and (var-lst-complete-for-subnodes a nodes vars)
      (member n (collect-nodes a))
      (member n nodes)
      (not (member v vars)))
    (not (member v (aig-vars n))))
  :hints (("goal" :use var-lst-complete-for-subnodes-necc))
  :rule-classes ((:rewrite :match-free :all)))

other

(defcong set-equiv
  equal
  (var-lst-complete-for-subnodes a nodes vars)
  2
  :hints (("goal" :cases ((var-lst-complete-for-subnodes a nodes vars))) (and stable-under-simplificationp
      (append (if (eq (caar clause) 'not)
          `(:expand (,(CAR (LAST CLAUSE))))
          `(:expand (,(CAR CLAUSE))))))))

other

(defcong set-equiv
  equal
  (var-lst-complete-for-subnodes a nodes vars)
  3
  :hints (("goal" :cases ((var-lst-complete-for-subnodes a nodes vars))) (and stable-under-simplificationp
      (append (if (eq (caar clause) 'not)
          `(:expand (,(CAR (LAST CLAUSE))))
          `(:expand (,(CAR CLAUSE))))))))

in-theory

(in-theory (disable var-lst-complete-for-subnodes-rw))

var-lst-complete-for-subnodes-of-niltheorem

(defthm var-lst-complete-for-subnodes-of-nil
  (var-lst-complete-for-subnodes nil nodes vars)
  :hints (("Goal" :in-theory (enable var-lst-complete-for-subnodes))))

var-lst-complete-for-subnodes-of-car-atheorem

(defthm var-lst-complete-for-subnodes-of-car-a
  (implies (var-lst-complete-for-subnodes a nodes vars)
    (var-lst-complete-for-subnodes (car a) nodes vars))
  :hints (("goal" :expand ((var-lst-complete-for-subnodes (car a) nodes vars))
     :use ((:instance var-lst-complete-for-subnodes-necc
        (v (mv-nth 0
            (var-lst-complete-for-subnodes-witness (car a) nodes vars)))
        (n (mv-nth 1
            (var-lst-complete-for-subnodes-witness (car a) nodes vars)))))
     :cases ((aig-atom-p a))
     :in-theory (enable car-of-aig-atom))))

var-lst-complete-for-subnodes-of-cdr-atheorem

(defthm var-lst-complete-for-subnodes-of-cdr-a
  (implies (and (var-lst-complete-for-subnodes a nodes vars)
      (not (aig-atom-p a)))
    (var-lst-complete-for-subnodes (cdr a) nodes vars))
  :hints (("goal" :expand ((var-lst-complete-for-subnodes (cdr a) nodes vars))
     :use ((:instance var-lst-complete-for-subnodes-necc
        (v (mv-nth 0
            (var-lst-complete-for-subnodes-witness (cdr a) nodes vars)))
        (n (mv-nth 1
            (var-lst-complete-for-subnodes-witness (cdr a) nodes vars))))))))

var-lst-complete-for-subnodes-cons-non-subnodetheorem

(defthm var-lst-complete-for-subnodes-cons-non-subnode
  (implies (and (var-lst-complete-for-subnodes a nodes vars)
      (not (member k (collect-nodes a))))
    (var-lst-complete-for-subnodes a (cons k nodes) vars))
  :hints ((and stable-under-simplificationp
     `(:expand (,(CAR (LAST CLAUSE)))
       :use ((:instance var-lst-complete-for-subnodes-necc
          (v (mv-nth 0
              (var-lst-complete-for-subnodes-witness a
                (cons k nodes)
                vars)))
          (n (mv-nth 1
              (var-lst-complete-for-subnodes-witness a
                (cons k nodes)
                vars)))))
       :do-not-induct t))))

var-lst-complete-for-vartheorem

(defthm var-lst-complete-for-var
  (implies (and (var-lst-complete-for-subnodes a nodes vars)
      (aig-var-p a)
      (member a nodes))
    (member a vars))
  :hints (("goal" :use ((:instance var-lst-complete-for-subnodes-necc (n a) (v a)))))
  :rule-classes ((:rewrite :match-free :all)))

var-lst-complete-for-andtheorem

(defthm var-lst-complete-for-and
  (implies (and (var-lst-complete-for-subnodes a nodes vars)
      (not (aig-atom-p a))
      (cdr a)
      (member a nodes)
      (not (member v vars)))
    (not (member v (aig-vars a))))
  :hints (("goal" :use ((:instance var-lst-complete-for-subnodes-necc (n a)))))
  :rule-classes ((:rewrite :match-free :all)))

accumulate-aig-vars-member-indmutual-recursion

(mutual-recursion (defun-nx accumulate-aig-vars-member-ind
    (a nodetable vars x)
    (declare (ignorable x)
      (xargs :measure (* 2 (acl2-count a))))
    (b* (((when (aig-atom-p a)) vars) ((when (eq (cdr a) nil)) (accumulate-aig-vars-member-ind (car a) nodetable vars x))
        ((when (hons-get a nodetable)) vars)
        (nodetable1 (hons-acons a t nodetable))
        ((mv nodetable2 vars2) (accumulate-aig-vars (car a) nodetable1 vars)))
      (list (accumulate-aig-vars-member-ind (car a) nodetable1 vars x)
        (accumulate-aig-vars-member-ind (cdr a) nodetable2 vars2 x)
        (accumulate-aig-vars-complete-ind (car a)
          (cdr a)
          nodetable1
          vars))))
  (defun-nx accumulate-aig-vars-complete-ind
    (a b nodetable vars)
    (declare (xargs :measure (+ 1 (* 2 (acl2-count a)))))
    (b* (((mv ?nodetable1 vars1) (accumulate-aig-vars a nodetable vars)) (nodetable-keys (append (alist-keys nodetable) (collect-nodes a)))
        ((mv v ?n) (var-lst-complete-for-subnodes-witness b
            nodetable-keys
            vars1)))
      (accumulate-aig-vars-member-ind a nodetable vars v))))

other

(make-flag accumulate-aig-vars-flg
  accumulate-aig-vars-member-ind)

in-theory

(in-theory (enable var-lst-complete-for-subnodes-rw))

local

(local (in-theory (e/d (hons-assoc-equal-iff-member-alist-keys)
      (alist-keys-member-hons-assoc-equal))))

variable-of-subnode-transtheorem

(defthm variable-of-subnode-trans
  (implies (and (member v (aig-vars n)) (member n (collect-nodes a)))
    (member v (aig-vars a)))
  :rule-classes ((:rewrite :match-free :all)))

other

(defthm-accumulate-aig-vars-flg (defthm member-of-accumulate-aig-vars
    (implies (and (var-lst-complete-for-subnodes a
          (alist-keys nodetable)
          vars)
        (subnode-lst-complete-for-subnodes a (alist-keys nodetable)))
      (let ((vars2 (mv-nth 1 (accumulate-aig-vars a nodetable vars))))
        (iff (member x vars2)
          (or (member x (aig-vars a)) (member x vars)))))
    :flag accumulate-aig-vars-member-ind)
  (defthm accumulate-aig-vars-preserves-complete
    (implies (and (var-lst-complete-for-subnodes b
          (alist-keys nodetable)
          vars)
        (var-lst-complete-for-subnodes a
          (alist-keys nodetable)
          vars)
        (subnode-lst-complete-for-subnodes a (alist-keys nodetable)))
      (mv-let (nodetable2 vars2)
        (accumulate-aig-vars a nodetable vars)
        (var-lst-complete-for-subnodes b
          (alist-keys nodetable2)
          vars2)))
    :hints ((and stable-under-simplificationp
       `(:expand (,(CAR (LAST CLAUSE))))))
    :flag accumulate-aig-vars-complete-ind))

var-lst-complete-for-subnodes-of-emptytheorem

(defthm var-lst-complete-for-subnodes-of-empty
  (var-lst-complete-for-subnodes a nil vars)
  :hints (("goal" :in-theory (enable var-lst-complete-for-subnodes))))

accumulate-aig-vars-under-set-equivtheorem

(defthm accumulate-aig-vars-under-set-equiv
  (implies (and (var-lst-complete-for-subnodes a
        (alist-keys nodetable)
        vars)
      (subnode-lst-complete-for-subnodes a (alist-keys nodetable)))
    (set-equiv (mv-nth 1 (accumulate-aig-vars a nodetable vars))
      (append (aig-vars a) vars)))
  :hints ((set-reasoning)))

accumulate-aig-vars-reduces-to-aig-varstheorem

(defthm accumulate-aig-vars-reduces-to-aig-vars
  (set-equiv (mv-nth 1 (accumulate-aig-vars a nil nil))
    (aig-vars a)))

in-theory

(in-theory (disable accumulate-aig-vars))

var-lst-completefunction

(defun-sk var-lst-complete
  (nodes vars)
  (forall (v n)
    (implies (and (member n nodes) (member v (aig-vars n)))
      (member v vars)))
  :rewrite :direct)

in-theory

(in-theory (disable var-lst-complete var-lst-complete-necc))

var-lst-complete-implies-var-lst-complete-for-subnodestheorem

(defthm var-lst-complete-implies-var-lst-complete-for-subnodes
  (implies (var-lst-complete nodes vars)
    (var-lst-complete-for-subnodes a nodes vars))
  :hints (("goal" :expand ((var-lst-complete-for-subnodes a nodes vars))
     :in-theory (enable var-lst-complete-necc))))

var-lst-complete-of-niltheorem

(defthm var-lst-complete-of-nil
  (var-lst-complete nil vars)
  :hints (("Goal" :in-theory (enable var-lst-complete))))

subnode-lst-complete-implies-subnode-lst-complete-for-subnodestheorem

(defthm subnode-lst-complete-implies-subnode-lst-complete-for-subnodes
  (implies (subnode-lst-complete lst)
    (subnode-lst-complete-for-subnodes a lst))
  :hints (("goal" :expand ((subnode-lst-complete-for-subnodes a lst))
     :in-theory (enable subnode-lst-complete-necc))))

accumulate-aig-vars-preserves-var-lst-completetheorem

(defthm accumulate-aig-vars-preserves-var-lst-complete
  (implies (and (var-lst-complete (alist-keys nodetable) vars)
      (subnode-lst-complete (alist-keys nodetable)))
    (b* (((mv & vars) (accumulate-aig-vars a nodetable vars)) (nodes (accumulate-nodes-pre a (alist-keys nodetable))))
      (var-lst-complete nodes vars)))
  :hints (("goal" :do-not-induct t
     :in-theory (disable accumulate-aig-vars)) (and stable-under-simplificationp
      `(:expand (,(CAR (LAST CLAUSE)))
        :in-theory (enable var-lst-complete-necc)))))

accumulate-nodes-pre-preserves-subnode-lst-completetheorem

(defthm accumulate-nodes-pre-preserves-subnode-lst-complete
  (implies (subnode-lst-complete nodetable)
    (b* ((nodetable (accumulate-nodes-pre a nodetable)))
      (subnode-lst-complete nodetable)))
  :hints (("goal" :do-not-induct t
     :in-theory (disable accumulate-nodes-pre)) (and stable-under-simplificationp
      `(:expand (,(CAR (LAST CLAUSE)))
        :in-theory (enable subnode-lst-complete-necc)))))

accumulate-aig-vars-list-preserves-subnode-lst-completetheorem

(defthm accumulate-aig-vars-list-preserves-subnode-lst-complete
  (implies (subnode-lst-complete (alist-keys nodetable))
    (subnode-lst-complete (alist-keys (mv-nth 0 (accumulate-aig-vars-list x nodetable vars)))))
  :hints (("Goal" :in-theory (enable accumulate-aig-vars-list))))

accumulate-aig-vars-list-preserves-var-lst-completetheorem

(defthm accumulate-aig-vars-list-preserves-var-lst-complete
  (implies (and (var-lst-complete (alist-keys nodetable) vars)
      (subnode-lst-complete (alist-keys nodetable)))
    (b* (((mv nodetable vars) (accumulate-aig-vars-list x nodetable vars)))
      (var-lst-complete (alist-keys nodetable) vars)))
  :hints (("Goal" :in-theory (enable accumulate-aig-vars-list))))

setp-of-aiglist-varstheorem

(defthm setp-of-aiglist-vars
  (setp (aiglist-vars x))
  :hints (("Goal" :in-theory (enable aiglist-vars))))

accumulate-aig-vars-list-under-set-equivtheorem

(defthm accumulate-aig-vars-list-under-set-equiv
  (implies (and (var-lst-complete (alist-keys nodetable) vars)
      (subnode-lst-complete (alist-keys nodetable)))
    (b* (((mv ?nodetable vars-out) (accumulate-aig-vars-list x nodetable vars)))
      (set-equiv vars-out (append (aiglist-vars x) vars))))
  :hints (("Goal" :in-theory (enable accumulate-aig-vars-list aiglist-vars))))

accumulate-aig-vars-list-reduces-to-aiglist-varstheorem

(defthm accumulate-aig-vars-list-reduces-to-aiglist-vars
  (b* (((mv ?nodetable vars-out) (accumulate-aig-vars-list x nil nil)))
    (set-equiv vars-out (aiglist-vars x))))

local

(local (defthm accumulate-aig-vars-preserves-vars-subset-of-nodetable-lemma
    (implies (subsetp-equal vars (alist-keys nodetable))
      (b* (((mv & vars) (accumulate-aig-vars a nodetable vars)) (nodes (accumulate-nodes-pre a (alist-keys nodetable))))
        (subsetp-equal vars nodes)))
    :hints (("Goal" :in-theory (enable accumulate-aig-vars)
       :induct (accumulate-aig-vars a nodetable vars)
       :expand ((accumulate-aig-vars a nodetable vars) (accumulate-nodes-pre a (alist-keys nodetable)))) (set-reasoning))))

accumulate-aig-vars-preserves-vars-subset-of-nodetabletheorem

(defthm accumulate-aig-vars-preserves-vars-subset-of-nodetable
  (implies (and (subsetp-equal vars (alist-keys nodetable))
      (equal keys (alist-keys nodetable)))
    (b* (((mv & vars) (accumulate-aig-vars a nodetable vars)) (nodes (accumulate-nodes-pre a keys)))
      (subsetp-equal vars nodes))))

accumulate-aig-vars-duplicate-freetheorem

(defthm accumulate-aig-vars-duplicate-free
  (implies (and (no-duplicatesp vars)
      (subsetp-equal vars (alist-keys nodetable)))
    (b* (((mv ?nodetable vars) (accumulate-aig-vars a nodetable vars)))
      (no-duplicatesp vars)))
  :hints (("Goal" :in-theory (enable accumulate-aig-vars) :induct t)))

accumulate-aig-vars-list-preserves-vars-subset-of-nodetabletheorem

(defthm accumulate-aig-vars-list-preserves-vars-subset-of-nodetable
  (implies (subsetp-equal vars (alist-keys nodetable))
    (b* (((mv nodetable vars) (accumulate-aig-vars-list a nodetable vars)))
      (subsetp-equal vars (alist-keys nodetable))))
  :hints (("Goal" :in-theory (enable accumulate-aig-vars-list)
     :induct t)))

accumulate-aig-vars-list-duplicate-freetheorem

(defthm accumulate-aig-vars-list-duplicate-free
  (implies (and (no-duplicatesp vars)
      (subsetp-equal vars (alist-keys nodetable)))
    (b* (((mv ?nodetable vars) (accumulate-aig-vars-list a nodetable vars)))
      (no-duplicatesp vars)))
  :hints (("Goal" :in-theory (enable accumulate-aig-vars-list)
     :induct t)))