nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/library/didactic/exercises/shannon.ma b/helm/software/matita/library/didactic/exercises/shannon.ma
index f978c91c55c40256a7b50dfb42581822691bf30d..78504385ffe20f0e267e0cbc74d6e076c83cf430 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/shannon.ma
+++ b/helm/software/matita/library/didactic/exercises/shannon.ma
@@ -38,7 +38,7 @@ include "nat/minus.ma".
 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.

-interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
+interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).

 definition max ≝ λn,m. if eqb (n - m) 0 then m else n. 
 definition min ≝ λn,m. if eqb (n - m) 0 then n else m. 
 
 definition max ≝ λn,m. if eqb (n - m) 0 then m else n. 
 definition min ≝ λn,m. if eqb (n - m) 0 then n else m. 
 


@@ -61,7 +61,7 @@ inductive Formula : Type ≝
 (* Ripasso 2
    =========
    
 (* Ripasso 2
    =========
    

-   La semantica di una formula `F` in un mondo `v`: `[[ F ]]_v` 
+   La semantica di una formula `F` in un mondo `v`: `[[ F ]]v` 

 *)
 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
  match F with
 *)
 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
  match F with


@@ -82,9 +82,9 @@ let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
 *)
 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 *)
 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.

-notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
+notation > "[[ term 19 a ]] term 90 v" non associative with precedence 90 for @{ sem $v $a }.

 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
 interpretation "Semantic of Formula" 'semantics v a = (sem v a).

-lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1.  intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ].  |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed.
+lemma sem_bool : ∀F,v. [[ F ]]v = 0 ∨ [[ F ]]v = 1.  intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ].  |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed.

 
 (* Ripasso 3
    =========
 
 (* Ripasso 3
    =========


@@ -112,12 +112,12 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).

-definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
+definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v.

 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).

-lemma min_1_sem: ∀F,v.min 1 [[ F ]]_v = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
-lemma max_0_sem: ∀F,v.max [[ F ]]_v 0 = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
+lemma min_1_sem: ∀F,v.min 1 [[ F ]]v = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
+lemma max_0_sem: ∀F,v.max [[ F ]]v 0 = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.

 definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C).
 
 (*DOCBEGIN
 definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C).
 
 (*DOCBEGIN


@@ -128,11 +128,11 @@ La libreria di Matita
 Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
 
 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
 Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
 
 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`

-* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1`
+* lemma `sem_bool` : `∀F,v. [[ F ]]v = 0 ∨ [[ F ]]v = 1`

 * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
 * lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true`
 * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
 * lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true`

-* lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v`
-* lemma `max_0_sem` : `∀F,v.max [[ F ]]_v 0 = [[ F ]]_v`
+* lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]v = [[ F ]]v`
+* lemma `max_0_sem` : `∀F,v.max [[ F ]]v 0 = [[ F ]]v`

 
 Nota su `x = y` e `eqb x y`
 ---------------------------
 
 Nota su `x = y` e `eqb x y`
 ---------------------------


@@ -177,10 +177,10 @@ La dimostrazione è composta da due lemmi, `shannon_false` e `shannon_true`.
 Vediamo solo la dimostrazione del primo, essendo il secondo del tutto analogo.
 Il lemma asserisce quanto segue:
 
 Vediamo solo la dimostrazione del primo, essendo il secondo del tutto analogo.
 Il lemma asserisce quanto segue:
 

-        ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v
+        ∀F,x,v. [[ FAtom x ]]v = 0 → [[ F[FBot/x] ]]v = [[ F ]]v

         
 Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver 
         
 Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver 

-supposto che `[[ FAtom x ]]_v = 0` si procede per induzione su `F`.
+supposto che `[[ FAtom x ]]v = 0` si procede per induzione su `F`.

 I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`,
 una volta assunte le sottoformule e le relative ipotesi induttive, 
 si conclude con una catena di uguaglianze.
 I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`,
 una volta assunte le sottoformule e le relative ipotesi induttive, 
 si conclude con una catena di uguaglianze.


@@ -194,7 +194,7 @@ si ottengolo le ipotesi aggiuntive `(eqb n x = true)` oppure `(eqb n x = false)`
 Entrambi i casi si concludono con una catena di uguaglianze.
 
 Il teorema principale si dimostra utilizzando il lemma `sem_bool` per 
 Entrambi i casi si concludono con una catena di uguaglianze.
 
 Il teorema principale si dimostra utilizzando il lemma `sem_bool` per 

-ottenre l'ipotesi `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1` su cui
+ottenre l'ipotesi `[[ FAtom x ]]v = 0 ∨ [[ FAtom x ]]v = 1` su cui

 si procede poi per casi. Entrambi i casi si concludono con
 una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza 
 e i lemmi `min_1_sem` oppure `max_0_sem`.
 si procede poi per casi. Entrambi i casi si concludono con
 una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza 
 e i lemmi `min_1_sem` oppure `max_0_sem`.


@@ -202,191 +202,191 @@ e i lemmi `min_1_sem` oppure `max_0_sem`.
 DOCEND*)
 
 lemma shannon_false: 
 DOCEND*)
 
 lemma shannon_false: 

-  ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v.
+  ∀F,x,v. [[ FAtom x ]]v = 0 → [[ F[FBot/x] ]]v = [[ F ]]v.

 (*BEGIN*)
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).
 (*BEGIN*)
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).

-suppose ([[ FAtom x ]]_v = 0) (H).
-we proceed by induction on F to prove ([[ F[FBot/x] ]]_v = [[ F ]]_v).
+suppose ([[ FAtom x ]]v = 0) (H).
+we proceed by induction on F to prove ([[ F[FBot/x] ]]v = [[ F ]]v).

 case FBot.
 case FBot.

-  the thesis becomes ([[ FBot[FBot/x] ]]_v = [[ FBot ]]_v).
-  the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v).
+  the thesis becomes ([[ FBot[FBot/x] ]]v = [[ FBot ]]v).
+  the thesis becomes ([[ FBot ]]v = [[ FBot ]]v).

   done. 
 case FTop.
   done. 
 case FTop.

-  the thesis becomes ([[ FTop[FBot/x] ]]_v = [[ FTop ]]_v).
-  the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v).
+  the thesis becomes ([[ FTop[FBot/x] ]]v = [[ FTop ]]v).
+  the thesis becomes ([[ FTop ]]v = [[ FTop ]]v).

   done.
 case FAtom.
   assume n : ℕ.
   done.
 case FAtom.
   assume n : ℕ.

-  the thesis becomes ([[ (FAtom n)[FBot/x] ]]_v = [[ FAtom n ]]_v).
-  the thesis becomes ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v).
+  the thesis becomes ([[ (FAtom n)[FBot/x] ]]v = [[ FAtom n ]]v).
+  the thesis becomes ([[ if eqb n x then FBot else (FAtom n) ]]v = [[ FAtom n ]]v).

   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).
   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).

-  we proceed by cases on H1 to prove ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v).
+  we proceed by cases on H1 to prove ([[ if eqb n x then FBot else (FAtom n) ]]v = [[ FAtom n ]]v).

     case Left.
       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
       conclude
     case Left.
       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
       conclude

-          ([[ if eqb n x then FBot else (FAtom n) ]]_v)
-        = ([[ if true then FBot else (FAtom n) ]]_v) by H3.
-        = ([[ FBot ]]_v). 
+          ([[ if eqb n x then FBot else (FAtom n) ]]v)
+        = ([[ if true then FBot else (FAtom n) ]]v) by H3.
+        = ([[ FBot ]]v). 

         = 0.
         = 0.

-        = ([[ FAtom x ]]_v) by H.
-        = ([[ FAtom n ]]_v) by H2.
+        = ([[ FAtom x ]]v) by H.
+        = ([[ FAtom n ]]v) by H2.

     done.
     case Right.
       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
       conclude
     done.
     case Right.
       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
       conclude

-          ([[ if eqb n x then FBot else (FAtom n) ]]_v)
-        = ([[ if false then FBot else (FAtom n) ]]_v) by H3.
-        = ([[ FAtom n ]]_v). 
+          ([[ if eqb n x then FBot else (FAtom n) ]]v)
+        = ([[ if false then FBot else (FAtom n) ]]v) by H3.
+        = ([[ FAtom n ]]v). 

     done.
 case FAnd.
   assume f1 : Formula.
     done.
 case FAnd.
   assume f1 : Formula.

-  by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
+  by induction hypothesis we know ([[ f1[FBot/x] ]]v = [[ f1 ]]v) (H1).

   assume f2 : Formula. 
   assume f2 : Formula. 

-  by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
-  the thesis becomes ([[ (FAnd f1 f2)[FBot/x] ]]_v = [[ FAnd f1 f2 ]]_v).
+  by induction hypothesis we know ([[ f2[FBot/x] ]]v = [[ f2 ]]v) (H2).
+  the thesis becomes ([[ (FAnd f1 f2)[FBot/x] ]]v = [[ FAnd f1 f2 ]]v).

   conclude 
   conclude 

-      ([[ (FAnd f1 f2)[FBot/x] ]]_v)
-    = ([[ FAnd (f1[FBot/x]) (f2[FBot/x]) ]]_v).
-    = (min [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v).
-    = (min [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1.
-    = (min [[ f1 ]]_v [[ f2 ]]_v) by H2.
-    = ([[ FAnd f1 f2 ]]_v).
+      ([[ (FAnd f1 f2)[FBot/x] ]]v)
+    = ([[ FAnd (f1[FBot/x]) (f2[FBot/x]) ]]v).
+    = (min [[ f1[FBot/x] ]]v [[ f2[FBot/x] ]]v).
+    = (min [[ f1 ]]v [[ f2[FBot/x] ]]v) by H1.
+    = (min [[ f1 ]]v [[ f2 ]]v) by H2.
+    = ([[ FAnd f1 f2 ]]v).

   done. 
 case FOr.
   assume f1 : Formula.
   done. 
 case FOr.
   assume f1 : Formula.

-  by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
+  by induction hypothesis we know ([[ f1[FBot/x] ]]v = [[ f1 ]]v) (H1).

   assume f2 : Formula. 
   assume f2 : Formula. 

-  by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
-  the thesis becomes ([[ (FOr f1 f2)[FBot/x] ]]_v = [[ FOr f1 f2 ]]_v).
+  by induction hypothesis we know ([[ f2[FBot/x] ]]v = [[ f2 ]]v) (H2).
+  the thesis becomes ([[ (FOr f1 f2)[FBot/x] ]]v = [[ FOr f1 f2 ]]v).

   conclude 
   conclude 

-      ([[ (FOr f1 f2)[FBot/x] ]]_v)
-    = ([[ FOr (f1[FBot/x]) (f2[FBot/x]) ]]_v).
-    = (max [[ f1[FBot/x] ]]_v  [[ f2[FBot/x] ]]_v).
-    = (max [[ f1 ]]_v  [[ f2[FBot/x] ]]_v) by H1.
-    = (max [[ f1 ]]_v  [[ f2 ]]_v) by H2.
-    = ([[ FOr f1 f2 ]]_v).
+      ([[ (FOr f1 f2)[FBot/x] ]]v)
+    = ([[ FOr (f1[FBot/x]) (f2[FBot/x]) ]]v).
+    = (max [[ f1[FBot/x] ]]v  [[ f2[FBot/x] ]]v).
+    = (max [[ f1 ]]v  [[ f2[FBot/x] ]]v) by H1.
+    = (max [[ f1 ]]v  [[ f2 ]]v) by H2.
+    = ([[ FOr f1 f2 ]]v).

   done.
 case FImpl.
   assume f1 : Formula.
   done.
 case FImpl.
   assume f1 : Formula.

-  by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
+  by induction hypothesis we know ([[ f1[FBot/x] ]]v = [[ f1 ]]v) (H1).

   assume f2 : Formula. 
   assume f2 : Formula. 

-  by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
-  the thesis becomes ([[ (FImpl f1 f2)[FBot/x] ]]_v = [[ FImpl f1 f2 ]]_v).
+  by induction hypothesis we know ([[ f2[FBot/x] ]]v = [[ f2 ]]v) (H2).
+  the thesis becomes ([[ (FImpl f1 f2)[FBot/x] ]]v = [[ FImpl f1 f2 ]]v).

   conclude
   conclude

-      ([[ (FImpl f1 f2)[FBot/x] ]]_v)
-    = ([[ FImpl (f1[FBot/x]) (f2[FBot/x]) ]]_v).
-    = (max (1 - [[ f1[FBot/x] ]]_v) [[ f2[FBot/x] ]]_v).
-    = (max (1 - [[ f1 ]]_v) [[ f2[FBot/x] ]]_v) by H1.
-    = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2.
-    = ([[ FImpl f1 f2 ]]_v).
+      ([[ (FImpl f1 f2)[FBot/x] ]]v)
+    = ([[ FImpl (f1[FBot/x]) (f2[FBot/x]) ]]v).
+    = (max (1 - [[ f1[FBot/x] ]]v) [[ f2[FBot/x] ]]v).
+    = (max (1 - [[ f1 ]]v) [[ f2[FBot/x] ]]v) by H1.
+    = (max (1 - [[ f1 ]]v) [[ f2 ]]v) by H2.
+    = ([[ FImpl f1 f2 ]]v).

   done.
 case FNot.
   assume f : Formula.
   done.
 case FNot.
   assume f : Formula.

-  by induction hypothesis we know ([[ f[FBot/x] ]]_v = [[ f ]]_v) (H1).
-  the thesis becomes ([[ (FNot f)[FBot/x] ]]_v = [[ FNot f ]]_v).
+  by induction hypothesis we know ([[ f[FBot/x] ]]v = [[ f ]]v) (H1).
+  the thesis becomes ([[ (FNot f)[FBot/x] ]]v = [[ FNot f ]]v).

   conclude 
   conclude 

-      ([[ (FNot f)[FBot/x] ]]_v)
-    = ([[ FNot (f[FBot/x]) ]]_v).
-    = (1 - [[ f[FBot/x] ]]_v).
-    = (1 - [[ f ]]_v) by H1.
-    = ([[ FNot f ]]_v).
+      ([[ (FNot f)[FBot/x] ]]v)
+    = ([[ FNot (f[FBot/x]) ]]v).
+    = (1 - [[ f[FBot/x] ]]v).
+    = (1 - [[ f ]]v) by H1.
+    = ([[ FNot f ]]v).

   done.
 (*END*)
 qed. 
 
 lemma shannon_true: 
   done.
 (*END*)
 qed. 
 
 lemma shannon_true: 

-  ∀F,x,v. [[ FAtom x ]]_v = 1 → [[ F[FTop/x] ]]_v = [[ F ]]_v.
+  ∀F,x,v. [[ FAtom x ]]v = 1 → [[ F[FTop/x] ]]v = [[ F ]]v.

 (*BEGIN*)
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).
 (*BEGIN*)
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).

-suppose ([[ FAtom x ]]_v = 1) (H).
-we proceed by induction on F to prove ([[ F[FTop/x] ]]_v = [[ F ]]_v).
+suppose ([[ FAtom x ]]v = 1) (H).
+we proceed by induction on F to prove ([[ F[FTop/x] ]]v = [[ F ]]v).

 case FBot.
 case FBot.

-  the thesis becomes ([[ FBot[FTop/x] ]]_v = [[ FBot ]]_v).
-  the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v).
+  the thesis becomes ([[ FBot[FTop/x] ]]v = [[ FBot ]]v).
+  the thesis becomes ([[ FBot ]]v = [[ FBot ]]v).

   done. 
 case FTop.
   done. 
 case FTop.

-  the thesis becomes ([[ FTop[FTop/x] ]]_v = [[ FTop ]]_v).
-  the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v).
+  the thesis becomes ([[ FTop[FTop/x] ]]v = [[ FTop ]]v).
+  the thesis becomes ([[ FTop ]]v = [[ FTop ]]v).

   done.
 case FAtom.
   assume n : ℕ.
   done.
 case FAtom.
   assume n : ℕ.

-  the thesis becomes ([[ (FAtom n)[FTop/x] ]]_v = [[ FAtom n ]]_v).
-  the thesis becomes ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v).
+  the thesis becomes ([[ (FAtom n)[FTop/x] ]]v = [[ FAtom n ]]v).
+  the thesis becomes ([[ if eqb n x then FTop else (FAtom n) ]]v = [[ FAtom n ]]v).

   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).
   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).

-  we proceed by cases on H1 to prove ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v).
+  we proceed by cases on H1 to prove ([[ if eqb n x then FTop else (FAtom n) ]]v = [[ FAtom n ]]v).

     case Left.
       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
       conclude
     case Left.
       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
       conclude

-          ([[ if eqb n x then FTop else (FAtom n) ]]_v)
-        = ([[ if true then FTop else (FAtom n) ]]_v) by H3.
-        = ([[ FTop ]]_v). 
+          ([[ if eqb n x then FTop else (FAtom n) ]]v)
+        = ([[ if true then FTop else (FAtom n) ]]v) by H3.
+        = ([[ FTop ]]v). 

         = 1.
         = 1.

-        = ([[ FAtom x ]]_v) by H.
-        = ([[ FAtom n ]]_v) by H2.
+        = ([[ FAtom x ]]v) by H.
+        = ([[ FAtom n ]]v) by H2.

     done.
     case Right.
       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
       conclude
     done.
     case Right.
       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
       conclude

-          ([[ if eqb n x then FTop else (FAtom n) ]]_v)
-        = ([[ if false then FTop else (FAtom n) ]]_v) by H3.
-        = ([[ FAtom n ]]_v). 
+          ([[ if eqb n x then FTop else (FAtom n) ]]v)
+        = ([[ if false then FTop else (FAtom n) ]]v) by H3.
+        = ([[ FAtom n ]]v). 

     done.
 case FAnd.
   assume f1 : Formula.
     done.
 case FAnd.
   assume f1 : Formula.

-  by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
+  by induction hypothesis we know ([[ f1[FTop/x] ]]v = [[ f1 ]]v) (H1).

   assume f2 : Formula. 
   assume f2 : Formula. 

-  by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
-  the thesis becomes ([[ (FAnd f1 f2)[FTop/x] ]]_v = [[ FAnd f1 f2 ]]_v).
+  by induction hypothesis we know ([[ f2[FTop/x] ]]v = [[ f2 ]]v) (H2).
+  the thesis becomes ([[ (FAnd f1 f2)[FTop/x] ]]v = [[ FAnd f1 f2 ]]v).

   conclude 
   conclude 

-      ([[ (FAnd f1 f2)[FTop/x] ]]_v)
-    = ([[ FAnd (f1[FTop/x]) (f2[FTop/x]) ]]_v).
-    = (min [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v).
-    = (min [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1.
-    = (min [[ f1 ]]_v [[ f2 ]]_v) by H2.
-    = ([[ FAnd f1 f2 ]]_v).
+      ([[ (FAnd f1 f2)[FTop/x] ]]v)
+    = ([[ FAnd (f1[FTop/x]) (f2[FTop/x]) ]]v).
+    = (min [[ f1[FTop/x] ]]v [[ f2[FTop/x] ]]v).
+    = (min [[ f1 ]]v [[ f2[FTop/x] ]]v) by H1.
+    = (min [[ f1 ]]v [[ f2 ]]v) by H2.
+    = ([[ FAnd f1 f2 ]]v).

   done. 
 case FOr.
   assume f1 : Formula.
   done. 
 case FOr.
   assume f1 : Formula.

-  by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
+  by induction hypothesis we know ([[ f1[FTop/x] ]]v = [[ f1 ]]v) (H1).

   assume f2 : Formula. 
   assume f2 : Formula. 

-  by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
-  the thesis becomes ([[ (FOr f1 f2)[FTop/x] ]]_v = [[ FOr f1 f2 ]]_v).
+  by induction hypothesis we know ([[ f2[FTop/x] ]]v = [[ f2 ]]v) (H2).
+  the thesis becomes ([[ (FOr f1 f2)[FTop/x] ]]v = [[ FOr f1 f2 ]]v).

   conclude 
   conclude 

-      ([[ (FOr f1 f2)[FTop/x] ]]_v)
-    = ([[ FOr (f1[FTop/x]) (f2[FTop/x]) ]]_v).
-    = (max [[ f1[FTop/x] ]]_v  [[ f2[FTop/x] ]]_v).
-    = (max [[ f1 ]]_v  [[ f2[FTop/x] ]]_v) by H1.
-    = (max [[ f1 ]]_v  [[ f2 ]]_v) by H2.
-    = ([[ FOr f1 f2 ]]_v).
+      ([[ (FOr f1 f2)[FTop/x] ]]v)
+    = ([[ FOr (f1[FTop/x]) (f2[FTop/x]) ]]v).
+    = (max [[ f1[FTop/x] ]]v  [[ f2[FTop/x] ]]v).
+    = (max [[ f1 ]]v  [[ f2[FTop/x] ]]v) by H1.
+    = (max [[ f1 ]]v  [[ f2 ]]v) by H2.
+    = ([[ FOr f1 f2 ]]v).

   done.
 case FImpl.
   assume f1 : Formula.
   done.
 case FImpl.
   assume f1 : Formula.

-  by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
+  by induction hypothesis we know ([[ f1[FTop/x] ]]v = [[ f1 ]]v) (H1).

   assume f2 : Formula. 
   assume f2 : Formula. 

-  by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
-  the thesis becomes ([[ (FImpl f1 f2)[FTop/x] ]]_v = [[ FImpl f1 f2 ]]_v).
+  by induction hypothesis we know ([[ f2[FTop/x] ]]v = [[ f2 ]]v) (H2).
+  the thesis becomes ([[ (FImpl f1 f2)[FTop/x] ]]v = [[ FImpl f1 f2 ]]v).

   conclude
   conclude

-      ([[ (FImpl f1 f2)[FTop/x] ]]_v)
-    = ([[ FImpl (f1[FTop/x]) (f2[FTop/x]) ]]_v).
-    = (max (1 - [[ f1[FTop/x] ]]_v) [[ f2[FTop/x] ]]_v).
-    = (max (1 - [[ f1 ]]_v) [[ f2[FTop/x] ]]_v) by H1.
-    = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2.
-    = ([[ FImpl f1 f2 ]]_v).
+      ([[ (FImpl f1 f2)[FTop/x] ]]v)
+    = ([[ FImpl (f1[FTop/x]) (f2[FTop/x]) ]]v).
+    = (max (1 - [[ f1[FTop/x] ]]v) [[ f2[FTop/x] ]]v).
+    = (max (1 - [[ f1 ]]v) [[ f2[FTop/x] ]]v) by H1.
+    = (max (1 - [[ f1 ]]v) [[ f2 ]]v) by H2.
+    = ([[ FImpl f1 f2 ]]v).

   done.
 case FNot.
   assume f : Formula.
   done.
 case FNot.
   assume f : Formula.

-  by induction hypothesis we know ([[ f[FTop/x] ]]_v = [[ f ]]_v) (H1).
-  the thesis becomes ([[ (FNot f)[FTop/x] ]]_v = [[ FNot f ]]_v).
+  by induction hypothesis we know ([[ f[FTop/x] ]]v = [[ f ]]v) (H1).
+  the thesis becomes ([[ (FNot f)[FTop/x] ]]v = [[ FNot f ]]v).

   conclude 
   conclude 

-      ([[ (FNot f)[FTop/x] ]]_v)
-    = ([[ FNot (f[FTop/x]) ]]_v).
-    = (1 - [[ f[FTop/x] ]]_v).
-    = (1 - [[ f ]]_v) by H1.
-    = ([[ FNot f ]]_v).
+      ([[ (FNot f)[FTop/x] ]]v)
+    = ([[ FNot (f[FTop/x]) ]]v).
+    = (1 - [[ f[FTop/x] ]]v).
+    = (1 - [[ f ]]v) by H1.
+    = ([[ FNot f ]]v).

   done.
 (*END*)
 qed. 
   done.
 (*END*)
 qed. 


@@ -397,33 +397,33 @@ theorem shannon :
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).

-the thesis becomes ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v).
-by sem_bool we proved ([[ FAtom x]]_v = 0 ∨ [[ FAtom x]]_v = 1) (H).
-we proceed by cases on H to prove ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v).
+the thesis becomes ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]v = [[ F ]]v).
+by sem_bool we proved ([[ FAtom x]]v = 0 ∨ [[ FAtom x]]v = 1) (H).
+we proceed by cases on H to prove ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]v = [[ F ]]v).

 case Left.
   conclude 
 case Left.
   conclude 

-      ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v)
-    = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
-    = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
-    = (max (min  [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
-    = (max (min  0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H1.    
-    = (max 0 (min 1 [[ F[FBot/x] ]]_v)).
-    = (max 0 [[ F[FBot/x] ]]_v) by min_1_sem.
-    = ([[ F[FBot/x] ]]_v).
-    = ([[ F ]]_v) by H1, shannon_false.
+      ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]v)
+    = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]v).
+    = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]v).
+    = (max (min  [[ FAtom x ]]v [[ F[FTop/x] ]]v) (min (1 - [[ FAtom x ]]v) [[ F[FBot/x] ]]v)).
+    = (max (min  0 [[ F[FTop/x] ]]v) (min (1 - 0) [[ F[FBot/x] ]]v)) by H1.    
+    = (max 0 (min 1 [[ F[FBot/x] ]]v)).
+    = (max 0 [[ F[FBot/x] ]]v) by min_1_sem.
+    = ([[ F[FBot/x] ]]v).
+    = ([[ F ]]v) by H1, shannon_false.

   done.
 case Right.
   conclude 
   done.
 case Right.
   conclude 

-      ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v)
-    = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
-    = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
-    = (max (min  [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
-    = (max (min  1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H1.    
-    = (max (min  1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)).
-    = (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem.
-    = (max [[ F[FTop/x] ]]_v 0).
-    = ([[ F[FTop/x] ]]_v) by max_0_sem.
-    = ([[ F ]]_v) by H1, shannon_true.
+      ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]v)
+    = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]v).
+    = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]v).
+    = (max (min  [[ FAtom x ]]v [[ F[FTop/x] ]]v) (min (1 - [[ FAtom x ]]v) [[ F[FBot/x] ]]v)).
+    = (max (min  1 [[ F[FTop/x] ]]v) (min (1 - 1) [[ F[FBot/x] ]]v)) by H1.    
+    = (max (min  1 [[ F[FTop/x] ]]v) (min 0 [[ F[FBot/x] ]]v)).
+    = (max [[ F[FTop/x] ]]v (min 0 [[ F[FBot/x] ]]v)) by min_1_sem.
+    = (max [[ F[FTop/x] ]]v 0).
+    = ([[ F[FTop/x] ]]v) by max_0_sem.
+    = ([[ F ]]v) by H1, shannon_true.

   done.
 (*END*)
 qed.
   done.
 (*END*)
 qed.


@@ -505,7 +505,7 @@ I comandi da utilizzare
   Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
   con cui si inizia una catena di uguaglianze. La prima formula che si
   scrive deve essere esattamente uguale alla parte sinistra della conclusione
   Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
   con cui si inizia una catena di uguaglianze. La prima formula che si
   scrive deve essere esattamente uguale alla parte sinistra della conclusione

-  originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.`
+  originale. Esempio `conclude ([[ FAtom x ]]v) = ([[ FAtom n ]]v) by H.`

   Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione
   di una definizione, la parte `by ...` deve essere omessa.
           
   Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione
   di una definizione, la parte `by ...` deve essere omessa.