From: Cosimo Oliboni Date: Tue, 4 Aug 2009 17:43:23 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3574 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=db235934efa41a0f38e79747f6db4f468367410b;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii.ma b/helm/software/matita/contribs/ng_assembly/common/ascii.ma new file mode 100755 index 000000000..9cebb3317 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/ascii.ma @@ -0,0 +1,167 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ************************** *) +(* DEFINIZIONE ASCII MINIMALE *) +(* ************************** *) + +ninductive ascii : Type ≝ +(* numeri *) + ch_0: ascii +| ch_1: ascii +| ch_2: ascii +| ch_3: ascii +| ch_4: ascii +| ch_5: ascii +| ch_6: ascii +| ch_7: ascii +| ch_8: ascii +| ch_9: ascii + +(* simboli *) +| ch__: ascii + +(* maiuscole *) +| ch_A: ascii +| ch_B: ascii +| ch_C: ascii +| ch_D: ascii +| ch_E: ascii +| ch_F: ascii +| ch_G: ascii +| ch_H: ascii +| ch_I: ascii +| ch_J: ascii +| ch_K: ascii +| ch_L: ascii +| ch_M: ascii +| ch_N: ascii +| ch_O: ascii +| ch_P: ascii +| ch_Q: ascii +| ch_R: ascii +| ch_S: ascii +| ch_T: ascii +| ch_U: ascii +| ch_V: ascii +| ch_W: ascii +| ch_X: ascii +| ch_Y: ascii +| ch_Z: ascii + +(* minuscole *) +| ch_a: ascii +| ch_b: ascii +| ch_c: ascii +| ch_d: ascii +| ch_e: ascii +| ch_f: ascii +| ch_g: ascii +| ch_h: ascii +| ch_i: ascii +| ch_j: ascii +| ch_k: ascii +| ch_l: ascii +| ch_m: ascii +| ch_n: ascii +| ch_o: ascii +| ch_p: ascii +| ch_q: ascii +| ch_r: ascii +| ch_s: ascii +| ch_t: ascii +| ch_u: ascii +| ch_v: ascii +| ch_w: ascii +| ch_x: ascii +| ch_y: ascii +| ch_z: ascii. + +(* confronto fra ascii *) +ndefinition eq_ascii ≝ +λc,c':ascii.match c with + [ ch_0 ⇒ match c' with [ ch_0 ⇒ true | _ ⇒ false ] + | ch_1 ⇒ match c' with [ ch_1 ⇒ true | _ ⇒ false ] + | ch_2 ⇒ match c' with [ ch_2 ⇒ true | _ ⇒ false ] + | ch_3 ⇒ match c' with [ ch_3 ⇒ true | _ ⇒ false ] + | ch_4 ⇒ match c' with [ ch_4 ⇒ true | _ ⇒ false ] + | ch_5 ⇒ match c' with [ ch_5 ⇒ true | _ ⇒ false ] + | ch_6 ⇒ match c' with [ ch_6 ⇒ true | _ ⇒ false ] + | ch_7 ⇒ match c' with [ ch_7 ⇒ true | _ ⇒ false ] + | ch_8 ⇒ match c' with [ ch_8 ⇒ true | _ ⇒ false ] + | ch_9 ⇒ match c' with [ ch_9 ⇒ true | _ ⇒ false ] + | ch__ ⇒ match c' with [ ch__ ⇒ true | _ ⇒ false ] + | ch_A ⇒ match c' with [ ch_A ⇒ true | _ ⇒ false ] + | ch_B ⇒ match c' with [ ch_B ⇒ true | _ ⇒ false ] + | ch_C ⇒ match c' with [ ch_C ⇒ true | _ ⇒ false ] + | ch_D ⇒ match c' with [ ch_D ⇒ true | _ ⇒ false ] + | ch_E ⇒ match c' with [ ch_E ⇒ true | _ ⇒ false ] + | ch_F ⇒ match c' with [ ch_F ⇒ true | _ ⇒ false ] + | ch_G ⇒ match c' with [ ch_G ⇒ true | _ ⇒ false ] + | ch_H ⇒ match c' with [ ch_H ⇒ true | _ ⇒ false ] + | ch_I ⇒ match c' with [ ch_I ⇒ true | _ ⇒ false ] + | ch_J ⇒ match c' with [ ch_J ⇒ true | _ ⇒ false ] + | ch_K ⇒ match c' with [ ch_K ⇒ true | _ ⇒ false ] + | ch_L ⇒ match c' with [ ch_L ⇒ true | _ ⇒ false ] + | ch_M ⇒ match c' with [ ch_M ⇒ true | _ ⇒ false ] + | ch_N ⇒ match c' with [ ch_N ⇒ true | _ ⇒ false ] + | ch_O ⇒ match c' with [ ch_O ⇒ true | _ ⇒ false ] + | ch_P ⇒ match c' with [ ch_P ⇒ true | _ ⇒ false ] + | ch_Q ⇒ match c' with [ ch_Q ⇒ true | _ ⇒ false ] + | ch_R ⇒ match c' with [ ch_R ⇒ true | _ ⇒ false ] + | ch_S ⇒ match c' with [ ch_S ⇒ true | _ ⇒ false ] + | ch_T ⇒ match c' with [ ch_T ⇒ true | _ ⇒ false ] + | ch_U ⇒ match c' with [ ch_U ⇒ true | _ ⇒ false ] + | ch_V ⇒ match c' with [ ch_V ⇒ true | _ ⇒ false ] + | ch_W ⇒ match c' with [ ch_W ⇒ true | _ ⇒ false ] + | ch_X ⇒ match c' with [ ch_X ⇒ true | _ ⇒ false ] + | ch_Y ⇒ match c' with [ ch_Y ⇒ true | _ ⇒ false ] + | ch_Z ⇒ match c' with [ ch_Z ⇒ true | _ ⇒ false ] + | ch_a ⇒ match c' with [ ch_a ⇒ true | _ ⇒ false ] + | ch_b ⇒ match c' with [ ch_b ⇒ true | _ ⇒ false ] + | ch_c ⇒ match c' with [ ch_c ⇒ true | _ ⇒ false ] + | ch_d ⇒ match c' with [ ch_d ⇒ true | _ ⇒ false ] + | ch_e ⇒ match c' with [ ch_e ⇒ true | _ ⇒ false ] + | ch_f ⇒ match c' with [ ch_f ⇒ true | _ ⇒ false ] + | ch_g ⇒ match c' with [ ch_g ⇒ true | _ ⇒ false ] + | ch_h ⇒ match c' with [ ch_h ⇒ true | _ ⇒ false ] + | ch_i ⇒ match c' with [ ch_i ⇒ true | _ ⇒ false ] + | ch_j ⇒ match c' with [ ch_j ⇒ true | _ ⇒ false ] + | ch_k ⇒ match c' with [ ch_k ⇒ true | _ ⇒ false ] + | ch_l ⇒ match c' with [ ch_l ⇒ true | _ ⇒ false ] + | ch_m ⇒ match c' with [ ch_m ⇒ true | _ ⇒ false ] + | ch_n ⇒ match c' with [ ch_n ⇒ true | _ ⇒ false ] + | ch_o ⇒ match c' with [ ch_o ⇒ true | _ ⇒ false ] + | ch_p ⇒ match c' with [ ch_p ⇒ true | _ ⇒ false ] + | ch_q ⇒ match c' with [ ch_q ⇒ true | _ ⇒ false ] + | ch_r ⇒ match c' with [ ch_r ⇒ true | _ ⇒ false ] + | ch_s ⇒ match c' with [ ch_s ⇒ true | _ ⇒ false ] + | ch_t ⇒ match c' with [ ch_t ⇒ true | _ ⇒ false ] + | ch_u ⇒ match c' with [ ch_u ⇒ true | _ ⇒ false ] + | ch_v ⇒ match c' with [ ch_v ⇒ true | _ ⇒ false ] + | ch_w ⇒ match c' with [ ch_w ⇒ true | _ ⇒ false ] + | ch_x ⇒ match c' with [ ch_x ⇒ true | _ ⇒ false ] + | ch_y ⇒ match c' with [ ch_y ⇒ true | _ ⇒ false ] + | ch_z ⇒ match c' with [ ch_z ⇒ true | _ ⇒ false ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas1.ma new file mode 100755 index 000000000..9d9920dea --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas1.ma @@ -0,0 +1,540 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/ascii.ma". + +(* ************************** *) +(* DEFINIZIONE ASCII MINIMALE *) +(* ************************** *) + +ndefinition ascii_destruct1 : Πc2.ΠP:Prop.ch_0 = c2 → match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##1: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct2 : Πc2.ΠP:Prop.ch_1 = c2 → match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##2: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct3 : Πc2.ΠP:Prop.ch_2 = c2 → match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##3: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct4 : Πc2.ΠP:Prop.ch_3 = c2 → match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##4: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct5 : Πc2.ΠP:Prop.ch_4 = c2 → match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##5: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct6 : Πc2.ΠP:Prop.ch_5 = c2 → match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##6: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct7 : Πc2.ΠP:Prop.ch_6 = c2 → match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##7: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct8 : Πc2.ΠP:Prop.ch_7 = c2 → match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##8: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct9 : Πc2.ΠP:Prop.ch_8 = c2 → match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##9: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##10: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct11 : Πc2.ΠP:Prop.ch__ = c2 → match c2 with [ ch__ ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##11: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct12 : Πc2.ΠP:Prop.ch_A = c2 → match c2 with [ ch_A ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##12: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct13 : Πc2.ΠP:Prop.ch_B = c2 → match c2 with [ ch_B ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##13: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct14 : Πc2.ΠP:Prop.ch_C = c2 → match c2 with [ ch_C ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##14: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct15 : Πc2.ΠP:Prop.ch_D = c2 → match c2 with [ ch_D ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##15: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct16 : Πc2.ΠP:Prop.ch_E = c2 → match c2 with [ ch_E ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##16: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct17 : Πc2.ΠP:Prop.ch_F = c2 → match c2 with [ ch_F ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##17: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct18 : Πc2.ΠP:Prop.ch_G = c2 → match c2 with [ ch_G ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##18: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct19 : Πc2.ΠP:Prop.ch_H = c2 → match c2 with [ ch_H ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##19: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct20 : Πc2.ΠP:Prop.ch_I = c2 → match c2 with [ ch_I ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##20: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct21 : Πc2.ΠP:Prop.ch_J = c2 → match c2 with [ ch_J ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##21: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct22 : Πc2.ΠP:Prop.ch_K = c2 → match c2 with [ ch_K ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##22: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct23 : Πc2.ΠP:Prop.ch_L = c2 → match c2 with [ ch_L ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##23: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct24 : Πc2.ΠP:Prop.ch_M = c2 → match c2 with [ ch_M ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##24: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct25 : Πc2.ΠP:Prop.ch_N = c2 → match c2 with [ ch_N ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##25: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct26 : Πc2.ΠP:Prop.ch_O = c2 → match c2 with [ ch_O ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##26: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct27 : Πc2.ΠP:Prop.ch_P = c2 → match c2 with [ ch_P ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##27: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct28 : Πc2.ΠP:Prop.ch_Q = c2 → match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##28: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct29 : Πc2.ΠP:Prop.ch_R = c2 → match c2 with [ ch_R ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##29: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct30 : Πc2.ΠP:Prop.ch_S = c2 → match c2 with [ ch_S ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##30: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct31 : Πc2.ΠP:Prop.ch_T = c2 → match c2 with [ ch_T ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##31: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct32 : Πc2.ΠP:Prop.ch_U = c2 → match c2 with [ ch_U ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##32: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct33 : Πc2.ΠP:Prop.ch_V = c2 → match c2 with [ ch_V ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##33: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct34 : Πc2.ΠP:Prop.ch_W = c2 → match c2 with [ ch_W ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##34: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct35 : Πc2.ΠP:Prop.ch_X = c2 → match c2 with [ ch_X ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##35: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct36 : Πc2.ΠP:Prop.ch_Y = c2 → match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##36: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct37 : Πc2.ΠP:Prop.ch_Z = c2 → match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##37: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct38 : Πc2.ΠP:Prop.ch_a = c2 → match c2 with [ ch_a ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##38: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct39 : Πc2.ΠP:Prop.ch_b = c2 → match c2 with [ ch_b ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##39: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct40 : Πc2.ΠP:Prop.ch_c = c2 → match c2 with [ ch_c ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##40: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct41 : Πc2.ΠP:Prop.ch_d = c2 → match c2 with [ ch_d ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##41: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct42 : Πc2.ΠP:Prop.ch_e = c2 → match c2 with [ ch_e ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##42: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct43 : Πc2.ΠP:Prop.ch_f = c2 → match c2 with [ ch_f ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##43: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct44 : Πc2.ΠP:Prop.ch_g = c2 → match c2 with [ ch_g ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##44: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct45 : Πc2.ΠP:Prop.ch_h = c2 → match c2 with [ ch_h ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##45: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct46 : Πc2.ΠP:Prop.ch_i = c2 → match c2 with [ ch_i ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##46: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct47 : Πc2.ΠP:Prop.ch_j = c2 → match c2 with [ ch_j ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##47: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct48 : Πc2.ΠP:Prop.ch_k = c2 → match c2 with [ ch_k ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##48: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct49 : Πc2.ΠP:Prop.ch_l = c2 → match c2 with [ ch_l ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##49: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct50 : Πc2.ΠP:Prop.ch_m = c2 → match c2 with [ ch_m ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##50: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct51 : Πc2.ΠP:Prop.ch_n = c2 → match c2 with [ ch_n ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##51: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct52 : Πc2.ΠP:Prop.ch_o = c2 → match c2 with [ ch_o ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##52: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct53 : Πc2.ΠP:Prop.ch_p = c2 → match c2 with [ ch_p ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##53: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct54 : Πc2.ΠP:Prop.ch_q = c2 → match c2 with [ ch_q ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##54: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct55 : Πc2.ΠP:Prop.ch_r = c2 → match c2 with [ ch_r ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##55: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct56 : Πc2.ΠP:Prop.ch_s = c2 → match c2 with [ ch_s ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##56: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct57 : Πc2.ΠP:Prop.ch_t = c2 → match c2 with [ ch_t ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##57: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct58 : Πc2.ΠP:Prop.ch_u = c2 → match c2 with [ ch_u ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##58: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct59 : Πc2.ΠP:Prop.ch_v = c2 → match c2 with [ ch_v ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##59: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct60 : Πc2.ΠP:Prop.ch_w = c2 → match c2 with [ ch_w ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##60: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct61 : Πc2.ΠP:Prop.ch_x = c2 → match c2 with [ ch_x ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##61: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct62 : Πc2.ΠP:Prop.ch_y = c2 → match c2 with [ ch_y ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##62: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct63 : Πc2.ΠP:Prop.ch_z = c2 → match c2 with [ ch_z ⇒ P → P | _ ⇒ P ]. + #c2; #P; ncases c2; nnormalize; + ##[ ##63: #H; napply (λx:P.x) + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition ascii_destruct_aux ≝ +Πc1,c2.ΠP:Prop.c1 = c2 → + match c1 with + [ ch_0 ⇒ match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ] | ch_1 ⇒ match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ] + | ch_2 ⇒ match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ] | ch_3 ⇒ match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ] + | ch_4 ⇒ match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ] | ch_5 ⇒ match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ] + | ch_6 ⇒ match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ] | ch_7 ⇒ match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ] + | ch_8 ⇒ match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ] | ch_9 ⇒ match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ] + | ch__ ⇒ match c2 with [ ch__ ⇒ P → P | _ ⇒ P ] | ch_A ⇒ match c2 with [ ch_A ⇒ P → P | _ ⇒ P ] + | ch_B ⇒ match c2 with [ ch_B ⇒ P → P | _ ⇒ P ] | ch_C ⇒ match c2 with [ ch_C ⇒ P → P | _ ⇒ P ] + | ch_D ⇒ match c2 with [ ch_D ⇒ P → P | _ ⇒ P ] | ch_E ⇒ match c2 with [ ch_E ⇒ P → P | _ ⇒ P ] + | ch_F ⇒ match c2 with [ ch_F ⇒ P → P | _ ⇒ P ] | ch_G ⇒ match c2 with [ ch_G ⇒ P → P | _ ⇒ P ] + | ch_H ⇒ match c2 with [ ch_H ⇒ P → P | _ ⇒ P ] | ch_I ⇒ match c2 with [ ch_I ⇒ P → P | _ ⇒ P ] + | ch_J ⇒ match c2 with [ ch_J ⇒ P → P | _ ⇒ P ] | ch_K ⇒ match c2 with [ ch_K ⇒ P → P | _ ⇒ P ] + | ch_L ⇒ match c2 with [ ch_L ⇒ P → P | _ ⇒ P ] | ch_M ⇒ match c2 with [ ch_M ⇒ P → P | _ ⇒ P ] + | ch_N ⇒ match c2 with [ ch_N ⇒ P → P | _ ⇒ P ] | ch_O ⇒ match c2 with [ ch_O ⇒ P → P | _ ⇒ P ] + | ch_P ⇒ match c2 with [ ch_P ⇒ P → P | _ ⇒ P ] | ch_Q ⇒ match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ] + | ch_R ⇒ match c2 with [ ch_R ⇒ P → P | _ ⇒ P ] | ch_S ⇒ match c2 with [ ch_S ⇒ P → P | _ ⇒ P ] + | ch_T ⇒ match c2 with [ ch_T ⇒ P → P | _ ⇒ P ] | ch_U ⇒ match c2 with [ ch_U ⇒ P → P | _ ⇒ P ] + | ch_V ⇒ match c2 with [ ch_V ⇒ P → P | _ ⇒ P ] | ch_W ⇒ match c2 with [ ch_W ⇒ P → P | _ ⇒ P ] + | ch_X ⇒ match c2 with [ ch_X ⇒ P → P | _ ⇒ P ] | ch_Y ⇒ match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ] + | ch_Z ⇒ match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ] | ch_a ⇒ match c2 with [ ch_a ⇒ P → P | _ ⇒ P ] + | ch_b ⇒ match c2 with [ ch_b ⇒ P → P | _ ⇒ P ] | ch_c ⇒ match c2 with [ ch_c ⇒ P → P | _ ⇒ P ] + | ch_d ⇒ match c2 with [ ch_d ⇒ P → P | _ ⇒ P ] | ch_e ⇒ match c2 with [ ch_e ⇒ P → P | _ ⇒ P ] + | ch_f ⇒ match c2 with [ ch_f ⇒ P → P | _ ⇒ P ] | ch_g ⇒ match c2 with [ ch_g ⇒ P → P | _ ⇒ P ] + | ch_h ⇒ match c2 with [ ch_h ⇒ P → P | _ ⇒ P ] | ch_i ⇒ match c2 with [ ch_i ⇒ P → P | _ ⇒ P ] + | ch_j ⇒ match c2 with [ ch_j ⇒ P → P | _ ⇒ P ] | ch_k ⇒ match c2 with [ ch_k ⇒ P → P | _ ⇒ P ] + | ch_l ⇒ match c2 with [ ch_l ⇒ P → P | _ ⇒ P ] | ch_m ⇒ match c2 with [ ch_m ⇒ P → P | _ ⇒ P ] + | ch_n ⇒ match c2 with [ ch_n ⇒ P → P | _ ⇒ P ] | ch_o ⇒ match c2 with [ ch_o ⇒ P → P | _ ⇒ P ] + | ch_p ⇒ match c2 with [ ch_p ⇒ P → P | _ ⇒ P ] | ch_q ⇒ match c2 with [ ch_q ⇒ P → P | _ ⇒ P ] + | ch_r ⇒ match c2 with [ ch_r ⇒ P → P | _ ⇒ P ] | ch_s ⇒ match c2 with [ ch_s ⇒ P → P | _ ⇒ P ] + | ch_t ⇒ match c2 with [ ch_t ⇒ P → P | _ ⇒ P ] | ch_u ⇒ match c2 with [ ch_u ⇒ P → P | _ ⇒ P ] + | ch_v ⇒ match c2 with [ ch_v ⇒ P → P | _ ⇒ P ] | ch_w ⇒ match c2 with [ ch_w ⇒ P → P | _ ⇒ P ] + | ch_x ⇒ match c2 with [ ch_x ⇒ P → P | _ ⇒ P ] | ch_y ⇒ match c2 with [ ch_y ⇒ P → P | _ ⇒ P ] + | ch_z ⇒ match c2 with [ ch_z ⇒ P → P | _ ⇒ P ]]. + +nlemma ascii_destruct : ascii_destruct_aux. + #c1; ncases c1; + ##[ ##1: napply ascii_destruct1 ##| ##2: napply ascii_destruct2 + ##| ##3: napply ascii_destruct3 ##| ##4: napply ascii_destruct4 + ##| ##5: napply ascii_destruct5 ##| ##6: napply ascii_destruct6 + ##| ##7: napply ascii_destruct7 ##| ##8: napply ascii_destruct8 + ##| ##9: napply ascii_destruct9 ##| ##10: napply ascii_destruct10 + ##| ##11: napply ascii_destruct11 ##| ##12: napply ascii_destruct12 + ##| ##13: napply ascii_destruct13 ##| ##14: napply ascii_destruct14 + ##| ##15: napply ascii_destruct15 ##| ##16: napply ascii_destruct16 + ##| ##17: napply ascii_destruct17 ##| ##18: napply ascii_destruct18 + ##| ##19: napply ascii_destruct19 ##| ##20: napply ascii_destruct20 + ##| ##21: napply ascii_destruct21 ##| ##22: napply ascii_destruct22 + ##| ##23: napply ascii_destruct23 ##| ##24: napply ascii_destruct24 + ##| ##25: napply ascii_destruct25 ##| ##26: napply ascii_destruct26 + ##| ##27: napply ascii_destruct27 ##| ##28: napply ascii_destruct28 + ##| ##29: napply ascii_destruct29 ##| ##30: napply ascii_destruct30 + ##| ##31: napply ascii_destruct31 ##| ##32: napply ascii_destruct32 + ##| ##33: napply ascii_destruct33 ##| ##34: napply ascii_destruct34 + ##| ##35: napply ascii_destruct35 ##| ##36: napply ascii_destruct36 + ##| ##37: napply ascii_destruct37 ##| ##38: napply ascii_destruct38 + ##| ##39: napply ascii_destruct39 ##| ##40: napply ascii_destruct40 + ##| ##41: napply ascii_destruct41 ##| ##42: napply ascii_destruct42 + ##| ##43: napply ascii_destruct43 ##| ##44: napply ascii_destruct44 + ##| ##45: napply ascii_destruct45 ##| ##46: napply ascii_destruct46 + ##| ##47: napply ascii_destruct47 ##| ##48: napply ascii_destruct48 + ##| ##49: napply ascii_destruct49 ##| ##50: napply ascii_destruct50 + ##| ##51: napply ascii_destruct51 ##| ##52: napply ascii_destruct52 + ##| ##53: napply ascii_destruct53 ##| ##54: napply ascii_destruct54 + ##| ##55: napply ascii_destruct55 ##| ##56: napply ascii_destruct56 + ##| ##57: napply ascii_destruct57 ##| ##58: napply ascii_destruct58 + ##| ##59: napply ascii_destruct59 ##| ##60: napply ascii_destruct60 + ##| ##61: napply ascii_destruct61 ##| ##62: napply ascii_destruct62 + ##| ##63: napply ascii_destruct63 ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas2.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas2.ma new file mode 100755 index 000000000..b3a559e10 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas2.ma @@ -0,0 +1,328 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/ascii_lemmas1.ma". +include "num/bool_lemmas.ma". + +(* ************************** *) +(* DEFINIZIONE ASCII MINIMALE *) +(* ************************** *) + +nlemma symmetric_eqascii1 : ∀a2.eq_ascii ch_0 a2 = eq_ascii a2 ch_0. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii2 : ∀a2.eq_ascii ch_1 a2 = eq_ascii a2 ch_1. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii3 : ∀a2.eq_ascii ch_2 a2 = eq_ascii a2 ch_2. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii4 : ∀a2.eq_ascii ch_3 a2 = eq_ascii a2 ch_3. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii5 : ∀a2.eq_ascii ch_4 a2 = eq_ascii a2 ch_4. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii6 : ∀a2.eq_ascii ch_5 a2 = eq_ascii a2 ch_5. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii7 : ∀a2.eq_ascii ch_6 a2 = eq_ascii a2 ch_6. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii8 : ∀a2.eq_ascii ch_7 a2 = eq_ascii a2 ch_7. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii9 : ∀a2.eq_ascii ch_8 a2 = eq_ascii a2 ch_8. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii10 : ∀a2.eq_ascii ch_9 a2 = eq_ascii a2 ch_9. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii11 : ∀a2.eq_ascii ch__ a2 = eq_ascii a2 ch__. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii12 : ∀a2.eq_ascii ch_A a2 = eq_ascii a2 ch_A. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii13 : ∀a2.eq_ascii ch_B a2 = eq_ascii a2 ch_B. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii14 : ∀a2.eq_ascii ch_C a2 = eq_ascii a2 ch_C. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii15 : ∀a2.eq_ascii ch_D a2 = eq_ascii a2 ch_D. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii16 : ∀a2.eq_ascii ch_E a2 = eq_ascii a2 ch_E. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii17 : ∀a2.eq_ascii ch_F a2 = eq_ascii a2 ch_F. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii18 : ∀a2.eq_ascii ch_G a2 = eq_ascii a2 ch_G. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii19 : ∀a2.eq_ascii ch_H a2 = eq_ascii a2 ch_H. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii20 : ∀a2.eq_ascii ch_I a2 = eq_ascii a2 ch_I. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii21 : ∀a2.eq_ascii ch_J a2 = eq_ascii a2 ch_J. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii22 : ∀a2.eq_ascii ch_K a2 = eq_ascii a2 ch_K. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii23 : ∀a2.eq_ascii ch_L a2 = eq_ascii a2 ch_L. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii24 : ∀a2.eq_ascii ch_M a2 = eq_ascii a2 ch_M. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii25 : ∀a2.eq_ascii ch_N a2 = eq_ascii a2 ch_N. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii26 : ∀a2.eq_ascii ch_O a2 = eq_ascii a2 ch_O. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii27 : ∀a2.eq_ascii ch_P a2 = eq_ascii a2 ch_P. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii28 : ∀a2.eq_ascii ch_Q a2 = eq_ascii a2 ch_Q. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii29 : ∀a2.eq_ascii ch_R a2 = eq_ascii a2 ch_R. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii30 : ∀a2.eq_ascii ch_S a2 = eq_ascii a2 ch_S. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii31 : ∀a2.eq_ascii ch_T a2 = eq_ascii a2 ch_T. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii32 : ∀a2.eq_ascii ch_U a2 = eq_ascii a2 ch_U. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii33 : ∀a2.eq_ascii ch_V a2 = eq_ascii a2 ch_V. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii34 : ∀a2.eq_ascii ch_W a2 = eq_ascii a2 ch_W. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii35 : ∀a2.eq_ascii ch_X a2 = eq_ascii a2 ch_X. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii36 : ∀a2.eq_ascii ch_Y a2 = eq_ascii a2 ch_Y. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii37 : ∀a2.eq_ascii ch_Z a2 = eq_ascii a2 ch_Z. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii38 : ∀a2.eq_ascii ch_a a2 = eq_ascii a2 ch_a. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii39 : ∀a2.eq_ascii ch_b a2 = eq_ascii a2 ch_b. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii40 : ∀a2.eq_ascii ch_c a2 = eq_ascii a2 ch_c. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii41 : ∀a2.eq_ascii ch_d a2 = eq_ascii a2 ch_d. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii42 : ∀a2.eq_ascii ch_e a2 = eq_ascii a2 ch_e. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii43 : ∀a2.eq_ascii ch_f a2 = eq_ascii a2 ch_f. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii44 : ∀a2.eq_ascii ch_g a2 = eq_ascii a2 ch_g. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii45 : ∀a2.eq_ascii ch_h a2 = eq_ascii a2 ch_h. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii46 : ∀a2.eq_ascii ch_i a2 = eq_ascii a2 ch_i. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii47 : ∀a2.eq_ascii ch_j a2 = eq_ascii a2 ch_j. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii48 : ∀a2.eq_ascii ch_k a2 = eq_ascii a2 ch_k. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii49 : ∀a2.eq_ascii ch_l a2 = eq_ascii a2 ch_l. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii50 : ∀a2.eq_ascii ch_m a2 = eq_ascii a2 ch_m. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii51 : ∀a2.eq_ascii ch_n a2 = eq_ascii a2 ch_n. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii52 : ∀a2.eq_ascii ch_o a2 = eq_ascii a2 ch_o. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii53 : ∀a2.eq_ascii ch_p a2 = eq_ascii a2 ch_p. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii54 : ∀a2.eq_ascii ch_q a2 = eq_ascii a2 ch_q. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii55 : ∀a2.eq_ascii ch_r a2 = eq_ascii a2 ch_r. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii56 : ∀a2.eq_ascii ch_s a2 = eq_ascii a2 ch_s. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii57 : ∀a2.eq_ascii ch_t a2 = eq_ascii a2 ch_t. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii58 : ∀a2.eq_ascii ch_u a2 = eq_ascii a2 ch_u. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii59 : ∀a2.eq_ascii ch_v a2 = eq_ascii a2 ch_v. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii60 : ∀a2.eq_ascii ch_w a2 = eq_ascii a2 ch_w. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii61 : ∀a2.eq_ascii ch_x a2 = eq_ascii a2 ch_x. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii62 : ∀a2.eq_ascii ch_y a2 = eq_ascii a2 ch_y. #a2; ncases a2; nnormalize; napply refl_eq.nqed. +nlemma symmetric_eqascii63 : ∀a2.eq_ascii ch_z a2 = eq_ascii a2 ch_z. #a2; ncases a2; nnormalize; napply refl_eq.nqed. + +nlemma symmetric_eqascii : symmetricT ascii bool eq_ascii. + #a1; ncases a1; + ##[ ##1: napply symmetric_eqascii1 ##| ##2: napply symmetric_eqascii2 + ##| ##3: napply symmetric_eqascii3 ##| ##4: napply symmetric_eqascii4 + ##| ##5: napply symmetric_eqascii5 ##| ##6: napply symmetric_eqascii6 + ##| ##7: napply symmetric_eqascii7 ##| ##8: napply symmetric_eqascii8 + ##| ##9: napply symmetric_eqascii9 ##| ##10: napply symmetric_eqascii10 + ##| ##11: napply symmetric_eqascii11 ##| ##12: napply symmetric_eqascii12 + ##| ##13: napply symmetric_eqascii13 ##| ##14: napply symmetric_eqascii14 + ##| ##15: napply symmetric_eqascii15 ##| ##16: napply symmetric_eqascii16 + ##| ##17: napply symmetric_eqascii17 ##| ##18: napply symmetric_eqascii18 + ##| ##19: napply symmetric_eqascii19 ##| ##20: napply symmetric_eqascii20 + ##| ##21: napply symmetric_eqascii21 ##| ##22: napply symmetric_eqascii22 + ##| ##23: napply symmetric_eqascii23 ##| ##24: napply symmetric_eqascii24 + ##| ##25: napply symmetric_eqascii25 ##| ##26: napply symmetric_eqascii26 + ##| ##27: napply symmetric_eqascii27 ##| ##28: napply symmetric_eqascii28 + ##| ##29: napply symmetric_eqascii29 ##| ##30: napply symmetric_eqascii30 + ##| ##31: napply symmetric_eqascii31 ##| ##32: napply symmetric_eqascii32 + ##| ##33: napply symmetric_eqascii33 ##| ##34: napply symmetric_eqascii34 + ##| ##35: napply symmetric_eqascii35 ##| ##36: napply symmetric_eqascii36 + ##| ##37: napply symmetric_eqascii37 ##| ##38: napply symmetric_eqascii38 + ##| ##39: napply symmetric_eqascii39 ##| ##40: napply symmetric_eqascii40 + ##| ##41: napply symmetric_eqascii41 ##| ##42: napply symmetric_eqascii42 + ##| ##43: napply symmetric_eqascii43 ##| ##44: napply symmetric_eqascii44 + ##| ##45: napply symmetric_eqascii45 ##| ##46: napply symmetric_eqascii46 + ##| ##47: napply symmetric_eqascii47 ##| ##48: napply symmetric_eqascii48 + ##| ##49: napply symmetric_eqascii49 ##| ##50: napply symmetric_eqascii50 + ##| ##51: napply symmetric_eqascii51 ##| ##52: napply symmetric_eqascii52 + ##| ##53: napply symmetric_eqascii53 ##| ##54: napply symmetric_eqascii54 + ##| ##55: napply symmetric_eqascii55 ##| ##56: napply symmetric_eqascii56 + ##| ##57: napply symmetric_eqascii57 ##| ##58: napply symmetric_eqascii58 + ##| ##59: napply symmetric_eqascii59 ##| ##60: napply symmetric_eqascii60 + ##| ##61: napply symmetric_eqascii61 ##| ##62: napply symmetric_eqascii62 + ##| ##63: napply symmetric_eqascii63 ##] +nqed. + +nlemma eqascii_to_eq1 : ∀a2.eq_ascii ch_0 a2 = true → ch_0 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq2 : ∀a2.eq_ascii ch_1 a2 = true → ch_1 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq3 : ∀a2.eq_ascii ch_2 a2 = true → ch_2 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq4 : ∀a2.eq_ascii ch_3 a2 = true → ch_3 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq5 : ∀a2.eq_ascii ch_4 a2 = true → ch_4 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq6 : ∀a2.eq_ascii ch_5 a2 = true → ch_5 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq7 : ∀a2.eq_ascii ch_6 a2 = true → ch_6 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq8 : ∀a2.eq_ascii ch_7 a2 = true → ch_7 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq9 : ∀a2.eq_ascii ch_8 a2 = true → ch_8 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq10 : ∀a2.eq_ascii ch_9 a2 = true → ch_9 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq11 : ∀a2.eq_ascii ch__ a2 = true → ch__ = a2. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq12 : ∀a2.eq_ascii ch_A a2 = true → ch_A = a2. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq13 : ∀a2.eq_ascii ch_B a2 = true → ch_B = a2. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq14 : ∀a2.eq_ascii ch_C a2 = true → ch_C = a2. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq15 : ∀a2.eq_ascii ch_D a2 = true → ch_D = a2. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq16 : ∀a2.eq_ascii ch_E a2 = true → ch_E = a2. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq17 : ∀a2.eq_ascii ch_F a2 = true → ch_F = a2. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq18 : ∀a2.eq_ascii ch_G a2 = true → ch_G = a2. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq19 : ∀a2.eq_ascii ch_H a2 = true → ch_H = a2. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq20 : ∀a2.eq_ascii ch_I a2 = true → ch_I = a2. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq21 : ∀a2.eq_ascii ch_J a2 = true → ch_J = a2. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq22 : ∀a2.eq_ascii ch_K a2 = true → ch_K = a2. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq23 : ∀a2.eq_ascii ch_L a2 = true → ch_L = a2. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq24 : ∀a2.eq_ascii ch_M a2 = true → ch_M = a2. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq25 : ∀a2.eq_ascii ch_N a2 = true → ch_N = a2. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq26 : ∀a2.eq_ascii ch_O a2 = true → ch_O = a2. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq27 : ∀a2.eq_ascii ch_P a2 = true → ch_P = a2. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq28 : ∀a2.eq_ascii ch_Q a2 = true → ch_Q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq29 : ∀a2.eq_ascii ch_R a2 = true → ch_R = a2. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq30 : ∀a2.eq_ascii ch_S a2 = true → ch_S = a2. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq31 : ∀a2.eq_ascii ch_T a2 = true → ch_T = a2. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq32 : ∀a2.eq_ascii ch_U a2 = true → ch_U = a2. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq33 : ∀a2.eq_ascii ch_V a2 = true → ch_V = a2. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq34 : ∀a2.eq_ascii ch_W a2 = true → ch_W = a2. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq35 : ∀a2.eq_ascii ch_X a2 = true → ch_X = a2. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq36 : ∀a2.eq_ascii ch_Y a2 = true → ch_Y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq37 : ∀a2.eq_ascii ch_Z a2 = true → ch_Z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq38 : ∀a2.eq_ascii ch_a a2 = true → ch_a = a2. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq39 : ∀a2.eq_ascii ch_b a2 = true → ch_b = a2. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq40 : ∀a2.eq_ascii ch_c a2 = true → ch_c = a2. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq41 : ∀a2.eq_ascii ch_d a2 = true → ch_d = a2. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq42 : ∀a2.eq_ascii ch_e a2 = true → ch_e = a2. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq43 : ∀a2.eq_ascii ch_f a2 = true → ch_f = a2. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq44 : ∀a2.eq_ascii ch_g a2 = true → ch_g = a2. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq45 : ∀a2.eq_ascii ch_h a2 = true → ch_h = a2. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq46 : ∀a2.eq_ascii ch_i a2 = true → ch_i = a2. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq47 : ∀a2.eq_ascii ch_j a2 = true → ch_j = a2. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq48 : ∀a2.eq_ascii ch_k a2 = true → ch_k = a2. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq49 : ∀a2.eq_ascii ch_l a2 = true → ch_l = a2. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq50 : ∀a2.eq_ascii ch_m a2 = true → ch_m = a2. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq51 : ∀a2.eq_ascii ch_n a2 = true → ch_n = a2. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq52 : ∀a2.eq_ascii ch_o a2 = true → ch_o = a2. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq53 : ∀a2.eq_ascii ch_p a2 = true → ch_p = a2. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq54 : ∀a2.eq_ascii ch_q a2 = true → ch_q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq55 : ∀a2.eq_ascii ch_r a2 = true → ch_r = a2. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq56 : ∀a2.eq_ascii ch_s a2 = true → ch_s = a2. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq57 : ∀a2.eq_ascii ch_t a2 = true → ch_t = a2. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq58 : ∀a2.eq_ascii ch_u a2 = true → ch_u = a2. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq59 : ∀a2.eq_ascii ch_v a2 = true → ch_v = a2. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq60 : ∀a2.eq_ascii ch_w a2 = true → ch_w = a2. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq61 : ∀a2.eq_ascii ch_x a2 = true → ch_x = a2. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq62 : ∀a2.eq_ascii ch_y a2 = true → ch_y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. +nlemma eqascii_to_eq63 : ∀a2.eq_ascii ch_z a2 = true → ch_z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed. + +nlemma eqascii_to_eq : ∀c1,c2.eq_ascii c1 c2 = true → c1 = c2. + #c1; ncases c1; + ##[ ##1: napply eqascii_to_eq1 ##| ##2: napply eqascii_to_eq2 + ##| ##3: napply eqascii_to_eq3 ##| ##4: napply eqascii_to_eq4 + ##| ##5: napply eqascii_to_eq5 ##| ##6: napply eqascii_to_eq6 + ##| ##7: napply eqascii_to_eq7 ##| ##8: napply eqascii_to_eq8 + ##| ##9: napply eqascii_to_eq9 ##| ##10: napply eqascii_to_eq10 + ##| ##11: napply eqascii_to_eq11 ##| ##12: napply eqascii_to_eq12 + ##| ##13: napply eqascii_to_eq13 ##| ##14: napply eqascii_to_eq14 + ##| ##15: napply eqascii_to_eq15 ##| ##16: napply eqascii_to_eq16 + ##| ##17: napply eqascii_to_eq17 ##| ##18: napply eqascii_to_eq18 + ##| ##19: napply eqascii_to_eq19 ##| ##20: napply eqascii_to_eq20 + ##| ##21: napply eqascii_to_eq21 ##| ##22: napply eqascii_to_eq22 + ##| ##23: napply eqascii_to_eq23 ##| ##24: napply eqascii_to_eq24 + ##| ##25: napply eqascii_to_eq25 ##| ##26: napply eqascii_to_eq26 + ##| ##27: napply eqascii_to_eq27 ##| ##28: napply eqascii_to_eq28 + ##| ##29: napply eqascii_to_eq29 ##| ##30: napply eqascii_to_eq30 + ##| ##31: napply eqascii_to_eq31 ##| ##32: napply eqascii_to_eq32 + ##| ##33: napply eqascii_to_eq33 ##| ##34: napply eqascii_to_eq34 + ##| ##35: napply eqascii_to_eq35 ##| ##36: napply eqascii_to_eq36 + ##| ##37: napply eqascii_to_eq37 ##| ##38: napply eqascii_to_eq38 + ##| ##39: napply eqascii_to_eq39 ##| ##40: napply eqascii_to_eq40 + ##| ##41: napply eqascii_to_eq41 ##| ##42: napply eqascii_to_eq42 + ##| ##43: napply eqascii_to_eq43 ##| ##44: napply eqascii_to_eq44 + ##| ##45: napply eqascii_to_eq45 ##| ##46: napply eqascii_to_eq46 + ##| ##47: napply eqascii_to_eq47 ##| ##48: napply eqascii_to_eq48 + ##| ##49: napply eqascii_to_eq49 ##| ##50: napply eqascii_to_eq50 + ##| ##51: napply eqascii_to_eq51 ##| ##52: napply eqascii_to_eq52 + ##| ##53: napply eqascii_to_eq53 ##| ##54: napply eqascii_to_eq54 + ##| ##55: napply eqascii_to_eq55 ##| ##56: napply eqascii_to_eq56 + ##| ##57: napply eqascii_to_eq57 ##| ##58: napply eqascii_to_eq58 + ##| ##59: napply eqascii_to_eq59 ##| ##60: napply eqascii_to_eq60 + ##| ##61: napply eqascii_to_eq61 ##| ##62: napply eqascii_to_eq62 + ##| ##63: napply eqascii_to_eq63 ##] +nqed. + +nlemma eq_to_eqascii1 : ∀a2.ch_0 = a2 → eq_ascii ch_0 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii2 : ∀a2.ch_1 = a2 → eq_ascii ch_1 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii3 : ∀a2.ch_2 = a2 → eq_ascii ch_2 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii4 : ∀a2.ch_3 = a2 → eq_ascii ch_3 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii5 : ∀a2.ch_4 = a2 → eq_ascii ch_4 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii6 : ∀a2.ch_5 = a2 → eq_ascii ch_5 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii7 : ∀a2.ch_6 = a2 → eq_ascii ch_6 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii8 : ∀a2.ch_7 = a2 → eq_ascii ch_7 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii9 : ∀a2.ch_8 = a2 → eq_ascii ch_8 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii10 : ∀a2.ch_9 = a2 → eq_ascii ch_9 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii11 : ∀a2.ch__ = a2 → eq_ascii ch__ a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii12 : ∀a2.ch_A = a2 → eq_ascii ch_A a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii13 : ∀a2.ch_B = a2 → eq_ascii ch_B a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii14 : ∀a2.ch_C = a2 → eq_ascii ch_C a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii15 : ∀a2.ch_D = a2 → eq_ascii ch_D a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii16 : ∀a2.ch_E = a2 → eq_ascii ch_E a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii17 : ∀a2.ch_F = a2 → eq_ascii ch_F a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii18 : ∀a2.ch_G = a2 → eq_ascii ch_G a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii19 : ∀a2.ch_H = a2 → eq_ascii ch_H a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii20 : ∀a2.ch_I = a2 → eq_ascii ch_I a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii21 : ∀a2.ch_J = a2 → eq_ascii ch_J a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii22 : ∀a2.ch_K = a2 → eq_ascii ch_K a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii23 : ∀a2.ch_L = a2 → eq_ascii ch_L a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii24 : ∀a2.ch_M = a2 → eq_ascii ch_M a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii25 : ∀a2.ch_N = a2 → eq_ascii ch_N a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii26 : ∀a2.ch_O = a2 → eq_ascii ch_O a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii27 : ∀a2.ch_P = a2 → eq_ascii ch_P a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii28 : ∀a2.ch_Q = a2 → eq_ascii ch_Q a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii29 : ∀a2.ch_R = a2 → eq_ascii ch_R a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii30 : ∀a2.ch_S = a2 → eq_ascii ch_S a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii31 : ∀a2.ch_T = a2 → eq_ascii ch_T a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii32 : ∀a2.ch_U = a2 → eq_ascii ch_U a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii33 : ∀a2.ch_V = a2 → eq_ascii ch_V a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii34 : ∀a2.ch_W = a2 → eq_ascii ch_W a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii35 : ∀a2.ch_X = a2 → eq_ascii ch_X a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii36 : ∀a2.ch_Y = a2 → eq_ascii ch_Y a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii37 : ∀a2.ch_Z = a2 → eq_ascii ch_Z a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii38 : ∀a2.ch_a = a2 → eq_ascii ch_a a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii39 : ∀a2.ch_b = a2 → eq_ascii ch_b a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii40 : ∀a2.ch_c = a2 → eq_ascii ch_c a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii41 : ∀a2.ch_d = a2 → eq_ascii ch_d a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii42 : ∀a2.ch_e = a2 → eq_ascii ch_e a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii43 : ∀a2.ch_f = a2 → eq_ascii ch_f a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii44 : ∀a2.ch_g = a2 → eq_ascii ch_g a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii45 : ∀a2.ch_h = a2 → eq_ascii ch_h a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii46 : ∀a2.ch_i = a2 → eq_ascii ch_i a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii47 : ∀a2.ch_j = a2 → eq_ascii ch_j a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii48 : ∀a2.ch_k = a2 → eq_ascii ch_k a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii49 : ∀a2.ch_l = a2 → eq_ascii ch_l a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii50 : ∀a2.ch_m = a2 → eq_ascii ch_m a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii51 : ∀a2.ch_n = a2 → eq_ascii ch_n a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii52 : ∀a2.ch_o = a2 → eq_ascii ch_o a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii53 : ∀a2.ch_p = a2 → eq_ascii ch_p a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii54 : ∀a2.ch_q = a2 → eq_ascii ch_q a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii55 : ∀a2.ch_r = a2 → eq_ascii ch_r a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii56 : ∀a2.ch_s = a2 → eq_ascii ch_s a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii57 : ∀a2.ch_t = a2 → eq_ascii ch_t a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii58 : ∀a2.ch_u = a2 → eq_ascii ch_u a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii59 : ∀a2.ch_v = a2 → eq_ascii ch_v a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii60 : ∀a2.ch_w = a2 → eq_ascii ch_w a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii61 : ∀a2.ch_x = a2 → eq_ascii ch_x a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii62 : ∀a2.ch_y = a2 → eq_ascii ch_y a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. +nlemma eq_to_eqascii63 : ∀a2.ch_z = a2 → eq_ascii ch_z a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed. + +nlemma eq_to_eqascii : ∀c1,c2.c1 = c2 → eq_ascii c1 c2 = true. + #c1; ncases c1; + ##[ ##1: napply eq_to_eqascii1 ##| ##2: napply eq_to_eqascii2 + ##| ##3: napply eq_to_eqascii3 ##| ##4: napply eq_to_eqascii4 + ##| ##5: napply eq_to_eqascii5 ##| ##6: napply eq_to_eqascii6 + ##| ##7: napply eq_to_eqascii7 ##| ##8: napply eq_to_eqascii8 + ##| ##9: napply eq_to_eqascii9 ##| ##10: napply eq_to_eqascii10 + ##| ##11: napply eq_to_eqascii11 ##| ##12: napply eq_to_eqascii12 + ##| ##13: napply eq_to_eqascii13 ##| ##14: napply eq_to_eqascii14 + ##| ##15: napply eq_to_eqascii15 ##| ##16: napply eq_to_eqascii16 + ##| ##17: napply eq_to_eqascii17 ##| ##18: napply eq_to_eqascii18 + ##| ##19: napply eq_to_eqascii19 ##| ##20: napply eq_to_eqascii20 + ##| ##21: napply eq_to_eqascii21 ##| ##22: napply eq_to_eqascii22 + ##| ##23: napply eq_to_eqascii23 ##| ##24: napply eq_to_eqascii24 + ##| ##25: napply eq_to_eqascii25 ##| ##26: napply eq_to_eqascii26 + ##| ##27: napply eq_to_eqascii27 ##| ##28: napply eq_to_eqascii28 + ##| ##29: napply eq_to_eqascii29 ##| ##30: napply eq_to_eqascii30 + ##| ##31: napply eq_to_eqascii31 ##| ##32: napply eq_to_eqascii32 + ##| ##33: napply eq_to_eqascii33 ##| ##34: napply eq_to_eqascii34 + ##| ##35: napply eq_to_eqascii35 ##| ##36: napply eq_to_eqascii36 + ##| ##37: napply eq_to_eqascii37 ##| ##38: napply eq_to_eqascii38 + ##| ##39: napply eq_to_eqascii39 ##| ##40: napply eq_to_eqascii40 + ##| ##41: napply eq_to_eqascii41 ##| ##42: napply eq_to_eqascii42 + ##| ##43: napply eq_to_eqascii43 ##| ##44: napply eq_to_eqascii44 + ##| ##45: napply eq_to_eqascii45 ##| ##46: napply eq_to_eqascii46 + ##| ##47: napply eq_to_eqascii47 ##| ##48: napply eq_to_eqascii48 + ##| ##49: napply eq_to_eqascii49 ##| ##50: napply eq_to_eqascii50 + ##| ##51: napply eq_to_eqascii51 ##| ##52: napply eq_to_eqascii52 + ##| ##53: napply eq_to_eqascii53 ##| ##54: napply eq_to_eqascii54 + ##| ##55: napply eq_to_eqascii55 ##| ##56: napply eq_to_eqascii56 + ##| ##57: napply eq_to_eqascii57 ##| ##58: napply eq_to_eqascii58 + ##| ##59: napply eq_to_eqascii59 ##| ##60: napply eq_to_eqascii60 + ##| ##61: napply eq_to_eqascii61 ##| ##62: napply eq_to_eqascii62 + ##| ##63: napply eq_to_eqascii63 ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/list.ma b/helm/software/matita/contribs/ng_assembly/common/list.ma new file mode 100644 index 000000000..a5322a996 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/list.ma @@ -0,0 +1,84 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/theory.ma". + +(* *************** *) +(* LISTE GENERICHE *) +(* *************** *) + +ninductive list (A:Type) : Type ≝ + nil: list A +| cons: A → list A → list A. + +nlet rec append A (l1: list A) l2 on l1 ≝ + match l1 with + [ nil ⇒ l2 + | (cons hd tl) ⇒ cons A hd (append A tl l2) ]. + +notation "hvbox(hd break :: tl)" + right associative with precedence 47 + for @{'cons $hd $tl}. + +notation "[ list0 x sep ; ]" + non associative with precedence 90 + for ${fold right @'nil rec acc @{'cons $x $acc}}. + +notation "hvbox(l1 break @ l2)" + right associative with precedence 47 + for @{'append $l1 $l2 }. + +interpretation "nil" 'nil = (nil ?). +interpretation "cons" 'cons hd tl = (cons ? hd tl). +interpretation "append" 'append l1 l2 = (append ? l1 l2). + +(* ************** *) +(* NON-EMPTY LIST *) +(* ************** *) + +(* lista non vuota *) +ninductive ne_list (A:Type) : Type ≝ + | ne_nil: A → ne_list A + | ne_cons: A → ne_list A → ne_list A. + +(* append *) +nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝ + match l1 with + [ ne_nil hd ⇒ ne_cons A hd l2 + | ne_cons hd tl ⇒ ne_cons A hd (ne_append A tl l2) ]. + +notation "hvbox(hd break §§ tl)" + right associative with precedence 46 + for @{'ne_cons $hd $tl}. + +(* \laquo \raquo *) +notation "« list0 x sep ; break £ y break »" + non associative with precedence 90 + for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}. + +notation "hvbox(l1 break & l2)" + right associative with precedence 47 + for @{'ne_append $l1 $l2 }. + +interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd). +interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl). +interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2). diff --git a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma new file mode 100644 index 000000000..51654011e --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma @@ -0,0 +1,162 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/list.ma". + +(* *************** *) +(* LISTE GENERICHE *) +(* *************** *) + +nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2. + #T; #x1; #x2; #y1; #y2; #H; + nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2. + #T; #x1; #x2; #y1; #y2; #H; + nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False. + #T; #x; #y; #H; + nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]); + nrewrite > H; + nnormalize; + napply I. +nqed. + +nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False. + #T; #x; #y; #H; + nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]); + nrewrite < H; + nnormalize; + napply I. +nqed. + +nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l. + #T; #l; + nelim l; + nnormalize; + ##[ ##1: napply refl_eq + ##| ##2: #x; #y; #H; + nrewrite > H; + napply refl_eq + ##] +nqed. + +nlemma associative_list : ∀T.associative (list T) (append T). + #T; #x; #y; #z; + nelim x; + nnormalize; + ##[ ##1: napply refl_eq + ##| ##2: #a; #b; #H; + nrewrite > H; + napply refl_eq + ##] +nqed. + +nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2. + #T; #l1; #l2; #a; + nnormalize; + napply refl_eq. +nqed. + +nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1. + #T; #a; #l; #l1; + nrewrite > (associative_list T l [a] l1); + nnormalize; + napply refl_eq. +nqed. + +(* ************** *) +(* NON-EMPTY LIST *) +(* ************** *) + +nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2. + #T; #x1; #x2; #H; + nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → x1 = x2. + #T; #x1; #x2; #y1; #y2; #H; + nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → y1 = y2. + #T; #x1; #x2; #y1; #y2; #H; + nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False. + #T; #x1; #x2; #y1; #H; + nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]); + nrewrite > H; + nnormalize; + napply I. +nqed. + +nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False. + #T; #x1; #x2; #y2; #H; + nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]); + nrewrite < H; + nnormalize; + napply I. +nqed. + +nlemma associative_nelist : ∀T.associative (ne_list T) (ne_append T). + #T; #x; #y; #z; + nelim x; + nnormalize; + ##[ ##1: #hh; napply refl_eq + ##| ##2: #hh; #tt; #H; + nrewrite > H; + napply refl_eq + ##] +nqed. + +nlemma necons_append_commute : ∀T:Type.∀l1,l2:ne_list T.∀a:T.(a §§ (l1 & l2)) = ((a §§ l1) & l2). + #T; #l1; #l2; #a; + nnormalize; + napply refl_eq. +nqed. + +nlemma append_necons_commute : ∀T:Type.∀a:T.∀l,l1:ne_list T.(l & (a §§ l1)) = (l & «£a») & l1. + #T; #a; #l; #l1; + nrewrite > (associative_nelist T l «£a» l1); + nnormalize; + napply refl_eq. +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/nat.ma b/helm/software/matita/contribs/ng_assembly/common/nat.ma new file mode 100755 index 000000000..874ab7d8c --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/nat.ma @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ******** *) +(* NATURALI *) +(* ******** *) + +inductive nat : Type ≝ + O : nat +| S : nat → nat. + +interpretation "Natural numbers" 'N = nat. + +default "natural numbers" cic:/matita/common/nat/nat.ind. + +alias num (instance 0) = "natural number". + +nlet rec eq_nat (n1,n2:nat) on n1 ≝ + match n1 with + [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ] + | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ] + ]. + +nlet rec le_nat n m ≝ + match n with + [ O ⇒ true + | (S p) ⇒ match m with + [ O ⇒ false | (S q) ⇒ le_nat p q ] + ]. + +nlet rec plus (n1,n2:nat) on n1 ≝ + match n1 with + [ O ⇒ n2 + | (S n1') ⇒ S (plus n1' n2) ]. + +interpretation "natural plus" 'plus x y = (plus x y). + +nlet rec times (n1,n2:nat) on n1 ≝ + match n1 with + [ O ⇒ O + | (S n1') ⇒ n2 + (times n1' n2) ]. + +interpretation "natural times" 'times x y = (times x y). + +nlet rec minus n m ≝ + match n with + [ O ⇒ O + | (S p) ⇒ + match m with + [O ⇒ (S p) + | (S q) ⇒ minus p q ]]. + +interpretation "natural minus" 'minus x y = (minus x y). + +nlet rec div_aux p m n : nat ≝ +match (le_nat m n) with +[ true ⇒ O +| false ⇒ + match p with + [ O ⇒ O + | (S q) ⇒ S (div_aux q (m-(S n)) n)]]. + +ndefinition div : nat → nat → nat ≝ +λn,m.match m with + [ O ⇒ S n + | (S p) ⇒ div_aux n n p]. + +interpretation "natural divide" 'divide x y = (div x y). diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma new file mode 100644 index 000000000..f4525c463 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma @@ -0,0 +1,161 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/nat.ma". +include "num/bool_lemmas.ma". + +(* ******** *) +(* NATURALI *) +(* ******** *) + +nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2. + #n1; #n2; #H; + nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma nat_destruct_0_S : ∀n:nat.O = S n → False. + #n; #H; + nchange with (match S n with [ O ⇒ True | S a ⇒ False ]); + nrewrite < H; + nnormalize; + napply I. +nqed. + +nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False. + #n; #H; + nchange with (match S n with [ O ⇒ True | S a ⇒ False ]); + nrewrite > H; + nnormalize; + napply I. +nqed. + +nlemma symmetric_eqnat : symmetricT nat bool eq_nat. + nnormalize; + #n1; + nelim n1; + ##[ ##1: #n2; + nelim n2; + nnormalize; + ##[ ##1: napply refl_eq + ##| ##2: #n3; #H; napply refl_eq + ##] + ##| ##2: #n2; #H; #n3; + nnormalize; + ncases n3; + nnormalize; + ##[ ##1: napply refl_eq + ##| ##2: #n4; napply (H n4) + ##] + ##] +nqed. + +nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true. + #n1; + nelim n1; + ##[ ##1: #n2; + nelim n2; + nnormalize; + ##[ ##1: #H; napply refl_eq + ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1) + ##] + ##| ##2: #n2; #H; #n3; #H1; + ncases n3 in H1:(%) ⊢ %; + nnormalize; + ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1) + ##| ##2: #n4; #H1; + napply (H n4 (nat_destruct_S_S … H1)) + ##] + ##] +nqed. + +nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2). + #n1; + nelim n1; + ##[ ##1: #n2; + nelim n2; + nnormalize; + ##[ ##1: #H; napply refl_eq + ##| ##2: #n3; #H; #H1; napply (bool_destruct … (O = S n3) H1) + ##] + ##| ##2: #n2; #H; #n3; #H1; + ncases n3 in H1:(%) ⊢ %; + nnormalize; + ##[ ##1: #H1; napply (bool_destruct … (S n2 = O) H1) + ##| ##2: #n4; #H1; + nrewrite > (H n4 H1); + napply refl_eq + ##] + ##] +nqed. + +nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2). + #n1; + nelim n1; + ##[ ##1: nnormalize; #n2; napply refl_eq + ##| ##2: #n; #H; #n2; nrewrite > (H n2); + ncases n in H:(%) ⊢ %; + ##[ ##1: nnormalize; #H; napply refl_eq + ##| ##2: #n3; nnormalize; #H; napply refl_eq + ##] + ##] +nqed. + +nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2). + #n1; + nelim n1; + ##[ ##1: nnormalize; #n2; napply refl_eq + ##| ##2: #n; #H; #n2; + nrewrite > (Sn_p_n_to_S_npn n (S n2)); + nrewrite > (H n2); + napply refl_eq + ##] +nqed. + +nlemma Opn_to_n : ∀n.O + n = n. + #n; nnormalize; napply refl_eq. +nqed. + +nlemma npO_to_n : ∀n.n + O = n. + #n; + nelim n; + ##[ ##1: nnormalize; napply refl_eq + ##| ##2: #n1; #H; + nrewrite > (Sn_p_n_to_S_npn n1 O); + nrewrite > H; + napply refl_eq + ##] +nqed. + +nlemma symmetric_plusnat : symmetricT nat nat plus. + #n1; + nelim n1; + ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq + ##| ##2: #n2; #H; #n3; + nrewrite > (Sn_p_n_to_S_npn n2 n3); + nrewrite > (n_p_Sn_to_S_npn n3 n2); + nrewrite > (H n3); + napply refl_eq + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index b365c9fe8..e9d1d4c63 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,22 +1,29 @@ +num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma +common/nat.ma num/bool.ma num/word32.ma num/word16.ma -num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma -common/option.ma num/bool.ma -num/word16.ma num/byte8.ma -num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma -num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma test_errori.ma -common/theory.ma -num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma -num/quatern.ma num/bool.ma -common/prod.ma num/bool.ma -num/byte8.ma num/bitrigesim.ma num/exadecim.ma -num/bool.ma common/theory.ma -num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +common/list_lemmas.ma common/list.ma num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma -common/option_lemmas.ma common/option.ma num/bool_lemmas.ma -common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma -num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma num/bitrigesim.ma num/bool.ma +common/ascii_lemmas1.ma common/ascii.ma +num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma +common/prod.ma num/bool.ma +common/ascii_lemmas2.ma common/ascii_lemmas1.ma num/bool_lemmas.ma num/bool_lemmas.ma num/bool.ma +common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma +common/option_lemmas.ma common/option.ma num/bool_lemmas.ma +num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma +common/theory.ma +num/quatern.ma num/bool.ma num/oct.ma num/bool.ma +num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma +num/byte8.ma num/bitrigesim.ma num/exadecim.ma +num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +common/option.ma num/bool.ma +common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma +num/bool.ma common/theory.ma +num/word16.ma num/byte8.ma +common/ascii.ma num/bool.ma +common/list.ma common/theory.ma +num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma