Package map-reduce-bit3x3-sat: SAT problem for the map reduce 3x3 bit matrix example

Information

name	map-reduce-bit3x3-sat
version	1.3
description	SAT problem for the map reduce 3x3 bit matrix example
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-01-29
requires	base
show	Data.Bool

Files

Package tarball map-reduce-bit3x3-sat-1.3.tgz
Theory file map-reduce-bit3x3-sat.thy (included in the package tarball)

Theorem

⊦ ((¬(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'')))

Input Type Operators

→
bool

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∨
  - ¬
  - ⊥
  - ⊤

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀t. t ⇒ t

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

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

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

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r