helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/byte8.ma".
  24 include "freescale/nat.ma".
  25
  26 (* ****** *)
  27 (* OTTALI *)
  28 (* ****** *)
  29
  30 ninductive oct : Type ≝
  31   o0: oct
  32 | o1: oct
  33 | o2: oct
  34 | o3: oct
  35 | o4: oct
  36 | o5: oct
  37 | o6: oct
  38 | o7: oct.
  39
  40 (*ndefinition oct_ind :
  41  ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
  42 λP:oct → Prop.
  43 λ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.
  44  match n with
  45   [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
  46
  47 ndefinition oct_rec :
  48  ΠP:oct → Set.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
  49 λP:oct → Set.
  50 λ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.
  51  match n with
  52   [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
  53
  54 ndefinition oct_rect :
  55  ΠP:oct → Type.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
  56 λP:oct → Type.
  57 λ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.
  58  match n with
  59   [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
  60 *)
  61 (* operatore = *)
  62 ndefinition eq_oct ≝
  63 λn1,n2:oct.
  64  match n1 with
  65   [ o0 ⇒ match n2 with
  66    [ o0 ⇒ true  | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
  67    | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
  68   | o1 ⇒ match n2 with
  69    [ o0 ⇒ false | o1 ⇒ true  | o2 ⇒ false | o3 ⇒ false
  70    | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
  71   | o2 ⇒ match n2 with
  72    [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ true  | o3 ⇒ false
  73    | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
  74   | o3 ⇒ match n2 with
  75    [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ true
  76    | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
  77   | o4 ⇒ match n2 with
  78    [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
  79    | o4 ⇒ true  | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
  80   | o5 ⇒ match n2 with
  81    [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
  82    | o4 ⇒ false | o5 ⇒ true  | o6 ⇒ false | o7 ⇒ false ]
  83   | o6 ⇒ match n2 with
  84    [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
  85    | o4 ⇒ false | o5 ⇒ false | o6 ⇒ true  | o7 ⇒ false ]
  86   | o7 ⇒ match n2 with
  87    [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
  88    | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ true  ]
  89   ].
  90
  91 (* ottali → naturali *)
  92 ndefinition nat_of_oct ≝
  93 λn:oct.
  94  match n with
  95   [ o0 ⇒ 0 | o1 ⇒ 1 | o2 ⇒ 2  | o3 ⇒ 3  | o4 ⇒ 4  | o5 ⇒ 5  | o6 ⇒ 6  | o7 ⇒ 7 ].
  96
  97 (* iteratore sugli ottali *)
  98 ndefinition forall_oct ≝ λP.
  99  P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
 100
 101 (* ************* *)
 102 (* BITRIGESIMALI *)
 103 (* ************* *)
 104
 105 ninductive bitrigesim : Type ≝
 106   t00: bitrigesim
 107 | t01: bitrigesim
 108 | t02: bitrigesim
 109 | t03: bitrigesim
 110 | t04: bitrigesim
 111 | t05: bitrigesim
 112 | t06: bitrigesim
 113 | t07: bitrigesim
 114 | t08: bitrigesim
 115 | t09: bitrigesim
 116 | t0A: bitrigesim
 117 | t0B: bitrigesim
 118 | t0C: bitrigesim
 119 | t0D: bitrigesim
 120 | t0E: bitrigesim
 121 | t0F: bitrigesim
 122 | t10: bitrigesim
 123 | t11: bitrigesim
 124 | t12: bitrigesim
 125 | t13: bitrigesim
 126 | t14: bitrigesim
 127 | t15: bitrigesim
 128 | t16: bitrigesim
 129 | t17: bitrigesim
 130 | t18: bitrigesim
 131 | t19: bitrigesim
 132 | t1A: bitrigesim
 133 | t1B: bitrigesim
 134 | t1C: bitrigesim
 135 | t1D: bitrigesim
 136 | t1E: bitrigesim
 137 | t1F: bitrigesim.
 138
 139 (*ndefinition bitrigesim_ind :
 140  ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
 141                       P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
 142                       P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
 143                       P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
 144 λP:bitrigesim → Prop.
 145 λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
 146 λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
 147 λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
 148 λ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.
 149  match t with
 150   [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
 151   | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
 152   | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
 153   | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
 154
 155 ndefinition bitrigesim_rec :
 156  ΠP:bitrigesim → Set.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
 157                      P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
 158                      P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
 159                      P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
 160 λP:bitrigesim → Set.
 161 λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
 162 λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
 163 λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
 164 λ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.
 165  match t with
 166   [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
 167   | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
 168   | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
 169   | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
 170
 171 ndefinition bitrigesim_rect :
 172  ΠP:bitrigesim → Type.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
 173                       P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
 174                       P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
 175                       P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
 176 λP:bitrigesim → Type.
 177 λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
 178 λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
 179 λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
 180 λ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.
 181  match t with
 182   [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
 183   | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
 184   | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
 185   | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
 186 *)
 187 (* operatore = *)
 188 ndefinition eq_bitrig ≝
 189 λt1,t2:bitrigesim.
 190  match t1 with
 191   [ t00 ⇒ match t2 with
 192    [ t00 ⇒ true  | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 193    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 194    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 195    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 196   | t01 ⇒ match t2 with
 197    [ t00 ⇒ false | t01 ⇒ true  | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 198    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 199    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 200    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 201   | t02 ⇒ match t2 with
 202    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ true  | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 203    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 204    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 205    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 206   | t03 ⇒ match t2 with
 207    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ true  | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 208    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 209    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 210    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 211   | t04 ⇒ match t2 with
 212    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ true  | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 213    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 214    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 215    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 216   | t05 ⇒ match t2 with
 217    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ true  | t06 ⇒ false | t07 ⇒ false
 218    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 219    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 220    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 221   | t06 ⇒ match t2 with
 222    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ true  | t07 ⇒ false
 223    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 224    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 225    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 226   | t07 ⇒ match t2 with
 227    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ true
 228    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 229    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 230    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 231   | t08 ⇒ match t2 with
 232    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 233    | t08 ⇒ true  | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 234    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 235    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 236   | t09 ⇒ match t2 with
 237    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 238    | t08 ⇒ false | t09 ⇒ true  | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 239    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 240    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 241   | t0A ⇒ match t2 with
 242    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 243    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ true  | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 244    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 245    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 246   | t0B ⇒ match t2 with
 247    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 248    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ true  | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 249    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 250    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 251   | t0C ⇒ match t2 with
 252    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 253    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ true  | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 254    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 255    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 256   | t0D ⇒ match t2 with
 257    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 258    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ true  | t0E ⇒ false | t0F ⇒ false
 259    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 260    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 261   | t0E ⇒ match t2 with
 262    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 263    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ true  | t0F ⇒ false
 264    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 265    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 266   | t0F ⇒ match t2 with
 267    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 268    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ true
 269    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 270    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 271   | t10 ⇒ match t2 with
 272    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 273    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 274    | t10 ⇒ true  | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 275    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 276   | t11 ⇒ match t2 with
 277    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 278    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 279    | t10 ⇒ false | t11 ⇒ true  | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 280    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 281   | t12 ⇒ match t2 with
 282    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 283    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 284    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ true  | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 285    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 286   | t13 ⇒ match t2 with
 287    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 288    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 289    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ true  | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 290    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 291   | t14 ⇒ match t2 with
 292    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 293    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 294    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ true  | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 295    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 296   | t15 ⇒ match t2 with
 297    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 298    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 299    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ true  | t16 ⇒ false | t17 ⇒ false
 300    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 301   | t16 ⇒ match t2 with
 302    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 303    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 304    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ true  | t17 ⇒ false
 305    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 306   | t17 ⇒ match t2 with
 307    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 308    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 309    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ true
 310    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 311   | t18 ⇒ match t2 with
 312    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 313    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 314    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 315    | t18 ⇒ true  | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 316   | t19 ⇒ match t2 with
 317    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 318    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 319    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 320    | t18 ⇒ false | t19 ⇒ true  | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 321   | t1A ⇒ match t2 with
 322    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 323    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 324    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 325    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ true  | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 326   | t1B ⇒ match t2 with
 327    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 328    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 329    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 330    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ true  | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 331   | t1C ⇒ match t2 with
 332    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 333    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 334    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 335    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ true  | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
 336   | t1D ⇒ match t2 with
 337    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 338    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 339    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 340    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ true  | t1E ⇒ false | t1F ⇒ false ]
 341   | t1E ⇒ match t2 with
 342    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 343    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 344    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 345    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ true  | t1F ⇒ false ]
 346   | t1F ⇒ match t2 with
 347    [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
 348    | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
 349    | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
 350    | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ true  ]
 351   ].
 352
 353 (* bitrigesimali → naturali *)
 354 ndefinition nat_of_bitrigesim ≝
 355 λt:bitrigesim.
 356  match t with
 357   [ t00 ⇒ 0  | t01 ⇒ 1  | t02 ⇒ 2  | t03 ⇒ 3  | t04 ⇒ 4  | t05 ⇒ 5  | t06 ⇒ 6  | t07 ⇒ 7
 358   | t08 ⇒ 8  | t09 ⇒ 9  | t0A ⇒ 10 | t0B ⇒ 11 | t0C ⇒ 12 | t0D ⇒ 13 | t0E ⇒ 14 | t0F ⇒ 15
 359   | t10 ⇒ 16 | t11 ⇒ 17 | t12 ⇒ 18 | t13 ⇒ 19 | t14 ⇒ 20 | t15 ⇒ 21 | t16 ⇒ 22 | t17 ⇒ 23
 360   | t18 ⇒ 24 | t19 ⇒ 25 | t1A ⇒ 26 | t1B ⇒ 27 | t1C ⇒ 28 | t1D ⇒ 29 | t1E ⇒ 30 | t1F ⇒ 31 ].
 361
 362 ndefinition byte8_of_bitrigesim ≝
 363 λt:bitrigesim.
 364  match t with
 365   [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
 366   | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
 367   | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
 368   | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
 369   | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
 370   | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
 371   | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
 372   | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉 ].
 373
 374 (* iteratore sui bitrigesimali *)
 375 ndefinition forall_bitrigesim ≝ λP.
 376  P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
 377  P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
 378  P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
 379  P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.