apply rule (⇒_i [h3] (D ⇒ C));
apply rule (⇒_i [h4] (C));
apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
- [ apply rule (lem EM);
+ [ apply rule (lem 0 EM);
| apply rule (⇒_e (B∧D⇒C) (B∧D));
[ apply rule (discharge [h2]);
| apply rule (∧_i (B) (D));
(*BEGIN*)
apply rule (⇒_i [h1] (¬A∨¬B));
apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
- [ apply rule (lem EM);
+ [ apply rule (lem 0 EM);
| apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
- [ apply rule (lem EM);
+ [ apply rule (lem 0 EM);
| apply rule (⊥_e (⊥));
apply rule (¬_e (¬(A∧B)) (A∧B));
[ apply rule (discharge [h1]);
(*BEGIN*)
apply rule (⇒_i [h1] (¬A ∧ ¬B));
apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
- [ apply rule (lem EM);
+ [ apply rule (lem 0 EM);
| apply rule (⊥_e (⊥));
apply rule (¬_e (¬(A∨B)) (A∨B));
[ apply rule (discharge [h1]);
apply rule (discharge [h2]);
]
| apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
- [ apply rule (lem EM);
+ [ apply rule (lem 0 EM);
| apply rule (⊥_e (⊥));
apply rule (¬_e (¬(A∨B)) (A∨B));
[ apply rule (discharge [h1]);
]
]
(*END*)
-qed.
+qed.