- forall_eq_thm
-
|- (∀s. P s ⇔ Q s) ⇒ ((∀s. P s) ⇔ ∀s. Q s)
- exists_eq_thm
-
|- (∀s. P s ⇔ Q s) ⇒ ((∃s. P s) ⇔ ∃s. Q s)
- true_imp
-
|- ∀t. t ⇒ T
- false_imp
-
|- ∀t. F ⇒ t
- NOT_CLAUSES_X
-
|- ∀t. ¬ ¬t ⇔ t
- NOT_CLAUSES_T
-
|- ¬T ⇔ F
- NOT_CLAUSES_F
-
|- ¬F ⇔ T
- IMP_CONG_conj_strengthen
-
|- ∀x x' y y'. (y ⇒ x' ⇒ x) ∧ (x' ⇒ y' ⇒ y) ⇒ x' ∧ y' ⇒ x ∧ y
- IMP_CONG_conj_weaken
-
|- ∀x x' y y'. (y ⇒ x ⇒ x') ∧ (x' ⇒ y ⇒ y') ⇒ x ∧ y ⇒ x' ∧ y'
- AND_CLAUSES_TX
-
|- ∀t. T ∧ t ⇔ t
- AND_CLAUSES_XT
-
|- ∀t. t ∧ T ⇔ t
- AND_CLAUSES_FX
-
|- ∀t. F ∧ t ⇔ F
- AND_CLAUSES_XF
-
|- ∀t. t ∧ F ⇔ F
- AND_CLAUSES_XX
-
|- ∀t. t ∧ t ⇔ t
- IMP_CONG_disj_strengthen
-
|- ∀x x' y y'. (¬y ⇒ x' ⇒ x) ∧ (¬x' ⇒ y' ⇒ y) ⇒ x' ∨ y' ⇒ x ∨ y
- IMP_CONG_disj_weaken
-
|- ∀x x' y y'. (¬y ⇒ x ⇒ x') ∧ (¬x' ⇒ y ⇒ y') ⇒ x ∨ y ⇒ x' ∨ y'
- OR_CLAUSES_TX
-
|- ∀t. T ∨ t ⇔ T
- OR_CLAUSES_XT
-
|- ∀t. t ∨ T ⇔ T
- OR_CLAUSES_FX
-
|- ∀t. F ∨ t ⇔ t
- OR_CLAUSES_XF
-
|- ∀t. t ∨ F ⇔ t
- OR_CLAUSES_XX
-
|- ∀t. t ∨ t ⇔ t
- IMP_CONG_imp_strengthen
-
|- ∀x x' y y'. (x ⇒ y' ⇒ y) ∧ (¬y' ⇒ x ⇒ x') ⇒ (x' ⇒ y') ⇒ x ⇒ y
- IMP_CONG_imp_weaken
-
|- ∀x x' y y'. (x ⇒ y ⇒ y') ∧ (¬y' ⇒ x' ⇒ x) ⇒ (x ⇒ y) ⇒ x' ⇒ y'
- IMP_CONG_simple_imp_strengthen
-
|- ∀x x' y y'. (x ⇒ x') ∧ (x' ⇒ y' ⇒ y) ⇒ (x' ⇒ y') ⇒ x ⇒ y
- IMP_CONG_simple_imp_weaken
-
|- ∀x x' y y'. (x' ⇒ x) ∧ (x' ⇒ y ⇒ y') ⇒ (x ⇒ y) ⇒ x' ⇒ y'
- IMP_CLAUSES_TX
-
|- ∀t. T ⇒ t ⇔ t
- IMP_CLAUSES_XT
-
|- ∀t. t ⇒ T ⇔ T
- IMP_CLAUSES_FX
-
|- ∀t. F ⇒ t ⇔ T
- IMP_CLAUSES_XX
-
|- ∀t. t ⇒ t ⇔ T
- IMP_CLAUSES_XF
-
|- ∀t. t ⇒ F ⇔ ¬t
- IMP_CONG_cond_simple
-
|- ∀c x x' y y'.
(x' ⇒ x) ∧ (y' ⇒ y) ⇒ (if c then x' else y') ⇒ if c then x else y
- IMP_CONG_cond
-
|- ∀c x x' y y'.
(c ⇒ x' ⇒ x) ∧ (¬c ⇒ y' ⇒ y) ⇒
(if c then x' else y') ⇒
if c then x else y
- COND_CLAUSES_CT
-
|- ∀t1 t2. (if T then t1 else t2) = t1
- COND_CLAUSES_CF
-
|- ∀t1 t2. (if F then t1 else t2) = t2
- COND_CLAUSES_ID
-
|- ∀b t. (if b then t else t) = t
- COND_CLAUSES_TT
-
|- ∀c x. (if c then T else x) ⇔ ¬c ⇒ x
- COND_CLAUSES_FT
-
|- ∀c x. (if c then x else T) ⇔ c ⇒ x
- COND_CLAUSES_TF
-
|- ∀c x. (if c then F else x) ⇔ ¬c ∧ x
- COND_CLAUSES_FF
-
|- ∀c x. (if c then x else F) ⇔ c ∧ x
- ASM_MARKER_THM
-
|- ∀y x. ASM_MARKER y x ⇔ x