The Theory misc
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
fill= (λ b x1 x2
fill• ε 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
fill• (if a then t1 else t2)
fill= (ε 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
fill• ¬ (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
fill• ((T ⇔ t) ⇔ t)
fill∧ ((t ⇔ T) ⇔ t)
fill∧ ((F ⇔ t) ⇔ ¬ t)
fill∧ ((t ⇔ F) ⇔ ¬ t)
¬_rewrite_thm
⊢ ∀ t• (¬ ¬ t ⇔ t) ∧ (¬ T ⇔ F) ∧ (¬ F ⇔ T)
∧_rewrite_thm
⊢ ∀ t
fill• (T ∧ t ⇔ t)
fill∧ (t ∧ T ⇔ t)
fill∧ ¬ (F ∧ t)
fill∧ ¬ (t ∧ F)
fill∧ (t ∧ t ⇔ t)
∨_rewrite_thm
⊢ ∀ t
fill• (T ∨ t)
fill∧ (t ∨ T)
fill∧ (F ∨ t ⇔ t)
fill∧ (t ∨ F ⇔ t)
fill∧ (t ∨ t ⇔ t)
⇒_rewrite_thm
⊢ ∀ t
fill• (T ⇒ t ⇔ t)
fill∧ (F ⇒ t ⇔ T)
fill∧ (t ⇒ T ⇔ T)
fill∧ (t ⇒ t ⇔ T)
fill∧ (t ⇒ F ⇔ ¬ t)
if_rewrite_thm
⊢ ∀ t1 t2
fill• (if T then t1 else t2) = t1
fill∧ (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
fill• (∃ f• TypeDefn pred f)
fill⇒ (∃ abs rep
fill• (∀ a• abs (rep a) = a)
fill∧ (∀ r• pred r ⇔ rep (abs r) = r))
fun_rel_thm
⊢ ∀ r
fill• (∃ f• ∀ x y• f x = y ⇔ r x y)
fill⇔ (∀ x• ∃ y• r x y ∧ (∀ z• r x z ⇒ z = y))

up quick index

privacy policy

Created:

V