13 lines
621 B
Text
13 lines
621 B
Text
-- Testing the unit pre-processor
|
||
|
||
open simplifier.unit_simp
|
||
set_option simplify.max_steps 10000
|
||
variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop}
|
||
variables {A B C D E F G : Prop}
|
||
variables {X : Type.{1}}
|
||
|
||
example (H : A ∨ B → E) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
|
||
example (H : A ∨ B → E) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
|
||
example (H : A ∨ B → E ∧ F) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
|
||
example (H : A ∨ (B ∧ C) → E ∧ F) (c : C) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
|
||
example (H : A ∨ (B ∧ C) → (G → E ∧ F)) (g : G) (c : C) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
|