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 = (λ 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))