Theory "ConseqConv"

Signature

Definitions

ASM_MARKER_DEF

⊢ ASM_MARKER = (λy x. x)

Theorems

AND_CLAUSES_FX

⊢ ∀t. F ∧ t ⇔ F

AND_CLAUSES_TX

⊢ ∀t. T ∧ t ⇔ t

AND_CLAUSES_XF

⊢ ∀t. t ∧ F ⇔ F

AND_CLAUSES_XT

⊢ ∀t. t ∧ T ⇔ t

AND_CLAUSES_XX

⊢ ∀t. t ∧ t ⇔ t

ASM_MARKER_THM

⊢ ∀y x. ASM_MARKER y x ⇔ x

COND_CLAUSES_CF

⊢ ∀t1 t2. (if F then t1 else t2) = t2

COND_CLAUSES_CT

⊢ ∀t1 t2. (if T then t1 else t2) = t1

COND_CLAUSES_FF

⊢ ∀c x. (if c then x else F) ⇔ c ∧ x

COND_CLAUSES_FT

⊢ ∀c x. (if c then x else T) ⇔ c ⇒ x

COND_CLAUSES_ID

⊢ ∀b t. (if b then t else t) = t

COND_CLAUSES_TF

⊢ ∀c x. (if c then F else x) ⇔ ¬c ∧ x

COND_CLAUSES_TT

⊢ ∀c x. (if c then T else x) ⇔ ¬c ⇒ x

IMP_CLAUSES_FX

⊢ ∀t. F ⇒ t ⇔ T

IMP_CLAUSES_TX

⊢ ∀t. T ⇒ t ⇔ t

IMP_CLAUSES_XF

⊢ ∀t. t ⇒ F ⇔ ¬t

IMP_CLAUSES_XT

⊢ ∀t. t ⇒ T ⇔ T

IMP_CLAUSES_XX

⊢ ∀t. t ⇒ t ⇔ T

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

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_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'

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'

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'

NOT_CLAUSES_F

⊢ ¬F ⇔ T

NOT_CLAUSES_T

⊢ ¬T ⇔ F

NOT_CLAUSES_X

⊢ ∀t. ¬¬t ⇔ t

OR_CLAUSES_FX

⊢ ∀t. F ∨ t ⇔ t

OR_CLAUSES_TX

⊢ ∀t. T ∨ t ⇔ T

OR_CLAUSES_XF

⊢ ∀t. t ∨ F ⇔ t

OR_CLAUSES_XT

⊢ ∀t. t ∨ T ⇔ T

OR_CLAUSES_XX

⊢ ∀t. t ∨ t ⇔ t

exists_eq_thm

⊢ (∀s. P s ⇔ Q s) ⇒ ((∃s. P s) ⇔ ∃s. Q s)

false_imp

⊢ ∀t. F ⇒ t

forall_eq_thm

⊢ (∀s. P s ⇔ Q s) ⇒ ((∀s. P s) ⇔ ∀s. Q s)

true_imp

⊢ ∀t. t ⇒ T