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