| name | bool-choice-induct |
| version | 1.0 |
| description | bool-choice-induct |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2011-02-19 |
| show | Data.Bool |
⊦ ∀P. P F ∧ P T ⇒ ∀x. P x
⊦ ∀a b. ∃f. f F = a ∧ f T = b
⊦ T
⊦ (∀) = λP. P = λx. T
⊦ ∀x. x = x ⇔ T
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀t1 t2. (if T then t1 else t2) = t1 ∧ (if F then t1 else t2) = t2
⊦ ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)