Package axiom: Basic axioms

Information

name	axiom
version	1.0
description	Basic axioms
author	Joe Hurd <joe@gilith.com>
license	MIT
show	Data.Bool Function

Files

Package tarball axiom-1.0.tgz
Theory file axiom.thy (included in the package tarball)

Theorems

⊦ ∀t. (λx. t x) = t

⊦ ∃f. injective f ∧ ¬surjective f

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

Input Type Operators

→
bool
ind

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ¬
  - select
Function
- injective
- surjective

Assumptions

⊦ ∀t. (λx. t x) = t

⊦ ∃f. injective f ∧ ¬surjective f

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