• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
        • Mmp-trees
          • Mmp-encode-n/c
          • Mmp-encode-c-max
          • Mmp-encode
          • Mmp-write
          • Mmp-decode
          • Mmp-encode-u-map
          • Nibblelist-bytelist-map-sup-len-key
          • Mmp-encode-c-forall
          • Mmp-read
          • Mmp-encoding-p
          • Bytelist-to-nibblelist-keys
          • Mmp-encode-c-exists
          • Bytelist-bytelist-map
          • Nibblelist-bytelist-map
        • Semaphore
        • Database
        • Cryptography
        • Rlp
        • Transactions
        • Hex-prefix
        • Basics
        • Addresses
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Mmp-trees

Mmp-encode-c-exists

Existentially 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 and x is the argument x.

If this existentially quantified formula holds, the length of every key in the map is greater than or equal to x, because this follows from the universally quantified formula mmp-encode-c-forall.

Definitions and Theorems

Theorem: mmp-encode-c-exists-suff

(defthm mmp-encode-c-exists-suff
  (implies (and (nibble-listp l)
                (= (len l) (nfix x))
                (mmp-encode-c-forall map x l))
           (mmp-encode-c-exists map x)))

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

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

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

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

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

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

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

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

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

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

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

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