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