Package axiom-choice: axiom-choice

Information

Files

• Package tarball axiom-choice-1.3.tgz
• Theory file axiom-choice.thy (included in the package tarball)

Theorem

⊦ ∀p x. p x ⇒ p ((select) p)

Input Type Operators

• →
• bool

Input Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • T

Assumptions

⊦ T ⇔ (λp. p) = λp. p

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

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

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

⊦ let a d =
      let e g =
          (let h = d g in
           λi.
             (let j = h in
              λk. (λl. l j k) = λm. m ((λc. c) = λc. c) ((λc. c) = λc. c))
               i ⇔ h) (d ((select) d)) in
      e = (λf. (λc. c) = λc. c) in
  a = λb. (λc. c) = λc. c