| Parents |
| init |
| Children |
| pair |
| Constants |
|
Arbitrary
|
'a |
|
$∃1
|
('a → BOOL) → BOOL |
|
Let
|
('a → 'b) → 'a → 'b |
|
Cond
|
BOOL → 'a → 'a → 'a |
|
pp'TS
|
BOOL → BOOL |
| Aliases |
|
⇔
|
$= : BOOL → BOOL → BOOL |
| Fixity |
| Binder: | ∃1 |
Right Infix 10: |
⇔ |
| Terminators |
| ∃1 | ⇔ |
| Definitions |
|
∃1
∃1_def
|
⊢ $∃1 = (λ P• ∃ t• P t ∧ (∀ x• P x ⇒ x = t)) |
|
Let
let_def
|
⊢ Let = (λ f x• f x) |
|
Cond
cond_def
|
⊢ Cond  = (λ b x1 x2 • ε x• ((b ⇔ T) ⇒ x = x1) ∧ ((b ⇔ F) ⇒ x = x2))
|
|
pp'TS
pp'ts_def
|
⊢ ∀ x• pp'TS x ⇔ x |
| Theorems |
|
t_thm
|
⊢ T |
|
∨_thm
|
⊢ ∀ t1 t2• t1 ∨ t2 ⇔ (∀ b• (t1 ⇒ b) ⇒ (t2 ⇒ b) ⇒ b) |
|
¬_thm
|
⊢ ∀ t• ¬ t ⇔ t ⇒ F |
|
f_thm
|
⊢ ¬ F |
|
¬_t_thm
|
⊢ ¬ T ⇔ F |
|
∧_thm
|
⊢ ∀ t1 t2• t1 ∧ t2 ⇔ (∀ b• (t1 ⇒ t2 ⇒ b) ⇒ b) |
|
¬_thm1
|
⊢ ∀ t• ¬ t ⇔ t ⇔ F |
|
∃_intro_thm
|
⊢ ∀ P x• P x ⇒ $∃ P |
|
cond_thm
|
⊢ ∀ a t1 t2 • (if a then t1 else t2) = (ε x• ((a ⇔ T) ⇒ x = t1) ∧ ((a ⇔ F) ⇒ x = t2))
|
|
¬_∀_thm
|
⊢ ∀ p• ¬ $∀ p ⇔ (∃ x• ¬ p x) |
|
¬_∃_thm
|
⊢ ∀ p• ¬ $∃ p ⇔ (∀ x• ¬ p x) |
|
∃1_thm
|
⊢ ∀ P• $∃1 P ⇔ (∃ t• P t ∧ (∀ x• P x ⇒ x = t)) |
|
⇔_thm
|
⊢ ∀ a b• (a ⇔ b) ⇔ (a ⇒ b) ∧ (b ⇒ a) |
|
⇒_thm
|
⊢ ∀ a b• a ⇒ b ⇔ ¬ a ∨ b |
|
¬_¬_thm
|
⊢ ∀ a• ¬ ¬ a ⇔ a |
|
¬_∨_thm
|
⊢ ∀ a b• ¬ (a ∨ b) ⇔ ¬ a ∧ ¬ b |
|
¬_∧_thm
|
⊢ ∀ a b• ¬ (a ∧ b) ⇔ ¬ a ∨ ¬ b |
|
¬_⇒_thm
|
⊢ ∀ a b• ¬ (a ⇒ b) ⇔ a ∧ ¬ b |
|
¬_⇔_thm
|
⊢ ∀ a b• ¬ (a ⇔ b) ⇔ a ∧ ¬ b ∨ b ∧ ¬ a |
|
¬_f_thm
|
⊢ ¬ F ⇔ T |
|
¬_if_thm
|
⊢ ∀ a b c • ¬ (if a then b else c) ⇔ (if a then ¬ b else ¬ c)
|
|
if_thm
|
⊢ ∀ a b c• (if a then b else c) ⇔ a ∧ b ∨ ¬ a ∧ c |
|
eq_rewrite_thm
|
⊢ ∀ x• x = x ⇔ T |
|
⇔_rewrite_thm
|
⊢ ∀ t
• ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬ t) ∧ ((t ⇔ F) ⇔ ¬ t)
|
|
¬_rewrite_thm
|
⊢ ∀ t• (¬ ¬ t ⇔ t) ∧ (¬ T ⇔ F) ∧ (¬ F ⇔ T) |
|
∧_rewrite_thm
|
⊢ ∀ t
• (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ ¬ (F ∧ t) ∧ ¬ (t ∧ F) ∧ (t ∧ t ⇔ t)
|
|
∨_rewrite_thm
|
⊢ ∀ t
• (T ∨ t) ∧ (t ∨ T) ∧ (F ∨ t ⇔ t) ∧ (t ∨ F ⇔ t) ∧ (t ∨ t ⇔ t)
|
|
⇒_rewrite_thm
|
⊢ ∀ t
• (T ⇒ t ⇔ t) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ T ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬ t)
|
|
if_rewrite_thm
|
⊢ ∀ t1 t2
• (if T then t1 else t2) = t1 ∧ (if F then t1 else t2) = t2
|
|
∀_rewrite_thm
|
⊢ ∀ t• (∀ x• t) ⇔ t |
|
∃_rewrite_thm
|
⊢ ∀ t• (∃ x• t) ⇔ t |
|
β_rewrite_thm
|
⊢ ∀ t1 t2• (λ x• t1) t2 = t1 |
|
one_one_thm
|
⊢ ∀ f• OneOne f ⇔ (∀ x y• f x = f y ⇔ x = y) |
|
ext_thm
|
⊢ ∀ f g• f = g ⇔ (∀ x• f x = g x) |
|
type_lemmas_thm
|
⊢ ∀ pred
• (∃ f• TypeDefn pred f) ⇒ (∃ abs rep • (∀ a• abs (rep a) = a) ∧ (∀ r• pred r ⇔ rep (abs r) = r))
|
|
fun_rel_thm
|
⊢ ∀ r • (∃ f• ∀ x y• f x = y ⇔ r x y) ⇔ (∀ x• ∃ y• r x y ∧ (∀ z• r x z ⇒ z = y))
|
