-(* Esercitazione di logica 22/10/2008. *)
-
-(* Nota per gli studenti
- =====================
-
- * La lezione del pomeriggio con il Prof. Sacerdoti si terrà in aula
- Pinkerle e non Cremona.
-
- * Un piccolo manuale sul software Matita è disponibile al seguente URL:
-
- http://mowgli.cs.unibo.it/~tassi/exercise-induction.ma.html
-
-*)
-
(* Esercizio 0
===========
definition esempio1 ≝
(FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
-eval normalize on [[ esempio1 ]]_v1101.
+(* Decommenta ed esegui. *)
+
+(* eval normalize on [[ esempio1 ]]_v1101. *)
(* Esercizio 3
definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)).
-eval normalize on (esempio2 [ esempio3 / 2]).
+(* Decommenta ed esegui *)
+
+(* eval normalize on (esempio2 [ esempio3 / 2]). *)
(*DOCBEGIN