matita/matita/contribs/ng_assembly2/num/bitrigesim.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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/comp.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ************* *)
  27 (* BITRIGESIMALI *)
  28 (* ************* *)
  29
  30 ninductive bitrigesim : Type ≝
  31   t00: bitrigesim
  32 | t01: bitrigesim
  33 | t02: bitrigesim
  34 | t03: bitrigesim
  35 | t04: bitrigesim
  36 | t05: bitrigesim
  37 | t06: bitrigesim
  38 | t07: bitrigesim
  39 | t08: bitrigesim
  40 | t09: bitrigesim
  41 | t0A: bitrigesim
  42 | t0B: bitrigesim
  43 | t0C: bitrigesim
  44 | t0D: bitrigesim
  45 | t0E: bitrigesim
  46 | t0F: bitrigesim
  47 | t10: bitrigesim
  48 | t11: bitrigesim
  49 | t12: bitrigesim
  50 | t13: bitrigesim
  51 | t14: bitrigesim
  52 | t15: bitrigesim
  53 | t16: bitrigesim
  54 | t17: bitrigesim
  55 | t18: bitrigesim
  56 | t19: bitrigesim
  57 | t1A: bitrigesim
  58 | t1B: bitrigesim
  59 | t1C: bitrigesim
  60 | t1D: bitrigesim
  61 | t1E: bitrigesim
  62 | t1F: bitrigesim.
  63
  64 (* operatore = *)
  65 ndefinition eq_bit ≝
  66 λt1,t2:bitrigesim.
  67  match t1 with
  68   [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
  69   | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
  70   | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
  71   | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
  72   | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
  73   | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
  74   | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
  75   | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
  76   | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
  77   | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
  78   | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
  79   | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
  80   | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
  81   | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
  82   | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
  83   | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
  84   ].
  85
  86 (* iteratore sui bitrigesimali *)
  87 ndefinition forall_bit ≝ λP.
  88  P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
  89  P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
  90  P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
  91  P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.
  92
  93 (* operatore and *)
  94 ndefinition and_bit ≝
  95 λe1,e2.match e1 with
  96  [ t00 ⇒ match e2 with
  97   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t00 | t07 ⇒ t00
  98   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t00 | t0B ⇒ t00 | t0C ⇒ t00 | t0D ⇒ t00 | t0E ⇒ t00 | t0F ⇒ t00
  99   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t00 | t13 ⇒ t00 | t14 ⇒ t00 | t15 ⇒ t00 | t16 ⇒ t00 | t17 ⇒ t00
 100   | t18 ⇒ t00 | t19 ⇒ t00 | t1A ⇒ t00 | t1B ⇒ t00 | t1C ⇒ t00 | t1D ⇒ t00 | t1E ⇒ t00 | t1F ⇒ t00 ]
 101  | t01 ⇒ match e2 with
 102   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t00 | t07 ⇒ t01
 103   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t00 | t0B ⇒ t01 | t0C ⇒ t00 | t0D ⇒ t01 | t0E ⇒ t00 | t0F ⇒ t01
 104   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t00 | t13 ⇒ t01 | t14 ⇒ t00 | t15 ⇒ t01 | t16 ⇒ t00 | t17 ⇒ t01
 105   | t18 ⇒ t00 | t19 ⇒ t01 | t1A ⇒ t00 | t1B ⇒ t01 | t1C ⇒ t00 | t1D ⇒ t01 | t1E ⇒ t00 | t1F ⇒ t01 ]
 106  | t02 ⇒ match e2 with
 107   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t02 | t07 ⇒ t02
 108   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t02 | t0B ⇒ t02 | t0C ⇒ t00 | t0D ⇒ t00 | t0E ⇒ t02 | t0F ⇒ t02
 109   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t02 | t13 ⇒ t02 | t14 ⇒ t00 | t15 ⇒ t00 | t16 ⇒ t02 | t17 ⇒ t02
 110   | t18 ⇒ t00 | t19 ⇒ t00 | t1A ⇒ t02 | t1B ⇒ t02 | t1C ⇒ t00 | t1D ⇒ t00 | t1E ⇒ t02 | t1F ⇒ t02 ]
 111  | t03 ⇒ match e2 with
 112   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t02 | t07 ⇒ t03
 113   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t02 | t0B ⇒ t03 | t0C ⇒ t00 | t0D ⇒ t01 | t0E ⇒ t02 | t0F ⇒ t03
 114   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t02 | t13 ⇒ t03 | t14 ⇒ t00 | t15 ⇒ t01 | t16 ⇒ t02 | t17 ⇒ t03
 115   | t18 ⇒ t00 | t19 ⇒ t01 | t1A ⇒ t02 | t1B ⇒ t03 | t1C ⇒ t00 | t1D ⇒ t01 | t1E ⇒ t02 | t1F ⇒ t03 ]
 116  | t04 ⇒ match e2 with
 117   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t04 | t07 ⇒ t04
 118   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t00 | t0B ⇒ t00 | t0C ⇒ t04 | t0D ⇒ t04 | t0E ⇒ t04 | t0F ⇒ t04
 119   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t00 | t13 ⇒ t00 | t14 ⇒ t04 | t15 ⇒ t04 | t16 ⇒ t04 | t17 ⇒ t04
 120   | t18 ⇒ t00 | t19 ⇒ t00 | t1A ⇒ t00 | t1B ⇒ t00 | t1C ⇒ t04 | t1D ⇒ t04 | t1E ⇒ t04 | t1F ⇒ t04 ]
 121  | t05 ⇒ match e2 with
 122   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t04 | t07 ⇒ t05
 123   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t00 | t0B ⇒ t01 | t0C ⇒ t04 | t0D ⇒ t05 | t0E ⇒ t04 | t0F ⇒ t05
 124   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t00 | t13 ⇒ t01 | t14 ⇒ t04 | t15 ⇒ t05 | t16 ⇒ t04 | t17 ⇒ t05
 125   | t18 ⇒ t00 | t19 ⇒ t01 | t1A ⇒ t00 | t1B ⇒ t01 | t1C ⇒ t04 | t1D ⇒ t05 | t1E ⇒ t04 | t1F ⇒ t05 ]
 126  | t06 ⇒ match e2 with
 127   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t06 | t07 ⇒ t06
 128   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t02 | t0B ⇒ t02 | t0C ⇒ t04 | t0D ⇒ t04 | t0E ⇒ t06 | t0F ⇒ t06
 129   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t02 | t13 ⇒ t02 | t14 ⇒ t04 | t15 ⇒ t04 | t16 ⇒ t06 | t17 ⇒ t06
 130   | t18 ⇒ t00 | t19 ⇒ t00 | t1A ⇒ t02 | t1B ⇒ t02 | t1C ⇒ t04 | t1D ⇒ t04 | t1E ⇒ t06 | t1F ⇒ t06 ]
 131  | t07 ⇒ match e2 with
 132   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t06 | t07 ⇒ t07
 133   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t02 | t0B ⇒ t03 | t0C ⇒ t04 | t0D ⇒ t05 | t0E ⇒ t06 | t0F ⇒ t07
 134   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t02 | t13 ⇒ t03 | t14 ⇒ t04 | t15 ⇒ t05 | t16 ⇒ t06 | t17 ⇒ t07
 135   | t18 ⇒ t00 | t19 ⇒ t01 | t1A ⇒ t02 | t1B ⇒ t03 | t1C ⇒ t04 | t1D ⇒ t05 | t1E ⇒ t06 | t1F ⇒ t07 ]
 136  | t08 ⇒ match e2 with
 137   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t00 | t07 ⇒ t00
 138   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t08 | t0B ⇒ t08 | t0C ⇒ t08 | t0D ⇒ t08 | t0E ⇒ t08 | t0F ⇒ t08
 139   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t00 | t13 ⇒ t00 | t14 ⇒ t00 | t15 ⇒ t00 | t16 ⇒ t00 | t17 ⇒ t00
 140   | t18 ⇒ t08 | t19 ⇒ t08 | t1A ⇒ t08 | t1B ⇒ t08 | t1C ⇒ t08 | t1D ⇒ t08 | t1E ⇒ t08 | t1F ⇒ t08 ]
 141  | t09 ⇒ match e2 with
 142   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t00 | t07 ⇒ t01
 143   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t08 | t0B ⇒ t09 | t0C ⇒ t08 | t0D ⇒ t09 | t0E ⇒ t08 | t0F ⇒ t09
 144   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t00 | t13 ⇒ t01 | t14 ⇒ t00 | t15 ⇒ t01 | t16 ⇒ t00 | t17 ⇒ t01
 145   | t18 ⇒ t08 | t19 ⇒ t09 | t1A ⇒ t08 | t1B ⇒ t09 | t1C ⇒ t08 | t1D ⇒ t09 | t1E ⇒ t08 | t1F ⇒ t09 ]
 146  | t0A ⇒ match e2 with
 147   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t02 | t07 ⇒ t02
 148   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t0A | t0B ⇒ t0A | t0C ⇒ t08 | t0D ⇒ t08 | t0E ⇒ t0A | t0F ⇒ t0A
 149   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t02 | t13 ⇒ t02 | t14 ⇒ t00 | t15 ⇒ t00 | t16 ⇒ t02 | t17 ⇒ t02
 150   | t18 ⇒ t08 | t19 ⇒ t08 | t1A ⇒ t0A | t1B ⇒ t0A | t1C ⇒ t08 | t1D ⇒ t08 | t1E ⇒ t0A | t1F ⇒ t0A ]
 151  | t0B ⇒ match e2 with
 152   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t02 | t07 ⇒ t03
 153   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t08 | t0D ⇒ t09 | t0E ⇒ t0A | t0F ⇒ t0B
 154   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t02 | t13 ⇒ t03 | t14 ⇒ t00 | t15 ⇒ t01 | t16 ⇒ t02 | t17 ⇒ t03
 155   | t18 ⇒ t08 | t19 ⇒ t09 | t1A ⇒ t0A | t1B ⇒ t0B | t1C ⇒ t08 | t1D ⇒ t09 | t1E ⇒ t0A | t1F ⇒ t0B ]
 156  | t0C ⇒ match e2 with
 157   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t04 | t07 ⇒ t04
 158   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t08 | t0B ⇒ t08 | t0C ⇒ t0C | t0D ⇒ t0C | t0E ⇒ t0C | t0F ⇒ t0C
 159   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t00 | t13 ⇒ t00 | t14 ⇒ t04 | t15 ⇒ t04 | t16 ⇒ t04 | t17 ⇒ t04
 160   | t18 ⇒ t08 | t19 ⇒ t08 | t1A ⇒ t08 | t1B ⇒ t08 | t1C ⇒ t0C | t1D ⇒ t0C | t1E ⇒ t0C | t1F ⇒ t0C ]
 161  | t0D ⇒ match e2 with
 162   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t04 | t07 ⇒ t05
 163   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t08 | t0B ⇒ t09 | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0C | t0F ⇒ t0D
 164   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t00 | t13 ⇒ t01 | t14 ⇒ t04 | t15 ⇒ t05 | t16 ⇒ t04 | t17 ⇒ t05
 165   | t18 ⇒ t08 | t19 ⇒ t09 | t1A ⇒ t08 | t1B ⇒ t09 | t1C ⇒ t0C | t1D ⇒ t0D | t1E ⇒ t0C | t1F ⇒ t0D ]
 166  | t0E ⇒ match e2 with
 167   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t06 | t07 ⇒ t06
 168   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t0A | t0B ⇒ t0A | t0C ⇒ t0C | t0D ⇒ t0C | t0E ⇒ t0E | t0F ⇒ t0E
 169   | t10 ⇒ t00 | t11 ⇒ t00 | t12 ⇒ t02 | t13 ⇒ t02 | t14 ⇒ t04 | t15 ⇒ t04 | t16 ⇒ t06 | t17 ⇒ t06
 170   | t18 ⇒ t08 | t19 ⇒ t08 | t1A ⇒ t0A | t1B ⇒ t0A | t1C ⇒ t0C | t1D ⇒ t0C | t1E ⇒ t0E | t1F ⇒ t0E ]
 171  | t0F ⇒ match e2 with
 172   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t06 | t07 ⇒ t07
 173   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0E | t0F ⇒ t0F
 174   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t02 | t13 ⇒ t03 | t14 ⇒ t04 | t15 ⇒ t05 | t16 ⇒ t06 | t17 ⇒ t07
 175   | t18 ⇒ t08 | t19 ⇒ t09 | t1A ⇒ t0A | t1B ⇒ t0B | t1C ⇒ t0C | t1D ⇒ t0D | t1E ⇒ t0E | t1F ⇒ t0F ]
 176  | t10 ⇒ match e2 with
 177   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t00 | t07 ⇒ t00
 178   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t00 | t0B ⇒ t00 | t0C ⇒ t00 | t0D ⇒ t00 | t0E ⇒ t00 | t0F ⇒ t00
 179   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t10 | t13 ⇒ t10 | t14 ⇒ t10 | t15 ⇒ t10 | t16 ⇒ t10 | t17 ⇒ t10
 180   | t18 ⇒ t10 | t19 ⇒ t10 | t1A ⇒ t10 | t1B ⇒ t10 | t1C ⇒ t10 | t1D ⇒ t10 | t1E ⇒ t10 | t1F ⇒ t10 ]
 181  | t11 ⇒ match e2 with
 182   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t00 | t07 ⇒ t01
 183   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t00 | t0B ⇒ t01 | t0C ⇒ t00 | t0D ⇒ t01 | t0E ⇒ t00 | t0F ⇒ t01
 184   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t10 | t13 ⇒ t11 | t14 ⇒ t10 | t15 ⇒ t11 | t16 ⇒ t10 | t17 ⇒ t11
 185   | t18 ⇒ t10 | t19 ⇒ t11 | t1A ⇒ t10 | t1B ⇒ t11 | t1C ⇒ t10 | t1D ⇒ t11 | t1E ⇒ t10 | t1F ⇒ t11 ]
 186  | t12 ⇒ match e2 with
 187   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t02 | t07 ⇒ t02
 188   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t02 | t0B ⇒ t02 | t0C ⇒ t00 | t0D ⇒ t00 | t0E ⇒ t02 | t0F ⇒ t02
 189   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t12 | t13 ⇒ t12 | t14 ⇒ t10 | t15 ⇒ t10 | t16 ⇒ t12 | t17 ⇒ t12
 190   | t18 ⇒ t10 | t19 ⇒ t10 | t1A ⇒ t12 | t1B ⇒ t12 | t1C ⇒ t10 | t1D ⇒ t10 | t1E ⇒ t12 | t1F ⇒ t12 ]
 191  | t13 ⇒ match e2 with
 192   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t02 | t07 ⇒ t03
 193   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t02 | t0B ⇒ t03 | t0C ⇒ t00 | t0D ⇒ t01 | t0E ⇒ t02 | t0F ⇒ t03
 194   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t10 | t15 ⇒ t11 | t16 ⇒ t12 | t17 ⇒ t13
 195   | t18 ⇒ t10 | t19 ⇒ t11 | t1A ⇒ t12 | t1B ⇒ t13 | t1C ⇒ t10 | t1D ⇒ t11 | t1E ⇒ t12 | t1F ⇒ t13 ]
 196  | t14 ⇒ match e2 with
 197   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t04 | t07 ⇒ t04
 198   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t00 | t0B ⇒ t00 | t0C ⇒ t04 | t0D ⇒ t04 | t0E ⇒ t04 | t0F ⇒ t04
 199   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t10 | t13 ⇒ t10 | t14 ⇒ t14 | t15 ⇒ t14 | t16 ⇒ t14 | t17 ⇒ t14
 200   | t18 ⇒ t10 | t19 ⇒ t10 | t1A ⇒ t10 | t1B ⇒ t10 | t1C ⇒ t14 | t1D ⇒ t14 | t1E ⇒ t14 | t1F ⇒ t14 ]
 201  | t15 ⇒ match e2 with
 202   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t04 | t07 ⇒ t05
 203   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t00 | t0B ⇒ t01 | t0C ⇒ t04 | t0D ⇒ t05 | t0E ⇒ t04 | t0F ⇒ t05
 204   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t10 | t13 ⇒ t11 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t14 | t17 ⇒ t15
 205   | t18 ⇒ t10 | t19 ⇒ t11 | t1A ⇒ t10 | t1B ⇒ t11 | t1C ⇒ t14 | t1D ⇒ t15 | t1E ⇒ t14 | t1F ⇒ t15 ]
 206  | t16 ⇒ match e2 with
 207   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t06 | t07 ⇒ t06
 208   | t08 ⇒ t00 | t09 ⇒ t00 | t0A ⇒ t02 | t0B ⇒ t02 | t0C ⇒ t04 | t0D ⇒ t04 | t0E ⇒ t06 | t0F ⇒ t06
 209   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t12 | t13 ⇒ t12 | t14 ⇒ t14 | t15 ⇒ t14 | t16 ⇒ t16 | t17 ⇒ t16
 210   | t18 ⇒ t10 | t19 ⇒ t10 | t1A ⇒ t12 | t1B ⇒ t12 | t1C ⇒ t14 | t1D ⇒ t14 | t1E ⇒ t16 | t1F ⇒ t16 ]
 211  | t17 ⇒ match e2 with
 212   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t06 | t07 ⇒ t07
 213   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t02 | t0B ⇒ t03 | t0C ⇒ t04 | t0D ⇒ t05 | t0E ⇒ t06 | t0F ⇒ t07
 214   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t16 | t17 ⇒ t17
 215   | t18 ⇒ t10 | t19 ⇒ t11 | t1A ⇒ t12 | t1B ⇒ t13 | t1C ⇒ t14 | t1D ⇒ t15 | t1E ⇒ t16 | t1F ⇒ t17 ]
 216  | t18 ⇒ match e2 with
 217   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t00 | t07 ⇒ t00
 218   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t08 | t0B ⇒ t08 | t0C ⇒ t08 | t0D ⇒ t08 | t0E ⇒ t08 | t0F ⇒ t08
 219   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t10 | t13 ⇒ t10 | t14 ⇒ t10 | t15 ⇒ t10 | t16 ⇒ t10 | t17 ⇒ t10
 220   | t18 ⇒ t18 | t19 ⇒ t18 | t1A ⇒ t18 | t1B ⇒ t18 | t1C ⇒ t18 | t1D ⇒ t18 | t1E ⇒ t18 | t1F ⇒ t18 ]
 221  | t19 ⇒ match e2 with
 222   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t00 | t07 ⇒ t01
 223   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t08 | t0B ⇒ t09 | t0C ⇒ t08 | t0D ⇒ t09 | t0E ⇒ t08 | t0F ⇒ t09
 224   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t10 | t13 ⇒ t11 | t14 ⇒ t10 | t15 ⇒ t11 | t16 ⇒ t10 | t17 ⇒ t11
 225   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t18 | t1B ⇒ t19 | t1C ⇒ t18 | t1D ⇒ t19 | t1E ⇒ t18 | t1F ⇒ t19 ]
 226  | t1A ⇒ match e2 with
 227   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t00 | t05 ⇒ t00 | t06 ⇒ t02 | t07 ⇒ t02
 228   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t0A | t0B ⇒ t0A | t0C ⇒ t08 | t0D ⇒ t08 | t0E ⇒ t0A | t0F ⇒ t0A
 229   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t12 | t13 ⇒ t12 | t14 ⇒ t10 | t15 ⇒ t10 | t16 ⇒ t12 | t17 ⇒ t12
 230   | t18 ⇒ t18 | t19 ⇒ t18 | t1A ⇒ t1A | t1B ⇒ t1A | t1C ⇒ t18 | t1D ⇒ t18 | t1E ⇒ t1A | t1F ⇒ t1A ]
 231  | t1B ⇒ match e2 with
 232   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t02 | t07 ⇒ t03
 233   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t08 | t0D ⇒ t09 | t0E ⇒ t0A | t0F ⇒ t0B
 234   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t10 | t15 ⇒ t11 | t16 ⇒ t12 | t17 ⇒ t13
 235   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t18 | t1D ⇒ t19 | t1E ⇒ t1A | t1F ⇒ t1B ]
 236  | t1C ⇒ match e2 with
 237   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t00 | t03 ⇒ t00 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t04 | t07 ⇒ t04
 238   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t08 | t0B ⇒ t08 | t0C ⇒ t0C | t0D ⇒ t0C | t0E ⇒ t0C | t0F ⇒ t0C
 239   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t10 | t13 ⇒ t10 | t14 ⇒ t14 | t15 ⇒ t14 | t16 ⇒ t14 | t17 ⇒ t14
 240   | t18 ⇒ t18 | t19 ⇒ t18 | t1A ⇒ t18 | t1B ⇒ t18 | t1C ⇒ t1C | t1D ⇒ t1C | t1E ⇒ t1C | t1F ⇒ t1C ]
 241  | t1D ⇒ match e2 with
 242   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t04 | t07 ⇒ t05
 243   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t08 | t0B ⇒ t09 | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0C | t0F ⇒ t0D
 244   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t10 | t13 ⇒ t11 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t14 | t17 ⇒ t15
 245   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t18 | t1B ⇒ t19 | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1C | t1F ⇒ t1D ]
 246  | t1E ⇒ match e2 with
 247   [ t00 ⇒ t00 | t01 ⇒ t00 | t02 ⇒ t02 | t03 ⇒ t02 | t04 ⇒ t04 | t05 ⇒ t04 | t06 ⇒ t06 | t07 ⇒ t06
 248   | t08 ⇒ t08 | t09 ⇒ t08 | t0A ⇒ t0A | t0B ⇒ t0A | t0C ⇒ t0C | t0D ⇒ t0C | t0E ⇒ t0E | t0F ⇒ t0E
 249   | t10 ⇒ t10 | t11 ⇒ t10 | t12 ⇒ t12 | t13 ⇒ t12 | t14 ⇒ t14 | t15 ⇒ t14 | t16 ⇒ t16 | t17 ⇒ t16
 250   | t18 ⇒ t18 | t19 ⇒ t18 | t1A ⇒ t1A | t1B ⇒ t1A | t1C ⇒ t1C | t1D ⇒ t1C | t1E ⇒ t1E | t1F ⇒ t1E ]
 251  | t1F ⇒ match e2 with
 252   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t06 | t07 ⇒ t07
 253   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0E | t0F ⇒ t0F
 254   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t16 | t17 ⇒ t17
 255   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 256  ].
 257
 258 (* operatore or *)
 259 ndefinition or_bit ≝
 260 λe1,e2.match e1 with
 261  [ t00 ⇒ match e2 with
 262   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t06 | t07 ⇒ t07
 263   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0E | t0F ⇒ t0F
 264   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t16 | t17 ⇒ t17
 265   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 266  | t01 ⇒ match e2 with
 267   [ t00 ⇒ t01 | t01 ⇒ t01 | t02 ⇒ t03 | t03 ⇒ t03 | t04 ⇒ t05 | t05 ⇒ t05 | t06 ⇒ t07 | t07 ⇒ t07
 268   | t08 ⇒ t09 | t09 ⇒ t09 | t0A ⇒ t0B | t0B ⇒ t0B | t0C ⇒ t0D | t0D ⇒ t0D | t0E ⇒ t0F | t0F ⇒ t0F
 269   | t10 ⇒ t11 | t11 ⇒ t11 | t12 ⇒ t13 | t13 ⇒ t13 | t14 ⇒ t15 | t15 ⇒ t15 | t16 ⇒ t17 | t17 ⇒ t17
 270   | t18 ⇒ t19 | t19 ⇒ t19 | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 271  | t02 ⇒ match e2 with
 272   [ t00 ⇒ t02 | t01 ⇒ t03 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t06 | t05 ⇒ t07 | t06 ⇒ t06 | t07 ⇒ t07
 273   | t08 ⇒ t0A | t09 ⇒ t0B | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t0E | t0D ⇒ t0F | t0E ⇒ t0E | t0F ⇒ t0F
 274   | t10 ⇒ t12 | t11 ⇒ t13 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t16 | t15 ⇒ t17 | t16 ⇒ t16 | t17 ⇒ t17
 275   | t18 ⇒ t1A | t19 ⇒ t1B | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 276  | t03 ⇒ match e2 with
 277   [ t00 ⇒ t03 | t01 ⇒ t03 | t02 ⇒ t03 | t03 ⇒ t03 | t04 ⇒ t07 | t05 ⇒ t07 | t06 ⇒ t07 | t07 ⇒ t07
 278   | t08 ⇒ t0B | t09 ⇒ t0B | t0A ⇒ t0B | t0B ⇒ t0B | t0C ⇒ t0F | t0D ⇒ t0F | t0E ⇒ t0F | t0F ⇒ t0F
 279   | t10 ⇒ t13 | t11 ⇒ t13 | t12 ⇒ t13 | t13 ⇒ t13 | t14 ⇒ t17 | t15 ⇒ t17 | t16 ⇒ t17 | t17 ⇒ t17
 280   | t18 ⇒ t1B | t19 ⇒ t1B | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 281  | t04 ⇒ match e2 with
 282   [ t00 ⇒ t04 | t01 ⇒ t05 | t02 ⇒ t06 | t03 ⇒ t07 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t06 | t07 ⇒ t07
 283   | t08 ⇒ t0C | t09 ⇒ t0D | t0A ⇒ t0E | t0B ⇒ t0F | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0E | t0F ⇒ t0F
 284   | t10 ⇒ t14 | t11 ⇒ t15 | t12 ⇒ t16 | t13 ⇒ t17 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t16 | t17 ⇒ t17
 285   | t18 ⇒ t1C | t19 ⇒ t1D | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 286  | t05 ⇒ match e2 with
 287   [ t00 ⇒ t05 | t01 ⇒ t05 | t02 ⇒ t07 | t03 ⇒ t07 | t04 ⇒ t05 | t05 ⇒ t05 | t06 ⇒ t07 | t07 ⇒ t07
 288   | t08 ⇒ t0D | t09 ⇒ t0D | t0A ⇒ t0F | t0B ⇒ t0F | t0C ⇒ t0D | t0D ⇒ t0D | t0E ⇒ t0F | t0F ⇒ t0F
 289   | t10 ⇒ t15 | t11 ⇒ t15 | t12 ⇒ t17 | t13 ⇒ t17 | t14 ⇒ t15 | t15 ⇒ t15 | t16 ⇒ t17 | t17 ⇒ t17
 290   | t18 ⇒ t1D | t19 ⇒ t1D | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 291  | t06 ⇒ match e2 with
 292   [ t00 ⇒ t06 | t01 ⇒ t07 | t02 ⇒ t06 | t03 ⇒ t07 | t04 ⇒ t06 | t05 ⇒ t07 | t06 ⇒ t06 | t07 ⇒ t07
 293   | t08 ⇒ t0E | t09 ⇒ t0F | t0A ⇒ t0E | t0B ⇒ t0F | t0C ⇒ t0E | t0D ⇒ t0F | t0E ⇒ t0E | t0F ⇒ t0F
 294   | t10 ⇒ t16 | t11 ⇒ t17 | t12 ⇒ t16 | t13 ⇒ t17 | t14 ⇒ t16 | t15 ⇒ t17 | t16 ⇒ t16 | t17 ⇒ t17
 295   | t18 ⇒ t1E | t19 ⇒ t1F | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 296  | t07 ⇒ match e2 with
 297   [ t00 ⇒ t07 | t01 ⇒ t07 | t02 ⇒ t07 | t03 ⇒ t07 | t04 ⇒ t07 | t05 ⇒ t07 | t06 ⇒ t07 | t07 ⇒ t07
 298   | t08 ⇒ t0F | t09 ⇒ t0F | t0A ⇒ t0F | t0B ⇒ t0F | t0C ⇒ t0F | t0D ⇒ t0F | t0E ⇒ t0F | t0F ⇒ t0F
 299   | t10 ⇒ t17 | t11 ⇒ t17 | t12 ⇒ t17 | t13 ⇒ t17 | t14 ⇒ t17 | t15 ⇒ t17 | t16 ⇒ t17 | t17 ⇒ t17
 300   | t18 ⇒ t1F | t19 ⇒ t1F | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 301  | t08 ⇒ match e2 with
 302   [ t00 ⇒ t08 | t01 ⇒ t09 | t02 ⇒ t0A | t03 ⇒ t0B | t04 ⇒ t0C | t05 ⇒ t0D | t06 ⇒ t0E | t07 ⇒ t0F
 303   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0E | t0F ⇒ t0F
 304   | t10 ⇒ t18 | t11 ⇒ t19 | t12 ⇒ t1A | t13 ⇒ t1B | t14 ⇒ t1C | t15 ⇒ t1D | t16 ⇒ t1E | t17 ⇒ t1F
 305   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 306  | t09 ⇒ match e2 with
 307   [ t00 ⇒ t09 | t01 ⇒ t09 | t02 ⇒ t0B | t03 ⇒ t0B | t04 ⇒ t0D | t05 ⇒ t0D | t06 ⇒ t0F | t07 ⇒ t0F
 308   | t08 ⇒ t09 | t09 ⇒ t09 | t0A ⇒ t0B | t0B ⇒ t0B | t0C ⇒ t0D | t0D ⇒ t0D | t0E ⇒ t0F | t0F ⇒ t0F
 309   | t10 ⇒ t19 | t11 ⇒ t19 | t12 ⇒ t1B | t13 ⇒ t1B | t14 ⇒ t1D | t15 ⇒ t1D | t16 ⇒ t1F | t17 ⇒ t1F
 310   | t18 ⇒ t19 | t19 ⇒ t19 | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 311  | t0A ⇒ match e2 with
 312   [ t00 ⇒ t0A | t01 ⇒ t0B | t02 ⇒ t0A | t03 ⇒ t0B | t04 ⇒ t0E | t05 ⇒ t0F | t06 ⇒ t0E | t07 ⇒ t0F
 313   | t08 ⇒ t0A | t09 ⇒ t0B | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t0E | t0D ⇒ t0F | t0E ⇒ t0E | t0F ⇒ t0F
 314   | t10 ⇒ t1A | t11 ⇒ t1B | t12 ⇒ t1A | t13 ⇒ t1B | t14 ⇒ t1E | t15 ⇒ t1F | t16 ⇒ t1E | t17 ⇒ t1F
 315   | t18 ⇒ t1A | t19 ⇒ t1B | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 316  | t0B ⇒ match e2 with
 317   [ t00 ⇒ t0B | t01 ⇒ t0B | t02 ⇒ t0B | t03 ⇒ t0B | t04 ⇒ t0F | t05 ⇒ t0F | t06 ⇒ t0F | t07 ⇒ t0F
 318   | t08 ⇒ t0B | t09 ⇒ t0B | t0A ⇒ t0B | t0B ⇒ t0B | t0C ⇒ t0F | t0D ⇒ t0F | t0E ⇒ t0F | t0F ⇒ t0F
 319   | t10 ⇒ t1B | t11 ⇒ t1B | t12 ⇒ t1B | t13 ⇒ t1B | t14 ⇒ t1F | t15 ⇒ t1F | t16 ⇒ t1F | t17 ⇒ t1F
 320   | t18 ⇒ t1B | t19 ⇒ t1B | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 321  | t0C ⇒ match e2 with
 322   [ t00 ⇒ t0C | t01 ⇒ t0D | t02 ⇒ t0E | t03 ⇒ t0F | t04 ⇒ t0C | t05 ⇒ t0D | t06 ⇒ t0E | t07 ⇒ t0F
 323   | t08 ⇒ t0C | t09 ⇒ t0D | t0A ⇒ t0E | t0B ⇒ t0F | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0E | t0F ⇒ t0F
 324   | t10 ⇒ t1C | t11 ⇒ t1D | t12 ⇒ t1E | t13 ⇒ t1F | t14 ⇒ t1C | t15 ⇒ t1D | t16 ⇒ t1E | t17 ⇒ t1F
 325   | t18 ⇒ t1C | t19 ⇒ t1D | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 326  | t0D ⇒ match e2 with
 327   [ t00 ⇒ t0D | t01 ⇒ t0D | t02 ⇒ t0F | t03 ⇒ t0F | t04 ⇒ t0D | t05 ⇒ t0D | t06 ⇒ t0F | t07 ⇒ t0F
 328   | t08 ⇒ t0D | t09 ⇒ t0D | t0A ⇒ t0F | t0B ⇒ t0F | t0C ⇒ t0D | t0D ⇒ t0D | t0E ⇒ t0F | t0F ⇒ t0F
 329   | t10 ⇒ t1D | t11 ⇒ t1D | t12 ⇒ t1F | t13 ⇒ t1F | t14 ⇒ t1D | t15 ⇒ t1D | t16 ⇒ t1F | t17 ⇒ t1F
 330   | t18 ⇒ t1D | t19 ⇒ t1D | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 331  | t0E ⇒ match e2 with
 332   [ t00 ⇒ t0E | t01 ⇒ t0F | t02 ⇒ t0E | t03 ⇒ t0F | t04 ⇒ t0E | t05 ⇒ t0F | t06 ⇒ t0E | t07 ⇒ t0F
 333   | t08 ⇒ t0E | t09 ⇒ t0F | t0A ⇒ t0E | t0B ⇒ t0F | t0C ⇒ t0E | t0D ⇒ t0F | t0E ⇒ t0E | t0F ⇒ t0F
 334   | t10 ⇒ t1E | t11 ⇒ t1F | t12 ⇒ t1E | t13 ⇒ t1F | t14 ⇒ t1E | t15 ⇒ t1F | t16 ⇒ t1E | t17 ⇒ t1F
 335   | t18 ⇒ t1E | t19 ⇒ t1F | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 336  | t0F ⇒ match e2 with
 337   [ t00 ⇒ t0F | t01 ⇒ t0F | t02 ⇒ t0F | t03 ⇒ t0F | t04 ⇒ t0F | t05 ⇒ t0F | t06 ⇒ t0F | t07 ⇒ t0F
 338   | t08 ⇒ t0F | t09 ⇒ t0F | t0A ⇒ t0F | t0B ⇒ t0F | t0C ⇒ t0F | t0D ⇒ t0F | t0E ⇒ t0F | t0F ⇒ t0F
 339   | t10 ⇒ t1F | t11 ⇒ t1F | t12 ⇒ t1F | t13 ⇒ t1F | t14 ⇒ t1F | t15 ⇒ t1F | t16 ⇒ t1F | t17 ⇒ t1F
 340   | t18 ⇒ t1F | t19 ⇒ t1F | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 341  | t10 ⇒ match e2 with
 342   [ t00 ⇒ t10 | t01 ⇒ t11 | t02 ⇒ t12 | t03 ⇒ t13 | t04 ⇒ t14 | t05 ⇒ t15 | t06 ⇒ t16 | t07 ⇒ t17
 343   | t08 ⇒ t18 | t09 ⇒ t19 | t0A ⇒ t1A | t0B ⇒ t1B | t0C ⇒ t1C | t0D ⇒ t1D | t0E ⇒ t1E | t0F ⇒ t1F
 344   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t16 | t17 ⇒ t17
 345   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 346  | t11 ⇒ match e2 with
 347   [ t00 ⇒ t11 | t01 ⇒ t11 | t02 ⇒ t13 | t03 ⇒ t13 | t04 ⇒ t15 | t05 ⇒ t15 | t06 ⇒ t17 | t07 ⇒ t17
 348   | t08 ⇒ t19 | t09 ⇒ t19 | t0A ⇒ t1B | t0B ⇒ t1B | t0C ⇒ t1D | t0D ⇒ t1D | t0E ⇒ t1F | t0F ⇒ t1F
 349   | t10 ⇒ t11 | t11 ⇒ t11 | t12 ⇒ t13 | t13 ⇒ t13 | t14 ⇒ t15 | t15 ⇒ t15 | t16 ⇒ t17 | t17 ⇒ t17
 350   | t18 ⇒ t19 | t19 ⇒ t19 | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 351  | t12 ⇒ match e2 with
 352   [ t00 ⇒ t12 | t01 ⇒ t13 | t02 ⇒ t12 | t03 ⇒ t13 | t04 ⇒ t16 | t05 ⇒ t17 | t06 ⇒ t16 | t07 ⇒ t17
 353   | t08 ⇒ t1A | t09 ⇒ t1B | t0A ⇒ t1A | t0B ⇒ t1B | t0C ⇒ t1E | t0D ⇒ t1F | t0E ⇒ t1E | t0F ⇒ t1F
 354   | t10 ⇒ t12 | t11 ⇒ t13 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t16 | t15 ⇒ t17 | t16 ⇒ t16 | t17 ⇒ t17
 355   | t18 ⇒ t1A | t19 ⇒ t1B | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 356  | t13 ⇒ match e2 with
 357   [ t00 ⇒ t13 | t01 ⇒ t13 | t02 ⇒ t13 | t03 ⇒ t13 | t04 ⇒ t17 | t05 ⇒ t17 | t06 ⇒ t17 | t07 ⇒ t17
 358   | t08 ⇒ t1B | t09 ⇒ t1B | t0A ⇒ t1B | t0B ⇒ t1B | t0C ⇒ t1F | t0D ⇒ t1F | t0E ⇒ t1F | t0F ⇒ t1F
 359   | t10 ⇒ t13 | t11 ⇒ t13 | t12 ⇒ t13 | t13 ⇒ t13 | t14 ⇒ t17 | t15 ⇒ t17 | t16 ⇒ t17 | t17 ⇒ t17
 360   | t18 ⇒ t1B | t19 ⇒ t1B | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 361  | t14 ⇒ match e2 with
 362   [ t00 ⇒ t14 | t01 ⇒ t15 | t02 ⇒ t16 | t03 ⇒ t17 | t04 ⇒ t14 | t05 ⇒ t15 | t06 ⇒ t16 | t07 ⇒ t17
 363   | t08 ⇒ t1C | t09 ⇒ t1D | t0A ⇒ t1E | t0B ⇒ t1F | t0C ⇒ t1C | t0D ⇒ t1D | t0E ⇒ t1E | t0F ⇒ t1F
 364   | t10 ⇒ t14 | t11 ⇒ t15 | t12 ⇒ t16 | t13 ⇒ t17 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t16 | t17 ⇒ t17
 365   | t18 ⇒ t1C | t19 ⇒ t1D | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 366  | t15 ⇒ match e2 with
 367   [ t00 ⇒ t15 | t01 ⇒ t15 | t02 ⇒ t17 | t03 ⇒ t17 | t04 ⇒ t15 | t05 ⇒ t15 | t06 ⇒ t17 | t07 ⇒ t17
 368   | t08 ⇒ t1D | t09 ⇒ t1D | t0A ⇒ t1F | t0B ⇒ t1F | t0C ⇒ t1D | t0D ⇒ t1D | t0E ⇒ t1F | t0F ⇒ t1F
 369   | t10 ⇒ t15 | t11 ⇒ t15 | t12 ⇒ t17 | t13 ⇒ t17 | t14 ⇒ t15 | t15 ⇒ t15 | t16 ⇒ t17 | t17 ⇒ t17
 370   | t18 ⇒ t1D | t19 ⇒ t1D | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 371  | t16 ⇒ match e2 with
 372   [ t00 ⇒ t16 | t01 ⇒ t17 | t02 ⇒ t16 | t03 ⇒ t17 | t04 ⇒ t16 | t05 ⇒ t17 | t06 ⇒ t16 | t07 ⇒ t17
 373   | t08 ⇒ t1E | t09 ⇒ t1F | t0A ⇒ t1E | t0B ⇒ t1F | t0C ⇒ t1E | t0D ⇒ t1F | t0E ⇒ t1E | t0F ⇒ t1F
 374   | t10 ⇒ t16 | t11 ⇒ t17 | t12 ⇒ t16 | t13 ⇒ t17 | t14 ⇒ t16 | t15 ⇒ t17 | t16 ⇒ t16 | t17 ⇒ t17
 375   | t18 ⇒ t1E | t19 ⇒ t1F | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 376  | t17 ⇒ match e2 with
 377   [ t00 ⇒ t17 | t01 ⇒ t17 | t02 ⇒ t17 | t03 ⇒ t17 | t04 ⇒ t17 | t05 ⇒ t17 | t06 ⇒ t17 | t07 ⇒ t17
 378   | t08 ⇒ t1F | t09 ⇒ t1F | t0A ⇒ t1F | t0B ⇒ t1F | t0C ⇒ t1F | t0D ⇒ t1F | t0E ⇒ t1F | t0F ⇒ t1F
 379   | t10 ⇒ t17 | t11 ⇒ t17 | t12 ⇒ t17 | t13 ⇒ t17 | t14 ⇒ t17 | t15 ⇒ t17 | t16 ⇒ t17 | t17 ⇒ t17
 380   | t18 ⇒ t1F | t19 ⇒ t1F | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 381  | t18 ⇒ match e2 with
 382   [ t00 ⇒ t18 | t01 ⇒ t19 | t02 ⇒ t1A | t03 ⇒ t1B | t04 ⇒ t1C | t05 ⇒ t1D | t06 ⇒ t1E | t07 ⇒ t1F
 383   | t08 ⇒ t18 | t09 ⇒ t19 | t0A ⇒ t1A | t0B ⇒ t1B | t0C ⇒ t1C | t0D ⇒ t1D | t0E ⇒ t1E | t0F ⇒ t1F
 384   | t10 ⇒ t18 | t11 ⇒ t19 | t12 ⇒ t1A | t13 ⇒ t1B | t14 ⇒ t1C | t15 ⇒ t1D | t16 ⇒ t1E | t17 ⇒ t1F
 385   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 386  | t19 ⇒ match e2 with
 387   [ t00 ⇒ t19 | t01 ⇒ t19 | t02 ⇒ t1B | t03 ⇒ t1B | t04 ⇒ t1D | t05 ⇒ t1D | t06 ⇒ t1F | t07 ⇒ t1F
 388   | t08 ⇒ t19 | t09 ⇒ t19 | t0A ⇒ t1B | t0B ⇒ t1B | t0C ⇒ t1D | t0D ⇒ t1D | t0E ⇒ t1F | t0F ⇒ t1F
 389   | t10 ⇒ t19 | t11 ⇒ t19 | t12 ⇒ t1B | t13 ⇒ t1B | t14 ⇒ t1D | t15 ⇒ t1D | t16 ⇒ t1F | t17 ⇒ t1F
 390   | t18 ⇒ t19 | t19 ⇒ t19 | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 391  | t1A ⇒ match e2 with
 392   [ t00 ⇒ t1A | t01 ⇒ t1B | t02 ⇒ t1A | t03 ⇒ t1B | t04 ⇒ t1E | t05 ⇒ t1F | t06 ⇒ t1E | t07 ⇒ t1F
 393   | t08 ⇒ t1A | t09 ⇒ t1B | t0A ⇒ t1A | t0B ⇒ t1B | t0C ⇒ t1E | t0D ⇒ t1F | t0E ⇒ t1E | t0F ⇒ t1F
 394   | t10 ⇒ t1A | t11 ⇒ t1B | t12 ⇒ t1A | t13 ⇒ t1B | t14 ⇒ t1E | t15 ⇒ t1F | t16 ⇒ t1E | t17 ⇒ t1F
 395   | t18 ⇒ t1A | t19 ⇒ t1B | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 396  | t1B ⇒ match e2 with
 397   [ t00 ⇒ t1B | t01 ⇒ t1B | t02 ⇒ t1B | t03 ⇒ t1B | t04 ⇒ t1F | t05 ⇒ t1F | t06 ⇒ t1F | t07 ⇒ t1F
 398   | t08 ⇒ t1B | t09 ⇒ t1B | t0A ⇒ t1B | t0B ⇒ t1B | t0C ⇒ t1F | t0D ⇒ t1F | t0E ⇒ t1F | t0F ⇒ t1F
 399   | t10 ⇒ t1B | t11 ⇒ t1B | t12 ⇒ t1B | t13 ⇒ t1B | t14 ⇒ t1F | t15 ⇒ t1F | t16 ⇒ t1F | t17 ⇒ t1F
 400   | t18 ⇒ t1B | t19 ⇒ t1B | t1A ⇒ t1B | t1B ⇒ t1B | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 401  | t1C ⇒ match e2 with
 402   [ t00 ⇒ t1C | t01 ⇒ t1D | t02 ⇒ t1E | t03 ⇒ t1F | t04 ⇒ t1C | t05 ⇒ t1D | t06 ⇒ t1E | t07 ⇒ t1F
 403   | t08 ⇒ t1C | t09 ⇒ t1D | t0A ⇒ t1E | t0B ⇒ t1F | t0C ⇒ t1C | t0D ⇒ t1D | t0E ⇒ t1E | t0F ⇒ t1F
 404   | t10 ⇒ t1C | t11 ⇒ t1D | t12 ⇒ t1E | t13 ⇒ t1F | t14 ⇒ t1C | t15 ⇒ t1D | t16 ⇒ t1E | t17 ⇒ t1F
 405   | t18 ⇒ t1C | t19 ⇒ t1D | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 406  | t1D ⇒ match e2 with
 407   [ t00 ⇒ t1D | t01 ⇒ t1D | t02 ⇒ t1F | t03 ⇒ t1F | t04 ⇒ t1D | t05 ⇒ t1D | t06 ⇒ t1F | t07 ⇒ t1F
 408   | t08 ⇒ t1D | t09 ⇒ t1D | t0A ⇒ t1F | t0B ⇒ t1F | t0C ⇒ t1D | t0D ⇒ t1D | t0E ⇒ t1F | t0F ⇒ t1F
 409   | t10 ⇒ t1D | t11 ⇒ t1D | t12 ⇒ t1F | t13 ⇒ t1F | t14 ⇒ t1D | t15 ⇒ t1D | t16 ⇒ t1F | t17 ⇒ t1F
 410   | t18 ⇒ t1D | t19 ⇒ t1D | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1D | t1D ⇒ t1D | t1E ⇒ t1F | t1F ⇒ t1F ]
 411  | t1E ⇒ match e2 with
 412   [ t00 ⇒ t1E | t01 ⇒ t1F | t02 ⇒ t1E | t03 ⇒ t1F | t04 ⇒ t1E | t05 ⇒ t1F | t06 ⇒ t1E | t07 ⇒ t1F
 413   | t08 ⇒ t1E | t09 ⇒ t1F | t0A ⇒ t1E | t0B ⇒ t1F | t0C ⇒ t1E | t0D ⇒ t1F | t0E ⇒ t1E | t0F ⇒ t1F
 414   | t10 ⇒ t1E | t11 ⇒ t1F | t12 ⇒ t1E | t13 ⇒ t1F | t14 ⇒ t1E | t15 ⇒ t1F | t16 ⇒ t1E | t17 ⇒ t1F
 415   | t18 ⇒ t1E | t19 ⇒ t1F | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1E | t1F ⇒ t1F ]
 416  | t1F ⇒ match e2 with
 417   [ t00 ⇒ t1F | t01 ⇒ t1F | t02 ⇒ t1F | t03 ⇒ t1F | t04 ⇒ t1F | t05 ⇒ t1F | t06 ⇒ t1F | t07 ⇒ t1F
 418   | t08 ⇒ t1F | t09 ⇒ t1F | t0A ⇒ t1F | t0B ⇒ t1F | t0C ⇒ t1F | t0D ⇒ t1F | t0E ⇒ t1F | t0F ⇒ t1F
 419   | t10 ⇒ t1F | t11 ⇒ t1F | t12 ⇒ t1F | t13 ⇒ t1F | t14 ⇒ t1F | t15 ⇒ t1F | t16 ⇒ t1F | t17 ⇒ t1F
 420   | t18 ⇒ t1F | t19 ⇒ t1F | t1A ⇒ t1F | t1B ⇒ t1F | t1C ⇒ t1F | t1D ⇒ t1F | t1E ⇒ t1F | t1F ⇒ t1F ]
 421  ].
 422
 423 (* operatore xor *)
 424 ndefinition xor_bit ≝
 425 λe1,e2.match e1 with
 426  [ t00 ⇒ match e2 with
 427   [ t00 ⇒ t00 | t01 ⇒ t01 | t02 ⇒ t02 | t03 ⇒ t03 | t04 ⇒ t04 | t05 ⇒ t05 | t06 ⇒ t06 | t07 ⇒ t07
 428   | t08 ⇒ t08 | t09 ⇒ t09 | t0A ⇒ t0A | t0B ⇒ t0B | t0C ⇒ t0C | t0D ⇒ t0D | t0E ⇒ t0E | t0F ⇒ t0F
 429   | t10 ⇒ t10 | t11 ⇒ t11 | t12 ⇒ t12 | t13 ⇒ t13 | t14 ⇒ t14 | t15 ⇒ t15 | t16 ⇒ t16 | t17 ⇒ t17
 430   | t18 ⇒ t18 | t19 ⇒ t19 | t1A ⇒ t1A | t1B ⇒ t1B | t1C ⇒ t1C | t1D ⇒ t1D | t1E ⇒ t1E | t1F ⇒ t1F ]
 431  | t01 ⇒ match e2 with
 432   [ t00 ⇒ t01 | t01 ⇒ t00 | t02 ⇒ t03 | t03 ⇒ t02 | t04 ⇒ t05 | t05 ⇒ t04 | t06 ⇒ t07 | t07 ⇒ t06
 433   | t08 ⇒ t09 | t09 ⇒ t08 | t0A ⇒ t0B | t0B ⇒ t0A | t0C ⇒ t0D | t0D ⇒ t0C | t0E ⇒ t0F | t0F ⇒ t0E
 434   | t10 ⇒ t11 | t11 ⇒ t10 | t12 ⇒ t13 | t13 ⇒ t12 | t14 ⇒ t15 | t15 ⇒ t14 | t16 ⇒ t17 | t17 ⇒ t16
 435   | t18 ⇒ t19 | t19 ⇒ t18 | t1A ⇒ t1B | t1B ⇒ t1A | t1C ⇒ t1D | t1D ⇒ t1C | t1E ⇒ t1F | t1F ⇒ t1E ]
 436  | t02 ⇒ match e2 with
 437   [ t00 ⇒ t02 | t01 ⇒ t03 | t02 ⇒ t00 | t03 ⇒ t01 | t04 ⇒ t06 | t05 ⇒ t07 | t06 ⇒ t04 | t07 ⇒ t05
 438   | t08 ⇒ t0A | t09 ⇒ t0B | t0A ⇒ t08 | t0B ⇒ t09 | t0C ⇒ t0E | t0D ⇒ t0F | t0E ⇒ t0C | t0F ⇒ t0D
 439   | t10 ⇒ t12 | t11 ⇒ t13 | t12 ⇒ t10 | t13 ⇒ t11 | t14 ⇒ t16 | t15 ⇒ t17 | t16 ⇒ t14 | t17 ⇒ t15
 440   | t18 ⇒ t1A | t19 ⇒ t1B | t1A ⇒ t18 | t1B ⇒ t19 | t1C ⇒ t1E | t1D ⇒ t1F | t1E ⇒ t1C | t1F ⇒ t1D ]
 441  | t03 ⇒ match e2 with
 442   [ t00 ⇒ t03 | t01 ⇒ t02 | t02 ⇒ t01 | t03 ⇒ t00 | t04 ⇒ t07 | t05 ⇒ t06 | t06 ⇒ t05 | t07 ⇒ t04
 443   | t08 ⇒ t0B | t09 ⇒ t0A | t0A ⇒ t09 | t0B ⇒ t08 | t0C ⇒ t0F | t0D ⇒ t0E | t0E ⇒ t0D | t0F ⇒ t0C
 444   | t10 ⇒ t13 | t11 ⇒ t12 | t12 ⇒ t11 | t13 ⇒ t10 | t14 ⇒ t17 | t15 ⇒ t16 | t16 ⇒ t15 | t17 ⇒ t14
 445   | t18 ⇒ t1B | t19 ⇒ t1A | t1A ⇒ t19 | t1B ⇒ t18 | t1C ⇒ t1F | t1D ⇒ t1E | t1E ⇒ t1D | t1F ⇒ t1C ]
 446  | t04 ⇒ match e2 with
 447   [ t00 ⇒ t04 | t01 ⇒ t05 | t02 ⇒ t06 | t03 ⇒ t07 | t04 ⇒ t00 | t05 ⇒ t01 | t06 ⇒ t02 | t07 ⇒ t03
 448   | t08 ⇒ t0C | t09 ⇒ t0D | t0A ⇒ t0E | t0B ⇒ t0F | t0C ⇒ t08 | t0D ⇒ t09 | t0E ⇒ t0A | t0F ⇒ t0B
 449   | t10 ⇒ t14 | t11 ⇒ t15 | t12 ⇒ t16 | t13 ⇒ t17 | t14 ⇒ t10 | t15 ⇒ t11 | t16 ⇒ t12 | t17 ⇒ t13
 450   | t18 ⇒ t1C | t19 ⇒ t1D | t1A ⇒ t1E | t1B ⇒ t1F | t1C ⇒ t18 | t1D ⇒ t19 | t1E ⇒ t1A | t1F ⇒ t1B ]
 451  | t05 ⇒ match e2 with
 452   [ t00 ⇒ t05 | t01 ⇒ t04 | t02 ⇒ t07 | t03 ⇒ t06 | t04 ⇒ t01 | t05 ⇒ t00 | t06 ⇒ t03 | t07 ⇒ t02
 453   | t08 ⇒ t0D | t09 ⇒ t0C | t0A ⇒ t0F | t0B ⇒ t0E | t0C ⇒ t09 | t0D ⇒ t08 | t0E ⇒ t0B | t0F ⇒ t0A
 454   | t10 ⇒ t15 | t11 ⇒ t14 | t12 ⇒ t17 | t13 ⇒ t16 | t14 ⇒ t11 | t15 ⇒ t10 | t16 ⇒ t13 | t17 ⇒ t12
 455   | t18 ⇒ t1D | t19 ⇒ t1C | t1A ⇒ t1F | t1B ⇒ t1E | t1C ⇒ t19 | t1D ⇒ t18 | t1E ⇒ t1B | t1F ⇒ t1A ]
 456  | t06 ⇒ match e2 with
 457   [ t00 ⇒ t06 | t01 ⇒ t07 | t02 ⇒ t04 | t03 ⇒ t05 | t04 ⇒ t02 | t05 ⇒ t03 | t06 ⇒ t00 | t07 ⇒ t01
 458   | t08 ⇒ t0E | t09 ⇒ t0F | t0A ⇒ t0C | t0B ⇒ t0D | t0C ⇒ t0A | t0D ⇒ t0B | t0E ⇒ t08 | t0F ⇒ t09
 459   | t10 ⇒ t16 | t11 ⇒ t17 | t12 ⇒ t14 | t13 ⇒ t15 | t14 ⇒ t12 | t15 ⇒ t13 | t16 ⇒ t10 | t17 ⇒ t11
 460   | t18 ⇒ t1E | t19 ⇒ t1F | t1A ⇒ t1C | t1B ⇒ t1D | t1C ⇒ t1A | t1D ⇒ t1B | t1E ⇒ t18 | t1F ⇒ t19 ]
 461  | t07 ⇒ match e2 with
 462   [ t00 ⇒ t07 | t01 ⇒ t06 | t02 ⇒ t05 | t03 ⇒ t04 | t04 ⇒ t03 | t05 ⇒ t02 | t06 ⇒ t01 | t07 ⇒ t00
 463   | t08 ⇒ t0F | t09 ⇒ t0E | t0A ⇒ t0D | t0B ⇒ t0C | t0C ⇒ t0B | t0D ⇒ t0A | t0E ⇒ t09 | t0F ⇒ t08
 464   | t10 ⇒ t17 | t11 ⇒ t16 | t12 ⇒ t15 | t13 ⇒ t14 | t14 ⇒ t13 | t15 ⇒ t12 | t16 ⇒ t11 | t17 ⇒ t10
 465   | t18 ⇒ t1F | t19 ⇒ t1E | t1A ⇒ t1D | t1B ⇒ t1C | t1C ⇒ t1B | t1D ⇒ t1A | t1E ⇒ t19 | t1F ⇒ t18 ]
 466  | t08 ⇒ match e2 with
 467   [ t00 ⇒ t08 | t01 ⇒ t09 | t02 ⇒ t0A | t03 ⇒ t0B | t04 ⇒ t0C | t05 ⇒ t0D | t06 ⇒ t0E | t07 ⇒ t0F
 468   | t08 ⇒ t00 | t09 ⇒ t01 | t0A ⇒ t02 | t0B ⇒ t03 | t0C ⇒ t04 | t0D ⇒ t05 | t0E ⇒ t06 | t0F ⇒ t07
 469   | t10 ⇒ t18 | t11 ⇒ t19 | t12 ⇒ t1A | t13 ⇒ t1B | t14 ⇒ t1C | t15 ⇒ t1D | t16 ⇒ t1E | t17 ⇒ t1F
 470   | t18 ⇒ t10 | t19 ⇒ t11 | t1A ⇒ t12 | t1B ⇒ t13 | t1C ⇒ t14 | t1D ⇒ t15 | t1E ⇒ t16 | t1F ⇒ t17 ]
 471  | t09 ⇒ match e2 with
 472   [ t00 ⇒ t09 | t01 ⇒ t08 | t02 ⇒ t0B | t03 ⇒ t0A | t04 ⇒ t0D | t05 ⇒ t0C | t06 ⇒ t0F | t07 ⇒ t0E
 473   | t08 ⇒ t01 | t09 ⇒ t00 | t0A ⇒ t03 | t0B ⇒ t02 | t0C ⇒ t05 | t0D ⇒ t04 | t0E ⇒ t07 | t0F ⇒ t06
 474   | t10 ⇒ t19 | t11 ⇒ t18 | t12 ⇒ t1B | t13 ⇒ t1A | t14 ⇒ t1D | t15 ⇒ t1C | t16 ⇒ t1F | t17 ⇒ t1E
 475   | t18 ⇒ t11 | t19 ⇒ t10 | t1A ⇒ t13 | t1B ⇒ t12 | t1C ⇒ t15 | t1D ⇒ t14 | t1E ⇒ t17 | t1F ⇒ t16 ]
 476  | t0A ⇒ match e2 with
 477   [ t00 ⇒ t0A | t01 ⇒ t0B | t02 ⇒ t08 | t03 ⇒ t09 | t04 ⇒ t0E | t05 ⇒ t0F | t06 ⇒ t0C | t07 ⇒ t0D
 478   | t08 ⇒ t02 | t09 ⇒ t03 | t0A ⇒ t00 | t0B ⇒ t01 | t0C ⇒ t06 | t0D ⇒ t07 | t0E ⇒ t04 | t0F ⇒ t05
 479   | t10 ⇒ t1A | t11 ⇒ t1B | t12 ⇒ t18 | t13 ⇒ t19 | t14 ⇒ t1E | t15 ⇒ t1F | t16 ⇒ t1C | t17 ⇒ t1D
 480   | t18 ⇒ t12 | t19 ⇒ t13 | t1A ⇒ t10 | t1B ⇒ t11 | t1C ⇒ t16 | t1D ⇒ t17 | t1E ⇒ t14 | t1F ⇒ t15 ]
 481  | t0B ⇒ match e2 with
 482   [ t00 ⇒ t0B | t01 ⇒ t0A | t02 ⇒ t09 | t03 ⇒ t08 | t04 ⇒ t0F | t05 ⇒ t0E | t06 ⇒ t0D | t07 ⇒ t0C
 483   | t08 ⇒ t03 | t09 ⇒ t02 | t0A ⇒ t01 | t0B ⇒ t00 | t0C ⇒ t07 | t0D ⇒ t06 | t0E ⇒ t05 | t0F ⇒ t04
 484   | t10 ⇒ t1B | t11 ⇒ t1A | t12 ⇒ t19 | t13 ⇒ t18 | t14 ⇒ t1F | t15 ⇒ t1E | t16 ⇒ t1D | t17 ⇒ t1C
 485   | t18 ⇒ t13 | t19 ⇒ t12 | t1A ⇒ t11 | t1B ⇒ t10 | t1C ⇒ t17 | t1D ⇒ t16 | t1E ⇒ t15 | t1F ⇒ t14 ]
 486  | t0C ⇒ match e2 with
 487   [ t00 ⇒ t0C | t01 ⇒ t0D | t02 ⇒ t0E | t03 ⇒ t0F | t04 ⇒ t08 | t05 ⇒ t09 | t06 ⇒ t0A | t07 ⇒ t0B
 488   | t08 ⇒ t04 | t09 ⇒ t05 | t0A ⇒ t06 | t0B ⇒ t07 | t0C ⇒ t00 | t0D ⇒ t01 | t0E ⇒ t02 | t0F ⇒ t03
 489   | t10 ⇒ t1C | t11 ⇒ t1D | t12 ⇒ t1E | t13 ⇒ t1F | t14 ⇒ t18 | t15 ⇒ t19 | t16 ⇒ t1A | t17 ⇒ t1B
 490   | t18 ⇒ t14 | t19 ⇒ t15 | t1A ⇒ t16 | t1B ⇒ t17 | t1C ⇒ t10 | t1D ⇒ t11 | t1E ⇒ t12 | t1F ⇒ t13 ]
 491  | t0D ⇒ match e2 with
 492   [ t00 ⇒ t0D | t01 ⇒ t0C | t02 ⇒ t0F | t03 ⇒ t0E | t04 ⇒ t09 | t05 ⇒ t08 | t06 ⇒ t0B | t07 ⇒ t0A
 493   | t08 ⇒ t05 | t09 ⇒ t04 | t0A ⇒ t07 | t0B ⇒ t06 | t0C ⇒ t01 | t0D ⇒ t00 | t0E ⇒ t03 | t0F ⇒ t02
 494   | t10 ⇒ t1D | t11 ⇒ t1C | t12 ⇒ t1F | t13 ⇒ t1E | t14 ⇒ t19 | t15 ⇒ t18 | t16 ⇒ t1B | t17 ⇒ t1A
 495   | t18 ⇒ t15 | t19 ⇒ t14 | t1A ⇒ t17 | t1B ⇒ t16 | t1C ⇒ t11 | t1D ⇒ t10 | t1E ⇒ t13 | t1F ⇒ t12 ]
 496  | t0E ⇒ match e2 with
 497   [ t00 ⇒ t0E | t01 ⇒ t0F | t02 ⇒ t0C | t03 ⇒ t0D | t04 ⇒ t0A | t05 ⇒ t0B | t06 ⇒ t08 | t07 ⇒ t09
 498   | t08 ⇒ t06 | t09 ⇒ t07 | t0A ⇒ t04 | t0B ⇒ t05 | t0C ⇒ t02 | t0D ⇒ t03 | t0E ⇒ t00 | t0F ⇒ t01
 499   | t10 ⇒ t1E | t11 ⇒ t1F | t12 ⇒ t1C | t13 ⇒ t1D | t14 ⇒ t1A | t15 ⇒ t1B | t16 ⇒ t18 | t17 ⇒ t19
 500   | t18 ⇒ t16 | t19 ⇒ t17 | t1A ⇒ t14 | t1B ⇒ t15 | t1C ⇒ t12 | t1D ⇒ t13 | t1E ⇒ t10 | t1F ⇒ t11 ]
 501  | t0F ⇒ match e2 with
 502   [ t00 ⇒ t0F | t01 ⇒ t0E | t02 ⇒ t0D | t03 ⇒ t0C | t04 ⇒ t0B | t05 ⇒ t0A | t06 ⇒ t09 | t07 ⇒ t08
 503   | t08 ⇒ t07 | t09 ⇒ t06 | t0A ⇒ t05 | t0B ⇒ t04 | t0C ⇒ t03 | t0D ⇒ t02 | t0E ⇒ t01 | t0F ⇒ t00
 504   | t10 ⇒ t1F | t11 ⇒ t1E | t12 ⇒ t1D | t13 ⇒ t1C | t14 ⇒ t1B | t15 ⇒ t1A | t16 ⇒ t19 | t17 ⇒ t18
 505   | t18 ⇒ t17 | t19 ⇒ t16 | t1A ⇒ t15 | t1B ⇒ t14 | t1C ⇒ t13 | t1D ⇒ t12 | t1E ⇒ t11 | t1F ⇒ t10 ]
 506  | t10 ⇒ match e2 with
 507   [ t00 ⇒ t10 | t01 ⇒ t11 | t02 ⇒ t12 | t03 ⇒ t13 | t04 ⇒ t14 | t05 ⇒ t15 | t06 ⇒ t16 | t07 ⇒ t17
 508   | t08 ⇒ t18 | t09 ⇒ t19 | t0A ⇒ t1A | t0B ⇒ t1B | t0C ⇒ t1C | t0D ⇒ t1D | t0E ⇒ t1E | t0F ⇒ t1F
 509   | t10 ⇒ t00 | t11 ⇒ t01 | t12 ⇒ t02 | t13 ⇒ t03 | t14 ⇒ t04 | t15 ⇒ t05 | t16 ⇒ t06 | t17 ⇒ t07
 510   | t18 ⇒ t08 | t19 ⇒ t09 | t1A ⇒ t0A | t1B ⇒ t0B | t1C ⇒ t0C | t1D ⇒ t0D | t1E ⇒ t0E | t1F ⇒ t0F ]
 511  | t11 ⇒ match e2 with
 512   [ t00 ⇒ t11 | t01 ⇒ t10 | t02 ⇒ t13 | t03 ⇒ t12 | t04 ⇒ t15 | t05 ⇒ t14 | t06 ⇒ t17 | t07 ⇒ t16
 513   | t08 ⇒ t19 | t09 ⇒ t18 | t0A ⇒ t1B | t0B ⇒ t1A | t0C ⇒ t1D | t0D ⇒ t1C | t0E ⇒ t1F | t0F ⇒ t1E
 514   | t10 ⇒ t01 | t11 ⇒ t00 | t12 ⇒ t03 | t13 ⇒ t02 | t14 ⇒ t05 | t15 ⇒ t04 | t16 ⇒ t07 | t17 ⇒ t06
 515   | t18 ⇒ t09 | t19 ⇒ t08 | t1A ⇒ t0B | t1B ⇒ t0A | t1C ⇒ t0D | t1D ⇒ t0C | t1E ⇒ t0F | t1F ⇒ t0E ]
 516  | t12 ⇒ match e2 with
 517   [ t00 ⇒ t12 | t01 ⇒ t13 | t02 ⇒ t10 | t03 ⇒ t11 | t04 ⇒ t16 | t05 ⇒ t17 | t06 ⇒ t14 | t07 ⇒ t15
 518   | t08 ⇒ t1A | t09 ⇒ t1B | t0A ⇒ t18 | t0B ⇒ t19 | t0C ⇒ t1E | t0D ⇒ t1F | t0E ⇒ t1C | t0F ⇒ t1D
 519   | t10 ⇒ t02 | t11 ⇒ t03 | t12 ⇒ t00 | t13 ⇒ t01 | t14 ⇒ t06 | t15 ⇒ t07 | t16 ⇒ t04 | t17 ⇒ t05
 520   | t18 ⇒ t0A | t19 ⇒ t0B | t1A ⇒ t08 | t1B ⇒ t09 | t1C ⇒ t0E | t1D ⇒ t0F | t1E ⇒ t0C | t1F ⇒ t0D ]
 521  | t13 ⇒ match e2 with
 522   [ t00 ⇒ t13 | t01 ⇒ t12 | t02 ⇒ t11 | t03 ⇒ t10 | t04 ⇒ t17 | t05 ⇒ t16 | t06 ⇒ t15 | t07 ⇒ t14
 523   | t08 ⇒ t1B | t09 ⇒ t1A | t0A ⇒ t19 | t0B ⇒ t18 | t0C ⇒ t1F | t0D ⇒ t1E | t0E ⇒ t1D | t0F ⇒ t1C
 524   | t10 ⇒ t03 | t11 ⇒ t02 | t12 ⇒ t01 | t13 ⇒ t00 | t14 ⇒ t07 | t15 ⇒ t06 | t16 ⇒ t05 | t17 ⇒ t04
 525   | t18 ⇒ t0B | t19 ⇒ t0A | t1A ⇒ t09 | t1B ⇒ t08 | t1C ⇒ t0F | t1D ⇒ t0E | t1E ⇒ t0D | t1F ⇒ t0C ]
 526  | t14 ⇒ match e2 with
 527   [ t00 ⇒ t14 | t01 ⇒ t15 | t02 ⇒ t16 | t03 ⇒ t17 | t04 ⇒ t10 | t05 ⇒ t11 | t06 ⇒ t12 | t07 ⇒ t13
 528   | t08 ⇒ t1C | t09 ⇒ t1D | t0A ⇒ t1E | t0B ⇒ t1F | t0C ⇒ t18 | t0D ⇒ t19 | t0E ⇒ t1A | t0F ⇒ t1B
 529   | t10 ⇒ t04 | t11 ⇒ t05 | t12 ⇒ t06 | t13 ⇒ t07 | t14 ⇒ t00 | t15 ⇒ t01 | t16 ⇒ t02 | t17 ⇒ t03
 530   | t18 ⇒ t0C | t19 ⇒ t0D | t1A ⇒ t0E | t1B ⇒ t0F | t1C ⇒ t08 | t1D ⇒ t09 | t1E ⇒ t0A | t1F ⇒ t0B ]
 531  | t15 ⇒ match e2 with
 532   [ t00 ⇒ t15 | t01 ⇒ t14 | t02 ⇒ t17 | t03 ⇒ t16 | t04 ⇒ t11 | t05 ⇒ t10 | t06 ⇒ t13 | t07 ⇒ t12
 533   | t08 ⇒ t1D | t09 ⇒ t1C | t0A ⇒ t1F | t0B ⇒ t1E | t0C ⇒ t19 | t0D ⇒ t18 | t0E ⇒ t1B | t0F ⇒ t1A
 534   | t10 ⇒ t05 | t11 ⇒ t04 | t12 ⇒ t07 | t13 ⇒ t06 | t14 ⇒ t01 | t15 ⇒ t00 | t16 ⇒ t03 | t17 ⇒ t02
 535   | t18 ⇒ t0D | t19 ⇒ t0C | t1A ⇒ t0F | t1B ⇒ t0E | t1C ⇒ t09 | t1D ⇒ t08 | t1E ⇒ t0B | t1F ⇒ t0A ]
 536  | t16 ⇒ match e2 with
 537   [ t00 ⇒ t16 | t01 ⇒ t17 | t02 ⇒ t14 | t03 ⇒ t15 | t04 ⇒ t12 | t05 ⇒ t13 | t06 ⇒ t10 | t07 ⇒ t11
 538   | t08 ⇒ t1E | t09 ⇒ t1F | t0A ⇒ t1C | t0B ⇒ t1D | t0C ⇒ t1A | t0D ⇒ t1B | t0E ⇒ t18 | t0F ⇒ t19
 539   | t10 ⇒ t06 | t11 ⇒ t07 | t12 ⇒ t04 | t13 ⇒ t05 | t14 ⇒ t02 | t15 ⇒ t03 | t16 ⇒ t00 | t17 ⇒ t01
 540   | t18 ⇒ t0E | t19 ⇒ t0F | t1A ⇒ t0C | t1B ⇒ t0D | t1C ⇒ t0A | t1D ⇒ t0B | t1E ⇒ t08 | t1F ⇒ t09 ]
 541  | t17 ⇒ match e2 with
 542   [ t00 ⇒ t17 | t01 ⇒ t16 | t02 ⇒ t15 | t03 ⇒ t14 | t04 ⇒ t13 | t05 ⇒ t12 | t06 ⇒ t11 | t07 ⇒ t10
 543   | t08 ⇒ t1F | t09 ⇒ t1E | t0A ⇒ t1D | t0B ⇒ t1C | t0C ⇒ t1B | t0D ⇒ t1A | t0E ⇒ t19 | t0F ⇒ t18
 544   | t10 ⇒ t07 | t11 ⇒ t06 | t12 ⇒ t05 | t13 ⇒ t04 | t14 ⇒ t03 | t15 ⇒ t02 | t16 ⇒ t01 | t17 ⇒ t00
 545   | t18 ⇒ t0F | t19 ⇒ t0E | t1A ⇒ t0D | t1B ⇒ t0C | t1C ⇒ t0B | t1D ⇒ t0A | t1E ⇒ t09 | t1F ⇒ t08 ]
 546  | t18 ⇒ match e2 with
 547   [ t00 ⇒ t18 | t01 ⇒ t19 | t02 ⇒ t1A | t03 ⇒ t1B | t04 ⇒ t1C | t05 ⇒ t1D | t06 ⇒ t1E | t07 ⇒ t1F
 548   | t08 ⇒ t10 | t09 ⇒ t11 | t0A ⇒ t12 | t0B ⇒ t13 | t0C ⇒ t14 | t0D ⇒ t15 | t0E ⇒ t16 | t0F ⇒ t17
 549   | t10 ⇒ t08 | t11 ⇒ t09 | t12 ⇒ t0A | t13 ⇒ t0B | t14 ⇒ t0C | t15 ⇒ t0D | t16 ⇒ t0E | t17 ⇒ t0F
 550   | t18 ⇒ t00 | t19 ⇒ t01 | t1A ⇒ t02 | t1B ⇒ t03 | t1C ⇒ t04 | t1D ⇒ t05 | t1E ⇒ t06 | t1F ⇒ t07 ]
 551  | t19 ⇒ match e2 with
 552   [ t00 ⇒ t19 | t01 ⇒ t18 | t02 ⇒ t1B | t03 ⇒ t1A | t04 ⇒ t1D | t05 ⇒ t1C | t06 ⇒ t1F | t07 ⇒ t1E
 553   | t08 ⇒ t11 | t09 ⇒ t10 | t0A ⇒ t13 | t0B ⇒ t12 | t0C ⇒ t15 | t0D ⇒ t14 | t0E ⇒ t17 | t0F ⇒ t16
 554   | t10 ⇒ t09 | t11 ⇒ t08 | t12 ⇒ t0B | t13 ⇒ t0A | t14 ⇒ t0D | t15 ⇒ t0C | t16 ⇒ t0F | t17 ⇒ t0E
 555   | t18 ⇒ t01 | t19 ⇒ t00 | t1A ⇒ t03 | t1B ⇒ t02 | t1C ⇒ t05 | t1D ⇒ t04 | t1E ⇒ t07 | t1F ⇒ t06 ]
 556  | t1A ⇒ match e2 with
 557   [ t00 ⇒ t1A | t01 ⇒ t1B | t02 ⇒ t18 | t03 ⇒ t19 | t04 ⇒ t1E | t05 ⇒ t1F | t06 ⇒ t1C | t07 ⇒ t1D
 558   | t08 ⇒ t12 | t09 ⇒ t13 | t0A ⇒ t10 | t0B ⇒ t11 | t0C ⇒ t16 | t0D ⇒ t17 | t0E ⇒ t14 | t0F ⇒ t15
 559   | t10 ⇒ t0A | t11 ⇒ t0B | t12 ⇒ t08 | t13 ⇒ t09 | t14 ⇒ t0E | t15 ⇒ t0F | t16 ⇒ t0C | t17 ⇒ t0D
 560   | t18 ⇒ t02 | t19 ⇒ t03 | t1A ⇒ t00 | t1B ⇒ t01 | t1C ⇒ t06 | t1D ⇒ t07 | t1E ⇒ t04 | t1F ⇒ t05 ]
 561  | t1B ⇒ match e2 with
 562   [ t00 ⇒ t1B | t01 ⇒ t1A | t02 ⇒ t19 | t03 ⇒ t18 | t04 ⇒ t1F | t05 ⇒ t1E | t06 ⇒ t1D | t07 ⇒ t1C
 563   | t08 ⇒ t13 | t09 ⇒ t12 | t0A ⇒ t11 | t0B ⇒ t10 | t0C ⇒ t17 | t0D ⇒ t16 | t0E ⇒ t15 | t0F ⇒ t14
 564   | t10 ⇒ t0B | t11 ⇒ t0A | t12 ⇒ t09 | t13 ⇒ t08 | t14 ⇒ t0F | t15 ⇒ t0E | t16 ⇒ t0D | t17 ⇒ t0C
 565   | t18 ⇒ t03 | t19 ⇒ t02 | t1A ⇒ t01 | t1B ⇒ t00 | t1C ⇒ t07 | t1D ⇒ t06 | t1E ⇒ t05 | t1F ⇒ t04 ]
 566  | t1C ⇒ match e2 with
 567   [ t00 ⇒ t1C | t01 ⇒ t1D | t02 ⇒ t1E | t03 ⇒ t1F | t04 ⇒ t18 | t05 ⇒ t19 | t06 ⇒ t1A | t07 ⇒ t1B
 568   | t08 ⇒ t14 | t09 ⇒ t15 | t0A ⇒ t16 | t0B ⇒ t17 | t0C ⇒ t10 | t0D ⇒ t11 | t0E ⇒ t12 | t0F ⇒ t13
 569   | t10 ⇒ t0C | t11 ⇒ t0D | t12 ⇒ t0E | t13 ⇒ t0F | t14 ⇒ t08 | t15 ⇒ t09 | t16 ⇒ t0A | t17 ⇒ t0B
 570   | t18 ⇒ t04 | t19 ⇒ t05 | t1A ⇒ t06 | t1B ⇒ t07 | t1C ⇒ t00 | t1D ⇒ t01 | t1E ⇒ t02 | t1F ⇒ t03 ]
 571  | t1D ⇒ match e2 with
 572   [ t00 ⇒ t1D | t01 ⇒ t1C | t02 ⇒ t1F | t03 ⇒ t1E | t04 ⇒ t19 | t05 ⇒ t18 | t06 ⇒ t1B | t07 ⇒ t1A
 573   | t08 ⇒ t15 | t09 ⇒ t14 | t0A ⇒ t17 | t0B ⇒ t16 | t0C ⇒ t11 | t0D ⇒ t10 | t0E ⇒ t13 | t0F ⇒ t12
 574   | t10 ⇒ t0D | t11 ⇒ t0C | t12 ⇒ t0F | t13 ⇒ t0E | t14 ⇒ t09 | t15 ⇒ t08 | t16 ⇒ t0B | t17 ⇒ t0A
 575   | t18 ⇒ t05 | t19 ⇒ t04 | t1A ⇒ t07 | t1B ⇒ t06 | t1C ⇒ t01 | t1D ⇒ t00 | t1E ⇒ t03 | t1F ⇒ t02 ]
 576  | t1E ⇒ match e2 with
 577   [ t00 ⇒ t1E | t01 ⇒ t1F | t02 ⇒ t1C | t03 ⇒ t1D | t04 ⇒ t1A | t05 ⇒ t1B | t06 ⇒ t18 | t07 ⇒ t19
 578   | t08 ⇒ t16 | t09 ⇒ t17 | t0A ⇒ t14 | t0B ⇒ t15 | t0C ⇒ t12 | t0D ⇒ t13 | t0E ⇒ t10 | t0F ⇒ t11
 579   | t10 ⇒ t0E | t11 ⇒ t0F | t12 ⇒ t0C | t13 ⇒ t0D | t14 ⇒ t0A | t15 ⇒ t0B | t16 ⇒ t08 | t17 ⇒ t09
 580   | t18 ⇒ t06 | t19 ⇒ t07 | t1A ⇒ t04 | t1B ⇒ t05 | t1C ⇒ t02 | t1D ⇒ t03 | t1E ⇒ t00 | t1F ⇒ t01 ]
 581  | t1F ⇒ match e2 with
 582   [ t00 ⇒ t1F | t01 ⇒ t1E | t02 ⇒ t1D | t03 ⇒ t1C | t04 ⇒ t1B | t05 ⇒ t1A | t06 ⇒ t19 | t07 ⇒ t18
 583   | t08 ⇒ t17 | t09 ⇒ t16 | t0A ⇒ t15 | t0B ⇒ t14 | t0C ⇒ t13 | t0D ⇒ t12 | t0E ⇒ t11 | t0F ⇒ t10
 584   | t10 ⇒ t0F | t11 ⇒ t0E | t12 ⇒ t0D | t13 ⇒ t0C | t14 ⇒ t0B | t15 ⇒ t0A | t16 ⇒ t09 | t17 ⇒ t08
 585   | t18 ⇒ t07 | t19 ⇒ t06 | t1A ⇒ t05 | t1B ⇒ t04 | t1C ⇒ t03 | t1D ⇒ t02 | t1E ⇒ t01 | t1F ⇒ t00 ]
 586  ].
 587
 588 (* operatore predecessore *)
 589 ndefinition pred_bit ≝
 590 λn.match n with
 591  [ t00 ⇒ t1F | t01 ⇒ t00 | t02 ⇒ t01 | t03 ⇒ t02 | t04 ⇒ t03 | t05 ⇒ t04 | t06 ⇒ t05 | t07 ⇒ t06
 592  | t08 ⇒ t07 | t09 ⇒ t08 | t0A ⇒ t09 | t0B ⇒ t0A | t0C ⇒ t0B | t0D ⇒ t0C | t0E ⇒ t0D | t0F ⇒ t0E
 593  | t10 ⇒ t0F | t11 ⇒ t10 | t12 ⇒ t11 | t13 ⇒ t12 | t14 ⇒ t13 | t15 ⇒ t14 | t16 ⇒ t15 | t17 ⇒ t16
 594  | t18 ⇒ t17 | t19 ⇒ t18 | t1A ⇒ t19 | t1B ⇒ t1A | t1C ⇒ t1B | t1D ⇒ t1C | t1E ⇒ t1D | t1F ⇒ t0E
 595  ].
 596
 597 (* operatore successore *)
 598 ndefinition succ_bit ≝
 599 λn.match n with
 600  [ t00 ⇒ t01 | t01 ⇒ t02 | t02 ⇒ t03 | t03 ⇒ t04 | t04 ⇒ t05 | t05 ⇒ t06 | t06 ⇒ t07 | t07 ⇒ t08
 601  | t08 ⇒ t09 | t09 ⇒ t0A | t0A ⇒ t0B | t0B ⇒ t0C | t0C ⇒ t0D | t0D ⇒ t0E | t0E ⇒ t0F | t0F ⇒ t10
 602  | t10 ⇒ t11 | t11 ⇒ t12 | t12 ⇒ t13 | t13 ⇒ t14 | t14 ⇒ t15 | t15 ⇒ t16 | t16 ⇒ t17 | t17 ⇒ t18
 603  | t18 ⇒ t19 | t19 ⇒ t1A | t1A ⇒ t1B | t1B ⇒ t1C | t1C ⇒ t1D | t1D ⇒ t1E | t1E ⇒ t1F | t1F ⇒ t00
 604  ].
 605
 606 (* bitrigesimali ricorsivi *)
 607 ninductive rec_bitrigesim : bitrigesim → Type ≝
 608   bi_O : rec_bitrigesim t00
 609 | bi_S : ∀n.rec_bitrigesim n → rec_bitrigesim (succ_bit n).
 610
 611 (* bitrigesimali → bitrigesimali ricorsivi *)
 612 ndefinition bit_to_recbit ≝
 613 λn.match n return λx.rec_bitrigesim x with
 614  [ t00 ⇒ bi_O
 615  | t01 ⇒ bi_S ? bi_O
 616  | t02 ⇒ bi_S ? (bi_S ? bi_O)
 617  | t03 ⇒ bi_S ? (bi_S ? (bi_S ? bi_O))
 618  | t04 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))
 619  | t05 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))
 620  | t06 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))
 621  | t07 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))
 622  | t08 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 623          bi_O)))))))
 624  | t09 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 625         (bi_S ? bi_O))))))))
 626  | t0A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 627         (bi_S ? (bi_S ? bi_O)))))))))
 628  | t0B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 629         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))
 630  | t0C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 631         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))
 632  | t0D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 633         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))
 634  | t0E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 635         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))
 636  | t0F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 637         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))
 638  | t10 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 639         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 640          bi_O)))))))))))))))
 641  | t11 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 642         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 643         (bi_S ? bi_O))))))))))))))))
 644  | t12 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 645         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 646         (bi_S ? (bi_S ? bi_O)))))))))))))))))
 647  | t13 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 648         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 649         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))
 650  | t14 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 651         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 652         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))
 653  | t15 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 654         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 655         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))
 656  | t16 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 657         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 658         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))
 659  | t17 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 660         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 661         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))
 662  | t18 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 663         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 664         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 665          bi_O)))))))))))))))))))))))
 666  | t19 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 667         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 668         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 669         (bi_S ? bi_O))))))))))))))))))))))))
 670  | t1A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 671         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 672         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 673         (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))
 674  | t1B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 675         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 676         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 677         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))
 678  | t1C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 679         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 680         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 681         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))
 682  | t1D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 683         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 684         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 685         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))
 686  | t1E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 687         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 688         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 689         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))))
 690  | t1F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 691         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 692         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 693         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))))
 694  ].
 695
 696 ndefinition bitrigesim_destruct_aux ≝
 697 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
 698  match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ P ].
 699
 700 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
 701  #t1; #t2; #P; #H;
 702  nrewrite < H;
 703  nelim t1;
 704  nnormalize;
 705  napply (λx.x).
 706 nqed.
 707
 708 nlemma eq_to_eqbit : ∀n1,n2.n1 = n2 → eq_bit n1 n2 = true.
 709  #n1; #n2; #H;
 710  nrewrite > H;
 711  nelim n2;
 712  nnormalize;
 713  napply refl_eq.
 714 nqed.
 715
 716 nlemma neqbit_to_neq : ∀n1,n2.eq_bit n1 n2 = false → n1 ≠ n2.
 717  #n1; #n2; #H;
 718  napply (not_to_not (n1 = n2) (eq_bit n1 n2 = true) …);
 719  ##[ ##1: napply (eq_to_eqbit n1 n2)
 720  ##| ##2: napply (eqfalse_to_neqtrue … H)
 721  ##]
 722 nqed.
 723
 724 (* !!! per brevita... *)
 725 naxiom eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
 726
 727 nlemma neq_to_neqbit : ∀n1,n2.n1 ≠ n2 → eq_bit n1 n2 = false.
 728  #n1; #n2; #H;
 729  napply (neqtrue_to_eqfalse (eq_bit n1 n2));
 730  napply (not_to_not (eq_bit n1 n2 = true) (n1 = n2) ? H);
 731  napply (eqbit_to_eq n1 n2).
 732 nqed.
 733
 734 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
 735  #x; #y; nnormalize;
 736  napply (or2_elim (eq_bit x y = true) (eq_bit x y = false) ? (decidable_bexpr ?));
 737  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqbit_to_eq … H))
 738  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqbit_to_neq … H))
 739  ##]
 740 nqed.
 741
 742 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
 743  #n1; #n2;
 744  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_bit n1 n2));
 745  ##[ ##1: #H; nrewrite > H; napply refl_eq
 746  ##| ##2: #H; nrewrite > (neq_to_neqbit n1 n2 H);
 747           napply (symmetric_eq ? (eq_bit n2 n1) false);
 748           napply (neq_to_neqbit n2 n1 (symmetric_neq ? n1 n2 H))
 749  ##]
 750 nqed.
 751
 752 nlemma bitrigesim_is_comparable : comparable.
 753  @ bitrigesim
 754   ##[ napply t00
 755   ##| napply forall_bit
 756   ##| napply eq_bit
 757   ##| napply eqbit_to_eq
 758   ##| napply eq_to_eqbit
 759   ##| napply neqbit_to_neq
 760   ##| napply neq_to_neqbit
 761   ##| napply decidable_bit
 762   ##| napply symmetric_eqbit
 763   ##]
 764 nqed.
 765
 766 unification hint 0 ≔ ⊢ carr bitrigesim_is_comparable ≡ bitrigesim.