1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "common/comp.ma".
24 include "num/bool_lemmas.ma".
30 ninductive bitrigesim : Type ≝
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 ]
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.
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 ]
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 ]
424 ndefinition xor_bit ≝
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 ]
588 (* operatore predecessore *)
589 ndefinition pred_bit ≝
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
597 (* operatore successore *)
598 ndefinition succ_bit ≝
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
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).
611 (* bitrigesimali → bitrigesimali ricorsivi *)
612 ndefinition bit_to_recbit ≝
613 λn.match n return λx.rec_bitrigesim x with
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 ?
624 | t09 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
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 ?
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))))))))))))))))))))))))))))))
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 ].
700 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
708 nlemma eq_to_eqbit : ∀n1,n2.n1 = n2 → eq_bit n1 n2 = true.
716 nlemma neqbit_to_neq : ∀n1,n2.eq_bit n1 n2 = false → n1 ≠ n2.
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)
724 (* !!! per brevita... *)
725 naxiom eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
727 nlemma neq_to_neqbit : ∀n1,n2.n1 ≠ n2 → eq_bit n1 n2 = false.
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).
734 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
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))
742 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
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))
752 nlemma bitrigesim_is_comparable : comparable.
755 ##| napply forall_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
766 unification hint 0 ≔ ⊢ carr bitrigesim_is_comparable ≡ bitrigesim.