apply rule (prove (A ∨ ¬ A));
apply rule (RAA [H] ⊥);
- apply rule (¬_e (¬A) A);
- [ apply rule (¬_i [H1] ⊥);
- apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ apply rule (¬#e (¬A) A);
+ [ apply rule (¬#i [H1] ⊥);
+ apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
[ apply rule (discharge [H]);
- | apply rule (∨_i_l A);
+ | apply rule (∨#i_l A);
apply rule (discharge [H1]);
]
| apply rule (RAA [H2] ⊥);
- apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
[ apply rule (discharge [H]);
- | apply rule (∨_i_r (¬A));
+ | apply rule (∨#i_r (¬A));
apply rule (discharge [H2]);
]
]
apply rule (prove (A ∨ ¬ A));
apply rule (RAA [H] ⊥);
- apply rule (¬_e (¬¬A) (¬A));
- [ apply rule (¬_i [H2] ⊥);
- apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ apply rule (¬#e (¬¬A) (¬A));
+ [ apply rule (¬#i [H2] ⊥);
+ apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
[ apply rule (discharge [H]);
- | apply rule (∨_i_r (¬A));
+ | apply rule (∨#i_r (¬A));
apply rule (discharge [H2]);
]
- | apply rule (¬_i [H1] ⊥);
- apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ | apply rule (¬#i [H1] ⊥);
+ apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
[ apply rule (discharge [H]);
- | apply rule (∨_i_l A);
+ | apply rule (∨#i_l A);
apply rule (discharge [H1]);
]
]
apply rule (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
- apply rule (⇒_i [H] (A∧C⇒E∧C∨B));
- apply rule (⇒_i [K] (E∧C∨B));
- apply rule (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
+ apply rule (⇒#i [H] (A∧C⇒E∧C∨B));
+ apply rule (⇒#i [K] (E∧C∨B));
+ apply rule (∨#e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
[ apply rule (discharge [H]);
-| apply rule (∨_i_l (E∧C));
- apply rule (∧_i E C);
- [ apply rule (⇒_e (A⇒E) A);
+| apply rule (∨#i_l (E∧C));
+ apply rule (∧#i E C);
+ [ apply rule (⇒#e (A⇒E) A);
[ apply rule (discharge [C1]);
- | apply rule (∧_e_l (A∧C)); apply rule (discharge [K]);
+ | apply rule (∧#e_l (A∧C)); apply rule (discharge [K]);
]
- | apply rule (∧_e_r (A∧C)); apply rule (discharge [K]);
+ | apply rule (∧#e_r (A∧C)); apply rule (discharge [K]);
]
-| apply rule (∨_i_r B); apply rule (discharge [C2]);
+| apply rule (∨#i_r B); apply rule (discharge [C2]);
]
qed.