		Search-engine friendly clone of the ACL2 documentation.

Rlp-decodability

Rlp-encode-scalar-injectivity-proof

Injectivity of rlp-encode-scalar, over the encodable scalars.

This is also formulated similarly to the other injectivity theorems. It readily follows from the injectivity of rlp-encode-bytes.

Definitions and Theorems

Theorem: rlp-encode-scalar-injective

(defthm rlp-encode-scalar-injective
  (implies (and (not (mv-nth 0 (rlp-encode-scalar x)))
                (not (mv-nth 0 (rlp-encode-scalar y))))
           (equal (equal (mv-nth 1 (rlp-encode-scalar x))
                         (mv-nth 1 (rlp-encode-scalar y)))
                  (equal (nfix x) (nfix y)))))