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