helm/software/matita/contribs/didactic/shannon.ma

   1 (* Esercizio 0
   2    ===========
   3
   4    Compilare i seguenti campi:
   5
   6    Nome1: ...
   7    Cognome1: ...
   8    Matricola1: ...
   9    Account1: ...
  10
  11    Nome2: ...
  12    Cognome2: ...
  13    Matricola2: ...
  14    Account2: ...
  15
  16 *)
  17
  18 (* ATTENZIONE
  19    ==========
  20
  21    Non modificare quanto segue
  22 *)
  23 include "nat/minus.ma".
  24 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  25 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 }.
  26 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 }.
  27 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
  28 definition max ≝ λn,m. if eqb (n - m) 0 then m else n.
  29 definition min ≝ λn,m. if eqb (n - m) 0 then n else m.
  30
  31 (* Ripasso
  32    =======
  33
  34    Il linguaggio delle formule, dove gli atomi sono
  35    rapperesentati da un numero naturale
  36 *)
  37 inductive Formula : Type ≝
  38 | FBot: Formula
  39 | FTop: Formula
  40 | FAtom: nat → Formula
  41 | FAnd: Formula → Formula → Formula
  42 | FOr: Formula → Formula → Formula
  43 | FImpl: Formula → Formula → Formula
  44 | FNot: Formula → Formula
  45 .
  46
  47 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
  48  match F with
  49   [ FBot ⇒ 0
  50   | FTop ⇒ 1
  51   | FAtom n ⇒ min (v n) 1
  52   | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
  53   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
  54   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
  55   | FNot F1 ⇒ 1 - (sem v F1)
  56   ]
  57 .
  58
  59 (* ATTENZIONE
  60    ==========
  61
  62    Non modificare quanto segue.
  63 *)
  64 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  65 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  66 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
  67 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
  68
  69 (*DOCBEGIN
  70
  71 La libreria di Matita
  72 =====================
  73
  74 Gli strumenti per la dimostrazione assistita sono corredati da
  75 librerie di teoremi già dimostrati. Per portare a termine l'esercitazione
  76 sono necessari i seguenti lemmi:
  77
  78 * lemma `sem_le_1` : `∀F,v. [[ F ]]_v ≤ 1`
  79 * lemma `min_1_1` : `∀x. x ≤ 1 → 1 - (1 - x) = x`
  80 * lemma `min_bool` : `∀n. min n 1 = 0 ∨ min n 1 = 1`
  81 * lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v`
  82 * lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v`
  83 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
  84
  85
  86 DOCEND*)
  87
  88 (* ATTENZIONE
  89    ==========
  90
  91    Non modificare quanto segue.
  92 *)
  93 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.
  94 lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1.  intros; cases n; [left;reflexivity] cases n1; right; reflexivity; qed.
  95 lemma min_max : ∀F,G,v.  min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v.  intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed.
  96 lemma max_min : ∀F,G,v.  max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v.  intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed.
  97 lemma min_1_1 : ∀x.x ≤ 1 → 1 - (1 - x) = x. intros; inversion H; intros; destruct; [reflexivity;] rewrite < (le_n_O_to_eq ? H1); reflexivity;qed.
  98 lemma sem_le_1 : ∀F,v.[[F]]_v ≤ 1. intros; cases (sem_bool F v); rewrite > H; [apply le_O_n|apply le_n]qed.
  99 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 100  match F with
 101   [ FBot ⇒ FBot
 102   | FTop ⇒ (*BEGIN*)FTop(*END*)
 103   | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*))
 104   (*BEGIN*)
 105   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
 106   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
 107   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
 108   (*END*)
 109   | FNot F ⇒ FNot (subst x G F)
 110   ].
 111
 112 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 113 notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 114 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 115 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 116 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 117 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 118 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 119
 120 theorem shannon :
 121   ∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v.
 122 assume F : Formula.
 123 assume x : ℕ.
 124 assume v : (ℕ → ℕ).
 125 we proceed by induction on F to prove ([[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v).
 126 case FBot.
 127   the thesis becomes ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
 128   we proceed by cases on (eqb [[ FAtom x ]]_v 0)
 129     to prove ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
 130   case true.
 131     the thesis becomes ([[ if true then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
 132     the thesis becomes ([[ FBot[FBot/x]]]_v = [[FBot]]_v).
 133     the thesis becomes ([[ FBot ]]_v = [[FBot]]_v).
 134     the thesis becomes (0 = 0).
 135     done.
 136   case false.
 137     done.
 138 case FTop.
 139   we proceed by cases on (eqb [[ FAtom x ]]_v 0)
 140     to prove ([[ if eqb [[FAtom x]]_v 0 then FTop[FBot/x] else (FTop[FTop/x]) ]]_v = [[FTop]]_v).
 141   case true.
 142     done.
 143   case false.
 144     done.
 145 case FAtom.
 146   assume n : ℕ.
 147   the thesis becomes ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 148   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H).
 149   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H1).
 150   we proceed by cases on H to prove
 151     ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 152   case Left. (* H2 : n = x *)
 153     we proceed by cases on H1 to prove
 154       ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 155     case Left. (* H3 : [[ FAtom x ]]_v = 0 *)
 156       conclude
 157           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 158         = ([[ if eqb 0 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
 159         = ([[ if true then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v).
 160         = ([[ (FAtom n)[ FBot/x ] ]]_v).
 161         = ([[ if eqb n x then FBot else (FAtom  n) ]]_v).
 162         = ([[ if eqb n n then FBot else (FAtom  n) ]]_v) by H2.
 163         = ([[ if true then FBot else (FAtom  n) ]]_v) by eqb_n_n.
 164         = ([[ FBot ]]_v).
 165         = 0.
 166         = [[ FAtom x ]]_v by H3.
 167         = [[ FAtom n ]]_v by H2.
 168       done.
 169     case Right.
 170       conclude
 171           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 172         = ([[ if eqb 1 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
 173         = ([[ if false then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v).
 174         = ([[ (FAtom n)[ FTop/x ] ]]_v).
 175         = ([[ if eqb n x then FTop else (FAtom  n) ]]_v).
 176         = ([[ if eqb n n then FTop else (FAtom  n) ]]_v) by H2.
 177         = ([[ if true then FTop else (FAtom  n) ]]_v) by eqb_n_n.
 178         = ([[ FTop ]]_v).
 179         = 1.
 180         = [[ FAtom x ]]_v by H3.
 181         = [[ FAtom n ]]_v by H2.
 182       done.
 183   case Right.
 184     we proceed by cases on H1 to prove
 185       ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 186     case Left.
 187       conclude
 188           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 189         = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
 190         = [[ (FAtom n)[ FBot/x ] ]]_v.
 191         = [[ if eqb n x then FBot else (FAtom n) ]]_v.
 192         = [[ if false then FBot else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2).
 193         = [[ FAtom n ]]_v.
 194       done.
 195     case Right.
 196       conclude
 197           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 198         = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
 199         = [[ FAtom n[ FTop/x ] ]]_v.
 200         = [[ if eqb n x then FTop else (FAtom n) ]]_v.
 201         = [[ if false then FTop else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2).
 202         = [[ FAtom n ]]_v.
 203       done.
 204 case FAnd.
 205   assume f : Formula.
 206   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 207   assume f1 : Formula.
 208   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1).
 209   the thesis becomes
 210     ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v).
 211   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 212   we proceed by cases on H2 to prove
 213     ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v).
 214   case Left.
 215     by H3, H we proved
 216       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 217     using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 218     by H3, 1 we proved
 219       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 220     using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
 221     conclude
 222         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
 223       = ([[ if eqb 0 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
 224       = ([[ if true then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v).
 225       = ([[ (FAnd f f1)[ FBot/x ] ]]_v).
 226       = ([[ FAnd (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
 227       = (min [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v).
 228       = (min [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5.
 229       = (min [[ f ]]_v [[ f1 ]]_v) by H6.
 230       = ([[ FAnd f f1 ]]_v).
 231     done.
 232   case Right.
 233     by H3, H we proved
 234       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 235     using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 236     by H3, 1 we proved
 237       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 238     using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
 239     conclude
 240         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
 241       = ([[ if eqb 1 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
 242       = ([[ if false then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v).
 243       = ([[ (FAnd f f1)[ FTop/x ] ]]_v).
 244       = ([[ FAnd (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
 245       = (min [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v).
 246       = (min [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5.
 247       = (min [[ f ]]_v [[ f1 ]]_v) by H6.
 248       = ([[ FAnd f f1 ]]_v).
 249     done.
 250 case FOr.
 251   assume f : Formula.
 252   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 253   assume f1 : Formula.
 254   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1).
 255   the thesis becomes
 256     ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v).
 257   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 258   we proceed by cases on H2 to prove
 259     ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v).
 260   case Left.
 261     by H3, H we proved
 262       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 263     using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 264     by H3, 1 we proved
 265       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 266     using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
 267     conclude
 268         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
 269       = ([[ if eqb 0 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
 270       = ([[ if true then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v).
 271       = ([[ (FOr f f1)[ FBot/x ] ]]_v).
 272       = ([[ FOr (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
 273       = (max [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v).
 274       = (max [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5.
 275       = (max [[ f ]]_v [[ f1 ]]_v) by H6.
 276       = ([[ FOr f f1 ]]_v).
 277     done.
 278   case Right.
 279     by H3, H we proved
 280       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 281     using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 282     by H3, 1 we proved
 283       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 284     using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
 285     conclude
 286         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
 287       = ([[ if eqb 1 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
 288       = ([[ if false then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v).
 289       = ([[ (FOr f f1)[ FTop/x ] ]]_v).
 290       = ([[ FOr (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
 291       = (max [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v).
 292       = (max [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5.
 293       = (max [[ f ]]_v [[ f1 ]]_v) by H6.
 294       = ([[ FOr f f1 ]]_v).
 295     done.
 296 case FImpl.
 297   assume f : Formula.
 298   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 299   assume f1 : Formula.
 300   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1).
 301   the thesis becomes
 302     ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v).
 303   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 304   we proceed by cases on H2 to prove
 305     ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v).
 306   case Left.
 307     by H3, H we proved
 308       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 309     using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 310     by H3, 1 we proved
 311       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 312     using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
 313     conclude
 314         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
 315       = ([[ if eqb 0 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
 316       = ([[ if true then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v).
 317       = ([[ (FImpl f f1)[ FBot/x ] ]]_v).
 318       = ([[ FImpl (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
 319       = (max (1 - [[ f[ FBot/x ] ]]_v) [[ f1[ FBot/x ] ]]_v).
 320       = (max (1 -  [[ f ]]_v) [[ f1[ FBot/x ] ]]_v) by H5.
 321       = (max (1 -  [[ f ]]_v) [[ f1 ]]_v) by H6.
 322       = ([[ FImpl f f1 ]]_v).
 323     done.
 324   case Right.
 325     by H3, H we proved
 326       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 327     using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 328     by H3, 1 we proved
 329       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 330     using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
 331     conclude
 332         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
 333       = ([[ if eqb 1 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
 334       = ([[ if false then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v).
 335       = ([[ (FImpl f f1)[ FTop/x ] ]]_v).
 336       = ([[ FImpl (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
 337       = (max (1 - [[ f[ FTop/x ] ]]_v) [[ f1[ FTop/x ] ]]_v).
 338       = (max (1 - [[ f ]]_v) [[ f1[ FTop/x ] ]]_v) by H5.
 339       = (max (1 - [[ f ]]_v) [[ f1 ]]_v) by H6.
 340       = ([[ FImpl f f1 ]]_v).
 341     done.
 342 case FNot.
 343   assume f : Formula.
 344   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 345   the thesis becomes
 346     ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v).
 347   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 348   we proceed by cases on H2 to prove
 349     ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v).
 350   case Left.
 351     by H1, H we proved
 352       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 353     using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 354     conclude
 355         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
 356       = ([[ if eqb 0 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
 357       = ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
 358       = ([[ (FNot f)[ FBot/x ] ]]_v).
 359       = ([[ FNot (f[ FBot/x ]) ]]_v).
 360       change with (1 - [[ f[ FBot/x ] ]]_v = [[ FNot f ]]_v).
 361       = (1 - [[ f ]]_v) by H5.
 362       change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
 363     done.
 364   case Right.
 365     by H1, H we proved
 366       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 367     using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 368     conclude
 369         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
 370       = ([[ if eqb 1 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
 371       = ([[ if false then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
 372       = ([[ (FNot f)[ FTop/x ] ]]_v).
 373       = ([[ FNot (f[ FTop/x ]) ]]_v).
 374       change with (1 - [[ f[ FTop/x ] ]]_v = [[ FNot f ]]_v) .
 375       = (1 - [[ f ]]_v) by H5.
 376       change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
 377     done.
 378 qed.