helm/software/matita/library/freescale/memory_struct.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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 set "baseuri" "cic:/matita/freescale/memory_struct/".
  28
  29 (*include "/media/VIRTUOSO/freescale/translation.ma".*)
  30 include "freescale/translation.ma".
  31
  32 (* **************************** *)
  33 (* TIPI PER I MODULI DI MEMORIA *)
  34 (* **************************** *)
  35
  36 (* tipi di memoria:RAM/ROM/non installata *)
  37 inductive memory_type : Type ≝
  38   MEM_READ_ONLY: memory_type
  39 | MEM_READ_WRITE: memory_type
  40 | MEM_OUT_OF_BOUND: memory_type.
  41
  42 (* **************** *)
  43 (* TIPO ARRAY DA 16 *)
  44 (* **************** *)
  45
  46 (* definizione di un array omogeneo di dimensione 16 *)
  47 inductive Prod16T (T:Type) : Type ≝
  48 array_16T : T → T → T → T → T → T → T → T →
  49             T → T → T → T → T → T → T → T →
  50             Prod16T T.
  51
  52 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  53 (* posso definire un getter a matrice sull'array *)
  54 definition getn_array16T ≝
  55 λn:exadecim.λT:Type.λp:Prod16T T.
  56  match p with
  57   [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
  58  match n with
  59   [ x0 ⇒ e00 | x1 ⇒ e01 | x2 ⇒ e02 | x3 ⇒ e03 | x4 ⇒ e04 | x5 ⇒ e05 | x6 ⇒ e06 | x7 ⇒ e07
  60   | x8 ⇒ e08 | x9 ⇒ e09 | xA ⇒ e10 | xB ⇒ e11 | xC ⇒ e12 | xD ⇒ e13 | xE ⇒ e14 | xF ⇒ e15
  61   ]].
  62
  63 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  64 (* posso definire un setter a matrice sull'array *)
  65 definition setn_array16T ≝
  66 λn:exadecim.λT:Type.λp:Prod16T T.λv:T.
  67  match p with
  68   [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
  69  match n with
  70   [ x0 ⇒ array_16T T v   e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  71   | x1 ⇒ array_16T T e00 v   e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  72   | x2 ⇒ array_16T T e00 e01 v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  73   | x3 ⇒ array_16T T e00 e01 e02 v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  74   | x4 ⇒ array_16T T e00 e01 e02 e03 v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  75   | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  76   | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v   e07 e08 e09 e10 e11 e12 e13 e14 e15
  77   | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v   e08 e09 e10 e11 e12 e13 e14 e15
  78   | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v   e09 e10 e11 e12 e13 e14 e15
  79   | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v   e10 e11 e12 e13 e14 e15
  80   | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v   e11 e12 e13 e14 e15
  81   | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v   e12 e13 e14 e15
  82   | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v   e13 e14 e15
  83   | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v   e14 e15
  84   | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v   e15
  85   | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
  86   ]].
  87
  88 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  89 (* posso definire un setter multiplo [m,n] a matrice sull'array *)
  90 definition setmn_array16T ≝
  91 λm,n:exadecim.λT:Type.λp:Prod16T T.λv:T.
  92  match p with
  93   [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
  94  match m with
  95   [ x0 ⇒ match n with
  96    [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  97    | x1 ⇒ array_16T T v v   e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  98    | x2 ⇒ array_16T T v v   v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  99    | x3 ⇒ array_16T T v v   v   v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 100    | x4 ⇒ array_16T T v v   v   v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 101    | x5 ⇒ array_16T T v v   v   v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 102    | x6 ⇒ array_16T T v v   v   v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 103    | x7 ⇒ array_16T T v v   v   v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 104    | x8 ⇒ array_16T T v v   v   v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 105    | x9 ⇒ array_16T T v v   v   v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 106    | xA ⇒ array_16T T v v   v   v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 107    | xB ⇒ array_16T T v v   v   v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 108    | xC ⇒ array_16T T v v   v   v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 109    | xD ⇒ array_16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   e14 e15
 110    | xE ⇒ array_16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   v   e15
 111    | xF ⇒ array_16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   v   v ]
 112   | x1 ⇒ match n with
 113    [ x0 ⇒ p
 114    | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 115    | x2 ⇒ array_16T T e00 v v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 116    | x3 ⇒ array_16T T e00 v v   v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 117    | x4 ⇒ array_16T T e00 v v   v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 118    | x5 ⇒ array_16T T e00 v v   v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 119    | x6 ⇒ array_16T T e00 v v   v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 120    | x7 ⇒ array_16T T e00 v v   v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 121    | x8 ⇒ array_16T T e00 v v   v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 122    | x9 ⇒ array_16T T e00 v v   v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 123    | xA ⇒ array_16T T e00 v v   v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 124    | xB ⇒ array_16T T e00 v v   v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 125    | xC ⇒ array_16T T e00 v v   v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 126    | xD ⇒ array_16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   e14 e15
 127    | xE ⇒ array_16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   v   e15
 128    | xF ⇒ array_16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   v   v ]
 129   | x2 ⇒ match n with
 130    [ x0 ⇒ p | x1 ⇒ p
 131    | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 132    | x3 ⇒ array_16T T e00 e01 v v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 133    | x4 ⇒ array_16T T e00 e01 v v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 134    | x5 ⇒ array_16T T e00 e01 v v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 135    | x6 ⇒ array_16T T e00 e01 v v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 136    | x7 ⇒ array_16T T e00 e01 v v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 137    | x8 ⇒ array_16T T e00 e01 v v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 138    | x9 ⇒ array_16T T e00 e01 v v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 139    | xA ⇒ array_16T T e00 e01 v v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 140    | xB ⇒ array_16T T e00 e01 v v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 141    | xC ⇒ array_16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 142    | xD ⇒ array_16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   e14 e15
 143    | xE ⇒ array_16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   v   e15
 144    | xF ⇒ array_16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   v   v ]
 145   | x3 ⇒ match n with
 146    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p
 147    | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 148    | x4 ⇒ array_16T T e00 e01 e02 v v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 149    | x5 ⇒ array_16T T e00 e01 e02 v v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 150    | x6 ⇒ array_16T T e00 e01 e02 v v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 151    | x7 ⇒ array_16T T e00 e01 e02 v v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 152    | x8 ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 153    | x9 ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 154    | xA ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 155    | xB ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   v   v   v   e12 e13 e14 e15
 156    | xC ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   e13 e14 e15
 157    | xD ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   e14 e15
 158    | xE ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   v   e15
 159    | xF ⇒ array_16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   v   v ]
 160   | x4 ⇒ match n with
 161    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p
 162    | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 163    | x5 ⇒ array_16T T e00 e01 e02 e03 v v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 164    | x6 ⇒ array_16T T e00 e01 e02 e03 v v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 165    | x7 ⇒ array_16T T e00 e01 e02 e03 v v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 166    | x8 ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 167    | x9 ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   v   e10 e11 e12 e13 e14 e15
 168    | xA ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   v   v   e11 e12 e13 e14 e15
 169    | xB ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   e12 e13 e14 e15
 170    | xC ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   e13 e14 e15
 171    | xD ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   e14 e15
 172    | xE ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   v   e15
 173    | xF ⇒ array_16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   v   v ]
 174   | x5 ⇒ match n with
 175    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p
 176    | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 177    | x6 ⇒ array_16T T e00 e01 e02 e03 e04 v v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 178    | x7 ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   e08 e09 e10 e11 e12 e13 e14 e15
 179    | x8 ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   e09 e10 e11 e12 e13 e14 e15
 180    | x9 ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   v   e10 e11 e12 e13 e14 e15
 181    | xA ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   v   v   e11 e12 e13 e14 e15
 182    | xB ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   e12 e13 e14 e15
 183    | xC ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   e13 e14 e15
 184    | xD ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   e14 e15
 185    | xE ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   v   e15
 186    | xF ⇒ array_16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   v   v ]
 187   | x6 ⇒ match n with
 188    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p
 189    | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
 190    | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   e08 e09 e10 e11 e12 e13 e14 e15
 191    | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   e09 e10 e11 e12 e13 e14 e15
 192    | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   v   e10 e11 e12 e13 e14 e15
 193    | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   e11 e12 e13 e14 e15
 194    | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   e12 e13 e14 e15
 195    | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   e13 e14 e15
 196    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   e14 e15
 197    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   v   e15
 198    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   v   v ]
 199   | x7 ⇒ match n with
 200    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p
 201    | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
 202    | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   e09 e10 e11 e12 e13 e14 e15
 203    | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   v   e10 e11 e12 e13 e14 e15
 204    | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   e11 e12 e13 e14 e15
 205    | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   e12 e13 e14 e15
 206    | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   e13 e14 e15
 207    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   e14 e15
 208    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   v   e15
 209    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   v   v ]
 210   | x8 ⇒ match n with
 211    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 212    | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
 213    | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   e10 e11 e12 e13 e14 e15
 214    | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   e11 e12 e13 e14 e15
 215    | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   e12 e13 e14 e15
 216    | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   e13 e14 e15
 217    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   e14 e15
 218    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   v   e15
 219    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   v   v ]
 220   | x9 ⇒ match n with
 221    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p  | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 222    | x8 ⇒ p
 223    | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
 224    | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   e11 e12 e13 e14 e15
 225    | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   e12 e13 e14 e15
 226    | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   e13 e14 e15
 227    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   e14 e15
 228    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   v   e15
 229    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   v   v ]
 230   | xA ⇒ match n with
 231    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 232    | x8 ⇒ p | x9 ⇒ p
 233    | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
 234    | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   e12 e13 e14 e15
 235    | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   e13 e14 e15
 236    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   e14 e15
 237    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   v   e15
 238    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   v   v ]
 239   | xB ⇒ match n with
 240    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 241    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p
 242    | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
 243    | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   e13 e14 e15
 244    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   e14 e15
 245    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   v   e15
 246    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   v   v ]
 247   | xC ⇒ match n with
 248    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 249    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p
 250    | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
 251    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   e14 e15
 252    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   v   e15
 253    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   v   v ]
 254   | xD ⇒ match n with
 255    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 256    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p
 257    | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
 258    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v   e15
 259    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v   v ]
 260   | xE ⇒ match n with
 261    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 262    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p
 263    | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
 264    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ]
 265   | xF ⇒ match n with
 266    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 267    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p
 268    | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ]
 269   ]].
 270
 271 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 272 (* posso definire un setter composto [m+1,n-1] a matrice sull'array *)
 273 (* NB: obbiettivo evitare l'overflow *)
 274 definition setmn_array16T_succ_pred ≝
 275 λm,n:exadecim.λT:Type.λp:Prod16T T.λv:T.
 276  match lt_ex m xF with
 277   [ true ⇒ match gt_ex n x0 with
 278    [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v
 279    | false ⇒ p
 280    ]
 281   | false ⇒ p
 282   ].
 283
 284 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 285 (* posso definire un setter composto [m+1,F] a matrice sull'array *)
 286 (* NB: obbiettivo evitare l'overflow *)
 287 definition setmn_array16T_succ ≝
 288 λm:exadecim.λT:Type.λp:Prod16T T.λv:T.
 289  match lt_ex m xF with
 290   [ true ⇒ setmn_array16T (succ_ex m) xF T p v
 291   | false ⇒ p
 292   ].
 293
 294 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 295 (* posso definire un setter composto [0,n-1] a matrice sull'array *)
 296 (* NB: obbiettivo evitare l'overflow *)
 297 definition setmn_array16T_pred ≝
 298 λn:exadecim.λT:Type.λp:Prod16T T.λv:T.
 299  match gt_ex n x0 with
 300   [ true ⇒ setmn_array16T x0 (pred_ex n) T p v
 301   | false ⇒ p
 302   ].
 303
 304 (* ************************** *)
 305 (* TIPO BYTE COME INSIEME BIT *)
 306 (* ************************** *)
 307
 308 (* definizione di un byte come 8 bit *)
 309 inductive Prod8T (T:Type) : Type ≝
 310 array_8T : T → T → T → T → T → T → T → T →
 311            Prod8T T.
 312
 313 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 314 (* posso definire un getter a matrice sull'array *)
 315 definition getn_array8T ≝
 316 λn:oct.λT:Type.λp:Prod8T T.
 317  match p with
 318   [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
 319  match n with
 320   [ o0 ⇒ e00 | o1 ⇒ e01 | o2 ⇒ e02 | o3 ⇒ e03 | o4 ⇒ e04 | o5 ⇒ e05 | o6 ⇒ e06 | o7 ⇒ e07 ]].
 321
 322 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 323 (* posso definire un setter a matrice sull'array *)
 324 definition setn_array8T ≝
 325 λn:oct.λT:Type.λp:Prod8T T.λv:T.
 326  match p with
 327   [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
 328  match n with
 329   [ o0 ⇒ array_8T T e07 e06 e05 e04 e03 e02 e01 v
 330   | o1 ⇒ array_8T T e07 e06 e05 e04 e03 e02 v   e00
 331   | o2 ⇒ array_8T T e07 e06 e05 e04 e03 v   e01 e00
 332   | o3 ⇒ array_8T T e07 e06 e05 e04 v   e02 e01 e00
 333   | o4 ⇒ array_8T T e07 e06 e05 v   e03 e02 e01 e00
 334   | o5 ⇒ array_8T T e07 e06 v   e04 e03 e02 e01 e00
 335   | o6 ⇒ array_8T T e07 v   e05 e04 e03 e02 e01 e00
 336   | o7 ⇒ array_8T T v   e06 e05 e04 e03 e02 e01 e00
 337   ]].
 338
 339 (* lettura byte *)
 340 definition byte8_of_bits ≝
 341 λp:Prod8T bool.
 342  match p with
 343   [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
 344    mk_byte8
 345    (or_ex (match e07 with [ true ⇒ x8 | false ⇒ x0 ])
 346    (or_ex (match e06 with [ true ⇒ x4 | false ⇒ x0 ])
 347    (or_ex (match e05 with [ true ⇒ x2 | false ⇒ x0 ])
 348           (match e04 with [ true ⇒ x1 | false ⇒ x0 ]))))
 349    (or_ex (match e03 with [ true ⇒ x8 | false ⇒ x0 ])
 350    (or_ex (match e02 with [ true ⇒ x4 | false ⇒ x0 ])
 351    (or_ex (match e01 with [ true ⇒ x2 | false ⇒ x0 ])
 352           (match e00 with [ true ⇒ x1 | false ⇒ x0 ])))) ].
 353
 354 (* scrittura byte *)
 355 definition bits_of_byte8 ≝
 356 λp:byte8.
 357  match b8h p with
 358   [ x0 ⇒ match b8l p with
 359    [ x0 ⇒ array_8T bool false false false false false false false false
 360    | x1 ⇒ array_8T bool false false false false false false false true
 361    | x2 ⇒ array_8T bool false false false false false false true  false
 362    | x3 ⇒ array_8T bool false false false false false false true  true
 363    | x4 ⇒ array_8T bool false false false false false true  false false
 364    | x5 ⇒ array_8T bool false false false false false true  false true
 365    | x6 ⇒ array_8T bool false false false false false true  true  false
 366    | x7 ⇒ array_8T bool false false false false false true  true  true
 367    | x8 ⇒ array_8T bool false false false false true  false false false
 368    | x9 ⇒ array_8T bool false false false false true  false false true
 369    | xA ⇒ array_8T bool false false false false true  false true  false
 370    | xB ⇒ array_8T bool false false false false true  false true  true
 371    | xC ⇒ array_8T bool false false false false true  true  false false
 372    | xD ⇒ array_8T bool false false false false true  true  false true
 373    | xE ⇒ array_8T bool false false false false true  true  true  false
 374    | xF ⇒ array_8T bool false false false false true  true  true  true ]
 375   | x1 ⇒ match b8l p with
 376    [ x0 ⇒ array_8T bool false false false true  false false false false
 377    | x1 ⇒ array_8T bool false false false true  false false false true
 378    | x2 ⇒ array_8T bool false false false true  false false true  false
 379    | x3 ⇒ array_8T bool false false false true  false false true  true
 380    | x4 ⇒ array_8T bool false false false true  false true  false false
 381    | x5 ⇒ array_8T bool false false false true  false true  false true
 382    | x6 ⇒ array_8T bool false false false true  false true  true  false
 383    | x7 ⇒ array_8T bool false false false true  false true  true  true
 384    | x8 ⇒ array_8T bool false false false true  true  false false false
 385    | x9 ⇒ array_8T bool false false false true  true  false false true
 386    | xA ⇒ array_8T bool false false false true  true  false true  false
 387    | xB ⇒ array_8T bool false false false true  true  false true  true
 388    | xC ⇒ array_8T bool false false false true  true  true  false false
 389    | xD ⇒ array_8T bool false false false true  true  true  false true
 390    | xE ⇒ array_8T bool false false false true  true  true  true  false
 391    | xF ⇒ array_8T bool false false false true  true  true  true  true ]
 392   | x2 ⇒ match b8l p with
 393    [ x0 ⇒ array_8T bool false false true  false false false false false
 394    | x1 ⇒ array_8T bool false false true  false false false false true
 395    | x2 ⇒ array_8T bool false false true  false false false true  false
 396    | x3 ⇒ array_8T bool false false true  false false false true  true
 397    | x4 ⇒ array_8T bool false false true  false false true  false false
 398    | x5 ⇒ array_8T bool false false true  false false true  false true
 399    | x6 ⇒ array_8T bool false false true  false false true  true  false
 400    | x7 ⇒ array_8T bool false false true  false false true  true  true
 401    | x8 ⇒ array_8T bool false false true  false true  false false false
 402    | x9 ⇒ array_8T bool false false true  false true  false false true
 403    | xA ⇒ array_8T bool false false true  false true  false true  false
 404    | xB ⇒ array_8T bool false false true  false true  false true  true
 405    | xC ⇒ array_8T bool false false true  false true  true  false false
 406    | xD ⇒ array_8T bool false false true  false true  true  false true
 407    | xE ⇒ array_8T bool false false true  false true  true  true  false
 408    | xF ⇒ array_8T bool false false true  false true  true  true  true ]
 409   | x3 ⇒ match b8l p with
 410    [ x0 ⇒ array_8T bool false false true  true  false false false false
 411    | x1 ⇒ array_8T bool false false true  true  false false false true
 412    | x2 ⇒ array_8T bool false false true  true  false false true  false
 413    | x3 ⇒ array_8T bool false false true  true  false false true  true
 414    | x4 ⇒ array_8T bool false false true  true  false true  false false
 415    | x5 ⇒ array_8T bool false false true  true  false true  false true
 416    | x6 ⇒ array_8T bool false false true  true  false true  true  false
 417    | x7 ⇒ array_8T bool false false true  true  false true  true  true
 418    | x8 ⇒ array_8T bool false false true  true  true  false false false
 419    | x9 ⇒ array_8T bool false false true  true  true  false false true
 420    | xA ⇒ array_8T bool false false true  true  true  false true  false
 421    | xB ⇒ array_8T bool false false true  true  true  false true  true
 422    | xC ⇒ array_8T bool false false true  true  true  true  false false
 423    | xD ⇒ array_8T bool false false true  true  true  true  false true
 424    | xE ⇒ array_8T bool false false true  true  true  true  true  false
 425    | xF ⇒ array_8T bool false false true  true  true  true  true  true ]
 426   | x4 ⇒ match b8l p with
 427    [ x0 ⇒ array_8T bool false true  false false false false false false
 428    | x1 ⇒ array_8T bool false true  false false false false false true
 429    | x2 ⇒ array_8T bool false true  false false false false true  false
 430    | x3 ⇒ array_8T bool false true  false false false false true  true
 431    | x4 ⇒ array_8T bool false true  false false false true  false false
 432    | x5 ⇒ array_8T bool false true  false false false true  false true
 433    | x6 ⇒ array_8T bool false true  false false false true  true  false
 434    | x7 ⇒ array_8T bool false true  false false false true  true  true
 435    | x8 ⇒ array_8T bool false true  false false true  false false false
 436    | x9 ⇒ array_8T bool false true  false false true  false false true
 437    | xA ⇒ array_8T bool false true  false false true  false true  false
 438    | xB ⇒ array_8T bool false true  false false true  false true  true
 439    | xC ⇒ array_8T bool false true  false false true  true  false false
 440    | xD ⇒ array_8T bool false true  false false true  true  false true
 441    | xE ⇒ array_8T bool false true  false false true  true  true  false
 442    | xF ⇒ array_8T bool false true  false false true  true  true  true ]
 443   | x5 ⇒ match b8l p with
 444    [ x0 ⇒ array_8T bool false true  false true  false false false false
 445    | x1 ⇒ array_8T bool false true  false true  false false false true
 446    | x2 ⇒ array_8T bool false true  false true  false false true  false
 447    | x3 ⇒ array_8T bool false true  false true  false false true  true
 448    | x4 ⇒ array_8T bool false true  false true  false true  false false
 449    | x5 ⇒ array_8T bool false true  false true  false true  false true
 450    | x6 ⇒ array_8T bool false true  false true  false true  true  false
 451    | x7 ⇒ array_8T bool false true  false true  false true  true  true
 452    | x8 ⇒ array_8T bool false true  false true  true  false false false
 453    | x9 ⇒ array_8T bool false true  false true  true  false false true
 454    | xA ⇒ array_8T bool false true  false true  true  false true  false
 455    | xB ⇒ array_8T bool false true  false true  true  false true  true
 456    | xC ⇒ array_8T bool false true  false true  true  true  false false
 457    | xD ⇒ array_8T bool false true  false true  true  true  false true
 458    | xE ⇒ array_8T bool false true  false true  true  true  true  false
 459    | xF ⇒ array_8T bool false true  false true  true  true  true  true ]
 460   | x6 ⇒ match b8l p with
 461    [ x0 ⇒ array_8T bool false true  true  false false false false false
 462    | x1 ⇒ array_8T bool false true  true  false false false false true
 463    | x2 ⇒ array_8T bool false true  true  false false false true  false
 464    | x3 ⇒ array_8T bool false true  true  false false false true  true
 465    | x4 ⇒ array_8T bool false true  true  false false true  false false
 466    | x5 ⇒ array_8T bool false true  true  false false true  false true
 467    | x6 ⇒ array_8T bool false true  true  false false true  true  false
 468    | x7 ⇒ array_8T bool false true  true  false false true  true  true
 469    | x8 ⇒ array_8T bool false true  true  false true  false false false
 470    | x9 ⇒ array_8T bool false true  true  false true  false false true
 471    | xA ⇒ array_8T bool false true  true  false true  false true  false
 472    | xB ⇒ array_8T bool false true  true  false true  false true  true
 473    | xC ⇒ array_8T bool false true  true  false true  true  false false
 474    | xD ⇒ array_8T bool false true  true  false true  true  false true
 475    | xE ⇒ array_8T bool false true  true  false true  true  true  false
 476    | xF ⇒ array_8T bool false true  true  false true  true  true  true ]
 477   | x7 ⇒ match b8l p with
 478    [ x0 ⇒ array_8T bool false true  true  true  false false false false
 479    | x1 ⇒ array_8T bool false true  true  true  false false false true
 480    | x2 ⇒ array_8T bool false true  true  true  false false true  false
 481    | x3 ⇒ array_8T bool false true  true  true  false false true  true
 482    | x4 ⇒ array_8T bool false true  true  true  false true  false false
 483    | x5 ⇒ array_8T bool false true  true  true  false true  false true
 484    | x6 ⇒ array_8T bool false true  true  true  false true  true  false
 485    | x7 ⇒ array_8T bool false true  true  true  false true  true  true
 486    | x8 ⇒ array_8T bool false true  true  true  true  false false false
 487    | x9 ⇒ array_8T bool false true  true  true  true  false false true
 488    | xA ⇒ array_8T bool false true  true  true  true  false true  false
 489    | xB ⇒ array_8T bool false true  true  true  true  false true  true
 490    | xC ⇒ array_8T bool false true  true  true  true  true  false false
 491    | xD ⇒ array_8T bool false true  true  true  true  true  false true
 492    | xE ⇒ array_8T bool false true  true  true  true  true  true  false
 493    | xF ⇒ array_8T bool false true  true  true  true  true  true  true ]
 494   | x8 ⇒ match b8l p with
 495    [ x0 ⇒ array_8T bool true  false false false false false false false
 496    | x1 ⇒ array_8T bool true  false false false false false false true
 497    | x2 ⇒ array_8T bool true  false false false false false true  false
 498    | x3 ⇒ array_8T bool true  false false false false false true  true
 499    | x4 ⇒ array_8T bool true  false false false false true  false false
 500    | x5 ⇒ array_8T bool true  false false false false true  false true
 501    | x6 ⇒ array_8T bool true  false false false false true  true  false
 502    | x7 ⇒ array_8T bool true  false false false false true  true  true
 503    | x8 ⇒ array_8T bool true  false false false true  false false false
 504    | x9 ⇒ array_8T bool true  false false false true  false false true
 505    | xA ⇒ array_8T bool true  false false false true  false true  false
 506    | xB ⇒ array_8T bool true  false false false true  false true  true
 507    | xC ⇒ array_8T bool true  false false false true  true  false false
 508    | xD ⇒ array_8T bool true  false false false true  true  false true
 509    | xE ⇒ array_8T bool true  false false false true  true  true  false
 510    | xF ⇒ array_8T bool true  false false false true  true  true  true ]
 511   | x9 ⇒ match b8l p with
 512    [ x0 ⇒ array_8T bool true  false false true  false false false false
 513    | x1 ⇒ array_8T bool true  false false true  false false false true
 514    | x2 ⇒ array_8T bool true  false false true  false false true  false
 515    | x3 ⇒ array_8T bool true  false false true  false false true  true
 516    | x4 ⇒ array_8T bool true  false false true  false true  false false
 517    | x5 ⇒ array_8T bool true  false false true  false true  false true
 518    | x6 ⇒ array_8T bool true  false false true  false true  true  false
 519    | x7 ⇒ array_8T bool true  false false true  false true  true  true
 520    | x8 ⇒ array_8T bool true  false false true  true  false false false
 521    | x9 ⇒ array_8T bool true  false false true  true  false false true
 522    | xA ⇒ array_8T bool true  false false true  true  false true  false
 523    | xB ⇒ array_8T bool true  false false true  true  false true  true
 524    | xC ⇒ array_8T bool true  false false true  true  true  false false
 525    | xD ⇒ array_8T bool true  false false true  true  true  false true
 526    | xE ⇒ array_8T bool true  false false true  true  true  true  false
 527    | xF ⇒ array_8T bool true  false false true  true  true  true  true ]
 528   | xA ⇒ match b8l p with
 529    [ x0 ⇒ array_8T bool true  false true  false false false false false
 530    | x1 ⇒ array_8T bool true  false true  false false false false true
 531    | x2 ⇒ array_8T bool true  false true  false false false true  false
 532    | x3 ⇒ array_8T bool true  false true  false false false true  true
 533    | x4 ⇒ array_8T bool true  false true  false false true  false false
 534    | x5 ⇒ array_8T bool true  false true  false false true  false true
 535    | x6 ⇒ array_8T bool true  false true  false false true  true  false
 536    | x7 ⇒ array_8T bool true  false true  false false true  true  true
 537    | x8 ⇒ array_8T bool true  false true  false true  false false false
 538    | x9 ⇒ array_8T bool true  false true  false true  false false true
 539    | xA ⇒ array_8T bool true  false true  false true  false true  false
 540    | xB ⇒ array_8T bool true  false true  false true  false true  true
 541    | xC ⇒ array_8T bool true  false true  false true  true  false false
 542    | xD ⇒ array_8T bool true  false true  false true  true  false true
 543    | xE ⇒ array_8T bool true  false true  false true  true  true  false
 544    | xF ⇒ array_8T bool true  false true  false true  true  true  true ]
 545   | xB ⇒ match b8l p with
 546    [ x0 ⇒ array_8T bool true  false true  true  false false false false
 547    | x1 ⇒ array_8T bool true  false true  true  false false false true
 548    | x2 ⇒ array_8T bool true  false true  true  false false true  false
 549    | x3 ⇒ array_8T bool true  false true  true  false false true  true
 550    | x4 ⇒ array_8T bool true  false true  true  false true  false false
 551    | x5 ⇒ array_8T bool true  false true  true  false true  false true
 552    | x6 ⇒ array_8T bool true  false true  true  false true  true  false
 553    | x7 ⇒ array_8T bool true  false true  true  false true  true  true
 554    | x8 ⇒ array_8T bool true  false true  true  true  false false false
 555    | x9 ⇒ array_8T bool true  false true  true  true  false false true
 556    | xA ⇒ array_8T bool true  false true  true  true  false true  false
 557    | xB ⇒ array_8T bool true  false true  true  true  false true  true
 558    | xC ⇒ array_8T bool true  false true  true  true  true  false false
 559    | xD ⇒ array_8T bool true  false true  true  true  true  false true
 560    | xE ⇒ array_8T bool true  false true  true  true  true  true  false
 561    | xF ⇒ array_8T bool true  false true  true  true  true  true  true ]
 562   | xC ⇒ match b8l p with
 563    [ x0 ⇒ array_8T bool true  true  false false false false false false
 564    | x1 ⇒ array_8T bool true  true  false false false false false true
 565    | x2 ⇒ array_8T bool true  true  false false false false true  false
 566    | x3 ⇒ array_8T bool true  true  false false false false true  true
 567    | x4 ⇒ array_8T bool true  true  false false false true  false false
 568    | x5 ⇒ array_8T bool true  true  false false false true  false true
 569    | x6 ⇒ array_8T bool true  true  false false false true  true  false
 570    | x7 ⇒ array_8T bool true  true  false false false true  true  true
 571    | x8 ⇒ array_8T bool true  true  false false true  false false false
 572    | x9 ⇒ array_8T bool true  true  false false true  false false true
 573    | xA ⇒ array_8T bool true  true  false false true  false true  false
 574    | xB ⇒ array_8T bool true  true  false false true  false true  true
 575    | xC ⇒ array_8T bool true  true  false false true  true  false false
 576    | xD ⇒ array_8T bool true  true  false false true  true  false true
 577    | xE ⇒ array_8T bool true  true  false false true  true  true  false
 578    | xF ⇒ array_8T bool true  true  false false true  true  true  true ]
 579   | xD ⇒ match b8l p with
 580    [ x0 ⇒ array_8T bool true  true  false true  false false false false
 581    | x1 ⇒ array_8T bool true  true  false true  false false false true
 582    | x2 ⇒ array_8T bool true  true  false true  false false true  false
 583    | x3 ⇒ array_8T bool true  true  false true  false false true  true
 584    | x4 ⇒ array_8T bool true  true  false true  false true  false false
 585    | x5 ⇒ array_8T bool true  true  false true  false true  false true
 586    | x6 ⇒ array_8T bool true  true  false true  false true  true  false
 587    | x7 ⇒ array_8T bool true  true  false true  false true  true  true
 588    | x8 ⇒ array_8T bool true  true  false true  true  false false false
 589    | x9 ⇒ array_8T bool true  true  false true  true  false false true
 590    | xA ⇒ array_8T bool true  true  false true  true  false true  false
 591    | xB ⇒ array_8T bool true  true  false true  true  false true  true
 592    | xC ⇒ array_8T bool true  true  false true  true  true  false false
 593    | xD ⇒ array_8T bool true  true  false true  true  true  false true
 594    | xE ⇒ array_8T bool true  true  false true  true  true  true  false
 595    | xF ⇒ array_8T bool true  true  false true  true  true  true  true ]
 596   | xE ⇒ match b8l p with
 597    [ x0 ⇒ array_8T bool true  true  true  false false false false false
 598    | x1 ⇒ array_8T bool true  true  true  false false false false true
 599    | x2 ⇒ array_8T bool true  true  true  false false false true  false
 600    | x3 ⇒ array_8T bool true  true  true  false false false true  true
 601    | x4 ⇒ array_8T bool true  true  true  false false true  false false
 602    | x5 ⇒ array_8T bool true  true  true  false false true  false true
 603    | x6 ⇒ array_8T bool true  true  true  false false true  true  false
 604    | x7 ⇒ array_8T bool true  true  true  false false true  true  true
 605    | x8 ⇒ array_8T bool true  true  true  false true  false false false
 606    | x9 ⇒ array_8T bool true  true  true  false true  false false true
 607    | xA ⇒ array_8T bool true  true  true  false true  false true  false
 608    | xB ⇒ array_8T bool true  true  true  false true  false true  true
 609    | xC ⇒ array_8T bool true  true  true  false true  true  false false
 610    | xD ⇒ array_8T bool true  true  true  false true  true  false true
 611    | xE ⇒ array_8T bool true  true  true  false true  true  true  false
 612    | xF ⇒ array_8T bool true  true  true  false true  true  true  true ]
 613   | xF ⇒ match b8l p with
 614    [ x0 ⇒ array_8T bool true  true  true  true  false false false false
 615    | x1 ⇒ array_8T bool true  true  true  true  false false false true
 616    | x2 ⇒ array_8T bool true  true  true  true  false false true  false
 617    | x3 ⇒ array_8T bool true  true  true  true  false false true  true
 618    | x4 ⇒ array_8T bool true  true  true  true  false true  false false
 619    | x5 ⇒ array_8T bool true  true  true  true  false true  false true
 620    | x6 ⇒ array_8T bool true  true  true  true  false true  true  false
 621    | x7 ⇒ array_8T bool true  true  true  true  false true  true  true
 622    | x8 ⇒ array_8T bool true  true  true  true  true  false false false
 623    | x9 ⇒ array_8T bool true  true  true  true  true  false false true
 624    | xA ⇒ array_8T bool true  true  true  true  true  false true  false
 625    | xB ⇒ array_8T bool true  true  true  true  true  false true  true
 626    | xC ⇒ array_8T bool true  true  true  true  true  true  false false
 627    | xD ⇒ array_8T bool true  true  true  true  true  true  false true
 628    | xE ⇒ array_8T bool true  true  true  true  true  true  true  false
 629    | xF ⇒ array_8T bool true  true  true  true  true  true  true  true ]
 630   ].
 631
 632 (* ********************** *)
 633 (* TEOREMI/LEMMMI/ASSIOMI *)
 634 (* ********************** *)
 635
 636 (* check *)
 637 lemma ok_byte8_of_bits_bits_of_byte8 :
 638  ∀b.
 639   byte8_of_bits (bits_of_byte8 b) = b.
 640  intros;
 641  elim b; elim e; elim e1;
 642  reflexivity.
 643 qed.
 644
 645 (* check *)
 646 lemma ok_bits_of_byte8_byte8_of_bits :
 647  ∀b7,b6,b5,b4,b3,b2,b1,b0.
 648   bits_of_byte8 (byte8_of_bits (array_8T bool b7 b6 b5 b4 b3 b2 b1 b0))
 649   = array_8T bool b7 b6 b5 b4 b3 b2 b1 b0.
 650  intros;
 651  elim b0; elim b1; elim b2; elim b3; elim b4; elim b5; elim b6; elim b7;
 652  reflexivity.
 653 qed.