helm/software/matita/contribs/ng_assembly/common/ascii_lemmas5.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/ascii.ma".
  24
  25 (* ************************** *)
  26 (* DEFINIZIONE ASCII MINIMALE *)
  27 (* ************************** *)
  28
  29 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.
  30 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.
  31 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.
  32 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.
  33 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.
  34 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.
  35 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.
  36 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.
  37 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.
  38 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.
  39 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.
  40 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.
  41 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.
  42 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.
  43 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.
  44 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.
  45 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.
  46 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.
  47 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.
  48 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.
  49 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.
  50 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.
  51 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.
  52 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.
  53 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.
  54 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.
  55 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.
  56 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.
  57 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.
  58 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.
  59 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.
  60 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.
  61 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.
  62 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.
  63 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.
  64 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.
  65 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.
  66 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.
  67 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.
  68 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.
  69 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.
  70 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.
  71 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.
  72 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.
  73 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.
  74 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.
  75 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.
  76 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.
  77 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.
  78 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.
  79 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.
  80 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.
  81 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.
  82 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.
  83 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.
  84 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.
  85 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.
  86 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.
  87 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.
  88 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.
  89 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.
  90 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.
  91 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.
  92
  93 nlemma neq_to_neqascii : ∀a1,a2.a1 ≠ a2 → eq_ascii a1 a2 = false.
  94  #a1; nelim a1;
  95  ##[ ##1: napply neq_to_neqascii1 ##| ##2: napply neq_to_neqascii2
  96  ##| ##3: napply neq_to_neqascii3 ##| ##4: napply neq_to_neqascii4
  97  ##| ##5: napply neq_to_neqascii5 ##| ##6: napply neq_to_neqascii6
  98  ##| ##7: napply neq_to_neqascii7 ##| ##8: napply neq_to_neqascii8
  99  ##| ##9: napply neq_to_neqascii9 ##| ##10: napply neq_to_neqascii10
 100  ##| ##11: napply neq_to_neqascii11 ##| ##12: napply neq_to_neqascii12
 101  ##| ##13: napply neq_to_neqascii13 ##| ##14: napply neq_to_neqascii14
 102  ##| ##15: napply neq_to_neqascii15 ##| ##16: napply neq_to_neqascii16
 103  ##| ##17: napply neq_to_neqascii17 ##| ##18: napply neq_to_neqascii18
 104  ##| ##19: napply neq_to_neqascii19 ##| ##20: napply neq_to_neqascii20
 105  ##| ##21: napply neq_to_neqascii21 ##| ##22: napply neq_to_neqascii22
 106  ##| ##23: napply neq_to_neqascii23 ##| ##24: napply neq_to_neqascii24
 107  ##| ##25: napply neq_to_neqascii25 ##| ##26: napply neq_to_neqascii26
 108  ##| ##27: napply neq_to_neqascii27 ##| ##28: napply neq_to_neqascii28
 109  ##| ##29: napply neq_to_neqascii29 ##| ##30: napply neq_to_neqascii30
 110  ##| ##31: napply neq_to_neqascii31 ##| ##32: napply neq_to_neqascii32
 111  ##| ##33: napply neq_to_neqascii33 ##| ##34: napply neq_to_neqascii34
 112  ##| ##35: napply neq_to_neqascii35 ##| ##36: napply neq_to_neqascii36
 113  ##| ##37: napply neq_to_neqascii37 ##| ##38: napply neq_to_neqascii38
 114  ##| ##39: napply neq_to_neqascii39 ##| ##40: napply neq_to_neqascii40
 115  ##| ##41: napply neq_to_neqascii41 ##| ##42: napply neq_to_neqascii42
 116  ##| ##43: napply neq_to_neqascii43 ##| ##44: napply neq_to_neqascii44
 117  ##| ##45: napply neq_to_neqascii45 ##| ##46: napply neq_to_neqascii46
 118  ##| ##47: napply neq_to_neqascii47 ##| ##48: napply neq_to_neqascii48
 119  ##| ##49: napply neq_to_neqascii49 ##| ##50: napply neq_to_neqascii50
 120  ##| ##51: napply neq_to_neqascii51 ##| ##52: napply neq_to_neqascii52
 121  ##| ##53: napply neq_to_neqascii53 ##| ##54: napply neq_to_neqascii54
 122  ##| ##55: napply neq_to_neqascii55 ##| ##56: napply neq_to_neqascii56
 123  ##| ##57: napply neq_to_neqascii57 ##| ##58: napply neq_to_neqascii58
 124  ##| ##59: napply neq_to_neqascii59 ##| ##60: napply neq_to_neqascii60
 125  ##| ##61: napply neq_to_neqascii61 ##| ##62: napply neq_to_neqascii62
 126  ##| ##63: napply neq_to_neqascii63 ##]
 127 nqed.