Theory normalFormsContext

⊢ ∀x y z. (x ⇔ y ∧ z) ⇔ (y ∨ ¬x) ∧ (z ∨ ¬x) ∧ (x ∨ ¬y ∨ ¬z)

⊢ ∀t. t ∧ T ⇔ t

⊢ ∀a b. (a ⇒ b) ∧ (¬a ⇒ b) ⇒ b

⊢ ∀a b. a ∧ b ⇔ if a then b else F

⊢ ∀c. (if c then T else F) ⇔ c

⊢ ∀a b c x y.
    (if if a then b else c then x else y) =
    if a then if b then x else y else if c then x else y

⊢ ∀a b. (a ⇔ b) ⇔ if a then b else ¬b

⊢ ∀a. (if a then T else F) ⇔ a

⊢ ∀c a b. (if c then a else b) ⇔ (¬c ∨ a) ∧ (c ∨ b)

⊢ ∀a b. a ⇒ b ⇔ if a then b else T

⊢ ∀a. ¬a ⇔ if a then F else T

⊢ ∀a b. a ∨ b ⇔ if a then T else b

⊢ ∀a f g. (if a then f a else g a) = if a then f T else g F

⊢ ∀a b b'. (¬a ⇒ (b ⇔ b')) ⇒ ¬a ⇒ (a ∨ b ⇔ b')

⊢ ∀x y. ¬(x ∧ y) ⇔ ¬x ∨ ¬y

⊢ ∀x y. ¬(x ∨ y) ⇔ ¬x ∧ ¬y

⊢ ∀a b b'. (¬a ⇒ (b ⇔ b')) ⇒ (a ∨ b ⇔ a ∨ b')

⊢ ∀x y z.
    (x ⇔ (y ⇔ z)) ⇔
    (z ∨ ¬y ∨ ¬x) ∧ (y ∨ ¬z ∨ ¬x) ∧ (x ∨ ¬y ∨ ¬z) ∧ (x ∨ y ∨ z)

⊢ ∀x y. (x ⇔ y) ⇔ (x ∨ ¬y) ∧ (¬x ∨ y)

⊢ ∀s t. s = (λx. t x) ⇔ ∀x. s x = t x

⊢ ∀f g. (∀x. f x = g x) ⇔ f = g

⊢ ∀x y. x ⇒ y ⇔ y ∨ ¬x

⊢ ∀s t. (λx. s x) = t ⇔ ∀x. s x = t x

⊢ ∀x y. (λv. x v y) = flip x y

⊢ (λv. v) = I

⊢ ∀x. (λv. x) = K x

⊢ ∀x y. (λv. x v (y v)) = S x y

⊢ ∀x y. (λv. x (y v)) = x ∘ y

⊢ ∀c a b. ¬(if c then a else b) ⇔ (¬c ∨ ¬a) ∧ (c ∨ ¬b)

⊢ ∀a b. (a ⇎ b) ⇔ (a ⇔ ¬b)

⊢ ∀x y. (x ⇎ y) ⇔ (x ∨ y) ∧ (¬x ∨ ¬y)

⊢ (a ∧ b) ∧ c ⇔ b ∧ a ∧ c

⊢ (a ∨ b) ∨ c ⇔ b ∨ a ∨ c

⊢ (a ⇔ b) ∧ (c ⇔ d) ⇒ (a ∧ c ⇔ b ∧ d)

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

⊢ ∀p. $?! p ⇔ (∃x. p x) ∧ ∀x y. p x ∧ p y ⇒ x = y

⊢ ∀p. ¬$?! p ⇔ (∀x. ¬p x) ∨ ∃x y. p x ∧ p y ∧ x ≠ y

⊢ ¬F ⇔ T

⊢ ∀p m. ¬RES_EXISTS p m ⇔ ∀x. x ∈ p ⇒ ¬m x

⊢ ∀p m. ¬RES_FORALL p m ⇔ ∃x. x ∈ p ∧ ¬m x

⊢ ¬T ⇔ F

⊢ ∀x y z. (x ⇔ y ∨ z) ⇔ (y ∨ z ∨ ¬x) ∧ (x ∨ ¬y) ∧ (x ∨ ¬z)

⊢ ∀t. t ∨ F ⇔ t

⊢ ∀t. t ∨ T ⇔ T

⊢ (¬$! P ⇔ ∃x. ¬P x) ∧ (¬$? P ⇔ ∀x. ¬P x) ∧
  (¬$?! P ⇔ (∀x. ¬P x) ∨ ∃x y. P x ∧ P y ∧ y ≠ x)

⊢ $?! P ⇔ (∃x. P x) ∧ ∀x y. ¬P x ∨ ¬P y ∨ y = x

⊢ ∀p m. RES_EXISTS p m ⇔ ∃x. x ∈ p ∧ m x

⊢ ∀p m. RES_FORALL p m ⇔ ∀x. x ∈ p ⇒ m x

⊢ ((b ⇔ F) ⇒ (x ⇔ x0)) ∧ ((b ⇔ T) ⇒ (x ⇔ x1)) ⇒ (x ⇔ b ∧ x1 ∨ ¬b ∧ x0)

⊢ ((b ⇔ F) ⇒ (x ⇔ x0)) ∧ ((b ⇔ T) ⇒ (x ⇔ x1)) ⇒ (x ⇔ (¬b ∨ x1) ∧ (b ∨ x0))

⊢ ∀t. T ∧ t ⇔ t

⊢ ∀t. T ∨ t ⇔ T