...

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
new file mode 100644 (file)
index 0000000..0ea0c5e
--- /dev/null
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
@@ -0,0 +1,68 @@
+(* Esercizio 0
+   ===========
+
+   Compilare i seguenti campi:
+
+   Nome1: ...
+   Cognome1: ...
+   Matricola1: ...
+   Account1: ...
+
+   Nome2: ...
+   Cognome2: ...
+   Matricola2: ...
+   Account2: ...
+
+*)
+
+(*DOCBEGIN
+
+I connettivi logici
+===================
+
+Per digitare i connettivi logici:
+
+* `∧` : `\land`
+* `∨` : `\lor`
+* `¬` : `\lnot`
+* `⇒` : `=>`, `\Rightarrow` 
+* `⊥` : `\bot`
+* `⊤` : `\top`
+
+Per digitare i quantificatori:
+
+* `∀` : `\forall`
+* `∃` : `\exists`
+
+I termini, le formule e i nomi delle ipotesi
+============================================
+
+* I termini quantificati da `∀` e `∃`, quando argomenti di
+  una regola, vengono scritti tra `{` e `}`.
+
+* Le formule, quando argomenti di
+  una regola, vengono scritti tra `(` e `)`.
+
+* I nomi delle ipotesi, quando argomenti di
+  una regola, vengono scritti tra `[` e `]`.
+
+
+DOCEND*)
+
+
+include "didactic/support/natural_deduction.ma".
+
+theorem pippo : (∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y.
+apply rule (prove ((∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y));
+(*BEGIN*)
+apply rule (⇒_i [h1] ((∃x.Q x) ⇒ ∃y.P y));
+apply rule (⇒_i [h2] (∃y.P y));
+apply rule (∃_e (∃x.Q x) {t} [h3] (∃y.P y));
+  [ apply rule (discharge [h2]);
+  | apply rule (let ft ≝ (f t) in ∃_i {ft} (P ft));
+    apply rule (∧_e_l (P (f t) ∧ Q t));
+    apply rule (∀_e {t} (∀x.P (f x) ∧ Q x));
+    apply rule (discharge [h1]);
+  ]
+(*END*)
+qed.
\ No newline at end of file