helm/software/matita/contribs/ng_assembly/universe/bitrigesim.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 "universe/universe.ma".
  24
  25 ndefinition BIT_UN ≝ [ ut00; ut01; ut02; ut03; ut04; ut05; ut06; ut07; ut08; ut09; ut0A; ut0B; ut0C; ut0D; ut0E; ut0F;
  26                        ut10; ut11; ut12; ut13; ut14; ut15; ut16; ut17; ut18; ut19; ut1A; ut1B; ut1C; ut1D; ut1E; ut1F ].
  27
  28 (* derivati dall'universo
  29   1) SUN_destruct BIT_UN
  30   2) eq_to_eqSUN BIT_UN
  31   3) neq_to_neqSUN BIT_UN
  32   4) eqSUN_to_eq BIT_UN
  33   5) neqSUN_to_neq BIT_UN
  34   6) decidable_SUN BIT_UN
  35   7) symmetric_eqSUN BIT_UN
  36 *)
  37
  38 nlemma un_t00 : S_UN BIT_UN. napply (S_EL BIT_UN ut00 (refl_eq …) ?); #y; nelim y; ##[ ##29: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  39 nlemma un_t01 : S_UN BIT_UN. napply (S_EL BIT_UN ut01 (refl_eq …) ?); #y; nelim y; ##[ ##30: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  40 nlemma un_t02 : S_UN BIT_UN. napply (S_EL BIT_UN ut02 (refl_eq …) ?); #y; nelim y; ##[ ##31: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  41 nlemma un_t03 : S_UN BIT_UN. napply (S_EL BIT_UN ut03 (refl_eq …) ?); #y; nelim y; ##[ ##32: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  42 nlemma un_t04 : S_UN BIT_UN. napply (S_EL BIT_UN ut04 (refl_eq …) ?); #y; nelim y; ##[ ##33: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  43 nlemma un_t05 : S_UN BIT_UN. napply (S_EL BIT_UN ut05 (refl_eq …) ?); #y; nelim y; ##[ ##34: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  44 nlemma un_t06 : S_UN BIT_UN. napply (S_EL BIT_UN ut06 (refl_eq …) ?); #y; nelim y; ##[ ##35: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  45 nlemma un_t07 : S_UN BIT_UN. napply (S_EL BIT_UN ut07 (refl_eq …) ?); #y; nelim y; ##[ ##36: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  46 nlemma un_t08 : S_UN BIT_UN. napply (S_EL BIT_UN ut08 (refl_eq …) ?); #y; nelim y; ##[ ##37: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  47 nlemma un_t09 : S_UN BIT_UN. napply (S_EL BIT_UN ut09 (refl_eq …) ?); #y; nelim y; ##[ ##38: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  48 nlemma un_t0A : S_UN BIT_UN. napply (S_EL BIT_UN ut0A (refl_eq …) ?); #y; nelim y; ##[ ##39: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  49 nlemma un_t0B : S_UN BIT_UN. napply (S_EL BIT_UN ut0B (refl_eq …) ?); #y; nelim y; ##[ ##40: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  50 nlemma un_t0C : S_UN BIT_UN. napply (S_EL BIT_UN ut0C (refl_eq …) ?); #y; nelim y; ##[ ##41: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  51 nlemma un_t0D : S_UN BIT_UN. napply (S_EL BIT_UN ut0D (refl_eq …) ?); #y; nelim y; ##[ ##42: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  52 nlemma un_t0E : S_UN BIT_UN. napply (S_EL BIT_UN ut0E (refl_eq …) ?); #y; nelim y; ##[ ##43: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  53 nlemma un_t0F : S_UN BIT_UN. napply (S_EL BIT_UN ut0F (refl_eq …) ?); #y; nelim y; ##[ ##44: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  54 nlemma un_t10 : S_UN BIT_UN. napply (S_EL BIT_UN ut10 (refl_eq …) ?); #y; nelim y; ##[ ##45: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  55 nlemma un_t11 : S_UN BIT_UN. napply (S_EL BIT_UN ut11 (refl_eq …) ?); #y; nelim y; ##[ ##46: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  56 nlemma un_t12 : S_UN BIT_UN. napply (S_EL BIT_UN ut12 (refl_eq …) ?); #y; nelim y; ##[ ##47: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  57 nlemma un_t13 : S_UN BIT_UN. napply (S_EL BIT_UN ut13 (refl_eq …) ?); #y; nelim y; ##[ ##48: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  58 nlemma un_t14 : S_UN BIT_UN. napply (S_EL BIT_UN ut14 (refl_eq …) ?); #y; nelim y; ##[ ##49: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  59 nlemma un_t15 : S_UN BIT_UN. napply (S_EL BIT_UN ut15 (refl_eq …) ?); #y; nelim y; ##[ ##50: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  60 nlemma un_t16 : S_UN BIT_UN. napply (S_EL BIT_UN ut16 (refl_eq …) ?); #y; nelim y; ##[ ##51: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  61 nlemma un_t17 : S_UN BIT_UN. napply (S_EL BIT_UN ut17 (refl_eq …) ?); #y; nelim y; ##[ ##52: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  62 nlemma un_t18 : S_UN BIT_UN. napply (S_EL BIT_UN ut18 (refl_eq …) ?); #y; nelim y; ##[ ##53: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  63 nlemma un_t19 : S_UN BIT_UN. napply (S_EL BIT_UN ut19 (refl_eq …) ?); #y; nelim y; ##[ ##54: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  64 nlemma un_t1A : S_UN BIT_UN. napply (S_EL BIT_UN ut1A (refl_eq …) ?); #y; nelim y; ##[ ##55: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  65 nlemma un_t1B : S_UN BIT_UN. napply (S_EL BIT_UN ut1B (refl_eq …) ?); #y; nelim y; ##[ ##56: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  66 nlemma un_t1C : S_UN BIT_UN. napply (S_EL BIT_UN ut1C (refl_eq …) ?); #y; nelim y; ##[ ##57: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  67 nlemma un_t1D : S_UN BIT_UN. napply (S_EL BIT_UN ut1D (refl_eq …) ?); #y; nelim y; ##[ ##58: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  68 nlemma un_t1E : S_UN BIT_UN. napply (S_EL BIT_UN ut1E (refl_eq …) ?); #y; nelim y; ##[ ##59: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  69 nlemma un_t1F : S_UN BIT_UN. napply (S_EL BIT_UN ut1F (refl_eq …) ?); #y; nelim y; ##[ ##60: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.