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/byte8.ma".
28 include "freescale/nat.ma".
34 ninductive oct : Type ≝
45 ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
47 λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
49 [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
52 ΠP:oct → Set.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
54 λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
56 [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
58 ndefinition oct_rect :
59 ΠP:oct → Type.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
61 λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
63 [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
70 [ o0 ⇒ true | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
71 | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
73 [ o0 ⇒ false | o1 ⇒ true | o2 ⇒ false | o3 ⇒ false
74 | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
76 [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ true | o3 ⇒ false
77 | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
79 [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ true
80 | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
82 [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
83 | o4 ⇒ true | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
85 [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
86 | o4 ⇒ false | o5 ⇒ true | o6 ⇒ false | o7 ⇒ false ]
88 [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
89 | o4 ⇒ false | o5 ⇒ false | o6 ⇒ true | o7 ⇒ false ]
91 [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
92 | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ true ]
95 (* ottali → naturali *)
96 ndefinition nat_of_oct ≝
99 [ o0 ⇒ 0 | o1 ⇒ 1 | o2 ⇒ 2 | o3 ⇒ 3 | o4 ⇒ 4 | o5 ⇒ 5 | o6 ⇒ 6 | o7 ⇒ 7 ].
101 (* iteratore sugli ottali *)
102 ndefinition forall_oct ≝ λP.
103 P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
109 ninductive bitrigesim : Type ≝
143 ndefinition bitrigesim_ind :
144 ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
145 P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
146 P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
147 P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
148 λP:bitrigesim → Prop.
149 λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
150 λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
151 λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
152 λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
154 [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
155 | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
156 | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
157 | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
159 ndefinition bitrigesim_rec :
160 ΠP:bitrigesim → Set.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
161 P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
162 P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
163 P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
165 λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
166 λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
167 λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
168 λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
170 [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
171 | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
172 | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
173 | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
175 ndefinition bitrigesim_rect :
176 ΠP:bitrigesim → Type.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
177 P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
178 P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
179 P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
180 λP:bitrigesim → Type.
181 λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
182 λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
183 λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
184 λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
186 [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
187 | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
188 | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
189 | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
192 ndefinition eq_bitrig ≝
195 [ t00 ⇒ match t2 with
196 [ t00 ⇒ true | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
197 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
198 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
199 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
200 | t01 ⇒ match t2 with
201 [ t00 ⇒ false | t01 ⇒ true | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
202 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
203 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
204 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
205 | t02 ⇒ match t2 with
206 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ true | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
207 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
208 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
209 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
210 | t03 ⇒ match t2 with
211 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ true | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
212 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
213 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
214 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
215 | t04 ⇒ match t2 with
216 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ true | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
217 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
218 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
219 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
220 | t05 ⇒ match t2 with
221 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ true | t06 ⇒ false | t07 ⇒ false
222 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
223 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
224 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
225 | t06 ⇒ match t2 with
226 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ true | t07 ⇒ false
227 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
228 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
229 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
230 | t07 ⇒ match t2 with
231 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ true
232 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
233 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
234 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
235 | t08 ⇒ match t2 with
236 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
237 | t08 ⇒ true | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
238 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
239 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
240 | t09 ⇒ match t2 with
241 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
242 | t08 ⇒ false | t09 ⇒ true | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
243 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
244 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
245 | t0A ⇒ match t2 with
246 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
247 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ true | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
248 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
249 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
250 | t0B ⇒ match t2 with
251 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
252 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ true | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
253 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
254 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
255 | t0C ⇒ match t2 with
256 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
257 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ true | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
258 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
259 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
260 | t0D ⇒ match t2 with
261 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
262 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ true | t0E ⇒ false | t0F ⇒ false
263 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
264 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
265 | t0E ⇒ match t2 with
266 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
267 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ true | t0F ⇒ false
268 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
269 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
270 | t0F ⇒ match t2 with
271 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
272 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ true
273 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
274 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
275 | t10 ⇒ match t2 with
276 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
277 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
278 | t10 ⇒ true | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
279 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
280 | t11 ⇒ match t2 with
281 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
282 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
283 | t10 ⇒ false | t11 ⇒ true | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
284 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
285 | t12 ⇒ match t2 with
286 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
287 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
288 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ true | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
289 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
290 | t13 ⇒ match t2 with
291 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
292 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
293 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ true | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
294 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
295 | t14 ⇒ match t2 with
296 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
297 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
298 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ true | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
299 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
300 | t15 ⇒ match t2 with
301 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
302 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
303 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ true | t16 ⇒ false | t17 ⇒ false
304 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
305 | t16 ⇒ match t2 with
306 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
307 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
308 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ true | t17 ⇒ false
309 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
310 | t17 ⇒ match t2 with
311 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
312 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
313 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ true
314 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
315 | t18 ⇒ match t2 with
316 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
317 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
318 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
319 | t18 ⇒ true | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
320 | t19 ⇒ match t2 with
321 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
322 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
323 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
324 | t18 ⇒ false | t19 ⇒ true | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
325 | t1A ⇒ match t2 with
326 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
327 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
328 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
329 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ true | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
330 | t1B ⇒ match t2 with
331 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
332 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
333 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
334 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ true | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
335 | t1C ⇒ match t2 with
336 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
337 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
338 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
339 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ true | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
340 | t1D ⇒ match t2 with
341 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
342 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
343 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
344 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ true | t1E ⇒ false | t1F ⇒ false ]
345 | t1E ⇒ match t2 with
346 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
347 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
348 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
349 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ true | t1F ⇒ false ]
350 | t1F ⇒ match t2 with
351 [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
352 | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
353 | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
354 | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ true ]
357 (* bitrigesimali → naturali *)
358 ndefinition nat_of_bitrigesim ≝
361 [ t00 ⇒ 0 | t01 ⇒ 1 | t02 ⇒ 2 | t03 ⇒ 3 | t04 ⇒ 4 | t05 ⇒ 5 | t06 ⇒ 6 | t07 ⇒ 7
362 | t08 ⇒ 8 | t09 ⇒ 9 | t0A ⇒ 10 | t0B ⇒ 11 | t0C ⇒ 12 | t0D ⇒ 13 | t0E ⇒ 14 | t0F ⇒ 15
363 | t10 ⇒ 16 | t11 ⇒ 17 | t12 ⇒ 18 | t13 ⇒ 19 | t14 ⇒ 20 | t15 ⇒ 21 | t16 ⇒ 22 | t17 ⇒ 23
364 | t18 ⇒ 24 | t19 ⇒ 25 | t1A ⇒ 26 | t1B ⇒ 27 | t1C ⇒ 28 | t1D ⇒ 29 | t1E ⇒ 30 | t1F ⇒ 31 ].
366 ndefinition byte8_of_bitrigesim ≝
369 [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
370 | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
371 | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
372 | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
373 | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
374 | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
375 | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
376 | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉 ].
378 (* iteratore sui bitrigesimali *)
379 ndefinition forall_bitrigesim ≝ λP.
380 P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
381 P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
382 P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
383 P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.