		Search-engine friendly clone of the ACL2 documentation.

Mmp-trees

Mmp-encode-c-forall

Universally quantified formula in the second case of the definition of c [YP:(194)].

This is used (indirectly) in the definition of mmp-encode-c, hence the name.

Here \mathfrak{I} is the argument map, x is the argument x, and \mathbf{l} is the argument l.

Instead of quantifying over the pairs in the map and projecting their key component [YP:(189)] as in [YP:(194)], here we directly quantify over the keys in the map. The values in the map are not referenced in this formula.

If this universally quantified formula holds, the length of every key in the map is greater than or equal to x. The reason is that (take x key) returns a list with some nils at the end if x is greater than the length of key, but the formula requires all the elements in that list to be nibbles instead. This property is used to show the existence of the maximum defined by mmp-encode-c-max.

Definitions and Theorems

Theorem: mmp-encode-c-forall-necc

(defthm mmp-encode-c-forall-necc
  (implies (mmp-encode-c-forall map x l)
           (implies (omap::assoc key (nibblelist-bytelist-mfix map))
                    (equal (take x key)
                           (nibble-list-fix l)))))

Theorem: booleanp-of-mmp-encode-c-forall

(defthm booleanp-of-mmp-encode-c-forall
  (b* ((yes/no (mmp-encode-c-forall map x l)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: mmp-encode-c-forall-of-nibblelist-bytelist-mfix-map

(defthm mmp-encode-c-forall-of-nibblelist-bytelist-mfix-map
  (equal (mmp-encode-c-forall (nibblelist-bytelist-mfix map)
                              x l)
         (mmp-encode-c-forall map x l)))

Theorem: mmp-encode-c-forall-nibblelist-bytelist-mequiv-congruence-on-map

(defthm
   mmp-encode-c-forall-nibblelist-bytelist-mequiv-congruence-on-map
  (implies (nibblelist-bytelist-mequiv map map-equiv)
           (equal (mmp-encode-c-forall map x l)
                  (mmp-encode-c-forall map-equiv x l)))
  :rule-classes :congruence)

Theorem: mmp-encode-c-forall-of-nfix-x

(defthm mmp-encode-c-forall-of-nfix-x
  (equal (mmp-encode-c-forall map (nfix x) l)
         (mmp-encode-c-forall map x l)))

Theorem: mmp-encode-c-forall-nat-equiv-congruence-on-x

(defthm mmp-encode-c-forall-nat-equiv-congruence-on-x
  (implies (acl2::nat-equiv x x-equiv)
           (equal (mmp-encode-c-forall map x l)
                  (mmp-encode-c-forall map x-equiv l)))
  :rule-classes :congruence)

Theorem: mmp-encode-c-forall-of-nibble-list-fix-l

(defthm mmp-encode-c-forall-of-nibble-list-fix-l
  (equal (mmp-encode-c-forall map x (nibble-list-fix l))
         (mmp-encode-c-forall map x l)))

Theorem: mmp-encode-c-forall-nibble-list-equiv-congruence-on-l

(defthm mmp-encode-c-forall-nibble-list-equiv-congruence-on-l
  (implies (acl2::nibble-list-equiv l l-equiv)
           (equal (mmp-encode-c-forall map x l)
                  (mmp-encode-c-forall map x l-equiv)))
  :rule-classes :congruence)

Theorem: mmp-encode-c-forall-len-key-geq-x

(defthm mmp-encode-c-forall-len-key-geq-x
  (implies (and (mmp-encode-c-forall map x l)
                (nibblelist-bytelist-mapp map)
                (natp x)
                (nibble-listp l)
                (omap::assoc key map))
           (>= (len key) x))
  :rule-classes nil)