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