4 1. Leggere ATTENTAMENTE, e magari stampare, la documentazione reperibile
7 http://mowgli.cs.unibo.it/~tassi/exercise-shannon.ma.html
9 2. Questa volta si fa sul serio:
10 l'esercizio proposto è molto difficile, occorre la vostra massima
11 concentrazione (leggi: niente cut&paste selvaggio, cercate di capire!)
19 Compilare i seguenti campi:
36 Non modificare quanto segue
38 include "nat/minus.ma".
39 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
40 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 }.
41 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 }.
42 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
43 definition max ≝ λn,m. if eqb (n - m) 0 then m else n.
44 definition min ≝ λn,m. if eqb (n - m) 0 then n else m.
49 Il linguaggio delle formule, dove gli atomi sono
50 rapperesentati da un numero naturale
52 inductive Formula : Type ≝
55 | FAtom: nat → Formula
56 | FAnd: Formula → Formula → Formula
57 | FOr: Formula → Formula → Formula
58 | FImpl: Formula → Formula → Formula
59 | FNot: Formula → Formula
62 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
66 | FAtom n ⇒ min (v n) 1
67 | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
68 | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
69 | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
70 | FNot F1 ⇒ 1 - (sem v F1)
77 Non modificare quanto segue.
79 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
80 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
81 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
82 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
87 Non modificare quanto segue.
89 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.
91 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
95 | FAtom n ⇒ if eqb n x then G else (FAtom n)
96 | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
97 | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
98 | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
99 | FNot F ⇒ FNot (subst x G F)
102 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
103 notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
104 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
105 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
106 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }.
107 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
108 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
112 La libreria di Matita
113 =====================
115 Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
117 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
118 * lemma `eqb_n_n` : `∀x.eqb x x = true`
119 * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
121 Il teorema di espansione di Shannon
122 ===================================
124 Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente
125 formula ha in un mondo `v` la stessa semantica di `F`:
127 if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x])
129 Ovvero, sostituisco l'atomo `x` con `FBot` se tale atomo è falso
130 nel mondo `v`, altrimenti lo sostituisco con `FTop`.
135 ∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v.
139 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).
145 La dimostrazione procede per induzione sulla formula `F`. Si ricorda che:
147 1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un
148 simbolo `→` è opportuno usare il comando `assume` oppure `suppose` (che
149 vengono nuovamente spiegati in seguito).
151 2. Ogni caso (o sotto caso) della dimostrazione:
153 1. Inizia con una sequenza di comandi `assume` o `suppose` oppure
154 `by induction hypothesis we know`. Tale sequenza di comandi può anche
157 2. Continua poi con almeno un comando `the thesis becomes`.
159 3. Eventualmente seguono vari comandi `by ... we proved` per combinare le
160 ipotesi tra loro o utilizzare i teoremi già disponibili per generare nuove
163 4. Eventualmente uno o più comandi `we proceed by cases on (...) to prove (...)`.
165 5. Se necessario un comando `conclude` seguito da un numero anche
166 molto lungo di passi `= (...) by ... .` per rendere la parte
167 sinistra della vostra tesi uguale alla parte destra.
169 6. Ogni caso termina con `done`.
171 3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot)
172 avrà tante ipotesi induttive quante sono le sue sottoformule e tali
173 ipotesi sono necessarie per portare a termine la dimostrazione.
184 [[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v
186 Si procede per casi su `eqb [[FAtom x]]_v 0`. In entrambi i casi basta
187 espandere piano piano le definizioni.
189 ### I comandi da utilizzare
191 the thesis becomes (...).
193 we proceed by cases on (...) to prove (...).
200 the thesis becomes ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
201 we proceed by cases on (eqb [[ FAtom x ]]_v 0)
202 to prove ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
204 the thesis becomes ([[ if true then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
205 the thesis becomes ([[ FBot[FBot/x]]]_v = [[FBot]]_v).
206 the thesis becomes ([[ FBot ]]_v = [[FBot]]_v).
207 the thesis becomes (0 = 0).
220 we proceed by cases on (eqb [[ FAtom x ]]_v 0)
221 to prove ([[ if eqb [[FAtom x]]_v 0 then FTop[FBot/x] else (FTop[FTop/x]) ]]_v = [[FTop]]_v).
232 Questo è il caso più difficile di tutta la dimostrazione.
234 La tesi è `([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v)`
236 Per dimostrarla è necessario utilizzare il lemma `decidable_eq_nat` per
237 ottenere l'ipotesi agiuntiva `n = x ∨ n ≠ x` che chiameremo `H` e il lemma
238 `sem_bool` per ottenre l'ipotesi aggiuntiva `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1`
241 Si procede poi per casi sull'ipotesi `H`, e in ogni suo sotto caso si procede
244 Nei casi in cui è presente l'ipotesi aggiuntiva `n ≠ x` è bene
245 ottenre tramite il lemma `not_eq_to_eqb_false` l'ipotesi aggiuntiva
248 Abbiamo quindi quattro casi, in tutti si procede con un comando `conclude`:
250 1. Caso in cui `n=x` e `[[ FAtom x ]]_v = 0`.
252 Utilizzando l'ipotesi `[[ FAtom x ]]_v = 0` e espandendo alcune definizioni
253 si ottiene che la parte sinistra della conclusione è
255 ([[ if eqb n x then FBot else (FAtom n) ]]_v)
257 Usando l'ipotesi `n = x`, poi il lemma `eqb_n_n` e espandendo alcune
258 definizioni si ottiene `0`. Tornando ad usare le due ipotesi
259 `n=x` e `[[ FAtom x ]]_v = 0` si ottiene una formula uguale al
260 lato destro della conclusione.
262 2. Caso in cui `n=x` e `[[ FAtom x ]]_v = 1`.
264 Analogo al caso precedente.
266 3. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 0`.
268 Si ottiene l'ipotesi aggiuntiva `eqb n x = false` usando il lemma
269 `not_eq_to_eqb_false` insieme all'ipotesi `n ≠ x`. Usando il comando
270 conlude e l'ipotesi `[[ FAtom x ]]_v = 0`, la nuova ipotesi appena
271 ottenuta e espandendo alcune definizioni si ottiene una formula
272 uguale a quella di destra.
274 4. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 1`.
276 Analogo al caso precedente.
278 ### I comandi da usare
280 * `assume ... : (...) .`
282 Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume
283 un numero naturale `n`.
285 * `by ..., ..., ..., we proved (...) (...).`
287 Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi.
288 Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi
289 `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`.
291 * `conclude (...) = (...) by ... .`
293 Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
294 con cui sini inizia una catena di uguaglianze. La prima formula che si
295 scrive deve essere esattamente uguale alla parte sinistra della conclusione
296 originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.`
297 Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione
298 di una definizione, la parte `by ...` deve essere omessa.
302 Continua un comando `conclude`, lavorando sempre sulla parte sinistra della
307 the thesis becomes ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
308 by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H).
309 by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H1).
310 we proceed by cases on H to prove
311 ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
312 case Left. (* H2 : n = x *)
313 we proceed by cases on H1 to prove
314 ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
315 case Left. (* H3 : [[ FAtom x ]]_v = 0 *)
317 ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
318 = ([[ if eqb 0 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
319 = ([[ if true then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v).
320 = ([[ (FAtom n)[ FBot/x ] ]]_v).
321 = ([[ if eqb n x then FBot else (FAtom n) ]]_v).
322 = ([[ if eqb n n then FBot else (FAtom n) ]]_v) by H2.
323 = ([[ if true then FBot else (FAtom n) ]]_v) by eqb_n_n.
326 = [[ FAtom x ]]_v by H3.
327 = [[ FAtom n ]]_v by H2.
331 ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
332 = ([[ if eqb 1 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
333 = ([[ if false then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v).
334 = ([[ (FAtom n)[ FTop/x ] ]]_v).
335 = ([[ if eqb n x then FTop else (FAtom n) ]]_v).
336 = ([[ if eqb n n then FTop else (FAtom n) ]]_v) by H2.
337 = ([[ if true then FTop else (FAtom n) ]]_v) by eqb_n_n.
340 = [[ FAtom x ]]_v by H3.
341 = [[ FAtom n ]]_v by H2.
344 by not_eq_to_eqb_false, H2 we proved (eqb n x = false) (H3).
345 we proceed by cases on H1 to prove
346 ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
349 ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
350 = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.
351 = [[ (FAtom n)[ FBot/x ] ]]_v.
352 = [[ if eqb n x then FBot else (FAtom n) ]]_v.
353 = [[ if false then FBot else (FAtom n) ]]_v by H3.
358 ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
359 = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.
360 = [[ FAtom n[ FTop/x ] ]]_v.
361 = [[ if eqb n x then FTop else (FAtom n) ]]_v.
362 = [[ if false then FTop else (FAtom n) ]]_v by H3.
371 Una volta assunte eventuali sottoformule e ipotesi induttive
372 la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v)`.
376 by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
378 by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H1).
380 ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v).
381 by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
382 we proceed by cases on H2 to prove
383 ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v).
386 ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
387 by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
389 ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H6).
390 by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
392 ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
393 = ([[ if eqb 0 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
394 = ([[ if true then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v).
395 = ([[ (FAnd f f1)[ FBot/x ] ]]_v).
396 = ([[ FAnd (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
397 = (min [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v).
398 = (min [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5.
399 = (min [[ f ]]_v [[ f1 ]]_v) by H6.
400 = ([[ FAnd f f1 ]]_v).
404 ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
405 by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
407 ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H6).
408 by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
410 ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
411 = ([[ if eqb 1 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
412 = ([[ if false then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v).
413 = ([[ (FAnd f f1)[ FTop/x ] ]]_v).
414 = ([[ FAnd (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
415 = (min [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v).
416 = (min [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5.
417 = (min [[ f ]]_v [[ f1 ]]_v) by H6.
418 = ([[ FAnd f f1 ]]_v).
426 Una volta assunte eventuali sottoformule e ipotesi induttive
427 la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v)`.
429 Analogo al caso FAnd.
433 by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
435 by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H1).
437 ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v).
438 by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
439 we proceed by cases on H2 to prove
440 ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v).
443 ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
444 by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
446 ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H6).
447 by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
449 ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
450 = ([[ if eqb 0 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
451 = ([[ if true then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v).
452 = ([[ (FOr f f1)[ FBot/x ] ]]_v).
453 = ([[ FOr (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
454 = (max [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v).
455 = (max [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5.
456 = (max [[ f ]]_v [[ f1 ]]_v) by H6.
457 = ([[ FOr f f1 ]]_v).
461 ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
462 by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
464 ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H6).
465 by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
467 ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
468 = ([[ if eqb 1 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
469 = ([[ if false then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v).
470 = ([[ (FOr f f1)[ FTop/x ] ]]_v).
471 = ([[ FOr (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
472 = (max [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v).
473 = (max [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5.
474 = (max [[ f ]]_v [[ f1 ]]_v) by H6.
475 = ([[ FOr f f1 ]]_v).
483 Una volta assunte eventuali sottoformule e ipotesi induttive
484 la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v)`.
486 Analogo al caso FAnd.
490 by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
492 by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H1).
494 ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v).
495 by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
496 we proceed by cases on H2 to prove
497 ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v).
500 ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
501 by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
503 ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H6).
504 by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
506 ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
507 = ([[ if eqb 0 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
508 = ([[ if true then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v).
509 = ([[ (FImpl f f1)[ FBot/x ] ]]_v).
510 = ([[ FImpl (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
511 = (max (1 - [[ f[ FBot/x ] ]]_v) [[ f1[ FBot/x ] ]]_v).
512 = (max (1 - [[ f ]]_v) [[ f1[ FBot/x ] ]]_v) by H5.
513 = (max (1 - [[ f ]]_v) [[ f1 ]]_v) by H6.
514 = ([[ FImpl f f1 ]]_v).
518 ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
519 by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
521 ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ]) ]]_v = [[ f1 ]]_v) (H6).
522 by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
524 ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
525 = ([[ if eqb 1 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
526 = ([[ if false then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v).
527 = ([[ (FImpl f f1)[ FTop/x ] ]]_v).
528 = ([[ FImpl (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
529 = (max (1 - [[ f[ FTop/x ] ]]_v) [[ f1[ FTop/x ] ]]_v).
530 = (max (1 - [[ f ]]_v) [[ f1[ FTop/x ] ]]_v) by H5.
531 = (max (1 - [[ f ]]_v) [[ f1 ]]_v) by H6.
532 = ([[ FImpl f f1 ]]_v).
544 by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
546 ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v).
547 by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
548 we proceed by cases on H2 to prove
549 ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v).
552 ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
553 by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
555 ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
556 = ([[ if eqb 0 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
557 = ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
558 = ([[ (FNot f)[ FBot/x ] ]]_v).
559 = ([[ FNot (f[ FBot/x ]) ]]_v).
560 (* FIXME, ASSERT IN PARAMOD = (1 - [[ f[ FBot/x ] ]]_v). = [[ FNot f ]]_v). *)
561 change with (1 - [[ f[ FBot/x ] ]]_v = [[ FNot f ]]_v).
562 = (1 - [[ f ]]_v) by H5.
563 change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
567 ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H4).
568 by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
570 ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
571 = ([[ if eqb 1 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
572 = ([[ if false then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
573 = ([[ (FNot f)[ FTop/x ] ]]_v).
574 = ([[ FNot (f[ FTop/x ]) ]]_v).
575 change with (1 - [[ f[ FTop/x ] ]]_v = [[ FNot f ]]_v) .
576 = (1 - [[ f ]]_v) by H5.
577 change with ([[ FNot f ]]_v = [[ FNot f ]]_v).