		Search-engine friendly clone of the ACL2 documentation.

Svex-compose-dfs

Compose together a network of svex assignments, stopping when a variable depends on itself.

Signature
(svex-compose-dfs x assigns updates memo stack) → (mv x1 updates1 memo1)
Arguments: x — svex we're traversing.
Guard (svex-p x).; assigns — alist of assign stmts.
Guard (svex-alist-p assigns).; updates — alist of composed update fns.
Guard (svex-alist-p updates).; memo — memo table for internal nodes.
Guard (svex-svex-memo-p memo).; stack — alist of seen vars.
Guard (alistp stack).
Returns: x1 — composition of x with other internal wires.
Type (svex-p x1).; updates1 — extended update functions.
Type (svex-alist-p updates1).; memo1 — extended memo table.
Type (svex-svex-memo-p memo1).

Theorem: return-type-of-svex-compose-dfs.x1

(defthm return-type-of-svex-compose-dfs.x1
        (b* (((mv ?x1 ?updates1 ?memo1)
              (svex-compose-dfs x assigns updates memo stack)))
            (svex-p x1))
        :rule-classes :rewrite)

Theorem: return-type-of-svex-compose-dfs.updates1

(defthm return-type-of-svex-compose-dfs.updates1
        (b* (((mv ?x1 ?updates1 ?memo1)
              (svex-compose-dfs x assigns updates memo stack)))
            (svex-alist-p updates1))
        :rule-classes :rewrite)

Theorem: return-type-of-svex-compose-dfs.memo1

(defthm return-type-of-svex-compose-dfs.memo1
        (b* (((mv ?x1 ?updates1 ?memo1)
              (svex-compose-dfs x assigns updates memo stack)))
            (svex-svex-memo-p memo1))
        :rule-classes :rewrite)

Theorem: return-type-of-svexlist-compose-dfs.x1

(defthm return-type-of-svexlist-compose-dfs.x1
        (b* (((mv ?x1 ?updates1 ?memo1)
              (svexlist-compose-dfs x assigns updates memo stack)))
            (svexlist-p x1))
        :rule-classes :rewrite)

Theorem: return-type-of-svexlist-compose-dfs.updates1

(defthm return-type-of-svexlist-compose-dfs.updates1
        (b* (((mv ?x1 ?updates1 ?memo1)
              (svexlist-compose-dfs x assigns updates memo stack)))
            (svex-alist-p updates1))
        :rule-classes :rewrite)

Theorem: return-type-of-svexlist-compose-dfs.memo1

(defthm return-type-of-svexlist-compose-dfs.memo1
        (b* (((mv ?x1 ?updates1 ?memo1)
              (svexlist-compose-dfs x assigns updates memo stack)))
            (svex-svex-memo-p memo1))
        :rule-classes :rewrite)

Theorem: svex-compose-dfs-of-svex-fix-x

(defthm svex-compose-dfs-of-svex-fix-x
        (equal (svex-compose-dfs (svex-fix x)
                                 assigns updates memo stack)
               (svex-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-of-svex-alist-fix-assigns

(defthm svex-compose-dfs-of-svex-alist-fix-assigns
        (equal (svex-compose-dfs x (svex-alist-fix assigns)
                                 updates memo stack)
               (svex-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-of-svex-alist-fix-updates

(defthm svex-compose-dfs-of-svex-alist-fix-updates
        (equal (svex-compose-dfs x assigns (svex-alist-fix updates)
                                 memo stack)
               (svex-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-of-svex-svex-memo-fix-memo

(defthm svex-compose-dfs-of-svex-svex-memo-fix-memo
        (equal (svex-compose-dfs x assigns
                                 updates (svex-svex-memo-fix memo)
                                 stack)
               (svex-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svexlist-fix-x

(defthm svexlist-compose-dfs-of-svexlist-fix-x
        (equal (svexlist-compose-dfs (svexlist-fix x)
                                     assigns updates memo stack)
               (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svex-alist-fix-assigns

(defthm svexlist-compose-dfs-of-svex-alist-fix-assigns
        (equal (svexlist-compose-dfs x (svex-alist-fix assigns)
                                     updates memo stack)
               (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svex-alist-fix-updates

(defthm
     svexlist-compose-dfs-of-svex-alist-fix-updates
     (equal (svexlist-compose-dfs x assigns (svex-alist-fix updates)
                                  memo stack)
            (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svex-svex-memo-fix-memo

(defthm
     svexlist-compose-dfs-of-svex-svex-memo-fix-memo
     (equal (svexlist-compose-dfs x assigns
                                  updates (svex-svex-memo-fix memo)
                                  stack)
            (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-svex-equiv-congruence-on-x

(defthm
 svex-compose-dfs-svex-equiv-congruence-on-x
 (implies
      (svex-equiv x x-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x-equiv assigns updates memo stack)))
 :rule-classes :congruence)

Theorem: svex-compose-dfs-svex-alist-equiv-congruence-on-assigns

(defthm
 svex-compose-dfs-svex-alist-equiv-congruence-on-assigns
 (implies
      (svex-alist-equiv assigns assigns-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x assigns-equiv updates memo stack)))
 :rule-classes :congruence)

Theorem: svex-compose-dfs-svex-alist-equiv-congruence-on-updates

(defthm
 svex-compose-dfs-svex-alist-equiv-congruence-on-updates
 (implies
      (svex-alist-equiv updates updates-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x assigns updates-equiv memo stack)))
 :rule-classes :congruence)

Theorem: svex-compose-dfs-svex-svex-memo-equiv-congruence-on-memo

(defthm
 svex-compose-dfs-svex-svex-memo-equiv-congruence-on-memo
 (implies
      (svex-svex-memo-equiv memo memo-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x assigns updates memo-equiv stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svexlist-equiv-congruence-on-x

(defthm
 svexlist-compose-dfs-svexlist-equiv-congruence-on-x
 (implies
  (svexlist-equiv x x-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x-equiv assigns updates memo stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svex-alist-equiv-congruence-on-assigns

(defthm
 svexlist-compose-dfs-svex-alist-equiv-congruence-on-assigns
 (implies
  (svex-alist-equiv assigns assigns-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x assigns-equiv updates memo stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svex-alist-equiv-congruence-on-updates

(defthm
 svexlist-compose-dfs-svex-alist-equiv-congruence-on-updates
 (implies
  (svex-alist-equiv updates updates-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x assigns updates-equiv memo stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svex-svex-memo-equiv-congruence-on-memo

(defthm
 svexlist-compose-dfs-svex-svex-memo-equiv-congruence-on-memo
 (implies
  (svex-svex-memo-equiv memo memo-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x assigns updates memo-equiv stack)))
 :rule-classes :congruence)

Subtopics

Svexlist-compose-dfs