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 *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/aux_bases.ma".
24 include "freescale/byte8.ma".
26 (* **************************** *)
27 (* TIPI PER I MODULI DI MEMORIA *)
28 (* **************************** *)
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.
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 ].
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 ].
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 ].
48 (* **************** *)
49 (* TIPO ARRAY DA 16 *)
50 (* **************** *)
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 →
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 ].
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 ].
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 ].
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.
84 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
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
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.
95 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
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
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.
120 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
248 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ 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 ]
258 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ 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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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
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
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
331 (* ************************** *)
332 (* TIPO BYTE COME INSIEME BIT *)
333 (* ************************** *)
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 →
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 ].
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 ].
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 ].
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.
366 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
368 [ o0 ⇒ e00 | o1 ⇒ e01 | o2 ⇒ e02 | o3 ⇒ e03 | o4 ⇒ e04 | o5 ⇒ e05 | o6 ⇒ e06 | o7 ⇒ e07 ]].
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.
375 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
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
388 ndefinition byte8_of_bits ≝
391 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
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 ])))) ].
403 ndefinition bits_of_byte8 ≝
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 ]