Theory ConseqConv

⊢ ASM_MARKER = (λy x. x)

⊢ ∀t. F ∧ t ⇔ F

⊢ ∀t. T ∧ t ⇔ t

⊢ ∀t. t ∧ F ⇔ F

⊢ ∀t. t ∧ T ⇔ t

⊢ ∀t. t ∧ t ⇔ t

⊢ ∀y x. ASM_MARKER y x ⇔ x

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

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

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

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

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

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

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

⊢ ∀t. F ⇒ t ⇔ T

⊢ ∀t. T ⇒ t ⇔ t

⊢ ∀t. t ⇒ F ⇔ ¬t

⊢ ∀t. t ⇒ T ⇔ T

⊢ ∀t. t ⇒ t ⇔ T

⊢ ∀c x x' y y'.
    (c ⇒ x' ⇒ x) ∧ (¬c ⇒ y' ⇒ y) ⇒
    (if c then x' else y') ⇒
    if c then x else y

⊢ ∀c x x' y y'.
    (x' ⇒ x) ∧ (y' ⇒ y) ⇒ (if c then x' else y') ⇒ if c then x else y

⊢ ∀x x' y y'. (y ⇒ x' ⇒ x) ∧ (x' ⇒ y' ⇒ y) ⇒ x' ∧ y' ⇒ x ∧ y

⊢ ∀x x' y y'. (y ⇒ x ⇒ x') ∧ (x' ⇒ y ⇒ y') ⇒ x ∧ y ⇒ x' ∧ y'

⊢ ∀x x' y y'. (¬y ⇒ x' ⇒ x) ∧ (¬x' ⇒ y' ⇒ y) ⇒ x' ∨ y' ⇒ x ∨ y

⊢ ∀x x' y y'. (¬y ⇒ x ⇒ x') ∧ (¬x' ⇒ y ⇒ y') ⇒ x ∨ y ⇒ x' ∨ y'

⊢ ∀x x' y y'. (x ⇒ y' ⇒ y) ∧ (¬y' ⇒ x ⇒ x') ⇒ (x' ⇒ y') ⇒ x ⇒ y

⊢ ∀x x' y y'. (x ⇒ y ⇒ y') ∧ (¬y' ⇒ x' ⇒ x) ⇒ (x ⇒ y) ⇒ x' ⇒ y'

⊢ ∀x x' y y'. (x ⇒ x') ∧ (x' ⇒ y' ⇒ y) ⇒ (x' ⇒ y') ⇒ x ⇒ y

⊢ ∀x x' y y'. (x' ⇒ x) ∧ (x' ⇒ y ⇒ y') ⇒ (x ⇒ y) ⇒ x' ⇒ y'

⊢ ¬F ⇔ T

⊢ ¬T ⇔ F

⊢ ∀t. ¬¬t ⇔ t

⊢ ∀t. F ∨ t ⇔ t

⊢ ∀t. T ∨ t ⇔ T

⊢ ∀t. t ∨ F ⇔ t

⊢ ∀t. t ∨ T ⇔ T

⊢ ∀t. t ∨ t ⇔ t

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

⊢ ∀t. F ⇒ t

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

⊢ ∀t. t ⇒ T