1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/aux_bases.ma".
28 include "freescale/byte8.ma".
30 (* **************************** *)
31 (* TIPI PER I MODULI DI MEMORIA *)
32 (* **************************** *)
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.
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 ].
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 ].
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 ].
52 (* **************** *)
53 (* TIPO ARRAY DA 16 *)
54 (* **************** *)
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 →
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 ].
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 ].
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 ].
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.
88 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
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
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.
99 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
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
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.
124 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
252 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ 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 ]
262 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ 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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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
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
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
335 (* ************************** *)
336 (* TIPO BYTE COME INSIEME BIT *)
337 (* ************************** *)
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 →
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 ].
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 ].
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 ].
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.
370 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
372 [ o0 ⇒ e00 | o1 ⇒ e01 | o2 ⇒ e02 | o3 ⇒ e03 | o4 ⇒ e04 | o5 ⇒ e05 | o6 ⇒ e06 | o7 ⇒ e07 ]].
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.
379 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
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
392 ndefinition byte8_of_bits ≝
395 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
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 ])))) ].
407 ndefinition bits_of_byte8 ≝
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 ]