		Search-engine friendly clone of the ACL2 documentation.

Mmp-trees

Mmp-encode-u-map

Submaps used to define u(0),\ldots,u(15) in the third case of the definition of c [YP:(194)].

Signature
(mmp-encode-u-map map i nibble) → map1
Arguments: map — Guard (nibblelist-bytelist-mapp map).; i — Guard (natp i).; nibble — Guard (nibblep nibble).
Returns: map1 — Type (nibblelist-bytelist-mapp map1).

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

Here \mathfrak{I} is the argument map, i is the argument i, and j is the argument nibble.

This function returns the submap (i.e. subset) of map whose keys all have value nibble at index i. This is the set calculated in the third case of the definition of c and passed to the function n, whose result is assigned to u(j).

The supremum natural number of the lengths of the keys decreases or remains constant for the submap.

By construction, every key in the submap has the nibble at position i.

A nibble array is in the submap iff it is in the map and has the nibble at position i.

If i is an element of the set maximized by mmp-encode-c-max, then (1+ i) is an element of the set for the submap.

Definitions and Theorems

Function: mmp-encode-u-map

(defun mmp-encode-u-map (map i nibble)
  (declare (xargs :guard (and (nibblelist-bytelist-mapp map)
                              (natp i)
                              (nibblep nibble))))
  (b* (((unless (mbt (nibblelist-bytelist-mapp map)))
        nil)
       ((when (omap::emptyp map)) nil)
       ((mv key val) (omap::head map))
       (nibble (nibble-fix nibble)))
    (if (eql (nth i key) nibble)
        (omap::update key val
                      (mmp-encode-u-map (omap::tail map)
                                        i nibble))
      (mmp-encode-u-map (omap::tail map)
                        i nibble))))

Theorem: nibblelist-bytelist-mapp-of-mmp-encode-u-map

(defthm nibblelist-bytelist-mapp-of-mmp-encode-u-map
  (b* ((map1 (mmp-encode-u-map map i nibble)))
    (nibblelist-bytelist-mapp map1))
  :rule-classes :rewrite)

Theorem: nibblelist-bytelist-map-sup-len-key-of-mmp-encode-u-map-leq

(defthm nibblelist-bytelist-map-sup-len-key-of-mmp-encode-u-map-leq
  (<= (nibblelist-bytelist-map-sup-len-key
           (mmp-encode-u-map map i nibble))
      (nibblelist-bytelist-map-sup-len-key map))
  :rule-classes :linear)

Theorem: nth-of-key-in-mmp-encode-u-map

(defthm nth-of-key-in-mmp-encode-u-map
  (implies (and (nibblelist-bytelist-mapp map)
                (nibblep nibble)
                (omap::assoc key (mmp-encode-u-map map i nibble)))
           (equal (nth i key) nibble)))

Theorem: in-of-mmp-encode-u-map

(defthm in-of-mmp-encode-u-map
  (implies (and (nibblelist-bytelist-mapp map)
                (nibblep nibble))
           (equal (omap::assoc key (mmp-encode-u-map map i nibble))
                  (and (equal (nth i key) nibble)
                       (omap::assoc key map)))))

Theorem: mmp-encode-c-forall-of-mmp-encode-u-map

(defthm mmp-encode-c-forall-of-mmp-encode-u-map
  (implies (and (nibblelist-bytelist-mapp map)
                (natp i)
                (nibblep nibble)
                (nibble-listp l)
                (mmp-encode-c-forall map i l))
           (mmp-encode-c-forall (mmp-encode-u-map map i nibble)
                                (1+ i)
                                (rcons nibble l))))

Theorem: mmp-encode-c-max.elementp-of-mmp-encode-u-map

(defthm mmp-encode-c-max.elementp-of-mmp-encode-u-map
 (implies (and (nibblelist-bytelist-mapp map)
               (natp i)
               (nibblep nibble)
               (mmp-encode-c-max.elementp map i))
          (mmp-encode-c-max.elementp (mmp-encode-u-map map i nibble)
                                     (1+ i))))

Theorem: mmp-encode-u-map-of-nibblelist-bytelist-mfix-map

(defthm mmp-encode-u-map-of-nibblelist-bytelist-mfix-map
  (equal (mmp-encode-u-map (nibblelist-bytelist-mfix map)
                           i nibble)
         (mmp-encode-u-map map i nibble)))

Theorem: mmp-encode-u-map-nibblelist-bytelist-mequiv-congruence-on-map

(defthm
      mmp-encode-u-map-nibblelist-bytelist-mequiv-congruence-on-map
  (implies (nibblelist-bytelist-mequiv map map-equiv)
           (equal (mmp-encode-u-map map i nibble)
                  (mmp-encode-u-map map-equiv i nibble)))
  :rule-classes :congruence)

Theorem: mmp-encode-u-map-of-nfix-i

(defthm mmp-encode-u-map-of-nfix-i
  (equal (mmp-encode-u-map map (nfix i) nibble)
         (mmp-encode-u-map map i nibble)))

Theorem: mmp-encode-u-map-nat-equiv-congruence-on-i

(defthm mmp-encode-u-map-nat-equiv-congruence-on-i
  (implies (acl2::nat-equiv i i-equiv)
           (equal (mmp-encode-u-map map i nibble)
                  (mmp-encode-u-map map i-equiv nibble)))
  :rule-classes :congruence)

Theorem: mmp-encode-u-map-of-nibble-fix-nibble

(defthm mmp-encode-u-map-of-nibble-fix-nibble
  (equal (mmp-encode-u-map map i (nibble-fix nibble))
         (mmp-encode-u-map map i nibble)))

Theorem: mmp-encode-u-map-nibble-equiv-congruence-on-nibble

(defthm mmp-encode-u-map-nibble-equiv-congruence-on-nibble
  (implies (acl2::nibble-equiv nibble nibble-equiv)
           (equal (mmp-encode-u-map map i nibble)
                  (mmp-encode-u-map map i nibble-equiv)))
  :rule-classes :congruence)

Theorem: mmp-encode-u-map-when-not-natp-i

(defthm mmp-encode-u-map-when-not-natp-i
  (implies (and (syntaxp (not (equal i ''0)))
                (not (natp i)))
           (equal (mmp-encode-u-map map i nibble)
                  (mmp-encode-u-map map 0 nibble))))

Theorem: mmp-encode-u-map-when-not-nibblep-nibble

(defthm mmp-encode-u-map-when-not-nibblep-nibble
  (implies (and (syntaxp (not (equal nibble ''0)))
                (not (nibblep nibble)))
           (equal (mmp-encode-u-map map i nibble)
                  (mmp-encode-u-map map i 0))))

Theorem: mmp-encode-u-map-when-not-natp-nibble

(defthm mmp-encode-u-map-when-not-natp-nibble
  (implies (and (syntaxp (not (equal nibble ''0)))
                (not (natp nibble)))
           (equal (mmp-encode-u-map map i nibble)
                  (mmp-encode-u-map map i 0))))