Added test file for inversion in ng matita.

[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction.ma

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 98142db2fd7f19ea8462c81839918798f538f8c2..47cb9e4ab2f74b5874ca15720908492528184e99 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -1,3 +1,23 @@
+(**************************************************************************)
+(*       ___                                                             *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Istruzioni: 
+
+     http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
+
+*)
+

 (* Esercizio 0
    ===========
 
 (* Esercizio 0
    ===========
 


@@ -17,6 +37,16 @@
 
 (*DOCBEGIN
 
 
 (*DOCBEGIN
 

+Scopo della lezione
+===================
+
+Lo scopo della lezione è di farvi imparare ad usare Matita
+per auto-correggervi gli esercizi di deduzione naturale, che
+saranno parte dell'esame scritto. Il consiglio è di 
+fare prima gli esercizi su carta e poi digitarli in Matita
+per verificarne la correttezza. Fare direttamente gli esercizi
+con Matita è difficile e richiede molto più tempo.
+

 I connettivi logici
 ===================
 
 I connettivi logici
 ===================
 


@@ -29,6 +59,15 @@ Per digitare i connettivi logici:
 * `⊥` : `\bot`
 * `⊤` : `\top`
 
 * `⊥` : `\bot`
 * `⊤` : `\top`
 

+I termini, le formule e i nomi delle ipotesi
+============================================
+
+* Le formule, quando argomenti di
+  una regola, vengono scritte tra `(` e `)`.
+
+* I nomi delle ipotesi, quando argomenti di
+  una regola, vengono scritti tra `[` e `]`.
+

 Le regole di deduzione naturale
 ===============================
 
 Le regole di deduzione naturale
 ===============================
 


@@ -38,9 +77,9 @@ sulla sinistra dopo aver premuto `F2`.
 
 L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.
 
 L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.

-Ad esempio 
+Ad esempio: 

 
 

-        apply rule (∧_i (A∨B) ⊥);
+        apply rule (∧#i (A∨B) ⊥);

           [ …continua qui il sottoalbero per (A∨B)
           | …continua qui il sottoalbero per ⊥
           ] 
           [ …continua qui il sottoalbero per (A∨B)
           | …continua qui il sottoalbero per ⊥
           ] 


@@ -48,12 +87,16 @@ Ad esempio
 Le regole vengono applicate alle loro premesse, ovvero
 gli argomenti delle regole sono le formule che normalmente 
 scrivete sopra la linea che rappresenta l'applicazione della
 Le regole vengono applicate alle loro premesse, ovvero
 gli argomenti delle regole sono le formule che normalmente 
 scrivete sopra la linea che rappresenta l'applicazione della

-regola stessa.
+regola stessa. Ad esempio:
+
+        aply rule (∨#e (A∨B) [h1] C [h2] C);
+          [ …prova di (A∨B)
+          | …prova di C sotto l'ipotesi A (di nome h1)  
+          | …prova di C sotto l'ipotesi B (di nome h2)
+          ]

 
 

-Le formule sono racchiuse tra `(` e `)`, mentre i nomi
-che date ad ipotesi aggiuntive (nella regola di eliminazione
-dell' OR, in RAA, e nella regola di introduzione 
-dell'implicazione) sono ragghiusi tra `[` e `]`.  
+Le regole che hanno una sola premessa non vengono seguite 
+da parentesi quadre.

 
 L'albero di deduzione
 =====================
 
 L'albero di deduzione
 =====================


@@ -71,31 +114,68 @@ alto a sinistra.
 Applicazioni di regole errate vengono contrassegnate con
 il colore rosso.
 
 Applicazioni di regole errate vengono contrassegnate con
 il colore rosso.
 

+Usare i lemmi dimostrati in precedenza
+======================================
+
+Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
+riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
+
+La "regola" `lem` prende come argomenti:
+
+- Il numero delle ipotesi del lemma che si vuole utilizzare, nel
+  caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
+
+- Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
+
+- Infine, le formule che devono essere scritte come premesse per la 
+  "regola".
+
+Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
+`lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
+`lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario 
+far seguire le parentesi quadre come spiegato in precedenza.
+
+Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
+per rappresentare l'albero di prova del lemma che si sta riutilizzando.
+
+Per motivi che saranno più chiari una volta studiate logiche del 
+primo ordine o di ordine superiore, i lemmi che si intende 
+riutilizzare è bene che siano dimostrati astratti sugli atomi. 
+Ovvero per ogni atomo `A`...`Z` che compare nella formula, 
+è bene aggiungere una quantificazione all'inizio della formula stessa.
+Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
+La dimostrazione deve poi iniziare con il comando `assume`. 
+
+In tale modo il lemma EM può essere utilizzato sia per dimostrare 
+`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
+

 DOCEND*)
 
 include "didactic/support/natural_deduction.ma".
 
 DOCEND*)
 
 include "didactic/support/natural_deduction.ma".
 

-theorem EM: ∀A. A ∨ ¬ A.
+theorem EM: ∀A:CProp. A ∨ ¬ A.

 (* Il comando assume è necessario perchè dimostriamo A∨¬A
    per una A generica. *)
 assume A: CProp.
 (* Il comando assume è necessario perchè dimostriamo A∨¬A
    per una A generica. *)
 assume A: CProp.

+(* Questo comando inizia a disegnare l'albero *)

 apply rule (prove (A ∨ ¬A));
 apply rule (prove (A ∨ ¬A));

-
+(* qui inizia l'albero, eseguite passo passo osservando come
+   si modifica l'albero. *)

 apply rule (RAA [H] (⊥)).
 apply rule (RAA [H] (⊥)).

-apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));

        [ apply rule (discharge [H]).
        [ apply rule (discharge [H]).

-       | apply rule (⊥_e (⊥));
-         apply rule (¬_e (¬¬A) (¬A));
-          [ apply rule (¬_i [K] (⊥)).
-       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+       | apply rule (⊥#e (⊥));
+         apply rule (¬#e (¬¬A) (¬A));
+          [ apply rule (¬#i [K] (⊥)).
+       apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));

              [ (*BEGIN*)apply rule (discharge [H]).(*END*)
              [ (*BEGIN*)apply rule (discharge [H]).(*END*)

-             | (*BEGIN*)apply rule (∨_i_r (¬A)).
+             | (*BEGIN*)apply rule (∨#i_r (¬A)).

           apply rule (discharge [K]).(*END*)
              ]
           apply rule (discharge [K]).(*END*)
              ]

-          | (*BEGIN*)apply rule (¬_i [K] (⊥)).
-       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+          | (*BEGIN*)apply rule (¬#i [K] (⊥)).
+       apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));

              [ apply rule (discharge [H]).
              [ apply rule (discharge [H]).

-             | apply rule (∨_i_l (A)).
+             | apply rule (∨#i_l (A)).

           apply rule (discharge [K]).
              ](*END*)
           ]
           apply rule (discharge [K]).
              ](*END*)
           ]


@@ -105,28 +185,28 @@ qed.
 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 (*BEGIN*)
 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 (*BEGIN*)

-apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
-apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
-apply rule (⇒_i [h3] (¬L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
+apply rule (⇒#i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h2] (G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h3] (¬L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨L) [h5] (E) [h6] (E));

        [ apply rule (discharge [h3]);
        [ apply rule (discharge [h3]);

-       | apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
-           [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
+       | apply rule (∨#e (E∨C) [h6] (E) [h7] (E));
+           [ apply rule (⇒#e (¬L ⇒ E∨C) (¬L));

                [ apply rule (discharge [h2]);
                | apply rule (discharge [h4]);
                ]
            | apply rule (discharge [h6]);
                [ apply rule (discharge [h2]);
                | apply rule (discharge [h4]);
                ]
            | apply rule (discharge [h6]);

-           | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
+           | apply rule (⇒#e (C∧G ⇒ E) (C∧G));

                [ apply rule (discharge [h1]);
                [ apply rule (discharge [h1]);

-               | apply rule (∧_i (C) (G));
+               | apply rule (∧#i (C) (G));

                    [ apply rule (discharge [h7]);
                    | apply rule (discharge [h5]);
                ]
                ]
            ]
                    [ apply rule (discharge [h7]);
                    | apply rule (discharge [h5]);
                ]
                ]
            ]

-       | apply rule (⊥_e (⊥));
-         apply rule (¬_e (¬L) (L));
+       | apply rule (⊥#e (⊥));
+         apply rule (¬#e (¬L) (L));

            [ apply rule (discharge [h4]);
            | apply rule (discharge [h6]);
            ]
            [ apply rule (discharge [h4]);
            | apply rule (discharge [h6]);
            ]


@@ -137,23 +217,23 @@ qed.
 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 (*BEGIN*)
 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 (*BEGIN*)

-apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
-apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
-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 (⇒_e (B∧D⇒C) (B∧D));
+apply rule (⇒#i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h2] ((D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h3] (D ⇒ C));
+apply rule (⇒#i [h4] (C));
+apply rule (∨#e (B∨¬B) [h5] (C) [h6] (C));
+       [ apply rule (lem 0 EM);
+       | apply rule (⇒#e (B∧D⇒C) (B∧D));

            [ apply rule (discharge [h2]);
            [ apply rule (discharge [h2]);

-       | apply rule (∧_i (B) (D));
+       | apply rule (∧#i (B) (D));

                [ apply rule (discharge [h5]);
                | apply rule (discharge [h4]);
                ]
            ] 
                [ apply rule (discharge [h5]);
                | apply rule (discharge [h4]);
                ]
            ] 

-       | apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
+       | apply rule (⇒#e (A∧¬B⇒C) (A∧¬B));

            [ apply rule (discharge [h1]);
            [ apply rule (discharge [h1]);

-           | apply rule (∧_i (A) (¬B));
-               [ apply rule (⇒_e (D⇒A) (D));
+           | apply rule (∧#i (A) (¬B));
+               [ apply rule (⇒#e (D⇒A) (D));

                    [ apply rule (discharge [h3]);
                    | apply rule (discharge [h4]);
                    ]
                    [ apply rule (discharge [h3]);
                    | apply rule (discharge [h4]);
                    ]


@@ -164,28 +244,30 @@ apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
 (*END*)
 qed.
 
 (*END*)
 qed.
 

+(* Per dimostrare questo teorema torna comodo il lemma EM
+   dimostrato in precedenza. *)

 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 (*BEGIN*)
 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 (*BEGIN*)

-apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
-apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
-apply rule (⇒_i [h3] (L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
-       [ apply rule (⇒_e (F ⇒ G∨E) (F));
+apply rule (⇒#i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨E) [h5] (E) [h6] (E));
+       [ apply rule (⇒#e (F ⇒ G∨E) (F));

            [ apply rule (discharge [h1]);
            [ apply rule (discharge [h1]);

-           | apply rule (⇒_e (L⇒F) (L));
+           | apply rule (⇒#e (L⇒F) (L));

                [ apply rule (discharge [h3]);
                | apply rule (discharge [h4]);
                ]
            ]
                [ apply rule (discharge [h3]);
                | apply rule (discharge [h4]);
                ]
            ]

-       |apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
-           [ apply rule (⇒_e (G⇒¬L∨E) (G));
+       |apply rule (∨#e (¬L∨E) [h7] (E) [h8] (E));
+           [ apply rule (⇒#e (G⇒¬L∨E) (G));

                [ apply rule (discharge [h2]);
                | apply rule (discharge [h5]);
                ]
                [ apply rule (discharge [h2]);
                | apply rule (discharge [h5]);
                ]

-           | apply rule (⊥_e (⊥));
-        apply rule (¬_e (¬L) (L));
+           | apply rule (⊥#e (⊥));
+        apply rule (¬#e (¬L) (L));

                [ apply rule (discharge [h7]);
                | apply rule (discharge [h4]);
                ]
                [ apply rule (discharge [h7]);
                | apply rule (discharge [h4]);
                ]


@@ -199,23 +281,23 @@ qed.
 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 (*BEGIN*)
 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 (*BEGIN*)

-apply rule (⇒_i [h1] (¬A∨¬B));
-apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
-       [ apply rule (lem EM);
-       | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
-           [ apply rule (lem EM);
-           | apply rule (⊥_e (⊥));
-             apply rule (¬_e (¬(A∧B)) (A∧B));
+apply rule (⇒#i [h1] (¬A∨¬B));
+apply rule (∨#e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
+       [ apply rule (lem 0 EM);
+       | apply rule (∨#e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
+           [ apply rule (lem 0 EM);
+           | apply rule (⊥#e (⊥));
+             apply rule (¬#e (¬(A∧B)) (A∧B));

                [ apply rule (discharge [h1]);
                [ apply rule (discharge [h1]);

-               | apply rule (∧_i (A) (B));
+               | apply rule (∧#i (A) (B));

                    [ apply rule (discharge [h2]);
                    | apply rule (discharge [h4]);
                    ]
                ]
                    [ apply rule (discharge [h2]);
                    | apply rule (discharge [h4]);
                    ]
                ]

-           | apply rule (∨_i_r (¬B));
+           | apply rule (∨#i_r (¬B));

         apply rule (discharge [h5]);
            ]
         apply rule (discharge [h5]);
            ]

-       | apply rule (∨_i_l (¬A));
+       | apply rule (∨#i_l (¬A));

     apply rule (discharge [h3]);
        ]
 (*END*)
     apply rule (discharge [h3]);
        ]
 (*END*)


@@ -224,24 +306,24 @@ qed.
 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 (*BEGIN*)
 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 (*BEGIN*)

-apply rule (⇒_i [h1] (¬A ∧ ¬B));
-apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
-       [ apply rule (lem EM);
-       | apply rule (⊥_e (⊥));
-    apply rule (¬_e (¬(A∨B)) (A∨B));
+apply rule (⇒#i [h1] (¬A ∧ ¬B));
+apply rule (∨#e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
+       [ apply rule (lem 0 EM);
+       | apply rule (⊥#e (⊥));
+    apply rule (¬#e (¬(A∨B)) (A∨B));

            [ apply rule (discharge [h1]);
            [ apply rule (discharge [h1]);

-           | apply rule (∨_i_l (A));
+           | apply rule (∨#i_l (A));

         apply rule (discharge [h2]);
            ]
         apply rule (discharge [h2]);
            ]

-       | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
-           [ apply rule (lem EM);
-           | apply rule (⊥_e (⊥));
-        apply rule (¬_e (¬(A∨B)) (A∨B));
+       | apply rule (∨#e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
+           [ apply rule (lem 0 EM);
+           | apply rule (⊥#e (⊥));
+        apply rule (¬#e (¬(A∨B)) (A∨B));

                [ apply rule (discharge [h1]);
                [ apply rule (discharge [h1]);

-               | apply rule (∨_i_r (B));
+               | apply rule (∨#i_r (B));

             apply rule (discharge [h10]);
                ] 
             apply rule (discharge [h10]);
                ] 

-           | apply rule (∧_i (¬A) (¬B));
+           | apply rule (∧#i (¬A) (¬B));

                [ apply rule (discharge [h3]);
                |apply rule (discharge [h11]);
                ]
                [ apply rule (discharge [h3]);
                |apply rule (discharge [h11]);
                ]


@@ -253,17 +335,17 @@ qed.
 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 (*BEGIN*)
 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 (*BEGIN*)

-apply rule (⇒_i [h1] (¬(A∨B)));
-apply rule (¬_i [h2] (⊥));
-apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
+apply rule (⇒#i [h1] (¬(A∨B)));
+apply rule (¬#i [h2] (⊥));
+apply rule (∨#e (A∨B) [h3] (⊥) [h3] (⊥));

        [ apply rule (discharge [h2]);
        [ apply rule (discharge [h2]);

-       | apply rule (¬_e (¬A) (A));
-           [ apply rule (∧_e_l (¬A∧¬B));
+       | apply rule (¬#e (¬A) (A));
+           [ apply rule (∧#e_l (¬A∧¬B));

         apply rule (discharge [h1]);
            | apply rule (discharge [h3]);
            ]
         apply rule (discharge [h1]);
            | apply rule (discharge [h3]);
            ]

-       | apply rule (¬_e (¬B) (B));
-           [ apply rule (∧_e_r (¬A∧¬B));
+       | apply rule (¬#e (¬B) (B));
+           [ apply rule (∧#e_r (¬A∧¬B));

         apply rule (discharge [h1]);
            | apply rule (discharge [h3]);
            ]
         apply rule (discharge [h1]);
            | apply rule (discharge [h3]);
            ]


@@ -274,16 +356,16 @@ qed.
 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 (*BEGIN*)
 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 (*BEGIN*)

-apply rule (⇒_i [h1] (A));
+apply rule (⇒#i [h1] (A));

 apply rule (RAA [h2] (⊥));
 apply rule (RAA [h2] (⊥));

-apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
+apply rule (⇒#e ((A⇒⊥)⇒⊥) (A⇒⊥));

        [ apply rule (discharge [h1]);
        [ apply rule (discharge [h1]);

-       | apply rule (⇒_i [h3] (⊥));
-         apply rule (¬_e (¬A) (A));
+       | apply rule (⇒#i [h3] (⊥));
+         apply rule (¬#e (¬A) (A));

            [ apply rule (discharge [h2]);
            | apply rule (discharge [h3]);
            ]
        ]
 (*END*)
            [ apply rule (discharge [h2]);
            | apply rule (discharge [h3]);
            ]
        ]
 (*END*)

-qed. 
+qed.