Package map-reduce-bit3x3-product: Correctness statement for the map reduce 3x3 bit matrix example

Information

Files

• Package tarball map-reduce-bit3x3-product-1.5.tgz
• Theory file map-reduce-bit3x3-product.thy (included in the package tarball)

Defined Constants

• Bit
  • Bit.*
  • Bit.+
• Bit3
  • Bit3.dot
• Bit3x3
  • Bit3x3.*
  • Bit3x3.identity
  • Bit3x3.product

Theorems

⊦ Bit3x3.product = foldl Bit3x3.* Bit3x3.identity

⊦ ∀a b. Bit.* a b ⇔ a ∧ b

⊦ ∀a b. Bit.+ a b ⇔ ¬(a ⇔ b)

⊦ ∀l₁ l₂.
    Bit3x3.product (l₁ @ l₂) =
    Bit3x3.* (Bit3x3.product l₁) (Bit3x3.product l₂)

⊦ Bit3x3.identity = ((⊤, ⊥, ⊥), (⊥, ⊤, ⊥), ⊥, ⊥, ⊤)

⊦ ∀a₁ a₂ a₃ b₁ b₂ b₃.
    Bit3.dot (a₁, a₂, a₃) (b₁, b₂, b₃) ⇔
    Bit.+ (Bit.* a₁ b₁) (Bit.+ (Bit.* a₂ b₂) (Bit.* a₃ b₃))

⊦ ∀a.
    ∃a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃.
      a = ((a₁₁, a₁₂, a₁₃), (a₂₁, a₂₂, a₂₃), a₃₁, a₃₂, a₃₃)

⊦ ∀a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃.
    Bit3x3.* ((a₁₁, a₁₂, a₁₃), (a₂₁, a₂₂, a₂₃), a₃₁, a₃₂, a₃₃)
      ((b₁₁, b₁₂, b₁₃), (b₂₁, b₂₂, b₂₃), b₃₁, b₃₂, b₃₃) =
    ((Bit3.dot (a₁₁, a₁₂, a₁₃) (b₁₁, b₂₁, b₃₁),
      Bit3.dot (a₁₁, a₁₂, a₁₃) (b₁₂, b₂₂, b₃₂),
      Bit3.dot (a₁₁, a₁₂, a₁₃) (b₁₃, b₂₃, b₃₃)),
     (Bit3.dot (a₂₁, a₂₂, a₂₃) (b₁₁, b₂₁, b₃₁),
      Bit3.dot (a₂₁, a₂₂, a₂₃) (b₁₂, b₂₂, b₃₂),
      Bit3.dot (a₂₁, a₂₂, a₂₃) (b₁₃, b₂₃, b₃₃)),
     Bit3.dot (a₃₁, a₃₂, a₃₃) (b₁₁, b₂₁, b₃₁),
     Bit3.dot (a₃₁, a₃₂, a₃₃) (b₁₂, b₂₂, b₃₂),
     Bit3.dot (a₃₁, a₃₂, a₃₃) (b₁₃, b₂₃, b₃₃))

Input Type Operators

• →
• bool
• Data
  • List
    • list
  • Pair
    • ×

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ¬
    • ⊥
    • ⊤
  • List
    • @
    • foldl
  • Pair
    • ,
    • fst
    • snd

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀a. ∃x. x = a

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. t ∧ ⊥ ⇔ ⊥

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀x y. fst (x, y) = x

⊦ ∀x y. snd (x, y) = y

⊦ ∀p. ∃x y. p = (x, y)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀t₁ t₂. t₁ ∧ t₂ ⇔ t₂ ∧ t₁

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀p a. (∃x. a = x ∧ p x) ⇔ p a

⊦ ∀p q. (∃x. p x) ⇒ q ⇔ ∀x. p x ⇒ q

⊦ ∀t₁ t₂ t₃. (t₁ ∧ t₂) ∧ t₃ ⇔ t₁ ∧ t₂ ∧ t₃

⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b

⊦ ∀g f b l₁ l₂.
    (∀s. g s b = s) ∧ (∀s₁ s₂ x. g s₁ (f s₂ x) = f (g s₁ s₂) x) ⇒
    foldl f b (l₁ @ l₂) = g (foldl f b l₁) (foldl f b l₂)

⊦ ((¬(a₁₁ ∧ ¬(a11' ∧ a11'' ⇔ ¬(a12' ∧ a21'' ⇔ a13' ∧ a31'')) ⇔
       ¬(a₁₂ ∧ ¬(a21' ∧ a11'' ⇔ ¬(a22' ∧ a21'' ⇔ a23' ∧ a31'')) ⇔
          a₁₃ ∧ ¬(a31' ∧ a11'' ⇔ ¬(a32' ∧ a21'' ⇔ a33' ∧ a31'')))) ⇔
    ¬(¬(a₁₁ ∧ a11' ⇔ ¬(a₁₂ ∧ a21' ⇔ a₁₃ ∧ a31')) ∧ a11'' ⇔
       ¬(¬(a₁₁ ∧ a12' ⇔ ¬(a₁₂ ∧ a22' ⇔ a₁₃ ∧ a32')) ∧ a21'' ⇔
          ¬(a₁₁ ∧ a13' ⇔ ¬(a₁₂ ∧ a23' ⇔ a₁₃ ∧ a33')) ∧ a31''))) ∧
   (¬(a₁₁ ∧ ¬(a11' ∧ a12'' ⇔ ¬(a12' ∧ a22'' ⇔ a13' ∧ a32'')) ⇔
       ¬(a₁₂ ∧ ¬(a21' ∧ a12'' ⇔ ¬(a22' ∧ a22'' ⇔ a23' ∧ a32'')) ⇔
          a₁₃ ∧ ¬(a31' ∧ a12'' ⇔ ¬(a32' ∧ a22'' ⇔ a33' ∧ a32'')))) ⇔
    ¬(¬(a₁₁ ∧ a11' ⇔ ¬(a₁₂ ∧ a21' ⇔ a₁₃ ∧ a31')) ∧ a12'' ⇔
       ¬(¬(a₁₁ ∧ a12' ⇔ ¬(a₁₂ ∧ a22' ⇔ a₁₃ ∧ a32')) ∧ a22'' ⇔
          ¬(a₁₁ ∧ a13' ⇔ ¬(a₁₂ ∧ a23' ⇔ a₁₃ ∧ a33')) ∧ a32''))) ∧
   (¬(a₁₁ ∧ ¬(a11' ∧ a13'' ⇔ ¬(a12' ∧ a23'' ⇔ a13' ∧ a33'')) ⇔
       ¬(a₁₂ ∧ ¬(a21' ∧ a13'' ⇔ ¬(a22' ∧ a23'' ⇔ a23' ∧ a33'')) ⇔
          a₁₃ ∧ ¬(a31' ∧ a13'' ⇔ ¬(a32' ∧ a23'' ⇔ a33' ∧ a33'')))) ⇔
    ¬(¬(a₁₁ ∧ a11' ⇔ ¬(a₁₂ ∧ a21' ⇔ a₁₃ ∧ a31')) ∧ a13'' ⇔
       ¬(¬(a₁₁ ∧ a12' ⇔ ¬(a₁₂ ∧ a22' ⇔ a₁₃ ∧ a32')) ∧ a23'' ⇔
          ¬(a₁₁ ∧ a13' ⇔ ¬(a₁₂ ∧ a23' ⇔ a₁₃ ∧ a33')) ∧ a33'')))) ∧
  ((¬(a₂₁ ∧ ¬(a11' ∧ a11'' ⇔ ¬(a12' ∧ a21'' ⇔ a13' ∧ a31'')) ⇔
       ¬(a₂₂ ∧ ¬(a21' ∧ a11'' ⇔ ¬(a22' ∧ a21'' ⇔ a23' ∧ a31'')) ⇔
          a₂₃ ∧ ¬(a31' ∧ a11'' ⇔ ¬(a32' ∧ a21'' ⇔ a33' ∧ a31'')))) ⇔
    ¬(¬(a₂₁ ∧ a11' ⇔ ¬(a₂₂ ∧ a21' ⇔ a₂₃ ∧ a31')) ∧ a11'' ⇔
       ¬(¬(a₂₁ ∧ a12' ⇔ ¬(a₂₂ ∧ a22' ⇔ a₂₃ ∧ a32')) ∧ a21'' ⇔
          ¬(a₂₁ ∧ a13' ⇔ ¬(a₂₂ ∧ a23' ⇔ a₂₃ ∧ a33')) ∧ a31''))) ∧
   (¬(a₂₁ ∧ ¬(a11' ∧ a12'' ⇔ ¬(a12' ∧ a22'' ⇔ a13' ∧ a32'')) ⇔
       ¬(a₂₂ ∧ ¬(a21' ∧ a12'' ⇔ ¬(a22' ∧ a22'' ⇔ a23' ∧ a32'')) ⇔
          a₂₃ ∧ ¬(a31' ∧ a12'' ⇔ ¬(a32' ∧ a22'' ⇔ a33' ∧ a32'')))) ⇔
    ¬(¬(a₂₁ ∧ a11' ⇔ ¬(a₂₂ ∧ a21' ⇔ a₂₃ ∧ a31')) ∧ a12'' ⇔
       ¬(¬(a₂₁ ∧ a12' ⇔ ¬(a₂₂ ∧ a22' ⇔ a₂₃ ∧ a32')) ∧ a22'' ⇔
          ¬(a₂₁ ∧ a13' ⇔ ¬(a₂₂ ∧ a23' ⇔ a₂₃ ∧ a33')) ∧ a32''))) ∧
   (¬(a₂₁ ∧ ¬(a11' ∧ a13'' ⇔ ¬(a12' ∧ a23'' ⇔ a13' ∧ a33'')) ⇔
       ¬(a₂₂ ∧ ¬(a21' ∧ a13'' ⇔ ¬(a22' ∧ a23'' ⇔ a23' ∧ a33'')) ⇔
          a₂₃ ∧ ¬(a31' ∧ a13'' ⇔ ¬(a32' ∧ a23'' ⇔ a33' ∧ a33'')))) ⇔
    ¬(¬(a₂₁ ∧ a11' ⇔ ¬(a₂₂ ∧ a21' ⇔ a₂₃ ∧ a31')) ∧ a13'' ⇔
       ¬(¬(a₂₁ ∧ a12' ⇔ ¬(a₂₂ ∧ a22' ⇔ a₂₃ ∧ a32')) ∧ a23'' ⇔
          ¬(a₂₁ ∧ a13' ⇔ ¬(a₂₂ ∧ a23' ⇔ a₂₃ ∧ a33')) ∧ a33'')))) ∧
  (¬(a₃₁ ∧ ¬(a11' ∧ a11'' ⇔ ¬(a12' ∧ a21'' ⇔ a13' ∧ a31'')) ⇔
      ¬(a₃₂ ∧ ¬(a21' ∧ a11'' ⇔ ¬(a22' ∧ a21'' ⇔ a23' ∧ a31'')) ⇔
         a₃₃ ∧ ¬(a31' ∧ a11'' ⇔ ¬(a32' ∧ a21'' ⇔ a33' ∧ a31'')))) ⇔
   ¬(¬(a₃₁ ∧ a11' ⇔ ¬(a₃₂ ∧ a21' ⇔ a₃₃ ∧ a31')) ∧ a11'' ⇔
      ¬(¬(a₃₁ ∧ a12' ⇔ ¬(a₃₂ ∧ a22' ⇔ a₃₃ ∧ a32')) ∧ a21'' ⇔
         ¬(a₃₁ ∧ a13' ⇔ ¬(a₃₂ ∧ a23' ⇔ a₃₃ ∧ a33')) ∧ a31''))) ∧
  (¬(a₃₁ ∧ ¬(a11' ∧ a12'' ⇔ ¬(a12' ∧ a22'' ⇔ a13' ∧ a32'')) ⇔
      ¬(a₃₂ ∧ ¬(a21' ∧ a12'' ⇔ ¬(a22' ∧ a22'' ⇔ a23' ∧ a32'')) ⇔
         a₃₃ ∧ ¬(a31' ∧ a12'' ⇔ ¬(a32' ∧ a22'' ⇔ a33' ∧ a32'')))) ⇔
   ¬(¬(a₃₁ ∧ a11' ⇔ ¬(a₃₂ ∧ a21' ⇔ a₃₃ ∧ a31')) ∧ a12'' ⇔
      ¬(¬(a₃₁ ∧ a12' ⇔ ¬(a₃₂ ∧ a22' ⇔ a₃₃ ∧ a32')) ∧ a22'' ⇔
         ¬(a₃₁ ∧ a13' ⇔ ¬(a₃₂ ∧ a23' ⇔ a₃₃ ∧ a33')) ∧ a32''))) ∧
  (¬(a₃₁ ∧ ¬(a11' ∧ a13'' ⇔ ¬(a12' ∧ a23'' ⇔ a13' ∧ a33'')) ⇔
      ¬(a₃₂ ∧ ¬(a21' ∧ a13'' ⇔ ¬(a22' ∧ a23'' ⇔ a23' ∧ a33'')) ⇔
         a₃₃ ∧ ¬(a31' ∧ a13'' ⇔ ¬(a32' ∧ a23'' ⇔ a33' ∧ a33'')))) ⇔
   ¬(¬(a₃₁ ∧ a11' ⇔ ¬(a₃₂ ∧ a21' ⇔ a₃₃ ∧ a31')) ∧ a13'' ⇔
      ¬(¬(a₃₁ ∧ a12' ⇔ ¬(a₃₂ ∧ a22' ⇔ a₃₃ ∧ a32')) ∧ a23'' ⇔
         ¬(a₃₁ ∧ a13' ⇔ ¬(a₃₂ ∧ a23' ⇔ a₃₃ ∧ a33')) ∧ a33'')))

OpenTheory package summary generated by opentheory 1.2 (release 20120929)