From: Cosimo Oliboni <??>
Date: Thu, 6 Aug 2009 01:04:47 +0000 (+0000)
Subject:  freescale porting, work in progress
X-Git-Tag: make_still_working~3563
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0af747f54642b05b3232319b6ae1753af211dba5;p=helm.git

 freescale porting, work in progress
---

diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma
new file mode 100755
index 000000000..de510fe40
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma
@@ -0,0 +1,505 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/ascii_lemmas1.ma".
+include "num/bool_lemmas.ma".
+
+(* ************************** *)
+(* DEFINIZIONE ASCII MINIMALE *)
+(* ************************** *)
+
+nlemma decidable_ascii1 : ∀x:ascii.decidable (ch_0 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii2 : ∀x:ascii.decidable (ch_1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii3 : ∀x:ascii.decidable (ch_2 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii4 : ∀x:ascii.decidable (ch_3 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii5 : ∀x:ascii.decidable (ch_4 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii6 : ∀x:ascii.decidable (ch_5 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii7 : ∀x:ascii.decidable (ch_6 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii8 : ∀x:ascii.decidable (ch_7 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii9 : ∀x:ascii.decidable (ch_8 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii10 : ∀x:ascii.decidable (ch_9 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii11 : ∀x:ascii.decidable (ch__ = x).
+ #x; nnormalize; nelim x;
+ ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii12 : ∀x:ascii.decidable (ch_A = x).
+ #x; nnormalize; nelim x;
+ ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii13 : ∀x:ascii.decidable (ch_B = x).
+ #x; nnormalize; nelim x;
+ ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii14 : ∀x:ascii.decidable (ch_C = x).
+ #x; nnormalize; nelim x;
+ ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii15 : ∀x:ascii.decidable (ch_D = x).
+ #x; nnormalize; nelim x;
+ ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii16 : ∀x:ascii.decidable (ch_E = x).
+ #x; nnormalize; nelim x;
+ ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii17 : ∀x:ascii.decidable (ch_F = x).
+ #x; nnormalize; nelim x;
+ ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii18 : ∀x:ascii.decidable (ch_G = x).
+ #x; nnormalize; nelim x;
+ ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii19 : ∀x:ascii.decidable (ch_H = x).
+ #x; nnormalize; nelim x;
+ ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii20 : ∀x:ascii.decidable (ch_I = x).
+ #x; nnormalize; nelim x;
+ ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii21 : ∀x:ascii.decidable (ch_J = x).
+ #x; nnormalize; nelim x;
+ ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii22 : ∀x:ascii.decidable (ch_K = x).
+ #x; nnormalize; nelim x;
+ ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii23 : ∀x:ascii.decidable (ch_L = x).
+ #x; nnormalize; nelim x;
+ ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii24 : ∀x:ascii.decidable (ch_M = x).
+ #x; nnormalize; nelim x;
+ ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii25 : ∀x:ascii.decidable (ch_N = x).
+ #x; nnormalize; nelim x;
+ ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii26 : ∀x:ascii.decidable (ch_O = x).
+ #x; nnormalize; nelim x;
+ ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii27 : ∀x:ascii.decidable (ch_P = x).
+ #x; nnormalize; nelim x;
+ ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii28 : ∀x:ascii.decidable (ch_Q = x).
+ #x; nnormalize; nelim x;
+ ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii29 : ∀x:ascii.decidable (ch_R = x).
+ #x; nnormalize; nelim x;
+ ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii30 : ∀x:ascii.decidable (ch_S = x).
+ #x; nnormalize; nelim x;
+ ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii31 : ∀x:ascii.decidable (ch_T = x).
+ #x; nnormalize; nelim x;
+ ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii32 : ∀x:ascii.decidable (ch_U = x).
+ #x; nnormalize; nelim x;
+ ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii33 : ∀x:ascii.decidable (ch_V = x).
+ #x; nnormalize; nelim x;
+ ##[ ##33: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii34 : ∀x:ascii.decidable (ch_W = x).
+ #x; nnormalize; nelim x;
+ ##[ ##34: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii35 : ∀x:ascii.decidable (ch_X = x).
+ #x; nnormalize; nelim x;
+ ##[ ##35: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii36 : ∀x:ascii.decidable (ch_Y = x).
+ #x; nnormalize; nelim x;
+ ##[ ##36: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii37 : ∀x:ascii.decidable (ch_Z = x).
+ #x; nnormalize; nelim x;
+ ##[ ##37: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii38 : ∀x:ascii.decidable (ch_a = x).
+ #x; nnormalize; nelim x;
+ ##[ ##38: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii39 : ∀x:ascii.decidable (ch_b = x).
+ #x; nnormalize; nelim x;
+ ##[ ##39: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii40 : ∀x:ascii.decidable (ch_c = x).
+ #x; nnormalize; nelim x;
+ ##[ ##40: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii41 : ∀x:ascii.decidable (ch_d = x).
+ #x; nnormalize; nelim x;
+ ##[ ##41: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii42 : ∀x:ascii.decidable (ch_e = x).
+ #x; nnormalize; nelim x;
+ ##[ ##42: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii43 : ∀x:ascii.decidable (ch_f = x).
+ #x; nnormalize; nelim x;
+ ##[ ##43: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii44 : ∀x:ascii.decidable (ch_g = x).
+ #x; nnormalize; nelim x;
+ ##[ ##44: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii45 : ∀x:ascii.decidable (ch_h = x).
+ #x; nnormalize; nelim x;
+ ##[ ##45: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii46 : ∀x:ascii.decidable (ch_i = x).
+ #x; nnormalize; nelim x;
+ ##[ ##46: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii47 : ∀x:ascii.decidable (ch_j = x).
+ #x; nnormalize; nelim x;
+ ##[ ##47: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii48 : ∀x:ascii.decidable (ch_k = x).
+ #x; nnormalize; nelim x;
+ ##[ ##48: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii49 : ∀x:ascii.decidable (ch_l = x).
+ #x; nnormalize; nelim x;
+ ##[ ##49: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii50 : ∀x:ascii.decidable (ch_m = x).
+ #x; nnormalize; nelim x;
+ ##[ ##50: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii51 : ∀x:ascii.decidable (ch_n = x).
+ #x; nnormalize; nelim x;
+ ##[ ##51: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii52 : ∀x:ascii.decidable (ch_o = x).
+ #x; nnormalize; nelim x;
+ ##[ ##52: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii53 : ∀x:ascii.decidable (ch_p = x).
+ #x; nnormalize; nelim x;
+ ##[ ##53: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii54 : ∀x:ascii.decidable (ch_q = x).
+ #x; nnormalize; nelim x;
+ ##[ ##54: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii55 : ∀x:ascii.decidable (ch_r = x).
+ #x; nnormalize; nelim x;
+ ##[ ##55: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii56 : ∀x:ascii.decidable (ch_s = x).
+ #x; nnormalize; nelim x;
+ ##[ ##56: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii57 : ∀x:ascii.decidable (ch_t = x).
+ #x; nnormalize; nelim x;
+ ##[ ##57: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii58 : ∀x:ascii.decidable (ch_u = x).
+ #x; nnormalize; nelim x;
+ ##[ ##58: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii59 : ∀x:ascii.decidable (ch_v = x).
+ #x; nnormalize; nelim x;
+ ##[ ##59: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii60 : ∀x:ascii.decidable (ch_w = x).
+ #x; nnormalize; nelim x;
+ ##[ ##60: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii61 : ∀x:ascii.decidable (ch_x = x).
+ #x; nnormalize; nelim x;
+ ##[ ##61: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii62 : ∀x:ascii.decidable (ch_y = x).
+ #x; nnormalize; nelim x;
+ ##[ ##62: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii63 : ∀x:ascii.decidable (ch_z = x).
+ #x; nnormalize; nelim x;
+ ##[ ##63: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_ascii : ∀x,y:ascii.decidable (x = y).
+ #a1; ncases a1;
+ ##[ ##1: napply decidable_ascii1 ##| ##2: napply decidable_ascii2
+ ##| ##3: napply decidable_ascii3 ##| ##4: napply decidable_ascii4
+ ##| ##5: napply decidable_ascii5 ##| ##6: napply decidable_ascii6
+ ##| ##7: napply decidable_ascii7 ##| ##8: napply decidable_ascii8
+ ##| ##9: napply decidable_ascii9 ##| ##10: napply decidable_ascii10
+ ##| ##11: napply decidable_ascii11 ##| ##12: napply decidable_ascii12
+ ##| ##13: napply decidable_ascii13 ##| ##14: napply decidable_ascii14
+ ##| ##15: napply decidable_ascii15 ##| ##16: napply decidable_ascii16
+ ##| ##17: napply decidable_ascii17 ##| ##18: napply decidable_ascii18
+ ##| ##19: napply decidable_ascii19 ##| ##20: napply decidable_ascii20
+ ##| ##21: napply decidable_ascii21 ##| ##22: napply decidable_ascii22
+ ##| ##23: napply decidable_ascii23 ##| ##24: napply decidable_ascii24
+ ##| ##25: napply decidable_ascii25 ##| ##26: napply decidable_ascii26
+ ##| ##27: napply decidable_ascii27 ##| ##28: napply decidable_ascii28
+ ##| ##29: napply decidable_ascii29 ##| ##30: napply decidable_ascii30
+ ##| ##31: napply decidable_ascii31 ##| ##32: napply decidable_ascii32
+ ##| ##33: napply decidable_ascii33 ##| ##34: napply decidable_ascii34
+ ##| ##35: napply decidable_ascii35 ##| ##36: napply decidable_ascii36
+ ##| ##37: napply decidable_ascii37 ##| ##38: napply decidable_ascii38
+ ##| ##39: napply decidable_ascii39 ##| ##40: napply decidable_ascii40
+ ##| ##41: napply decidable_ascii41 ##| ##42: napply decidable_ascii42
+ ##| ##43: napply decidable_ascii43 ##| ##44: napply decidable_ascii44
+ ##| ##45: napply decidable_ascii45 ##| ##46: napply decidable_ascii46
+ ##| ##47: napply decidable_ascii47 ##| ##48: napply decidable_ascii48
+ ##| ##49: napply decidable_ascii49 ##| ##50: napply decidable_ascii50
+ ##| ##51: napply decidable_ascii51 ##| ##52: napply decidable_ascii52
+ ##| ##53: napply decidable_ascii53 ##| ##54: napply decidable_ascii54
+ ##| ##55: napply decidable_ascii55 ##| ##56: napply decidable_ascii56
+ ##| ##57: napply decidable_ascii57 ##| ##58: napply decidable_ascii58
+ ##| ##59: napply decidable_ascii59 ##| ##60: napply decidable_ascii60
+ ##| ##61: napply decidable_ascii61 ##| ##62: napply decidable_ascii62
+ ##| ##63: napply decidable_ascii63 ##]
+nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas4.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas4.ma
new file mode 100755
index 000000000..64ee7b2e9
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas4.ma
@@ -0,0 +1,505 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/ascii_lemmas1.ma".
+include "num/bool_lemmas.ma".
+
+(* ************************** *)
+(* DEFINIZIONE ASCII MINIMALE *)
+(* ************************** *)
+
+nlemma neqascii_to_neq1 : ∀a2.eq_ascii ch_0 a2 = false → ch_0 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##1: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq2 : ∀a2.eq_ascii ch_1 a2 = false → ch_1 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##2: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq3 : ∀a2.eq_ascii ch_2 a2 = false → ch_2 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##3: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq4 : ∀a2.eq_ascii ch_3 a2 = false → ch_3 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##4: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq5 : ∀a2.eq_ascii ch_4 a2 = false → ch_4 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##5: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq6 : ∀a2.eq_ascii ch_5 a2 = false → ch_5 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##6: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq7 : ∀a2.eq_ascii ch_6 a2 = false → ch_6 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##7: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq8 : ∀a2.eq_ascii ch_7 a2 = false → ch_7 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##8: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq9 : ∀a2.eq_ascii ch_8 a2 = false → ch_8 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##9: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq10 : ∀a2.eq_ascii ch_9 a2 = false → ch_9 ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##10: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq11 : ∀a2.eq_ascii ch__ a2 = false → ch__ ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##11: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq12 : ∀a2.eq_ascii ch_A a2 = false → ch_A ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##12: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq13 : ∀a2.eq_ascii ch_B a2 = false → ch_B ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##13: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq14 : ∀a2.eq_ascii ch_C a2 = false → ch_C ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##14: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq15 : ∀a2.eq_ascii ch_D a2 = false → ch_D ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##15: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq16 : ∀a2.eq_ascii ch_E a2 = false → ch_E ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##16: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq17 : ∀a2.eq_ascii ch_F a2 = false → ch_F ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##17: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq18 : ∀a2.eq_ascii ch_G a2 = false → ch_G ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##18: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq19 : ∀a2.eq_ascii ch_H a2 = false → ch_H ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##19: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq20 : ∀a2.eq_ascii ch_I a2 = false → ch_I ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##20: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq21 : ∀a2.eq_ascii ch_J a2 = false → ch_J ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##21: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq22 : ∀a2.eq_ascii ch_K a2 = false → ch_K ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##22: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq23 : ∀a2.eq_ascii ch_L a2 = false → ch_L ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##23: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq24 : ∀a2.eq_ascii ch_M a2 = false → ch_M ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##24: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq25 : ∀a2.eq_ascii ch_N a2 = false → ch_N ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##25: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq26 : ∀a2.eq_ascii ch_O a2 = false → ch_O ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##26: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq27 : ∀a2.eq_ascii ch_P a2 = false → ch_P ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##27: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq28 : ∀a2.eq_ascii ch_Q a2 = false → ch_Q ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##28: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq29 : ∀a2.eq_ascii ch_R a2 = false → ch_R ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##29: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq30 : ∀a2.eq_ascii ch_S a2 = false → ch_S ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##30: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq31 : ∀a2.eq_ascii ch_T a2 = false → ch_T ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##31: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq32 : ∀a2.eq_ascii ch_U a2 = false → ch_U ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##32: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq33 : ∀a2.eq_ascii ch_V a2 = false → ch_V ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##33: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq34 : ∀a2.eq_ascii ch_W a2 = false → ch_W ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##34: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq35 : ∀a2.eq_ascii ch_X a2 = false → ch_X ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##35: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq36 : ∀a2.eq_ascii ch_Y a2 = false → ch_Y ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##36: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq37 : ∀a2.eq_ascii ch_Z a2 = false → ch_Z ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##37: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq38 : ∀a2.eq_ascii ch_a a2 = false → ch_a ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##38: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq39 : ∀a2.eq_ascii ch_b a2 = false → ch_b ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##39: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq40 : ∀a2.eq_ascii ch_c a2 = false → ch_c ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##40: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq41 : ∀a2.eq_ascii ch_d a2 = false → ch_d ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##41: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq42 : ∀a2.eq_ascii ch_e a2 = false → ch_e ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##42: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq43 : ∀a2.eq_ascii ch_f a2 = false → ch_f ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##43: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq44 : ∀a2.eq_ascii ch_g a2 = false → ch_g ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##44: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq45 : ∀a2.eq_ascii ch_h a2 = false → ch_h ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##45: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq46 : ∀a2.eq_ascii ch_i a2 = false → ch_i ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##46: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq47 : ∀a2.eq_ascii ch_j a2 = false → ch_j ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##47: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq48 : ∀a2.eq_ascii ch_k a2 = false → ch_k ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##48: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq49 : ∀a2.eq_ascii ch_l a2 = false → ch_l ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##49: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq50 : ∀a2.eq_ascii ch_m a2 = false → ch_m ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##50: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq51 : ∀a2.eq_ascii ch_n a2 = false → ch_n ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##51: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq52 : ∀a2.eq_ascii ch_o a2 = false → ch_o ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##52: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq53 : ∀a2.eq_ascii ch_p a2 = false → ch_p ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##53: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq54 : ∀a2.eq_ascii ch_q a2 = false → ch_q ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##54: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq55 : ∀a2.eq_ascii ch_r a2 = false → ch_r ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##55: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq56 : ∀a2.eq_ascii ch_s a2 = false → ch_s ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##56: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq57 : ∀a2.eq_ascii ch_t a2 = false → ch_t ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##57: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq58 : ∀a2.eq_ascii ch_u a2 = false → ch_u ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##58: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq59 : ∀a2.eq_ascii ch_v a2 = false → ch_v ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##59: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq60 : ∀a2.eq_ascii ch_w a2 = false → ch_w ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##60: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq61 : ∀a2.eq_ascii ch_x a2 = false → ch_x ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##61: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq62 : ∀a2.eq_ascii ch_y a2 = false → ch_y ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##62: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq63 : ∀a2.eq_ascii ch_z a2 = false → ch_z ≠ a2.
+ #a2; ncases a2; nnormalize; #H;
+ ##[ ##63: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqascii_to_neq : ∀c1,c2.eq_ascii c1 c2 = false → c1 ≠ c2.
+ #c1; ncases c1;
+ ##[ ##1: napply neqascii_to_neq1 ##| ##2: napply neqascii_to_neq2
+ ##| ##3: napply neqascii_to_neq3 ##| ##4: napply neqascii_to_neq4
+ ##| ##5: napply neqascii_to_neq5 ##| ##6: napply neqascii_to_neq6
+ ##| ##7: napply neqascii_to_neq7 ##| ##8: napply neqascii_to_neq8 
+ ##| ##9: napply neqascii_to_neq9 ##| ##10: napply neqascii_to_neq10
+ ##| ##11: napply neqascii_to_neq11 ##| ##12: napply neqascii_to_neq12 
+ ##| ##13: napply neqascii_to_neq13 ##| ##14: napply neqascii_to_neq14 
+ ##| ##15: napply neqascii_to_neq15 ##| ##16: napply neqascii_to_neq16 
+ ##| ##17: napply neqascii_to_neq17 ##| ##18: napply neqascii_to_neq18
+ ##| ##19: napply neqascii_to_neq19 ##| ##20: napply neqascii_to_neq20 
+ ##| ##21: napply neqascii_to_neq21 ##| ##22: napply neqascii_to_neq22 
+ ##| ##23: napply neqascii_to_neq23 ##| ##24: napply neqascii_to_neq24 
+ ##| ##25: napply neqascii_to_neq25 ##| ##26: napply neqascii_to_neq26
+ ##| ##27: napply neqascii_to_neq27 ##| ##28: napply neqascii_to_neq28
+ ##| ##29: napply neqascii_to_neq29 ##| ##30: napply neqascii_to_neq30 
+ ##| ##31: napply neqascii_to_neq31 ##| ##32: napply neqascii_to_neq32 
+ ##| ##33: napply neqascii_to_neq33 ##| ##34: napply neqascii_to_neq34
+ ##| ##35: napply neqascii_to_neq35 ##| ##36: napply neqascii_to_neq36
+ ##| ##37: napply neqascii_to_neq37 ##| ##38: napply neqascii_to_neq38
+ ##| ##39: napply neqascii_to_neq39 ##| ##40: napply neqascii_to_neq40
+ ##| ##41: napply neqascii_to_neq41 ##| ##42: napply neqascii_to_neq42
+ ##| ##43: napply neqascii_to_neq43 ##| ##44: napply neqascii_to_neq44 
+ ##| ##45: napply neqascii_to_neq45 ##| ##46: napply neqascii_to_neq46
+ ##| ##47: napply neqascii_to_neq47 ##| ##48: napply neqascii_to_neq48 
+ ##| ##49: napply neqascii_to_neq49 ##| ##50: napply neqascii_to_neq50
+ ##| ##51: napply neqascii_to_neq51 ##| ##52: napply neqascii_to_neq52
+ ##| ##53: napply neqascii_to_neq53 ##| ##54: napply neqascii_to_neq54 
+ ##| ##55: napply neqascii_to_neq55 ##| ##56: napply neqascii_to_neq56
+ ##| ##57: napply neqascii_to_neq57 ##| ##58: napply neqascii_to_neq58
+ ##| ##59: napply neqascii_to_neq59 ##| ##60: napply neqascii_to_neq60 
+ ##| ##61: napply neqascii_to_neq61 ##| ##62: napply neqascii_to_neq62 
+ ##| ##63: napply neqascii_to_neq63 ##]
+nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas5.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas5.ma
new file mode 100755
index 000000000..425f4a556
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas5.ma
@@ -0,0 +1,127 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/ascii.ma".
+
+(* ************************** *)
+(* DEFINIZIONE ASCII MINIMALE *)
+(* ************************** *)
+
+nlemma neq_to_neqascii1 : ∀a2.ch_0 ≠ a2 → eq_ascii ch_0 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii2 : ∀a2.ch_1 ≠ a2 → eq_ascii ch_1 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii3 : ∀a2.ch_2 ≠ a2 → eq_ascii ch_2 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii4 : ∀a2.ch_3 ≠ a2 → eq_ascii ch_3 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii5 : ∀a2.ch_4 ≠ a2 → eq_ascii ch_4 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii6 : ∀a2.ch_5 ≠ a2 → eq_ascii ch_5 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii7 : ∀a2.ch_6 ≠ a2 → eq_ascii ch_6 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii8 : ∀a2.ch_7 ≠ a2 → eq_ascii ch_7 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii9 : ∀a2.ch_8 ≠ a2 → eq_ascii ch_8 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii10 : ∀a2.ch_9 ≠ a2 → eq_ascii ch_9 a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii11 : ∀a2.ch__ ≠ a2 → eq_ascii ch__ a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii12 : ∀a2.ch_A ≠ a2 → eq_ascii ch_A a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii13 : ∀a2.ch_B ≠ a2 → eq_ascii ch_B a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii14 : ∀a2.ch_C ≠ a2 → eq_ascii ch_C a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii15 : ∀a2.ch_D ≠ a2 → eq_ascii ch_D a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii16 : ∀a2.ch_E ≠ a2 → eq_ascii ch_E a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii17 : ∀a2.ch_F ≠ a2 → eq_ascii ch_F a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii18 : ∀a2.ch_G ≠ a2 → eq_ascii ch_G a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii19 : ∀a2.ch_H ≠ a2 → eq_ascii ch_H a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii20 : ∀a2.ch_I ≠ a2 → eq_ascii ch_I a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii21 : ∀a2.ch_J ≠ a2 → eq_ascii ch_J a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii22 : ∀a2.ch_K ≠ a2 → eq_ascii ch_K a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii23 : ∀a2.ch_L ≠ a2 → eq_ascii ch_L a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii24 : ∀a2.ch_M ≠ a2 → eq_ascii ch_M a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii25 : ∀a2.ch_N ≠ a2 → eq_ascii ch_N a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii26 : ∀a2.ch_O ≠ a2 → eq_ascii ch_O a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii27 : ∀a2.ch_P ≠ a2 → eq_ascii ch_P a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii28 : ∀a2.ch_Q ≠ a2 → eq_ascii ch_Q a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii29 : ∀a2.ch_R ≠ a2 → eq_ascii ch_R a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii30 : ∀a2.ch_S ≠ a2 → eq_ascii ch_S a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii31 : ∀a2.ch_T ≠ a2 → eq_ascii ch_T a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii32 : ∀a2.ch_U ≠ a2 → eq_ascii ch_U a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii33 : ∀a2.ch_V ≠ a2 → eq_ascii ch_V a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##33: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii34 : ∀a2.ch_W ≠ a2 → eq_ascii ch_W a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##34: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii35 : ∀a2.ch_X ≠ a2 → eq_ascii ch_X a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##35: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii36 : ∀a2.ch_Y ≠ a2 → eq_ascii ch_Y a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##36: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii37 : ∀a2.ch_Z ≠ a2 → eq_ascii ch_Z a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##37: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii38 : ∀a2.ch_a ≠ a2 → eq_ascii ch_a a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##38: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii39 : ∀a2.ch_b ≠ a2 → eq_ascii ch_b a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##39: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii40 : ∀a2.ch_c ≠ a2 → eq_ascii ch_c a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##40: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii41 : ∀a2.ch_d ≠ a2 → eq_ascii ch_d a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##41: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii42 : ∀a2.ch_e ≠ a2 → eq_ascii ch_e a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##42: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii43 : ∀a2.ch_f ≠ a2 → eq_ascii ch_f a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##43: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii44 : ∀a2.ch_g ≠ a2 → eq_ascii ch_g a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##44: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii45 : ∀a2.ch_h ≠ a2 → eq_ascii ch_h a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##45: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii46 : ∀a2.ch_i ≠ a2 → eq_ascii ch_i a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##46: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii47 : ∀a2.ch_j ≠ a2 → eq_ascii ch_j a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##47: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii48 : ∀a2.ch_k ≠ a2 → eq_ascii ch_k a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##48: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii49 : ∀a2.ch_l ≠ a2 → eq_ascii ch_l a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##49: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii50 : ∀a2.ch_m ≠ a2 → eq_ascii ch_m a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##50: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii51 : ∀a2.ch_n ≠ a2 → eq_ascii ch_n a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##51: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii52 : ∀a2.ch_o ≠ a2 → eq_ascii ch_o a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##52: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii53 : ∀a2.ch_p ≠ a2 → eq_ascii ch_p a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##53: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii54 : ∀a2.ch_q ≠ a2 → eq_ascii ch_q a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##54: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii55 : ∀a2.ch_r ≠ a2 → eq_ascii ch_r a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##55: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii56 : ∀a2.ch_s ≠ a2 → eq_ascii ch_s a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##56: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii57 : ∀a2.ch_t ≠ a2 → eq_ascii ch_t a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##57: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii58 : ∀a2.ch_u ≠ a2 → eq_ascii ch_u a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##58: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii59 : ∀a2.ch_v ≠ a2 → eq_ascii ch_v a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##59: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii60 : ∀a2.ch_w ≠ a2 → eq_ascii ch_w a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##60: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii61 : ∀a2.ch_x ≠ a2 → eq_ascii ch_x a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##61: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii62 : ∀a2.ch_y ≠ a2 → eq_ascii ch_y a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##62: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqascii63 : ∀a2.ch_z ≠ a2 → eq_ascii ch_z a2 = false. #a2; ncases a2; nnormalize; #H; ##[ ##63: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+
+nlemma neq_to_neqascii : ∀a1,a2.a1 ≠ a2 → eq_ascii a1 a2 = false.
+ #a1; nelim a1;
+ ##[ ##1: napply neq_to_neqascii1 ##| ##2: napply neq_to_neqascii2
+ ##| ##3: napply neq_to_neqascii3 ##| ##4: napply neq_to_neqascii4
+ ##| ##5: napply neq_to_neqascii5 ##| ##6: napply neq_to_neqascii6
+ ##| ##7: napply neq_to_neqascii7 ##| ##8: napply neq_to_neqascii8
+ ##| ##9: napply neq_to_neqascii9 ##| ##10: napply neq_to_neqascii10
+ ##| ##11: napply neq_to_neqascii11 ##| ##12: napply neq_to_neqascii12
+ ##| ##13: napply neq_to_neqascii13 ##| ##14: napply neq_to_neqascii14
+ ##| ##15: napply neq_to_neqascii15 ##| ##16: napply neq_to_neqascii16
+ ##| ##17: napply neq_to_neqascii17 ##| ##18: napply neq_to_neqascii18
+ ##| ##19: napply neq_to_neqascii19 ##| ##20: napply neq_to_neqascii20
+ ##| ##21: napply neq_to_neqascii21 ##| ##22: napply neq_to_neqascii22
+ ##| ##23: napply neq_to_neqascii23 ##| ##24: napply neq_to_neqascii24
+ ##| ##25: napply neq_to_neqascii25 ##| ##26: napply neq_to_neqascii26
+ ##| ##27: napply neq_to_neqascii27 ##| ##28: napply neq_to_neqascii28
+ ##| ##29: napply neq_to_neqascii29 ##| ##30: napply neq_to_neqascii30
+ ##| ##31: napply neq_to_neqascii31 ##| ##32: napply neq_to_neqascii32
+ ##| ##33: napply neq_to_neqascii33 ##| ##34: napply neq_to_neqascii34
+ ##| ##35: napply neq_to_neqascii35 ##| ##36: napply neq_to_neqascii36
+ ##| ##37: napply neq_to_neqascii37 ##| ##38: napply neq_to_neqascii38
+ ##| ##39: napply neq_to_neqascii39 ##| ##40: napply neq_to_neqascii40
+ ##| ##41: napply neq_to_neqascii41 ##| ##42: napply neq_to_neqascii42
+ ##| ##43: napply neq_to_neqascii43 ##| ##44: napply neq_to_neqascii44
+ ##| ##45: napply neq_to_neqascii45 ##| ##46: napply neq_to_neqascii46
+ ##| ##47: napply neq_to_neqascii47 ##| ##48: napply neq_to_neqascii48
+ ##| ##49: napply neq_to_neqascii49 ##| ##50: napply neq_to_neqascii50
+ ##| ##51: napply neq_to_neqascii51 ##| ##52: napply neq_to_neqascii52
+ ##| ##53: napply neq_to_neqascii53 ##| ##54: napply neq_to_neqascii54
+ ##| ##55: napply neq_to_neqascii55 ##| ##56: napply neq_to_neqascii56
+ ##| ##57: napply neq_to_neqascii57 ##| ##58: napply neq_to_neqascii58
+ ##| ##59: napply neq_to_neqascii59 ##| ##60: napply neq_to_neqascii60
+ ##| ##61: napply neq_to_neqascii61 ##| ##62: napply neq_to_neqascii62
+ ##| ##63: napply neq_to_neqascii63 ##]
+nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends
index be208f0d6..4c4e9187b 100644
--- a/helm/software/matita/contribs/ng_assembly/depends
+++ b/helm/software/matita/contribs/ng_assembly/depends
@@ -21,8 +21,9 @@ num/byte8.ma num/bitrigesim.ma num/exadecim.ma
 freescale/opcode_base_lemmas_opcode1.ma freescale/opcode_base.ma num/bool_lemmas.ma
 freescale/memory_func.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma
 freescale/load_write.ma freescale/model.ma freescale/translation.ma
-freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma
+common/ascii_lemmas4.ma common/ascii_lemmas1.ma num/bool_lemmas.ma
 common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
+freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma
 common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma
 freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma
 freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
@@ -35,6 +36,7 @@ freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma
 common/string.ma common/ascii.ma common/list_utility.ma
 common/theory.ma 
 compiler/ast_type.ma common/list_utility.ma
+common/ascii_lemmas3.ma common/ascii_lemmas1.ma num/bool_lemmas.ma
 num/word16.ma num/byte8.ma
 freescale/memory_trees.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma
 common/prod.ma num/bool.ma
@@ -64,6 +66,7 @@ freescale/opcode_base_lemmas_instrmode1.ma freescale/opcode_base.ma num/bitriges
 num/bitrigesim.ma num/bool.ma
 common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
 freescale/opcode_base_lemmas_opcode2.ma freescale/opcode_base_lemmas_opcode1.ma
+common/ascii_lemmas5.ma common/ascii.ma
 common/list.ma common/theory.ma
 num/oct.ma num/bool.ma
 freescale/opcode.ma common/list.ma freescale/opcode_base.ma