From 9dfc8aced0bb2c643d2e04d582f5c288698b1d9e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 2 Nov 2008 16:23:30 +0000 Subject: [PATCH] shannon proved --- .../matita/contribs/didactic/shannon.ma | 350 +++++++++++++----- 1 file changed, 260 insertions(+), 90 deletions(-) diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma index ccbaf956d..e35f8046e 100644 --- a/helm/software/matita/contribs/didactic/shannon.ma +++ b/helm/software/matita/contribs/didactic/shannon.ma @@ -1,11 +1,3 @@ -(* Esercitazione di logica 29/10/2008. - - Note per gli esercizi: - - http://www.cs.unibo.it/~tassi/exercise-duality.ma.html - -*) - (* Esercizio 0 =========== @@ -21,49 +13,8 @@ Matricola2: ... Account2: ... - Prima di abbandonare la postazione: - - * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella) - /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui - account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma - - * mandatevi via email o stampate il file. Per stampare potete usare - usare l'editor gedit che offre la funzionalità di stampa *) -(*DOCBEGIN - -Il teorema di dualità -===================== - -Il teorema di dualizzazione dice che date due formule `F1` ed `F2`, -se le due formule sono equivalenti (`F1 ≡ F2`) allora anche le -loro dualizzate lo sono (`dualize F1 ≡ dualize F2`). - -L'ingrediente principale è la funzione di dualizzazione di una formula `F`: - - * Scambia FTop con FBot e viceversa - - * Scambia il connettivo FAnd con FOr e viceversa - - * Sostituisce il connettivo FImpl con FAnd e nega la - prima sottoformula. - - Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in - `¬A ∧ (B ∨ ⊤)`. - -Per dimostrare il teorema di dualizzazione in modo agevole è necessario -definire altre nozioni: - -* La funzione `negate` che presa una formula `F` ne nega gli atomi. - Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare `¬A ∨ (⊤ → ¬B)`. - -* La funzione `invert` permette di invertire un mondo `v`. - Ovvero, per ogni indice di atomo `i`, se `v i` restituisce - `1` allora `(invert v) i` restituisce `0` e viceversa. - -DOCEND*) - (* ATTENZIONE ========== @@ -93,23 +44,11 @@ inductive Formula : Type ≝ | FNot: Formula → Formula . -(* Esercizio 1 - =========== - - Modificare la funzione `sem` scritta nella precedente - esercitazione in modo che valga solo 0 oppure 1 nel caso degli - atomi, anche nel caso in cui il mondo `v` restituisca un numero - maggiore di 1. - - Suggerimento: non è necessario usare il costrutto if_then_else - e tantomento il predicato di maggiore o uguale. È invece possibile - usare la funzione `min`. -*) let rec sem (v: nat → nat) (F: Formula) on F : nat ≝ match F with [ FBot ⇒ 0 | FTop ⇒ 1 - | FAtom n ⇒ (*BEGIN*)min (v n) 1(*END*) + | FAtom n ⇒ min (v n) 1 | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) @@ -127,20 +66,6 @@ notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 f 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). -definition v20 ≝ λx. - if eqb x 0 then 2 - else if eqb x 1 then 1 - else 0. - -(* Test 1 - ====== - - La semantica della formula `(A ∨ C)` nel mondo `v20` in cui - `A` vale `2` e `C` vale `0` deve valere `1`. - -*) -eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. - (*DOCBEGIN La libreria di Matita @@ -155,7 +80,8 @@ sono necessari i seguenti lemmi: * lemma `min_bool` : `∀n. min n 1 = 0 ∨ min n 1 = 1` * lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v` * lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v` -* lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3` +* lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y` + DOCEND*) @@ -192,17 +118,261 @@ notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). theorem shannon : - ∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v. -intros; elim F; -[1,2: cases (eqb [[FAtom x]]_v 0); reflexivity; -|4,5,6: cases (eqb [[FAtom x]]_v 0) in H H1; simplify; intros; rewrite > H; rewrite > H1; reflexivity; -|7: cases (eqb [[FAtom x]]_v 0) in H; simplify; intros; rewrite > H; reflexivity; -| cases (sem_bool (FAtom x) v); rewrite > H; simplify; - cases (decidable_eq_nat n x); destruct H1; - [1,3: rewrite > eqb_n_n; simplify; rewrite >H;reflexivity;. - |*:simplify in H; rewrite > (not_eq_to_eqb_false ?? H1); simplify; reflexivity;]] + ∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v. +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +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). +case FBot. + the thesis becomes ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v). + we proceed by cases on (eqb [[ FAtom x ]]_v 0) + to prove ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v). + case true. + the thesis becomes ([[ if true then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v). + the thesis becomes ([[ FBot[FBot/x]]]_v = [[FBot]]_v). + the thesis becomes ([[ FBot ]]_v = [[FBot]]_v). + the thesis becomes (0 = 0). + done. + case false. + done. +case FTop. + we proceed by cases on (eqb [[ FAtom x ]]_v 0) + to prove ([[ if eqb [[FAtom x]]_v 0 then FTop[FBot/x] else (FTop[FTop/x]) ]]_v = [[FTop]]_v). + case true. + done. + case false. + done. +case FAtom. + assume n : ℕ. + the thesis becomes ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v). + by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H). + by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H1). + we proceed by cases on H to prove + ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v). + case Left. (* H2 : n = x *) + we proceed by cases on H1 to prove + ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v). + case Left. (* H3 : [[ FAtom x ]]_v = 0 *) + conclude + ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) + = ([[ if eqb 0 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3. + = ([[ if true then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v). + = ([[ (FAtom n)[ FBot/x ] ]]_v). + = ([[ if eqb n x then FBot else (FAtom n) ]]_v). + = ([[ if eqb n n then FBot else (FAtom n) ]]_v) by H2. + = ([[ if true then FBot else (FAtom n) ]]_v) by eqb_n_n. + = ([[ FBot ]]_v). + = 0. + = [[ FAtom x ]]_v by H3. + = [[ FAtom n ]]_v by H2. + done. + case Right. + conclude + ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) + = ([[ if eqb 1 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3. + = ([[ if false then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v). + = ([[ (FAtom n)[ FTop/x ] ]]_v). + = ([[ if eqb n x then FTop else (FAtom n) ]]_v). + = ([[ if eqb n n then FTop else (FAtom n) ]]_v) by H2. + = ([[ if true then FTop else (FAtom n) ]]_v) by eqb_n_n. + = ([[ FTop ]]_v). + = 1. + = [[ FAtom x ]]_v by H3. + = [[ FAtom n ]]_v by H2. + done. + case Right. + we proceed by cases on H1 to prove + ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v). + case Left. + conclude + ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) + = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3. + = [[ (FAtom n)[ FBot/x ] ]]_v. + = [[ if eqb n x then FBot else (FAtom n) ]]_v. + = [[ if false then FBot else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2). + = [[ FAtom n ]]_v. + done. + case Right. + conclude + ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) + = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3. + = [[ FAtom n[ FTop/x ] ]]_v. + = [[ if eqb n x then FTop else (FAtom n) ]]_v. + = [[ if false then FTop else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2). + = [[ FAtom n ]]_v. + done. +case FAnd. + assume f : Formula. + by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H). + assume f1 : Formula. + by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1). + the thesis becomes + ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v). + by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2). + we proceed by cases on H2 to prove + ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v). + case Left. + by H3, H we proved + ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5). + by H3, 1 we proved + ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6). + using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) + = ([[ if eqb 0 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3. + = ([[ if true then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v). + = ([[ (FAnd f f1)[ FBot/x ] ]]_v). + = ([[ FAnd (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v). + = (min [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v). + = (min [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5. + = (min [[ f ]]_v [[ f1 ]]_v) by H6. + = ([[ FAnd f f1 ]]_v). + done. + case Right. + by H3, H we proved + ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5). + by H3, 1 we proved + ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6). + using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) + = ([[ if eqb 1 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3. + = ([[ if false then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v). + = ([[ (FAnd f f1)[ FTop/x ] ]]_v). + = ([[ FAnd (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v). + = (min [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v). + = (min [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5. + = (min [[ f ]]_v [[ f1 ]]_v) by H6. + = ([[ FAnd f f1 ]]_v). + done. +case FOr. + assume f : Formula. + by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H). + assume f1 : Formula. + by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1). + the thesis becomes + ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v). + by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2). + we proceed by cases on H2 to prove + ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v). + case Left. + by H3, H we proved + ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5). + by H3, 1 we proved + ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6). + using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) + = ([[ if eqb 0 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3. + = ([[ if true then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v). + = ([[ (FOr f f1)[ FBot/x ] ]]_v). + = ([[ FOr (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v). + = (max [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v). + = (max [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5. + = (max [[ f ]]_v [[ f1 ]]_v) by H6. + = ([[ FOr f f1 ]]_v). + done. + case Right. + by H3, H we proved + ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5). + by H3, 1 we proved + ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6). + using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) + = ([[ if eqb 1 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3. + = ([[ if false then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v). + = ([[ (FOr f f1)[ FTop/x ] ]]_v). + = ([[ FOr (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v). + = (max [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v). + = (max [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5. + = (max [[ f ]]_v [[ f1 ]]_v) by H6. + = ([[ FOr f f1 ]]_v). + done. +case FImpl. + assume f : Formula. + by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H). + assume f1 : Formula. + by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1). + the thesis becomes + ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v). + by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2). + we proceed by cases on H2 to prove + ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v). + case Left. + by H3, H we proved + ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5). + by H3, 1 we proved + ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6). + using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) + = ([[ if eqb 0 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3. + = ([[ if true then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v). + = ([[ (FImpl f f1)[ FBot/x ] ]]_v). + = ([[ FImpl (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v). + = (max (1 - [[ f[ FBot/x ] ]]_v) [[ f1[ FBot/x ] ]]_v). + = (max (1 - [[ f ]]_v) [[ f1[ FBot/x ] ]]_v) by H5. + = (max (1 - [[ f ]]_v) [[ f1 ]]_v) by H6. + = ([[ FImpl f f1 ]]_v). + done. + case Right. + by H3, H we proved + ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5). + by H3, 1 we proved + ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6). + using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) + = ([[ if eqb 1 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3. + = ([[ if false then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v). + = ([[ (FImpl f f1)[ FTop/x ] ]]_v). + = ([[ FImpl (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v). + = (max (1 - [[ f[ FTop/x ] ]]_v) [[ f1[ FTop/x ] ]]_v). + = (max (1 - [[ f ]]_v) [[ f1[ FTop/x ] ]]_v) by H5. + = (max (1 - [[ f ]]_v) [[ f1 ]]_v) by H6. + = ([[ FImpl f f1 ]]_v). + done. +case FNot. + assume f : Formula. + by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H). + the thesis becomes + ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v). + by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2). + we proceed by cases on H2 to prove + ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v). + case Left. + by H1, H we proved + ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) + = ([[ if eqb 0 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1. + = ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v). + = ([[ (FNot f)[ FBot/x ] ]]_v). + = ([[ FNot (f[ FBot/x ]) ]]_v). + change with (1 - [[ f[ FBot/x ] ]]_v = [[ FNot f ]]_v). + = (1 - [[ f ]]_v) by H5. + change with ([[ FNot f ]]_v = [[ FNot f ]]_v). + done. + case Right. + by H1, H we proved + ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4). + using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5). + conclude + ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) + = ([[ if eqb 1 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1. + = ([[ if false then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v). + = ([[ (FNot f)[ FTop/x ] ]]_v). + = ([[ FNot (f[ FTop/x ]) ]]_v). + change with (1 - [[ f[ FTop/x ] ]]_v = [[ FNot f ]]_v) . + = (1 - [[ f ]]_v) by H5. + change with ([[ FNot f ]]_v = [[ FNot f ]]_v). + done. qed. - - - - \ No newline at end of file -- 2.39.2