from-hons-aig

(in-package "AIGNET")

(include-book "construction")

(include-book "misc/hons-help" :dir :system)

(include-book "centaur/aig/aig-vars-fast" :dir :system)

(include-book "centaur/aig/aig-base" :dir :system)

(include-book "centaur/aig/aig-vars" :dir :system)

(include-book "std/lists/index-of" :dir :system)

(local (include-book "arithmetic/top-with-meta" :dir :system))

(local (include-book "std/lists/nthcdr" :dir :system))

(local (include-book "std/lists/resize-list" :dir :system))

(local (include-book "std/lists/take" :dir :system))

(local (include-book "std/lists/nth" :dir :system))

(local (include-book "std/lists/update-nth" :dir :system))

(local (include-book "centaur/aig/accumulate-nodes-vars" :dir :system))

(local (in-theory (disable nth
      update-nth
      nfix-when-not-natp
      resize-list
      nthcdr-of-cdr
      nth-when-zp
      double-containment
      sets-are-true-lists
      make-list-ac)))

(local (in-theory (disable true-listp-update-nth
      aig-env-lookup)))

(define env-to-bitarr
  (vars env)
  (if (atom vars)
    nil
    (cons (if (aig-env-lookup (car vars) env)
        1
        0)
      (env-to-bitarr (cdr vars) env)))
  ///
  (defthm nth-in-env-to-bitarr
    (implies (< (nfix n) (len vars))
      (equal (nth n
          (env-to-bitarr vars env))
        (if (aig-env-lookup (nth n vars) env)
          1
          0)))
    :hints (("Goal" :in-theory (enable nth env-to-bitarr)))))

(define env-update-bitarr-aux
  ((n natp) vars
    env
    bitarr)
  :guard (<= (+ (nfix n) (len vars))
    (bits-length bitarr))
  :returns (new-bitarr)
  (if (atom vars)
    bitarr
    (b* ((bitarr (set-bit n
           (bool->bit (aig-env-lookup (car vars) env))
           bitarr)))
      (env-update-bitarr-aux (1+ (lnfix n))
        (cdr vars)
        env
        bitarr)))
  ///
  (local (defthm take-n-plus-one
      (equal (take (+ 1 (nfix n)) x)
        (append (take n x)
          (list (nth n x))))
      :hints (("Goal" :in-theory (e/d (nth repeat)
           (take-of-too-many take-of-1 take-of-zero))))))
  (local (defthm take-of-update-nth
      (equal (take n
          (update-nth n val x))
        (take n x))
      :hints (("Goal" :in-theory (enable update-nth)))))
  (local (defthm nthcdr-of-update-nth
      (equal (nthcdr n
          (update-nth m v x))
        (if (<= (nfix n) (nfix m))
          (update-nth (- (nfix m) (nfix n))
            v
            (nthcdr n x))
          (nthcdr n x)))
      :hints (("Goal" :in-theory (enable update-nth)))))
  (defret env-update-bitarr-aux-elim
    (implies (<= (+ (nfix n) (len vars))
        (len bitarr))
      (equal new-bitarr
        (append (take n bitarr)
          (env-to-bitarr vars env)
          (nthcdr (+ (nfix n) (len vars))
            bitarr))))
    :hints (("Goal" :in-theory (e/d (env-to-bitarr)
         (take nthcdr (force)))))))

(local (defthm nthcdr-of-length
    (implies (and (true-listp x)
        (<= (len x) (nfix n)))
      (equal (nthcdr n x) nil))))

(define env-update-bitarr
  (vars env bitarr)
  :enabled t
  (mbe :logic (non-exec (env-to-bitarr vars env))
    :exec (b* ((bitarr (resize-bits (len vars)
           bitarr)))
      (env-update-bitarr-aux 0
        vars
        env
        bitarr))))

(local (defthm hons-assoc-equal-in-pairlis
    (equal (hons-assoc-equal v
        (pairlis$ vars vals))
      (and (member v vars)
        (cons v
          (nth (index-of v vars) vals))))
    :hints (("Goal" :in-theory (enable pairlis$ index-of nth)))))

(define bits-to-bools-aux
  ((i natp) bitarr)
  :guard (<= i (bits-length bitarr))
  :measure (nfix (- (bits-length bitarr)
      (nfix i)))
  (b* (((when (mbe :logic (zp (- (bits-length bitarr)
              (nfix i)))
          :exec (eql (bits-length bitarr) i))) nil))
    (cons (equal (get-bit i bitarr) 1)
      (bits-to-bools-aux (1+ (lnfix i))
        bitarr))))

(define bits-to-bools
  (bitarr)
  :verify-guards nil
  (mbe :logic (non-exec (let ((x bitarr))
        (if (atom x)
          nil
          (cons (if (eql (bfix (car x)) 1)
              t
              nil)
            (bits-to-bools (cdr x))))))
    :exec (bits-to-bools-aux 0 bitarr))
  ///
  (defthm nth-of-bits-to-bools
    (equal (nth n (bits-to-bools x))
      (equal (nth n x) 1))
    :hints (("Goal" :in-theory (enable nth))))
  (local (defthm bits-to-bools-aux-is-bits-to-bools
      (equal (bits-to-bools-aux i bitarr)
        (bits-to-bools (nthcdr i bitarr)))
      :hints (("Goal" :in-theory (e/d (bits-to-bools-aux nthcdr nthcdr-of-cdr))
         :induct t
         :expand (bits-to-bools (nthcdr i bitarr))))))
  (verify-guards bits-to-bools
    :hints (("Goal" :in-theory (disable (bits-to-bools))))))

(define aignet-bitarr-to-aig-env
  ((vars true-listp) bitarr)
  :returns (env)
  (pairlis$ vars
    (bits-to-bools bitarr))
  ///
  (defret hons-assoc-equal-in-aignet-bitarr-to-aig-env
    (equal (hons-assoc-equal v env)
      (and (member v vars)
        (cons v
          (equal 1
            (nth (index-of v vars) bitarr))))))
  (defret aig-env-lookup-in-aignet-bitarr-to-aig-env
    (equal (aig-env-lookup v env)
      (or (not (member v vars))
        (equal 1
          (nth (index-of v vars) bitarr))))
    :hints (("Goal" :in-theory (enable aig-env-lookup)))))

(define frame-to-bools-aux
  ((n natp) (i natp)
    frames)
  :guard (and (< n (frames-nrows frames))
    (<= i (frames-ncols frames)))
  :measure (nfix (- (len (nth n (2darr->rows frames)))
      (nfix i)))
  (b* (((when (mbe :logic (non-exec (zp (- (len (nth n (2darr->rows frames)))
                (nfix i))))
          :exec (eql (frames-ncols frames) i))) nil))
    (cons (equal (frames-get2 n i frames)
        1)
      (frame-to-bools-aux n
        (1+ (lnfix i))
        frames))))

(define frame-to-bools
  ((n natp) frames)
  :verify-guards nil
  :guard (< n (frames-nrows frames))
  :enabled t
  (mbe :logic (non-exec (bits-to-bools (nth n (2darr->rows frames))))
    :exec (frame-to-bools-aux n 0 frames))
  ///
  (local (defthm frame-to-bools-aux-is-frame-to-bools
      (equal (frame-to-bools-aux n
          i
          frames)
        (bits-to-bools (nthcdr i
            (nth n (2darr->rows frames)))))
      :hints (("Goal" :in-theory (enable frame-to-bools-aux
           nthcdr
           nthcdr-of-cdr)
         :induct t
         :expand ((bits-to-bools (nthcdr i
              (nth n (2darr->rows frames)))))))))
  (verify-guards frame-to-bools
    :hints (("Goal" :in-theory (disable (frame-to-bools))))))

(define aignet-frames-to-aig-envs-aux
  ((n natp) frames
    (invars true-listp))
  :guard (and (<= n (frames-nrows frames))
    (equal (len invars)
      (frames-ncols frames)))
  :measure (nfix (- (frames-nrows frames)
      (nfix n)))
  (b* (((when (mbe :logic (zp (- (frames-nrows frames)
              (nfix n)))
          :exec (eql (frames-nrows frames) n))) nil))
    (cons (pairlis$ invars
        (frame-to-bools n frames))
      (aignet-frames-to-aig-envs-aux (1+ (lnfix n))
        frames
        invars))))

(define aignet-frame-array-to-aig-envs
  (frame-arr (invars true-listp))
  :non-executable t
  :verify-guards nil
  :returns (envs)
  (if (atom frame-arr)
    nil
    (cons (aignet-bitarr-to-aig-env invars
        (car frame-arr))
      (aignet-frame-array-to-aig-envs (cdr frame-arr)
        invars)))
  ///
  (defthm lookup-in-aignet-frame-array-to-aig-envs
    (implies (< (nfix n) (len frame-arr))
      (equal (nth n
          (aignet-frame-array-to-aig-envs frame-arr
            invars))
        (aignet-bitarr-to-aig-env invars
          (nth n frame-arr))))
    :hints (("Goal" :in-theory (enable nth))))
  (defret len-of-aignet-frame-array-to-aig-envs
    (equal (len envs)
      (len frame-arr)))
  (defthm aignet-frames-to-aig-envs-aux-in-terms-of-aignet-frame-array-to-aig-envs
    (equal (aignet-frames-to-aig-envs-aux n
        frames
        invars)
      (aignet-frame-array-to-aig-envs (nthcdr n (2darr->rows frames))
        invars))
    :hints (("Goal" :in-theory (enable aignet-frames-to-aig-envs-aux
         aignet-bitarr-to-aig-env)
       :induct t
       :expand ((aignet-frame-array-to-aig-envs (nthcdr n (2darr->rows frames))
          invars))))))

(define aignet-frames-to-aig-envs
  (frames (invars true-listp))
  :returns (envs)
  :guard (equal (len invars)
    (frames-ncols frames))
  :enabled t
  (mbe :logic (non-exec (aignet-frame-array-to-aig-envs (2darr->rows frames)
        invars))
    :exec (aignet-frames-to-aig-envs-aux 0
      frames
      invars))
  ///
  (verify-guards aignet-frames-to-aig-envs))

(defsection xmemo-well-formedp
  (defun xmemo-well-formedp
    (xmemo aignet)
    (declare (xargs :stobjs aignet))
    (b* (((when (atom xmemo)) t) ((when (atom (car xmemo))) (xmemo-well-formedp (cdr xmemo)
            aignet))
        (val (cdar xmemo)))
      (and (litp val)
        (fanin-litp val aignet)
        (xmemo-well-formedp (cdr xmemo)
          aignet))))
  (defthm xmemo-well-formedp-lookup
    (let ((look (hons-assoc-equal aig xmemo)))
      (implies (and look
          (xmemo-well-formedp xmemo aignet))
        (and (aignet-litp (cdr look) aignet)
          (litp (cdr look)))))
    :hints (("Goal" :in-theory (enable hons-assoc-equal))))
  (defthm xmemo-well-formedp-of-extension
    (implies (and (aignet-extension-binding)
        (xmemo-well-formedp xmemo orig))
      (xmemo-well-formedp xmemo new))))

(defsection good-varmap-p
  (defund good-varmap-p
    (varmap aignet)
    (declare (xargs :stobjs aignet))
    (if (atom varmap)
      t
      (and (or (atom (car varmap))
          (and (aig-var-p (caar varmap))
            (litp (cdar varmap))
            (fanin-litp (cdar varmap) aignet)))
        (good-varmap-p (cdr varmap) aignet))))
  (local (in-theory (enable good-varmap-p)))
  (deffixequiv good-varmap-p
    :args ((aignet aignet)))
  (defthm lookup-when-good-varmap-p
    (implies (and (good-varmap-p varmap aignet)
        (hons-assoc-equal var varmap))
      (and (aignet-litp (cdr (hons-assoc-equal var varmap))
          aignet)
        (litp (cdr (hons-assoc-equal var varmap)))))
    :hints (("Goal" :in-theory (enable hons-assoc-equal))))
  (defthm good-varmap-p-of-extension
    (implies (and (aignet-extension-binding)
        (good-varmap-p varmap orig))
      (good-varmap-p varmap new))))

(define aig-to-aignet
  ((x "hons aig") (xmemo "memo table (fast alist)")
    (varmap "input variable mapping")
    (gatesimp gatesimp-p)
    strash
    aignet)
  :returns (mv (lit litp
      :rule-classes (:rewrite :type-prescription))
    xmemo
    strash
    aignet)
  :guard (and (good-varmap-p varmap aignet)
    (xmemo-well-formedp xmemo aignet))
  :verify-guards nil
  (aig-cases x
    :true (mv 1 xmemo strash aignet)
    :false (mv 0 xmemo strash aignet)
    :var (b* ((look (hons-get x varmap)))
      (mv (if look
          (lit-fix (cdr look))
          1)
        xmemo
        strash
        aignet))
    :inv (b* (((mv lit
          xmemo
          strash
          aignet) (aig-to-aignet (car x)
           xmemo
           varmap
           gatesimp
           strash
           aignet)))
      (mv (lit-negate lit)
        xmemo
        strash
        aignet))
    :and (b* ((look (hons-get x xmemo)) ((when look) (mv (lit-fix (cdr look))
            xmemo
            strash
            aignet))
        ((mv lit1
           xmemo
           strash
           aignet) (aig-to-aignet (car x)
            xmemo
            varmap
            gatesimp
            strash
            aignet))
        ((when (int= (lit-fix lit1) 0)) (mv 0
            (hons-acons x 0 xmemo)
            strash
            aignet))
        ((mv lit2
           xmemo
           strash
           aignet) (aig-to-aignet (cdr x)
            xmemo
            varmap
            gatesimp
            strash
            aignet))
        ((mv lit strash aignet) (aignet-hash-and lit1
            lit2
            gatesimp
            strash
            aignet))
        (xmemo (hons-acons x lit xmemo)))
      (mv lit
        xmemo
        strash
        aignet)))
  ///
  (def-aignet-preservation-thms aig-to-aignet)
  (defthm aig-to-aignet-well-formed
    (implies (and (good-varmap-p varmap
          (double-rewrite aignet))
        (xmemo-well-formedp xmemo
          (double-rewrite aignet)))
      (b* (((mv lit
            xmemo
            ?strash
            aignet) (aig-to-aignet x
             xmemo
             varmap
             gatesimp
             strash
             aignet)))
        (and (aignet-litp lit aignet)
          (xmemo-well-formedp xmemo aignet))))
    :hints (("goal" :induct (aig-to-aignet x
         xmemo
         varmap
         gatesimp
         strash
         aignet)
       :expand ((aig-to-aignet x
          xmemo
          varmap
          gatesimp
          strash
          aignet) (aig-to-aignet nil
           xmemo
           varmap
           gatesimp
           strash
           aignet)
         (aig-to-aignet t
           xmemo
           varmap
           gatesimp
           strash
           aignet))
       :in-theory (e/d nil ((:definition aig-to-aignet))))))
  (verify-guards aig-to-aignet)
  (defthm stype-count-of-aig-to-aignet
    (implies (and (not (equal (stype-fix stype)
            (and-stype)))
        (not (equal (stype-fix stype)
            (xor-stype))))
      (equal (stype-count stype
          (mv-nth 3
            (aig-to-aignet x
              xmemo
              varmap
              gatesimp
              strash
              aignet)))
        (stype-count stype aignet)))
    :hints ((just-induct-and-expand (aig-to-aignet x
         xmemo
         varmap
         gatesimp
         strash
         aignet)))))

(defsection xmemo-ok
  (local (in-theory (disable id-eval)))
  (defun-nx aignet-eval-to-env
    (varmap in-vals
      reg-vals
      aignet)
    (b* (((when (atom varmap)) nil) ((when (atom (car varmap))) (aignet-eval-to-env (cdr varmap)
            in-vals
            reg-vals
            aignet))
        ((cons aig-var lit) (car varmap))
        (val (= 1
            (lit-eval lit
              in-vals
              reg-vals
              aignet))))
      (cons (cons aig-var val)
        (aignet-eval-to-env (cdr varmap)
          in-vals
          reg-vals
          aignet))))
  (defthm aignet-eval-to-env-of-extension
    (implies (and (aignet-extension-binding)
        (good-varmap-p varmap orig))
      (equal (aignet-eval-to-env varmap
          invals
          regvals
          new)
        (aignet-eval-to-env varmap
          invals
          regvals
          orig)))
    :hints (("Goal" :in-theory (enable good-varmap-p))))
  (defthm present-in-aignet-eval-to-env
    (iff (hons-assoc-equal x
        (aignet-eval-to-env varmap
          in-vals
          reg-vals
          aignet))
      (hons-assoc-equal x varmap)))
  (defthm not-present-in-aignet-eval-to-env
    (implies (not (hons-assoc-equal x varmap))
      (not (hons-assoc-equal x
          (aignet-eval-to-env varmap
            in-vals
            reg-vals
            aignet)))))
  (defthm lookup-in-aignet-eval-to-env
    (implies (hons-assoc-equal x varmap)
      (equal (cdr (hons-assoc-equal x
            (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet)))
        (= 1
          (lit-eval (cdr (hons-assoc-equal x varmap))
            in-vals
            reg-vals
            aignet))))
    :hints (("Goal" :induct (aignet-eval-to-env varmap
         in-vals
         reg-vals
         aignet))))
  (defthm aig-env-lookup-of-aignet-eval-to-env
    (implies (hons-assoc-equal v varmap)
      (equal (aig-env-lookup v
          (aignet-eval-to-env varmap
            in-vals
            reg-vals
            aignet))
        (= 1
          (lit-eval (cdr (hons-assoc-equal v varmap))
            in-vals
            reg-vals
            aignet))))
    :hints (("Goal" :in-theory (enable aignet-eval-to-env aig-env-lookup))))
  (defun-nx xmemo-ok
    (xmemo varmap
      in-vals
      reg-vals
      aignet)
    (b* (((when (atom xmemo)) t) ((when (atom (car xmemo))) (xmemo-ok (cdr xmemo)
            varmap
            in-vals
            reg-vals
            aignet))
        ((cons aig lit) (car xmemo))
        (env (aignet-eval-to-env varmap
            in-vals
            reg-vals
            aignet)))
      (and (equal (aig-eval aig env)
          (= 1
            (lit-eval lit
              in-vals
              reg-vals
              aignet)))
        (xmemo-ok (cdr xmemo)
          varmap
          in-vals
          reg-vals
          aignet))))
  (in-theory (disable xmemo-ok))
  (local (in-theory (enable xmemo-ok)))
  (local (defthmd equal-1-to-bitp
      (implies (not (equal x 0))
        (equal (equal x 1) (bitp x)))
      :hints (("Goal" :in-theory (enable bitp)))))
  (defthm xmemo-ok-lookup
    (implies (and (xmemo-ok xmemo
          varmap
          in-vals
          reg-vals
          aignet)
        (hons-assoc-equal aig xmemo))
      (equal (lit-eval (cdr (hons-assoc-equal aig xmemo))
          in-vals
          reg-vals
          aignet)
        (bool->bit (aig-eval aig
            (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet)))))
    :hints (("Goal" :in-theory (enable equal-1-to-bitp))))
  (defthm xmemo-ok-lookup-bind-free
    (implies (and (bind-free '((varmap . varmap)))
        (xmemo-ok xmemo
          varmap
          in-vals
          reg-vals
          aignet)
        (hons-assoc-equal aig xmemo))
      (equal (lit-eval (cdr (hons-assoc-equal aig xmemo))
          in-vals
          reg-vals
          aignet)
        (bool->bit (aig-eval aig
            (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet))))))
  (defthm xmemo-ok-of-acons
    (equal (xmemo-ok (cons (cons aig lit) xmemo)
        varmap
        in-vals
        reg-vals
        aignet)
      (and (xmemo-ok xmemo
          varmap
          in-vals
          reg-vals
          aignet)
        (equal (lit-eval lit
            in-vals
            reg-vals
            aignet)
          (bool->bit (aig-eval aig
              (aignet-eval-to-env varmap
                in-vals
                reg-vals
                aignet))))))
    :hints (("Goal" :in-theory (enable equal-1-to-bitp))))
  (defthm xmemo-ok-of-extension
    (implies (and (aignet-extension-binding)
        (good-varmap-p varmap orig)
        (xmemo-well-formedp xmemo orig))
      (iff (xmemo-ok xmemo
          varmap
          invals
          regvals
          new)
        (xmemo-ok xmemo
          varmap
          invals
          regvals
          orig))))
  (defthm xmemo-ok-of-nil
    (xmemo-ok nil
      varmap
      in-vals
      reg-vals
      aignet)
    :hints (("Goal" :in-theory (enable xmemo-ok)))))

(defsection aig-to-aignet-correct
  (local (in-theory (disable aignet-add-in)))
  (local (defthm id-eval-1
      (implies (not (equal (id-eval n
              in-vals
              reg-vals
              aignet)
            0))
        (equal (id-eval n
            in-vals
            reg-vals
            aignet)
          1))
      :hints (("goal" :use ((:instance (:type-prescription id-eval)))
         :in-theory (e/d (bitp) ((:t id-eval)))))))
  (defthm aig-to-aignet-correct
    (implies (and (good-varmap-p varmap
          (double-rewrite aignet))
        (xmemo-well-formedp xmemo1
          (double-rewrite aignet))
        (xmemo-ok xmemo1
          varmap
          in-vals
          reg-vals
          (double-rewrite aignet)))
      (b* (((mv lit
            xmemo
            ?strash
            aignet1) (aig-to-aignet x
             xmemo1
             varmap
             strash1
             gatesimp
             aignet)))
        (and (xmemo-ok xmemo
            varmap
            in-vals
            reg-vals
            aignet1)
          (equal (lit-eval lit
              in-vals
              reg-vals
              aignet1)
            (bool->bit (aig-eval x
                (aignet-eval-to-env varmap
                  in-vals
                  reg-vals
                  aignet))))
          (equal (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet1)
            (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet)))))
    :hints (("Goal" :in-theory (e/d ((:induction aig-to-aignet) aignet-eval-to-env
           eval-and-of-lits
           aig-env-lookup)
         (aig-eval xmemo-ok
           xmemo-well-formedp
           aignet-eval-to-env
           id-eval
           id-eval-1
           default-car
           default-cdr
           b-xor))
       :induct t
       :do-not-induct t
       :do-not '(generalize fertilize
         eliminate-destructors)
       :expand ((:free (env)
          (aig-eval x env)) (:free (env) (aig-eval nil env))
         (:free (env) (aig-eval t env))
         (aig-to-aignet x
           xmemo1
           varmap
           strash1
           gatesimp
           aignet)
         (aig-to-aignet nil
           xmemo1
           varmap
           strash1
           gatesimp
           aignet)
         (aig-to-aignet t
           xmemo1
           varmap
           strash1
           gatesimp
           aignet))) (and stable-under-simplificationp
        '(:in-theory (e/d (id-eval-1) nil))))
    :otf-flg t))

(defsection aiglist-to-aignet
  (local (in-theory (disable id-eval double-containment)))
  (defund aiglist-to-aignet-aux
    (x xmemo
      varmap
      gatesimp
      strash
      aignet
      lits)
    (declare (xargs :stobjs (aignet strash)
        :guard (and (gatesimp-p gatesimp)
          (good-varmap-p varmap aignet)
          (xmemo-well-formedp xmemo aignet)
          (true-listp lits))
        :verify-guards nil))
    (b* (((when (atom x)) (mv (reverse lits)
           xmemo
           strash
           aignet)) ((mv lit
           xmemo
           strash
           aignet) (aig-to-aignet (car x)
            xmemo
            varmap
            gatesimp
            strash
            aignet)))
      (aiglist-to-aignet-aux (cdr x)
        xmemo
        varmap
        gatesimp
        strash
        aignet
        (cons lit lits))))
  (defund aiglist-to-aignet
    (x xmemo
      varmap
      gatesimp
      strash
      aignet)
    (declare (xargs :stobjs (aignet strash)
        :guard (and (gatesimp-p gatesimp)
          (good-varmap-p varmap aignet)
          (xmemo-well-formedp xmemo aignet))
        :verify-guards nil))
    (mbe :logic (b* (((when (atom x)) (mv nil xmemo strash aignet)) ((mv lit
             xmemo
             strash
             aignet) (aig-to-aignet (car x)
              xmemo
              varmap
              gatesimp
              strash
              aignet))
          ((mv rest
             xmemo
             strash
             aignet) (aiglist-to-aignet (cdr x)
              xmemo
              varmap
              gatesimp
              strash
              aignet)))
        (mv (cons lit rest)
          xmemo
          strash
          aignet))
      :exec (aiglist-to-aignet-aux x
        xmemo
        varmap
        gatesimp
        strash
        aignet
        nil)))
  (local (in-theory (enable aiglist-to-aignet
        aiglist-to-aignet-aux)))
  (defthm aiglist-to-aignet-aux-elim
    (implies (true-listp lits)
      (equal (aiglist-to-aignet-aux x
          xmemo
          varmap
          gatesimp
          strash
          aignet
          lits)
        (mv-let (rest-lits xmemo
            strash
            aignet)
          (aiglist-to-aignet x
            xmemo
            varmap
            gatesimp
            strash
            aignet)
          (mv (revappend lits rest-lits)
            xmemo
            strash
            aignet)))))
  (def-aignet-preservation-thms aiglist-to-aignet)
  (defthm lit-listp-aiglist-to-aignet-lits
    (lit-listp (mv-nth 0
        (aiglist-to-aignet x
          xmemo
          varmap
          gatesimp
          strash
          aignet))))
  (defthm aiglist-to-aignet-well-formed
    (implies (and (good-varmap-p varmap
          (double-rewrite aignet))
        (xmemo-well-formedp xmemo
          (double-rewrite aignet)))
      (b* (((mv lits
            xmemo
            ?strash
            aignet) (aiglist-to-aignet x
             xmemo
             varmap
             gatesimp
             strash
             aignet)))
        (and (aignet-lit-listp lits aignet)
          (xmemo-well-formedp xmemo aignet)))))
  (defthm len-lits-of-aiglist-to-aignet
    (b* (((mv lits
          ?xmemo
          ?strash
          ?aignet) (aiglist-to-aignet x
           xmemo
           varmap
           gatesimp
           strash
           aignet)))
      (equal (len lits) (len x))))
  (defthm aignet-litp-nth-of-aignet-lit-list
    (implies (and (aignet-lit-listp lits aignet)
        (< (nfix n) (len lits)))
      (aignet-litp (nth n lits)
        aignet))
    :hints (("Goal" :in-theory (enable nth))))
  (defthm aignet-litp-nth-of-aiglist-to-aignet
    (implies (and (good-varmap-p varmap
          (double-rewrite aignet))
        (xmemo-well-formedp xmemo
          (double-rewrite aignet))
        (< (nfix n) (len x)))
      (b* (((mv lits
            ?xmemo
            ?strash
            aignet) (aiglist-to-aignet x
             xmemo
             varmap
             gatesimp
             strash
             aignet)))
        (aignet-litp (nth n lits)
          aignet))))
  (defthm aignet-litp-nth-of-aiglist-to-aignet-ext
    (implies (and (good-varmap-p varmap
          (double-rewrite aignet))
        (xmemo-well-formedp xmemo
          (double-rewrite aignet))
        (< (nfix n) (len x)))
      (b* (((mv lits
            ?xmemo
            ?strash
            new-aignet) (aiglist-to-aignet x
             xmemo
             varmap
             gatesimp
             strash
             aignet)))
        (implies (aignet-extension-p aignet-ext
            new-aignet)
          (aignet-litp (nth n lits)
            aignet-ext)))))
  (defun bools->bits
    (x)
    (declare (xargs :guard t))
    (if (atom x)
      nil
      (cons (bool->bit (car x))
        (bools->bits (cdr x)))))
  (defthm aiglist-to-aignet-correct
    (implies (and (good-varmap-p varmap aignet)
        (xmemo-well-formedp xmemo1 aignet)
        (xmemo-ok xmemo1
          varmap
          in-vals
          reg-vals
          aignet))
      (b* (((mv lits
            xmemo
            ?strash
            aignet1) (aiglist-to-aignet x
             xmemo1
             varmap
             strash1
             gatesimp
             aignet)))
        (and (xmemo-ok xmemo
            varmap
            in-vals
            reg-vals
            aignet1)
          (equal (lit-eval-list lits
              in-vals
              reg-vals
              aignet1)
            (bools->bits (aig-eval-list x
                (aignet-eval-to-env varmap
                  in-vals
                  reg-vals
                  aignet))))
          (equal (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet1)
            (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet))))))
  (local (defthm lit-eval-of-nth-in-terms-of-lit-eval-list
      (implies (< (nfix n) (len lst))
        (equal (lit-eval (nth n lst)
            in-vals
            reg-vals
            aignet)
          (nth n
            (lit-eval-list lst
              in-vals
              reg-vals
              aignet))))
      :hints (("Goal" :in-theory (enable nth lit-eval-list)))))
  (defthm nth-of-bools->bits
    (implies (< (nfix n) (len x))
      (equal (nth n (bools->bits x))
        (bool->bit (nth n x))))
    :hints (("Goal" :in-theory (enable nth))))
  (defthm nth-of-aig-eval-list
    (equal (nth n (aig-eval-list x env))
      (aig-eval (nth n x) env))
    :hints (("Goal" :in-theory (enable nth))))
  (defthm aiglist-to-aignet-nth-correct
    (implies (and (good-varmap-p varmap aignet)
        (xmemo-well-formedp xmemo1 aignet)
        (xmemo-ok xmemo1
          varmap
          in-vals
          reg-vals
          aignet)
        (< (nfix n) (len x)))
      (b* (((mv lits
            ?xmemo
            ?strash
            aignet1) (aiglist-to-aignet x
             xmemo1
             varmap
             strash1
             gatesimp
             aignet)))
        (equal (lit-eval (nth n lits)
            in-vals
            reg-vals
            aignet1)
          (bool->bit (aig-eval (nth n x)
              (aignet-eval-to-env varmap
                in-vals
                reg-vals
                aignet)))))))
  (verify-guards aiglist-to-aignet-aux)
  (verify-guards aiglist-to-aignet)
  (defun aiglist-to-aignet-top
    (x varmap
      gatesimp
      strash
      aignet)
    (declare (xargs :stobjs (aignet strash)
        :guard (and (gatesimp-p gatesimp)
          (good-varmap-p varmap aignet))))
    (b* (((mv lits
          xmemo
          strash
          aignet) (aiglist-to-aignet x
           nil
           varmap
           gatesimp
           strash
           aignet)))
      (fast-alist-free xmemo)
      (mv lits strash aignet)))
  (defthm len-aiglist-to-aignet
    (equal (len (mv-nth 0
          (aiglist-to-aignet x
            xmemo
            varmap
            gmemo
            gatesimp
            aignet)))
      (len x))
    :hints (("Goal" :in-theory (enable aiglist-to-aignet))))
  (defthm stype-count-of-aiglist-to-aignet
    (implies (and (not (equal (stype-fix stype)
            (and-stype)))
        (not (equal (stype-fix stype)
            (xor-stype))))
      (equal (stype-count stype
          (mv-nth 3
            (aiglist-to-aignet x
              xmemo
              varmap
              gatesimp
              strash
              aignet)))
        (stype-count stype aignet)))
    :hints (("goal" :in-theory (enable (:i aiglist-to-aignet))
       :induct (aiglist-to-aignet x
         xmemo
         varmap
         gatesimp
         strash
         aignet)
       :expand ((aiglist-to-aignet x
          xmemo
          varmap
          gatesimp
          strash
          aignet))))))

(defsection keys-bound
  (defund keys-bound
    (keys al)
    (declare (xargs :guard t))
    (if (atom keys)
      t
      (and (hons-get (car keys) al)
        (keys-bound (cdr keys) al))))
  (local (in-theory (enable keys-bound accumulate-aig-vars)))
  (defthm keys-bound-of-add-extra
    (implies (keys-bound keys al)
      (keys-bound keys
        (cons x al)))
    :hints (("Goal" :in-theory (enable hons-assoc-equal))))
  (defthm keys-bound-of-add
    (implies (keys-bound keys al)
      (keys-bound (cons x keys)
        (cons (cons x y) al)))
    :hints (("Goal" :in-theory (enable hons-assoc-equal))))
  (defthmd member-when-keys-bound
    (implies (and (keys-bound keys al)
        (not (hons-assoc-equal x al)))
      (not (member x keys))))
  (defthm keys-bound-of-accumulate-aig-vars
    (implies (keys-bound acc nodetable)
      (mv-let (nodetable acc)
        (accumulate-aig-vars x
          nodetable
          acc)
        (keys-bound acc nodetable))))
  (defthm no-duplicatesp-of-accumulate-aig-vars
    (implies (and (no-duplicatesp acc)
        (keys-bound acc nodetable))
      (mv-let (nodetable acc)
        (accumulate-aig-vars x
          nodetable
          acc)
        (declare (ignore nodetable))
        (no-duplicatesp acc)))
    :hints (("Goal" :in-theory (enable member-when-keys-bound)))))

(define fanin-id-range-p
  ((start natp) (n natp)
    aignet)
  :measure (nfix n)
  (if (zp n)
    t
    (and (fanin-litp (mk-lit start 0)
        aignet)
      (fanin-id-range-p (+ 1 (lnfix start))
        (1- n)
        aignet)))
  ///
  (set-define-current-function aignet-add-ins)
  (local (defret fanin-id-range-p-of-aignet-add-ins-lemma
      (fanin-id-range-p (+ 1 (fanin-count aignet))
        n
        new-aignet)
      :hints (("Goal" :in-theory (enable aignet-add-ins)))))
  (defret fanin-id-range-p-of-aignet-add-ins
    (implies (equal id
        (+ 1 (fanin-count aignet)))
      (fanin-id-range-p id
        n
        new-aignet))
    :hints (("Goal" :in-theory (enable aignet-add-ins))))
  (defret aignet-add-ins-preserves-fanin-id-range-p
    (implies (fanin-id-range-p id count aignet)
      (fanin-id-range-p id
        count
        new-aignet))
    :hints (("Goal" :in-theory (enable aignet-add-ins))))
  (set-define-current-function aignet-add-regs)
  (local (defret fanin-id-range-p-of-aignet-add-regs-lemma
      (fanin-id-range-p (+ 1 (fanin-count aignet))
        n
        new-aignet)
      :hints (("Goal" :in-theory (enable aignet-add-regs)))))
  (defret fanin-id-range-p-of-aignet-add-regs
    (implies (equal id
        (+ 1 (fanin-count aignet)))
      (fanin-id-range-p id
        n
        new-aignet))
    :hints (("Goal" :in-theory (enable aignet-add-regs))))
  (defret aignet-add-regs-preserves-fanin-id-range-p
    (implies (fanin-id-range-p id count aignet)
      (fanin-id-range-p id
        count
        new-aignet))
    :hints (("Goal" :in-theory (enable aignet-add-regs)))))

(define consecutive-vars-to-varmap
  ((n natp) vars varmap)
  :returns (new-varmap)
  (b* (((when (atom vars)) varmap) (varmap (hons-acons (car vars)
          (mk-lit n 0)
          varmap)))
    (consecutive-vars-to-varmap (1+ (lnfix n))
      (cdr vars)
      varmap))
  ///
  (defret lookup-in-consecutive-vars-to-varmap-under-iff
    (iff (hons-assoc-equal v new-varmap)
      (or (member v vars)
        (hons-assoc-equal v varmap))))
  (defret lookup-in-consecutive-vars-to-varmap-when-not-var
    (implies (double-rewrite (not (member v vars)))
      (equal (hons-assoc-equal v new-varmap)
        (hons-assoc-equal v varmap))))
  (defret lookup-in-consecutive-vars-to-varmap-when-var
    (implies (and (double-rewrite (member v vars))
        (no-duplicatesp vars))
      (equal (hons-assoc-equal v new-varmap)
        (cons v
          (mk-lit (+ (nfix n)
              (index-of v vars))
            0))))
    :hints (("Goal" :in-theory (enable index-of))))
  (defret good-varmap-p-of-consecutive-vars-to-varmap
    (implies (and (good-varmap-p varmap aignet)
        (aig-var-listp vars)
        (fanin-id-range-p n
          (len vars)
          aignet))
      (good-varmap-p new-varmap aignet))
    :hints (("Goal" :in-theory (enable fanin-id-range-p
         good-varmap-p)))))

(local (defthm member-implies-natp-index-of-strong
    (implies (double-rewrite (member k x))
      (natp (index-of k x)))))

(local (defthm member-implies-index-of-less-strong
    (implies (double-rewrite (member k x))
      (< (index-of k x) (len x)))
    :rule-classes (:rewrite :linear)))

(defsection aig-fsm-prepare-aignet/varmap
  (local (in-theory (enable length)))
  (defthm aiglist-vars-of-append
    (equal (aiglist-vars (append a b))
      (union (aiglist-vars a) (aiglist-vars b)))
    :hints (("Goal" :in-theory (enable aiglist-vars))))
  (local (defthm no-duplicatesp-of-set-diff
      (implies (no-duplicatesp x)
        (no-duplicatesp (set-difference$ x y)))
      :hints (("Goal" :in-theory (enable set-difference$)))))
  (define aig-fsm-prepare-aignet/varmap
    (reg-alist out-list
      max-nodes
      aignet)
    (declare (xargs :stobjs aignet
        :guard (posp max-nodes)
        :guard-debug t))
    :returns (mv varmap
      input-vars
      reg-vars
      new-aignet)
    (b* ((reg-aigs (alist-vals reg-alist)) (all-vars (aig-vars-unordered-list (append reg-aigs out-list)))
        (reg-vars (alist-keys reg-alist))
        (in-vars (hons-set-diff all-vars reg-vars))
        (nregs (len reg-vars))
        (nins (len in-vars))
        (nouts (len out-list))
        (max-nodes (mbe :logic (if (posp max-nodes)
              max-nodes
              1000)
            :exec max-nodes))
        (aignet (aignet-init nouts
            nregs
            nins
            max-nodes
            aignet))
        (aignet (aignet-add-ins nins aignet))
        (aignet (aignet-add-regs nregs aignet))
        (varmap (consecutive-vars-to-varmap 1 in-vars nil))
        (varmap (consecutive-vars-to-varmap (+ 1 nins)
            reg-vars
            varmap)))
      (mv varmap
        in-vars
        reg-vars
        aignet))
    ///
    (local (in-theory (enable aig-fsm-prepare-aignet/varmap)))
    (defthm true-listp-of-aig-fsm-prepare-aignet/varmap-invars
      (true-listp (mv-nth 1
          (aig-fsm-prepare-aignet/varmap reg-alist
            out-list
            max-gates
            aignet)))
      :rule-classes (:rewrite :type-prescription))
    (defthm true-listp-of-aig-fsm-prepare-aignet/varmap-regvars
      (true-listp (mv-nth 2
          (aig-fsm-prepare-aignet/varmap reg-alist
            out-list
            max-gates
            aignet)))
      :rule-classes (:rewrite :type-prescription))
    (defret num-outs-of-aig-fsm-prepare-aignet/varmap
      (equal (stype-count :po new-aignet) 0))
    (defret num-nxsts-of-aig-fsm-prepare-aignet/varmap
      (equal (stype-count :nxst new-aignet) 0))
    (defret num-ins-of-aig-fsm-prepare-aignet/varmap
      (equal (stype-count :pi new-aignet)
        (len input-vars)))
    (defret num-regs-of-aig-fsm-prepare-aignet/varmap
      (equal (stype-count :reg new-aignet)
        (len (alist-keys reg-alist))))
    (defret reg-vars-of-aig-fsm-prepare-aignet/varmap
      (equal reg-vars
        (alist-keys reg-alist)))
    (defret in-vars-of-aig-fsm-prepare-aignet/varmap
      (set-equiv input-vars
        (set-difference$ (aiglist-vars (append (alist-vals reg-alist)
              out-list))
          (alist-keys reg-alist))))
    (defret aig-fsm-prepare-input-varmap-lookup
      (implies (and (member v
            (aiglist-vars (append (alist-vals reg-alist)
                out-list)))
          (not (hons-assoc-equal v reg-alist)))
        (b* ((index (index-of v input-vars)) (input-id (fanin-count (lookup-stype index :pi new-aignet))))
          (equal (hons-assoc-equal v varmap)
            (cons v (mk-lit input-id 0))))))
    (defret aig-fsm-prepare-reg-varmap-lookup
      (implies (and (member v
            (aiglist-vars (append (alist-vals reg-alist)
                out-list)))
          (hons-assoc-equal v reg-alist)
          (no-duplicatesp (alist-keys reg-alist)))
        (b* ((index (index-of v (alist-keys reg-alist))) (reg-id (fanin-count (lookup-stype index :reg new-aignet))))
          (equal (hons-assoc-equal v varmap)
            (cons v (mk-lit reg-id 0))))))
    (defthm aig-var-listp-of-accumulate-aig-vars
      (equal (aig-var-listp (mv-nth 1
            (accumulate-aig-vars x
              nodetable
              acc)))
        (aig-var-listp acc))
      :hints (("Goal" :in-theory (enable accumulate-aig-vars))))
    (defthm aig-var-listp-of-set-difference
      (implies (aig-var-listp x)
        (aig-var-listp (set-difference$ x y)))
      :hints (("Goal" :in-theory (enable set-difference$))))
    (defthm aig-var-listp-of-accumulate-aig-vars-list
      (iff (aig-var-listp (mv-nth 1
            (accumulate-aig-vars-list x
              nodetable
              acc)))
        (aig-var-listp acc))
      :hints (("Goal" :in-theory (enable accumulate-aig-vars-list))))
    (defret good-varmap-p-of-aig-fsm-prepare-aignet/varmap
      (implies (aig-var-listp (alist-keys reg-alist))
        (good-varmap-p varmap new-aignet)))))

(local (defthm lit-listp-of-take
    (implies (and (lit-listp x)
        (<= (nfix n) (len x)))
      (lit-listp (take n x)))))

(local (defthm lit-listp-of-nthcdr
    (implies (lit-listp x)
      (lit-listp (nthcdr n x)))
    :hints (("Goal" :in-theory (enable nthcdr)))))

(local (defthm len-alist-vals
    (equal (len (alist-vals x))
      (len (alist-keys x)))
    :hints (("Goal" :in-theory (enable alist-keys alist-vals)))))

(local (defthm aignet-lit-listp-of-take
    (implies (and (aignet-lit-listp x aignet)
        (<= (nfix n) (len x)))
      (aignet-lit-listp (take n x)
        aignet))
    :hints (("Goal" :in-theory (enable aignet-lit-listp)))))

(local (defthm aignet-lit-listp-of-nthcdr
    (implies (aignet-lit-listp x aignet)
      (aignet-lit-listp (nthcdr n x)
        aignet))
    :hints (("Goal" :in-theory (enable aignet-lit-listp nthcdr)))))

(defthm lit-eval-list-of-take
  (implies (<= (nfix n) (len x))
    (equal (lit-eval-list (take n x)
        in-vals
        reg-vals
        aignet)
      (take n
        (lit-eval-list x
          in-vals
          reg-vals
          aignet))))
  :hints (("Goal" :in-theory (enable nfix))))

(defthm aig-eval-list-of-append
  (equal (aig-eval-list (append a b) env)
    (append (aig-eval-list a env)
      (aig-eval-list b env))))

(local (defthm nthcdr-nil
    (equal (nthcdr n nil) nil)))

(defthm lit-eval-list-of-nthcdr
  (equal (lit-eval-list (nthcdr n x)
      in-vals
      reg-vals
      aignet)
    (nthcdr n
      (lit-eval-list x
        in-vals
        reg-vals
        aignet)))
  :hints (("Goal" :in-theory (enable nthcdr))))

(defthm nthcdr-of-append
  (implies (equal (nfix n) (len a))
    (equal (nthcdr n (append a b))
      b))
  :hints (("Goal" :in-theory (enable nthcdr)
     :induct (nthcdr n a))))

(encapsulate nil
  (local (progn (defthm nthcdr-empty
        (implies (and (true-listp lst)
            (<= (len lst) (nfix n)))
          (equal (nthcdr n lst) nil))))))

(defsection aig-fsm-to-aignet
  (local (in-theory (enable alist-keys aignet-lit-listp)))
  (local (in-theory (enable good-varmap-p)))
  (local (defthm litp-integerp
      (implies (litp lit)
        (and (integerp lit) (<= 0 lit)))))
  (defthm car-nonnil-forward
    (implies (not (equal (car x) nil))
      (consp x))
    :rule-classes ((:forward-chaining :trigger-terms ((car x)))))
  (defthm stype-count-of-cdr-extension
    (implies (and (aignet-extension-bind-inverse)
        (consp orig)
        (equal (stype (car orig))
          (stype-fix stype)))
      (< (stype-count stype (cdr orig))
        (stype-count stype new)))
    :rule-classes ((:linear :trigger-terms ((stype-count stype (cdr orig))))))
  (defsection aignet-add-outs
    (local (in-theory (enable aignet-add-outs)))
    (defthm good-varmap-p-of-aignet-add-outs
      (implies (good-varmap-p varmap aignet)
        (good-varmap-p varmap
          (aignet-add-outs out-lits aignet)))
      :hints (("goal" :induct (aignet-add-outs out-lits aignet)))))
  (define aig-fsm-to-aignet
    (reg-alist out-list
      max-nodes
      gatesimp
      aignet)
    (declare (xargs :stobjs aignet
        :guard (and (posp max-nodes)
          (gatesimp-p gatesimp)
          (aig-var-listp (alist-keys reg-alist)))
        :verify-guards nil))
    :returns (mv (new-aignet)
      (varmap)
      (invars)
      (regvars))
    (b* (((local-stobjs strash) (mv aignet
           varmap
           invars
           regvars
           strash)) (reg-aigs (alist-vals reg-alist))
        ((mv varmap
           invars
           regvars
           aignet) (aig-fsm-prepare-aignet/varmap reg-alist
            out-list
            max-nodes
            aignet))
        (strash (if (gatesimp->hashp gatesimp)
            (strashtab-init max-nodes
              nil
              nil
              strash)
            strash))
        ((mv lits strash aignet) (cwtime (aiglist-to-aignet-top (append reg-aigs out-list)
              varmap
              gatesimp
              strash
              aignet)))
        (nregs (length reg-aigs))
        (out-lits (nthcdr nregs lits))
        (reg-lits (take nregs lits))
        (aignet (aignet-set-nxsts 0 reg-lits aignet))
        (aignet (aignet-add-outs out-lits aignet)))
      (mv aignet
        varmap
        invars
        regvars
        strash))
    ///
    (local (in-theory (enable aig-fsm-to-aignet)))
    (local (defthm true-listp-when-lit-listp-rw
        (implies (lit-listp x)
          (true-listp x))))
    (verify-guards aig-fsm-to-aignet
      :guard-debug t)
    (defthm true-listp-aig-fsm-to-aignet-invars
      (true-listp (mv-nth 2
          (aig-fsm-to-aignet regs
            outs
            max-gates
            gatesimp
            aignet)))
      :rule-classes (:rewrite :type-prescription))
    (defthm true-listp-aig-fsm-to-aignet-regvars
      (true-listp (mv-nth 3
          (aig-fsm-to-aignet regs
            outs
            max-gates
            gatesimp
            aignet)))
      :rule-classes (:rewrite :type-prescription))
    (defthm aig-fsm-to-aignet-output-correct
      (b* (((mv aignet
            varmap
            ?invars
            ?regvars) (aig-fsm-to-aignet reg-alist
             out-list
             max-gates
             gatesimp
             aignet)) (env (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet)))
        (implies (and (aig-var-listp (alist-keys reg-alist))
            (< (nfix n) (len out-list)))
          (equal (lit-eval (fanin 0
                (lookup-stype n
                  (po-stype)
                  aignet))
              in-vals
              reg-vals
              aignet)
            (bool->bit (aig-eval (nth n out-list)
                env)))))
      :hints (("goal" :do-not-induct t
         :expand ((:free (aignet1 aignet2)
            (id-eval (fanin-count (lookup-stype n
                  (po-stype)
                  aignet1))
              in-vals
              reg-vals
              aignet2))))))
    (defthm aig-fsm-to-aignet-nxst-correct
      (b* (((mv aignet
            varmap
            ?invars
            ?regvars) (aig-fsm-to-aignet reg-alist
             out-list
             max-gates
             gatesimp
             aignet)) (env (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet)))
        (implies (and (aig-var-listp (alist-keys reg-alist))
            (< (nfix n)
              (len (alist-keys reg-alist))))
          (equal (lit-eval (lookup-reg->nxst n aignet)
              in-vals
              reg-vals
              aignet)
            (bool->bit (aig-eval (nth n (alist-vals reg-alist))
                env)))))
      :hints (("goal" :do-not-induct t)))
    (local (defthm alist-keys-of-aignet-eval-to-env
        (equal (alist-keys (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet))
          (alist-keys varmap))
        :hints (("Goal" :in-theory (enable aignet-eval-to-env)))))
    (local (defthm alist-keys-of-consecutive-vars-to-varmap
        (equal (alist-keys (consecutive-vars-to-varmap n
              vars
              varmap))
          (append (rev (list-fix vars))
            (alist-keys varmap)))
        :hints (("Goal" :in-theory (enable consecutive-vars-to-varmap
             alist-keys)))))
    (local (defthm acl2-numberp-of-index-of-when-member
        (implies (double-rewrite (member x lst))
          (acl2-numberp (index-of x lst)))))
    (local (defthm no-duplicatesp-of-set-diff
        (implies (no-duplicatesp a)
          (no-duplicatesp (set-difference$ a b)))
        :hints (("Goal" :in-theory (enable set-difference$)))))
    (defthm aignet-eval-to-env-of-varmap-lookup
      (b* (((mv ?aignet
            varmap
            invars
            regvars) (aig-fsm-to-aignet reg-alist
             out-list
             max-gates
             gatesimp
             aignet)) (env (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet)))
        (implies (and (no-duplicatesp (alist-keys reg-alist))
            (aig-var-listp (alist-keys reg-alist)))
          (and (iff (hons-assoc-equal var env)
              (hons-assoc-equal var
                (append (aignet-bitarr-to-aig-env regvars
                    reg-vals)
                  (aignet-bitarr-to-aig-env invars
                    in-vals))))
            (equal (cdr (hons-assoc-equal var env))
              (cdr (hons-assoc-equal var
                  (append (aignet-bitarr-to-aig-env regvars
                      reg-vals)
                    (aignet-bitarr-to-aig-env invars
                      in-vals))))))))
      :hints (("Goal" :in-theory (e/d (aignet-eval-to-env aignet-bitarr-to-aig-env
             aig-fsm-prepare-aignet/varmap
             aignet-idp
             hons-assoc-equal-iff-member-alist-keys)
           (alist-keys-member-hons-assoc-equal))
         :do-not-induct t
         :expand ((:free (n aignet)
            (lit-eval (make-lit (+ 1 n) 0)
              in-vals
              reg-vals
              aignet)) (:free (n aignet)
             (id-eval (+ 1 n)
               in-vals
               reg-vals
               aignet))))))
    (local (defthmd equal-of-hons-assoc-equal
        (equal (equal (hons-assoc-equal k x)
            y)
          (if (hons-assoc-equal k x)
            (and (consp y)
              (equal (car y) k)
              (equal (cdr y)
                (cdr (hons-assoc-equal k x))))
            (not y)))
        :hints (("Goal" :in-theory (enable hons-assoc-equal)))))
    (defthm aignet-eval-to-env-of-varmap-lookup-alist-equiv
      (b* (((mv ?aignet
            varmap
            invars
            regvars) (aig-fsm-to-aignet reg-alist
             out-list
             max-gates
             gatesimp
             aignet)) (env (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet)))
        (implies (and (no-duplicatesp (alist-keys reg-alist))
            (aig-var-listp (alist-keys reg-alist)))
          (alist-equiv env
            (append (aignet-bitarr-to-aig-env regvars
                reg-vals)
              (aignet-bitarr-to-aig-env invars
                in-vals)))))
      :hints (("Goal" :in-theory (e/d (alist-equiv-iff-agree-on-bad-guy equal-of-hons-assoc-equal)
           (aig-fsm-to-aignet)))))
    (defthm good-varmap-p-of-aig-fsm-to-aignet
      (implies (aig-var-listp (alist-keys regs))
        (good-varmap-p (mv-nth 1
            (aig-fsm-to-aignet regs
              outs
              max-gates
              gatesimp
              aignet))
          (mv-nth 0
            (aig-fsm-to-aignet regs
              outs
              max-gates
              gatesimp
              aignet))))
      :hints (("Goal" :in-theory (e/d* nil
           (aiglist-to-aignet lit-eval-list
             aig-eval-list
             aignet-eval-to-env
             aig-vars
             hons-sd1
             len
             pairlis$
             hons-assoc-equal
             make-fal
             double-containment
             resize-list))
         :do-not-induct t)))
    (defret outputs-of-aig-fsm-to-aignet
      (equal (stype-count :po new-aignet)
        (len out-list)))
    (defret inputs-of-aig-fsm-to-aignet
      (equal (stype-count :pi new-aignet)
        (len invars)))
    (defret aig-fsm-to-aignet-input-varmap-lookup
      (implies (and (member v
            (aiglist-vars (append (alist-vals reg-alist)
                out-list)))
          (not (hons-assoc-equal v reg-alist)))
        (b* ((index (index-of v invars)) (input-id (fanin-count (lookup-stype index :pi new-aignet))))
          (equal (hons-assoc-equal v varmap)
            (cons v (mk-lit input-id 0))))))
    (defret aig-fsm-to-aignet-reg-varmap-lookup
      (implies (and (member v
            (aiglist-vars (append (alist-vals reg-alist)
                out-list)))
          (hons-assoc-equal v reg-alist)
          (no-duplicatesp (alist-keys reg-alist)))
        (b* ((index (index-of v (alist-keys reg-alist))) (reg-id (fanin-count (lookup-stype index :reg new-aignet))))
          (equal (hons-assoc-equal v varmap)
            (cons v (mk-lit reg-id 0))))))
    (defret in-vars-of-aig-fsm-to-aignet
      (set-equiv invars
        (set-difference$ (aiglist-vars (append (alist-vals reg-alist)
              out-list))
          (alist-keys reg-alist))))
    (defret reg-vars-of-aig-fsm-to-aignet
      (equal regvars
        (alist-keys reg-alist)))
    (defret reg-count-of-aig-fsm-to-aignet
      (equal (stype-count :reg new-aignet)
        (len (alist-keys reg-alist))))
    (defret in-count-of-aig-fsm-to-aignet
      (equal (stype-count :pi new-aignet)
        (len invars)))))

(define aig-fsm-frame-env
  ((regs "alist") (curr-st "bindings to t/nil")
    (in "bindings to t/nil"))
  (append (fast-alist-free (with-fast-alist curr-st
        (aig-env-extract (alist-keys regs)
          curr-st)))
    in)
  ///
  (defthm lookup-in-aig-fsm-frame-env
    (equal (aig-env-lookup v
        (aig-fsm-frame-env regs
          curr-st
          in))
      (if (hons-assoc-equal v regs)
        (aig-env-lookup v curr-st)
        (aig-env-lookup v in)))
    :hints (("Goal" :in-theory (enable aig-env-lookup))))
  (defthm hons-assoc-equal-in-aig-fsm-frame-env
    (equal (hons-assoc-equal v
        (aig-fsm-frame-env regs
          curr-st
          in))
      (if (hons-assoc-equal v regs)
        (cons v (aig-env-lookup v curr-st))
        (hons-assoc-equal v in)))
    :hints (("Goal" :in-theory (enable aig-env-lookup)))))

(define aig-fsm-frame-outs
  ((outputs "aig list") (regs "alist")
    (curr-st "bindings to t/nil")
    (in "bindings to t/nil"))
  (b* ((env (aig-fsm-frame-env regs
         curr-st
         in)))
    (aig-eval-list outputs env))
  ///
  (defthm nth-of-aig-fsm-frame-outs
    (equal (nth n
        (aig-fsm-frame-outs outputs
          regs
          curr-st
          in))
      (aig-eval (nth n outputs)
        (aig-fsm-frame-env regs
          curr-st
          in)))))

(define aig-fsm-frame-nextst
  ((regs "alist") (curr-st "bindings to t/nil")
    (in "bindings to t/nil"))
  :returns (nextst)
  (b* ((env (aig-fsm-frame-env regs
         curr-st
         in)))
    (aig-eval-alist regs env))
  ///
  (defret aig-env-lookup-in-aig-fsm-frame-nextst
    (implies (hons-assoc-equal v regs)
      (equal (aig-env-lookup v nextst)
        (aig-eval (cdr (hons-assoc-equal v regs))
          (aig-fsm-frame-env regs
            curr-st
            in))))
    :hints (("Goal" :in-theory (enable aig-env-lookup)))))

(define aig-fsm-run
  ((outputs "aig list") (regs "alist")
    (curr-st "bindings to t/nil")
    (ins "list of bindings to t/nil"))
  :returns (result-list "list of bool lists")
  (if (atom ins)
    nil
    (b* ((env (aig-fsm-frame-env regs
           curr-st
           (car ins))))
      (mbe :logic (b* ((outs (aig-eval-list outputs env)) (next-st (aig-eval-alist regs env)))
          (cons outs
            (aig-fsm-run outputs
              regs
              next-st
              (cdr ins))))
        :exec (if (atom (cdr ins))
          (with-fast-alist env
            (list (aig-eval-list outputs env)))
          (b* (((mv outs next-st) (with-fast-alist env
                 (b* ((outs (aig-eval-list outputs env)) (next-st (aig-eval-alist regs env)))
                   (mv outs next-st)))))
            (cons outs
              (aig-fsm-run outputs
                regs
                next-st
                (cdr ins))))))))
  ///
  (defthm aig-fsm-run-of-cons
    (equal (aig-fsm-run outputs
        regs
        curr-st
        (cons in1 rest-ins))
      (cons (aig-fsm-frame-outs outputs
          regs
          curr-st
          in1)
        (aig-fsm-run outputs
          regs
          (aig-fsm-frame-nextst regs
            curr-st
            in1)
          rest-ins)))
    :hints (("Goal" :in-theory (enable aig-fsm-frame-outs
         aig-fsm-frame-nextst))))
  (defthm car-of-aig-fsm-run
    (equal (car (aig-fsm-run outputs
          regs
          curr-st
          ins))
      (and (consp ins)
        (aig-fsm-frame-outs outputs
          regs
          curr-st
          (car ins)))))
  (defthm cdr-of-aig-fsm-run
    (equal (cdr (aig-fsm-run outputs
          regs
          curr-st
          ins))
      (and (consp ins)
        (aig-fsm-run outputs
          regs
          (aig-fsm-frame-nextst regs
            curr-st
            (car ins))
          (cdr ins))))))

(define aig-fsm-states
  ((regs "alist") (curr-st "bindings to t/nil")
    (ins "list of bindings to t/nil"))
  (b* (((when (atom ins)) nil) (next-st (aig-fsm-frame-nextst regs
          curr-st
          (car ins))))
    (cons next-st
      (aig-fsm-states regs
        next-st
        (cdr ins))))
  ///
  (defthm nth-of-aig-fsm-run
    (implies (< (nfix n) (len ins))
      (equal (nth n
          (aig-fsm-run outputs
            regs
            curr-st
            ins))
        (aig-fsm-frame-outs outputs
          regs
          (if (zp n)
            curr-st
            (nth (1- n)
              (aig-fsm-states regs
                curr-st
                ins)))
          (nth n ins))))
    :hints (("Goal" :in-theory (enable aig-fsm-states nth)))))

(defthm aig-fsm-run-in-terms-of-aig-eval
  (implies (< (nfix k) (len ins))
    (equal (nth n
        (nth k
          (aig-fsm-run outputs
            regs
            curr-st
            ins)))
      (aig-eval (nth n outputs)
        (aig-fsm-frame-env regs
          (if (zp k)
            curr-st
            (nth (1- k)
              (aig-fsm-states regs
                curr-st
                ins)))
          (nth k ins))))))

(local (defun aig-fsm-state-ind
    (k regs curr-st ins)
    (if (zp k)
      (list regs curr-st ins)
      (aig-fsm-state-ind (1- k)
        regs
        (aig-fsm-frame-nextst regs
          curr-st
          (car ins))
        (cdr ins)))))

(defthm aig-fsm-state-in-terms-of-aig-eval
  (implies (and (hons-assoc-equal v regs)
      (< (nfix k) (len ins)))
    (equal (aig-env-lookup v
        (nth k
          (aig-fsm-states regs
            curr-st
            ins)))
      (aig-eval (cdr (hons-assoc-equal v regs))
        (aig-fsm-frame-env regs
          (if (zp k)
            curr-st
            (nth (1- k)
              (aig-fsm-states regs
                curr-st
                ins)))
          (nth k ins)))))
  :hints (("Goal" :in-theory (e/d (aig-fsm-states nth) (aig-env-lookup))
     :induct (aig-fsm-state-ind k
       regs
       curr-st
       ins)
     :expand ((aig-fsm-states regs
        curr-st
        ins)))))

(defun-sk reg-vals-equivalent
  (regs aignet-frame aig-currst)
  (forall v
    (implies (hons-assoc-equal v regs)
      (equal (nth (index-of v (alist-keys regs))
          aignet-frame)
        (bool->bit (aig-env-lookup v aig-currst)))))
  :rewrite :direct)

(in-theory (disable reg-vals-equivalent))

(defun-sk aig-envs-agree
  (vars x y)
  (forall v
    (implies (member v vars)
      (equal (aig-env-lookup v x)
        (aig-env-lookup v y))))
  :rewrite :direct)

(in-theory (disable aig-envs-agree))

(local (defthmd equal-of-aig-env-extract-when-aig-envs-agree
    (implies (and (aig-envs-agree vars1 x y)
        (subsetp vars vars1))
      (equal (aig-env-extract vars x)
        (aig-env-extract vars y)))
    :hints (("Goal" :in-theory (enable aig-env-extract)))))

(local (defthmd not-equal-of-aig-env-extract-when-witness
    (implies (and (member v vars)
        (not (equal (aig-env-lookup v x)
            (aig-env-lookup v y))))
      (not (equal (aig-env-extract vars x)
          (aig-env-extract vars y))))
    :hints (("Goal" :in-theory (enable aig-env-extract)))))

(local (defthmd equal-of-aig-env-extract-by-aig-envs-agree
    (iff (equal (aig-env-extract vars x)
        (aig-env-extract vars y))
      (aig-envs-agree vars x y))
    :hints (("Goal" :in-theory (enable equal-of-aig-env-extract-when-aig-envs-agree)) (and stable-under-simplificationp
        '(:in-theory (enable aig-envs-agree
            not-equal-of-aig-env-extract-when-witness))))))

(defthm reg-vals-equivalent-implies-rewrite-aig-fsm-frame-env
  (implies (reg-vals-equivalent regs
      aignet-frame
      aig-currst)
    (equal (aig-fsm-frame-env regs
        (aignet-bitarr-to-aig-env (alist-keys regs)
          aignet-frame)
        ins)
      (aig-fsm-frame-env regs
        aig-currst
        ins)))
  :hints (("Goal" :in-theory (e/d (aig-fsm-frame-env aig-env-extract
         alist-keys
         equal-of-aig-env-extract-by-aig-envs-agree
         aig-envs-agree)
       (aig-env-lookup))
     :do-not-induct t)))

(defthm lit-eval-of-aignet-input
  (implies (< (nfix n)
      (stype-count :pi aignet))
    (equal (lit-eval (mk-lit (fanin-count (lookup-stype n :pi aignet))
          neg)
        in-vals
        reg-vals
        aignet)
      (b-xor neg (nth n in-vals))))
  :hints (("Goal" :in-theory (enable lit-eval id-eval))))

(defthm lit-eval-of-aignet-reg
  (implies (< (nfix n)
      (stype-count :reg aignet))
    (equal (lit-eval (mk-lit (fanin-count (lookup-stype n :reg aignet))
          neg)
        in-vals
        reg-vals
        aignet)
      (b-xor neg (nth n reg-vals))))
  :hints (("Goal" :in-theory (enable lit-eval id-eval))))

(local (defthm index-of-less-than-len
    (implies (double-rewrite (member v x))
      (< (nfix (index-of v x))
        (len x)))))

(local (defthm aig-env-lookup-of-aignet-eval-to-env-of-aig-fsm-to-aignet
    (b* (((mv aignet
          ?varmap
          ?invars
          ?regvars) (aig-fsm-to-aignet regs
           outs
           max-gates
           gatesimp
           aignet)))
      (implies (and (no-duplicatesp (alist-keys regs))
          (member v
            (aiglist-vars (append (alist-vals regs) outs))))
        (equal (aig-env-lookup v
            (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet))
          (if (hons-assoc-equal v regs)
            (equal 1
              (nth (index-of v regvars) reg-vals))
            (equal 1
              (nth (index-of v invars) in-vals))))))))

(local (defthm aig-eval-of-aignet-eval-to-env-of-aig-fsm-to-aignet
    (b* (((mv aignet
          ?varmap
          ?invars
          ?regvars) (aig-fsm-to-aignet regs
           outs
           max-gates
           gatesimp
           aignet)))
      (implies (and (subsetp-equal (aig-vars x)
            (aiglist-vars (append (alist-vals regs) outs)))
          (no-duplicatesp (alist-keys regs)))
        (equal (aig-eval x
            (aignet-eval-to-env varmap
              in-vals
              reg-vals
              aignet))
          (aig-eval x
            (aig-fsm-frame-env regs
              (aignet-bitarr-to-aig-env (alist-keys regs)
                reg-vals)
              (aignet-bitarr-to-aig-env invars
                in-vals))))))
    :hints (("Goal" :in-theory (e/d (aig-eval) (aig-env-lookup))
       :induct (aig-vars x)))))

(defines reg-eval-of-aig-fsm-to-aignet-ind
  :verify-guards nil
  (define frame-regvals-of-aig-fsm-to-aignet-ind
    (k regs
      outs
      max-gates
      gatesimp
      aignet0
      frames
      initsts)
    :non-executable t
    :measure (* 2 (nfix k))
    (b* (((when (zp k)) (list regs
           outs
           max-gates
           gatesimp
           aignet0
           frames
           initsts)) ((mv aignet
           ?varmap
           ?invars
           ?regvars) (aig-fsm-to-aignet regs
            outs
            max-gates
            gatesimp
            aignet0))
        (regvals (frame-regvals k
            frames
            initsts
            aignet))
        (frame-st (nth (1- k)
            (aig-fsm-states regs
              (aignet-bitarr-to-aig-env (alist-keys regs)
                initsts)
              (aignet-frames-to-aig-envs frames
                invars))))
        (reg-name (reg-vals-equivalent-witness regs
            regvals
            frame-st))
        (regnum (index-of reg-name
            (alist-keys regs))))
      (reg-eval-of-aig-fsm-to-aignet-ind regnum
        (1- k)
        regs
        outs
        max-gates
        gatesimp
        aignet0
        frames
        initsts)))
  (define reg-eval-of-aig-fsm-to-aignet-ind
    (n k
      regs
      outs
      max-gates
      gatesimp
      aignet0
      frames
      initsts)
    :non-executable t
    :measure (+ 1 (* 2 (nfix k)))
    (frame-regvals-of-aig-fsm-to-aignet-ind k
      regs
      outs
      max-gates
      gatesimp
      aignet0
      frames
      initsts))
  ///
  (local (in-theory (enable lit-eval-seq-in-terms-of-lit-eval)))
  (local (defthm subsetp-vars-of-nth-reg
      (subsetp (aig-vars (nth n regvals))
        (aiglist-vars (append regvals outs)))
      :hints (("Goal" :in-theory (enable nth aig-vars aiglist-vars)))))
  (local (in-theory (disable aig-env-lookup)))
  (local (defthm nth-index-of-alist-keys-in-alist-vals
      (implies (hons-assoc-equal v x)
        (equal (nth (index-of v (alist-keys x))
            (alist-vals x))
          (cdr (hons-assoc-equal v x))))
      :hints (("Goal" :in-theory (enable hons-assoc-equal
           nth
           index-of
           alist-keys
           alist-vals)))))
  (local (defthm subsetp-vars-of-nth
      (subsetp (aig-vars (nth n x))
        (aiglist-vars x))
      :hints (("Goal" :in-theory (enable aig-vars nth aiglist-vars)))))
  (local (defthm subsetp-vars-of-nth-out
      (subsetp (aig-vars (nth n outs))
        (aiglist-vars (append regvals outs)))
      :hints (("Goal" :in-theory (enable aig-vars append aiglist-vars)))))
  (local (defthm bits-to-bools-of-take
      (equal (bits-to-bools (take n x))
        (take n (bits-to-bools x)))
      :hints (("Goal" :in-theory (e/d (bits-to-bools (:i nthcdr))
           (take-of-too-many take-when-atom))
         :induct (nthcdr n x)))))
  (local (defthm pairlis$-of-take-len
      (equal (pairlis$ x
          (take (len x) y))
        (pairlis$ x y))
      :hints (("Goal" :in-theory (enable pairlis$)))))
  (local (defthm aignet-bitarr-to-aig-env-of-take
      (equal (aignet-bitarr-to-aig-env vars
          (take (len vars) bitarr))
        (aignet-bitarr-to-aig-env vars
          bitarr))
      :hints (("Goal" :in-theory (enable aignet-bitarr-to-aig-env)))))
  (local (defthm aignet-eval-to-env-of-take-num-regs
      (implies (equal (nfix n)
          (num-regs aignet))
        (equal (aignet-eval-to-env varmap
            invals
            (take n regvals)
            aignet)
          (aignet-eval-to-env varmap
            invals
            regvals
            aignet)))
      :hints (("Goal" :in-theory (enable aignet-eval-to-env)
         :induct (aignet-eval-to-env varmap
           invals
           regvals
           aignet)))))
  (defthm-reg-eval-of-aig-fsm-to-aignet-ind-flag (defthm frame-regvals-of-aig-fsm-to-aignet
      (b* (((mv aignet
            ?varmap
            ?invars
            ?regvars) (aig-fsm-to-aignet regs
             outs
             max-gates
             gatesimp
             aignet0)) (aig-ins (aignet-frames-to-aig-envs frames
              invars))
          (aig-initst (aignet-bitarr-to-aig-env (alist-keys regs)
              initsts)))
        (implies (and (< (nfix k)
              (len (2darr->rows frames)))
            (aig-var-listp (alist-keys regs))
            (no-duplicatesp (alist-keys regs)))
          (reg-vals-equivalent regs
            (frame-regvals k
              frames
              initsts
              aignet)
            (if (zp k)
              aig-initst
              (nth (1- k)
                (aig-fsm-states regs
                  aig-initst
                  aig-ins))))))
      :hints ((and stable-under-simplificationp
         `(:expand (,(CAR (LAST AIGNET::CLAUSE)))
           :in-theory (e/d (reg-eval-seq aig-env-lookup)))))
      :flag frame-regvals-of-aig-fsm-to-aignet-ind)
    (defthm reg-eval-of-aig-fsm-to-aignet
      (b* (((mv aignet
            ?varmap
            ?invars
            ?regvars) (aig-fsm-to-aignet regs
             outs
             max-gates
             gatesimp
             aignet0)) (aig-ins (aignet-frames-to-aig-envs frames
              invars))
          (aig-initst (aignet-bitarr-to-aig-env (alist-keys regs)
              initsts)))
        (implies (and (< (nfix n)
              (len (alist-keys regs)))
            (< (nfix k)
              (len (2darr->rows frames)))
            (aig-var-listp (alist-keys regs))
            (no-duplicatesp (alist-keys regs)))
          (equal (lit-eval-seq k
              (lookup-reg->nxst n aignet)
              frames
              initsts
              aignet)
            (bool->bit (aig-eval (nth n (alist-vals regs))
                (aig-fsm-frame-env regs
                  (if (zp k)
                    aig-initst
                    (nth (1- k)
                      (aig-fsm-states regs
                        aig-initst
                        aig-ins)))
                  (nth k aig-ins)))))))
      :flag reg-eval-of-aig-fsm-to-aignet-ind))
  (defthm out-eval-of-aig-fsm-to-aignet
    (b* (((mv aignet
          ?varmap
          ?invars
          ?regvars) (aig-fsm-to-aignet regs
           outs
           max-gates
           gatesimp
           aignet0)) (aig-ins (aignet-frames-to-aig-envs frames
            invars))
        (aig-initst (aignet-bitarr-to-aig-env (alist-keys regs)
            initsts)))
      (implies (and (< (nfix n) (len outs))
          (< (nfix k)
            (len (2darr->rows frames)))
          (aig-var-listp (alist-keys regs))
          (no-duplicatesp (alist-keys regs)))
        (equal (lit-eval-seq k
            (fanin 0
              (lookup-stype n :po aignet))
            frames
            initsts
            aignet)
          (bool->bit (nth n
              (nth k
                (aig-fsm-run outs
                  regs
                  aig-initst
                  aig-ins)))))))
    :hints (("Goal" :use ((:instance frame-regvals-of-aig-fsm-to-aignet))
       :in-theory (disable frame-regvals-of-aig-fsm-to-aignet)))))

(define frames-row-fix
  ((ncols natp) (row))
  :verify-guards nil
  :returns (new-row (and (framese-datap new-row)
      (equal (len new-row)
        (nfix ncols))))
  (if (zp ncols)
    nil
    (cons (bfix (car row))
      (frames-row-fix (1- ncols)
        (cdr row))))
  ///
  (defret frames-row-fix-when-framese-datap
    (implies (and (framese-datap row)
        (equal (len row)
          (nfix ncols)))
      (equal new-row row)))
  (local (defun nth-of-frames-row-fix-ind
      (n ncols row)
      (if (zp ncols)
        (list n row)
        (nth-of-frames-row-fix-ind (1- (nfix n))
          (1- ncols)
          (cdr row)))))
  (defret nth-of-frames-row-fix
    (equal (nth n new-row)
      (and (< (nfix n) (nfix ncols))
        (bfix (nth n row))))
    :hints (("Goal" :in-theory (enable nth)
       :induct (nth-of-frames-row-fix-ind n
         ncols
         row)
       :expand ((:free (x) (nth n x)))))))

(define frames-fix-row
  ((row natp) frames)
  :guard (< row (frames-nrows frames))
  :returns (new-frames 2darr-p
    :hyp (2darr-p frames))
  :guard-hints (("goal" :in-theory (enable redundant-update-nth)))
  (mbe :logic (non-exec (b* ((rows (2darr->rows frames)) (ncols (2darr->ncols frames))
          (nth-row (nth row rows))
          (new-rows (update-nth row
              (frames-row-fix ncols nth-row)
              rows)))
        (2darr ncols new-rows)))
    :exec frames)
  ///
  (defret ncols-of-frames-fix-row
    (equal (2darr->ncols new-frames)
      (2darr->ncols frames)))
  (defret nth-of-frames-fix-row
    (equal (nth n (2darr->rows new-frames))
      (if (equal (nfix n) (nfix row))
        (frames-row-fix (2darr->ncols frames)
          (nth row (2darr->rows frames)))
        (nth n (2darr->rows frames)))))
  (defret nrows-of-frames-fix-row
    (implies (< (nfix row)
        (len (2darr->rows frames)))
      (equal (len (2darr->rows new-frames))
        (len (2darr->rows frames)))))
  (deffixcong nat-equiv
    equal
    (frames-fix-row row frames)
    row))

(define env-to-frame-aux
  ((n natp) (i natp)
    vars
    env
    frames)
  :guard (and (< n (frames-nrows frames))
    (<= i (frames-ncols frames))
    (equal (len vars)
      (- (frames-ncols frames) i)))
  :returns (new-frames 2darr-p
    :hyp (2darr-p frames))
  (if (atom vars)
    (frames-fix-row n frames)
    (b* ((val (bool->bit (aig-env-lookup (car vars) env))) (frames (frames-set2 n
            i
            val
            frames)))
      (env-to-frame-aux n
        (1+ (lnfix i))
        (cdr vars)
        env
        frames)))
  ///
  (local (in-theory (disable aig-env-lookup)))
  (defret env-to-frame-aux-preserves-ncols
    (equal (2darr->ncols new-frames)
      (2darr->ncols frames)))
  (local (defthm frames-row-fix-of-append-when-first-len
      (implies (equal (len a) (nfix n))
        (equal (frames-row-fix n
            (append a b))
          (frames-row-fix n a)))
      :hints (("Goal" :in-theory (enable frames-row-fix)))))
  (local (defthm frames-row-fix-of-take-n
      (implies (equal (nfix i) (nfix n))
        (equal (frames-row-fix n
            (take i x))
          (frames-row-fix n x)))
      :hints (("Goal" :in-theory (enable frames-row-fix)))))
  (local (defthm take-n-plus-one
      (equal (take (+ 1 (nfix n)) x)
        (append (take n x)
          (list (nth n x))))
      :hints (("Goal" :in-theory (e/d (nth repeat)
           (take-of-too-many take-of-1 take-of-zero))))))
  (local (defthm take-of-update-nth
      (equal (take n
          (update-nth n val x))
        (take n x))
      :hints (("Goal" :in-theory (enable update-nth)))))
  (defretd env-to-frame-aux-is-update-nth
    (implies (equal (len vars)
        (- (frames-ncols frames)
          (nfix i)))
      (equal (2darr->rows new-frames)
        (update-nth n
          (frames-row-fix (frames-ncols frames)
            (append (take i
                (nth n (2darr->rows frames)))
              (env-to-bitarr vars env)))
          (2darr->rows frames))))
    :hints (("Goal" :in-theory (enable frames-fix-row
         env-to-bitarr))))
  (defret nth-of-env-to-frame-aux
    (implies (equal (len vars)
        (- (frames-ncols frames)
          (nfix i)))
      (equal (nth m (2darr->rows new-frames))
        (if (equal (nfix n) (nfix m))
          (frames-row-fix (frames-ncols frames)
            (append (take i
                (nth n (2darr->rows frames)))
              (env-to-bitarr vars env)))
          (nth m (2darr->rows frames)))))
    :hints (("Goal" :in-theory (e/d (env-to-frame-aux-is-update-nth)
         (env-to-frame-aux)))))
  (defret len-rows-of-env-to-frame-aux
    (implies (< (nfix n)
        (len (2darr->rows frames)))
      (equal (len (2darr->rows new-frames))
        (len (2darr->rows frames)))))
  (deffixcong nat-equiv
    equal
    (env-to-frame-aux n
      i
      vars
      env
      frames)
    n))

(define env-to-frame
  ((n natp) vars
    env
    frames)
  :guard (and (< n (frames-nrows frames))
    (equal (len vars)
      (frames-ncols frames)))
  :returns (new-frames 2darr-p
    :hyp (2darr-p frames))
  (env-to-frame-aux n
    0
    vars
    env
    frames)
  ///
  (defret env-to-frame-preserves-ncols
    (equal (2darr->ncols new-frames)
      (2darr->ncols frames)))
  (local (defthm frames-row-fix-of-env-to-bitarr
      (implies (equal n (len vars))
        (equal (frames-row-fix n
            (env-to-bitarr vars env))
          (env-to-bitarr vars env)))
      :hints (("goal" :induct (nthcdr n vars)
         :in-theory (enable env-to-bitarr
           frames-row-fix)))))
  (defret env-to-frame-is-update-nth
    (implies (equal (len vars)
        (frames-ncols frames))
      (equal (2darr->rows new-frames)
        (update-nth n
          (env-to-bitarr vars env)
          (2darr->rows frames))))
    :hints (("Goal" :in-theory (enable env-to-frame-aux-is-update-nth))))
  (defretd nth-of-env-to-frame
    (implies (equal (len vars)
        (frames-ncols frames))
      (equal (nth m (2darr->rows new-frames))
        (if (equal (nfix n) (nfix m))
          (env-to-bitarr vars env)
          (nth m (2darr->rows frames)))))
    :hints (("Goal" :in-theory (e/d (env-to-frame-is-update-nth)
         (env-to-frame)))))
  (defret len-rows-of-env-to-frame
    (implies (< (nfix n)
        (len (2darr->rows frames)))
      (equal (len (2darr->rows new-frames))
        (len (2darr->rows frames)))))
  (deffixcong nat-equiv
    equal
    (env-to-frame n
      vars
      env
      frames)
    n))

(define envs-to-bitarrs
  (vars envs)
  :returns (bitarrs)
  (if (atom envs)
    nil
    (cons (env-to-bitarr vars (car envs))
      (envs-to-bitarrs vars (cdr envs))))
  ///
  (defret len-of-envs-to-bitarrs
    (equal (len bitarrs)
      (len envs)))
  (defret consp-of-envs-to-bitarrs
    (equal (consp bitarrs) (consp envs))))

(define aig-envs-to-aignet-frames-aux
  ((n natp) vars
    envs
    frames)
  :guard (and (<= (+ n (len envs))
      (frames-nrows frames))
    (equal (len vars)
      (frames-ncols frames)))
  :returns (new-frames 2darr-p
    :hyp (2darr-p frames))
  :prepwork ((local (defthm len-equal-0
       (equal (equal (len x) 0)
         (not (consp x))))))
  :verify-guards nil
  (if (atom envs)
    frames
    (b* ((frames (env-to-frame n
           vars
           (car envs)
           frames)))
      (aig-envs-to-aignet-frames-aux (1+ (lnfix n))
        vars
        (cdr envs)
        frames)))
  ///
  (defret aig-envs-to-aignet-frames-aux-preserves-ncols
    (equal (2darr->ncols new-frames)
      (2darr->ncols frames)))
  (local (defthm take-n-plus-one
      (equal (take (+ 1 (nfix n)) x)
        (append (take n x)
          (list (nth n x))))
      :hints (("Goal" :in-theory (e/d (nth repeat)
           (take-of-too-many take-of-1 take-of-zero))))))
  (local (defthm take-of-update-nth
      (equal (take n
          (update-nth n val x))
        (take n x))
      :hints (("Goal" :in-theory (enable update-nth)))))
  (local (defthm nthcdr-of-update-nth
      (equal (nthcdr n
          (update-nth m v x))
        (if (<= (nfix n) (nfix m))
          (update-nth (- (nfix m) (nfix n))
            v
            (nthcdr n x))
          (nthcdr n x)))
      :hints (("Goal" :in-theory (enable update-nth)))))
  (defretd rows-of-aig-envs-to-aignet-frames-aux
    (implies (and (equal (len vars)
          (frames-ncols frames))
        (<= (+ (nfix n) (len envs))
          (frames-nrows frames)))
      (equal (2darr->rows new-frames)
        (append (take n
            (2darr->rows frames))
          (envs-to-bitarrs vars envs)
          (nthcdr (+ (nfix n) (len envs))
            (2darr->rows frames)))))
    :hints (("Goal" :in-theory (e/d (envs-to-bitarrs env-to-frame-is-update-nth)
         (take nthcdr (force))))))
  (defret aig-envs-to-aignet-frames-aux-lookup
    (implies (equal (len vars)
        (frames-ncols frames))
      (equal (nth m (2darr->rows new-frames))
        (if (and (<= (nfix n) (nfix m))
            (< (nfix m)
              (+ (nfix n) (len envs))))
          (env-to-bitarr vars
            (nth (- (nfix m) (nfix n))
              envs))
          (nth m (2darr->rows frames)))))
    :hints (("Goal" :in-theory (enable nth))))
  (defret len-rows-of-aig-envs-to-aignet-frames-aux
    (implies (<= (+ (nfix n) (len envs))
        (len (2darr->rows frames)))
      (equal (len (2darr->rows new-frames))
        (len (2darr->rows frames)))))
  (deffixcong nat-equiv
    equal
    (aig-envs-to-aignet-frames-aux n
      vars
      env
      frames)
    n)
  (verify-guards aig-envs-to-aignet-frames-aux))

(define aig-envs-to-aignet-frames
  (vars envs frames)
  :enabled t
  :prepwork ((local (defthm equal-of-2darr
       (equal (equal (2darr a b) c)
         (and (2darr-p c)
           (equal (nfix a)
             (2darr->ncols c))
           (equal (list-fix b) (2darr->rows c))))
       :hints (("Goal" :in-theory (enable 2darr
            2darr-p
            2darr->ncols
            2darr->rows))))))
  :guard-hints (("goal" :in-theory (enable rows-of-aig-envs-to-aignet-frames-aux)))
  (mbe :logic (non-exec (2darr (len vars)
        (envs-to-bitarrs vars envs)))
    :exec (b* ((frames (frames-resize-rows 0 frames)) (frames (frames-resize-cols (len vars)
            frames))
        (frames (frames-resize-rows (len envs)
            frames)))
      (aig-envs-to-aignet-frames-aux 0
        vars
        envs
        frames))))

(defthm aig-eval-of-aig-fsm-frame-env-of-bitarr-to-aig-env-of-env-to-bitarr
  (implies (subsetp (aig-vars x)
      (append vars (alist-keys regs)))
    (equal (aig-eval x
        (aig-fsm-frame-env regs
          curr-st
          (aignet-bitarr-to-aig-env vars
            (env-to-bitarr vars ins))))
      (aig-eval x
        (aig-fsm-frame-env regs
          curr-st
          ins))))
  :hints (("Goal" :in-theory (enable aig-fsm-frame-env
       aig-eval
       aig-env-lookup))))

(defthm aig-eval-list-of-aig-fsm-frame-env-of-bitarr-to-aig-env-of-env-to-bitarr
  (implies (subsetp (aiglist-vars x)
      (append vars (alist-keys regs)))
    (equal (aig-eval-list x
        (aig-fsm-frame-env regs
          curr-st
          (aignet-bitarr-to-aig-env vars
            (env-to-bitarr vars ins))))
      (aig-eval-list x
        (aig-fsm-frame-env regs
          curr-st
          ins))))
  :hints (("Goal" :in-theory (enable aig-eval-list aiglist-vars))))

(defthm aig-eval-alist-of-aig-fsm-frame-env-of-bitarr-to-aig-env-of-env-to-bitarr
  (implies (subsetp (aiglist-vars (alist-vals x))
      (append vars (alist-keys regs)))
    (equal (aig-eval-alist x
        (aig-fsm-frame-env regs
          curr-st
          (aignet-bitarr-to-aig-env vars
            (env-to-bitarr vars ins))))
      (aig-eval-alist x
        (aig-fsm-frame-env regs
          curr-st
          ins))))
  :hints (("Goal" :in-theory (enable aig-eval-alist aiglist-vars))))

(defthm aig-fsm-frame-outs-of-bitarr-to-aig-env-of-env-to-bitarr
  (implies (subsetp (aiglist-vars outputs)
      (append vars (alist-keys regs)))
    (equal (aig-fsm-frame-outs outputs
        regs
        curr-st
        (aignet-bitarr-to-aig-env vars
          (env-to-bitarr vars ins)))
      (aig-fsm-frame-outs outputs
        regs
        curr-st
        ins)))
  :hints (("Goal" :in-theory (enable aig-fsm-frame-outs))))

(defthm aig-fsm-frame-nextst-of-bitarr-to-aig-env-of-env-to-bitarr
  (implies (subsetp (aiglist-vars (alist-vals regs))
      (append vars (alist-keys regs)))
    (equal (aig-fsm-frame-nextst regs
        curr-st
        (aignet-bitarr-to-aig-env vars
          (env-to-bitarr vars ins)))
      (aig-fsm-frame-nextst regs
        curr-st
        ins)))
  :hints (("Goal" :in-theory (enable aig-fsm-frame-nextst))))

(local (defthm aig-fsm-run-of-atom
    (implies (atom ins)
      (equal (aig-fsm-run outputs
          regs
          curr-st
          ins)
        nil))
    :hints (("Goal" :in-theory (enable aig-fsm-run)))))

(defthm aig-fsm-run-of-frames-to-envs-of-envs-to-frames
  (implies (and (subsetp (aiglist-vars outputs)
        (append vars (alist-keys regs)))
      (subsetp (aiglist-vars (alist-vals regs))
        (append vars (alist-keys regs))))
    (equal (aig-fsm-run outputs
        regs
        curr-st
        (aignet-frame-array-to-aig-envs (envs-to-bitarrs vars ins)
          vars))
      (aig-fsm-run outputs
        regs
        curr-st
        ins)))
  :hints (("goal" :in-theory (e/d (envs-to-bitarrs aignet-frame-array-to-aig-envs
         (:i aig-fsm-states)))
     :induct (aig-fsm-states regs
       curr-st
       ins))))

(defthm aig-fsm-states-of-frames-to-envs-of-envs-to-frames
  (implies (subsetp (aiglist-vars (alist-vals regs))
      (append vars (alist-keys regs)))
    (equal (aig-fsm-states regs
        curr-st
        (aignet-frame-array-to-aig-envs (envs-to-bitarrs vars ins)
          vars))
      (aig-fsm-states regs
        curr-st
        ins)))
  :hints (("goal" :in-theory (e/d (envs-to-bitarrs aignet-frame-array-to-aig-envs
         aig-fsm-states))
     :induct (aig-fsm-states regs
       curr-st
       ins))))