helm/software/matita/contribs/ng_assembly/common/meta_type.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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/list_utility_lemmas.ma".
  24
  25 nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  26  match l with
  27   [ nil ⇒ true
  28   | cons h t ⇒ match f elem h with
  29    [ true ⇒ false | false ⇒ nmember_list T elem f t ]
  30   ].
  31
  32 (* elem presente una ed una sola volta in l *)
  33 nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  34  match l with
  35   [ nil ⇒ false
  36   | cons h t ⇒ match f elem h with
  37     [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ]
  38   ].
  39
  40 (* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
  41 ninductive UN : Type ≝
  42 (* quaternari[4] 1-4 *)
  43   uq0 : UN
  44 | uq1 : UN
  45 | uq2 : UN
  46 | uq3 : UN
  47
  48 (* ottali[8] 5-12 *)
  49 | uo0 : UN
  50 | uo1 : UN
  51 | uo2 : UN
  52 | uo3 : UN
  53 | uo4 : UN
  54 | uo5 : UN
  55 | uo6 : UN
  56 | uo7 : UN
  57
  58 (* esadecimali[16] 13-28 *)
  59 | ux0 : UN
  60 | ux1 : UN
  61 | ux2 : UN
  62 | ux3 : UN
  63 | ux4 : UN
  64 | ux5 : UN
  65 | ux6 : UN
  66 | ux7 : UN
  67 | ux8 : UN
  68 | ux9 : UN
  69 | uxA : UN
  70 | uxB : UN
  71 | uxC : UN
  72 | uxD : UN
  73 | uxE : UN
  74 | uxF : UN
  75
  76 (* bitrigesimali[32] 29-60 *)
  77 | ut00 : UN
  78 | ut01 : UN
  79 | ut02 : UN
  80 | ut03 : UN
  81 | ut04 : UN
  82 | ut05 : UN
  83 | ut06 : UN
  84 | ut07 : UN
  85 | ut08 : UN
  86 | ut09 : UN
  87 | ut0A : UN
  88 | ut0B : UN
  89 | ut0C : UN
  90 | ut0D : UN
  91 | ut0E : UN
  92 | ut0F : UN
  93 | ut10 : UN
  94 | ut11 : UN
  95 | ut12 : UN
  96 | ut13 : UN
  97 | ut14 : UN
  98 | ut15 : UN
  99 | ut16 : UN
 100 | ut17 : UN
 101 | ut18 : UN
 102 | ut19 : UN
 103 | ut1A : UN
 104 | ut1B : UN
 105 | ut1C : UN
 106 | ut1D : UN
 107 | ut1E : UN
 108 | ut1F : UN
 109
 110 (* ascii[63] 61-123 *)
 111 | uch_0 : UN
 112 | uch_1 : UN
 113 | uch_2 : UN
 114 | uch_3 : UN
 115 | uch_4 : UN
 116 | uch_5 : UN
 117 | uch_6 : UN
 118 | uch_7 : UN
 119 | uch_8 : UN
 120 | uch_9 : UN
 121 | uch__ : UN
 122 | uch_A : UN
 123 | uch_B : UN
 124 | uch_C : UN
 125 | uch_D : UN
 126 | uch_E : UN
 127 | uch_F : UN
 128 | uch_G : UN
 129 | uch_H : UN
 130 | uch_I : UN
 131 | uch_J : UN
 132 | uch_K : UN
 133 | uch_L : UN
 134 | uch_M : UN
 135 | uch_N : UN
 136 | uch_O : UN
 137 | uch_P : UN
 138 | uch_Q : UN
 139 | uch_R : UN
 140 | uch_S : UN
 141 | uch_T : UN
 142 | uch_U : UN
 143 | uch_V : UN
 144 | uch_W : UN
 145 | uch_X : UN
 146 | uch_Y : UN
 147 | uch_Z : UN
 148 | uch_a : UN
 149 | uch_b : UN
 150 | uch_c : UN
 151 | uch_d : UN
 152 | uch_e : UN
 153 | uch_f : UN
 154 | uch_g : UN
 155 | uch_h : UN
 156 | uch_i : UN
 157 | uch_j : UN
 158 | uch_k : UN
 159 | uch_l : UN
 160 | uch_m : UN
 161 | uch_n : UN
 162 | uch_o : UN
 163 | uch_p : UN
 164 | uch_q : UN
 165 | uch_r : UN
 166 | uch_s : UN
 167 | uch_t : UN
 168 | uch_u : UN
 169 | uch_v : UN
 170 | uch_w : UN
 171 | uch_x : UN
 172 | uch_y : UN
 173 | uch_z : UN
 174
 175 (* opcode[91] 124-214 *)
 176 | ADC    : UN
 177 | ADD    : UN
 178 | AIS    : UN
 179 | AIX    : UN
 180 | AND    : UN
 181 | ASL    : UN
 182 | ASR    : UN
 183 | BCC    : UN
 184 | BCLRn  : UN
 185 | BCS    : UN
 186 | BEQ    : UN
 187 | BGE    : UN
 188 | BGND   : UN
 189 | BGT    : UN
 190 | BHCC   : UN
 191 | BHCS   : UN
 192 | BHI    : UN
 193 | BIH    : UN
 194 | BIL    : UN
 195 | BIT    : UN
 196 | BLE    : UN
 197 | BLS    : UN
 198 | BLT    : UN
 199 | BMC    : UN
 200 | BMI    : UN
 201 | BMS    : UN
 202 | BNE    : UN
 203 | BPL    : UN
 204 | BRA    : UN
 205 | BRCLRn : UN
 206 | BRN    : UN
 207 | BRSETn : UN
 208 | BSETn  : UN
 209 | BSR    : UN
 210 | CBEQA  : UN
 211 | CBEQX  : UN
 212 | CLC    : UN
 213 | CLI    : UN
 214 | CLR    : UN
 215 | CMP    : UN
 216 | COM    : UN
 217 | CPHX   : UN
 218 | CPX    : UN
 219 | DAA    : UN
 220 | DBNZ   : UN
 221 | DEC    : UN
 222 | DIV    : UN
 223 | EOR    : UN
 224 | INC    : UN
 225 | JMP    : UN
 226 | JSR    : UN
 227 | LDA    : UN
 228 | LDHX   : UN
 229 | LDX    : UN
 230 | LSR    : UN
 231 | MOV    : UN
 232 | MUL    : UN
 233 | NEG    : UN
 234 | NOP    : UN
 235 | NSA    : UN
 236 | ORA    : UN
 237 | PSHA   : UN
 238 | PSHH   : UN
 239 | PSHX   : UN
 240 | PULA   : UN
 241 | PULH   : UN
 242 | PULX   : UN
 243 | ROL    : UN
 244 | ROR    : UN
 245 | RSP    : UN
 246 | RTI    : UN
 247 | RTS    : UN
 248 | SBC    : UN
 249 | SEC    : UN
 250 | SEI    : UN
 251 | SHA    : UN
 252 | SLA    : UN
 253 | STA    : UN
 254 | STHX   : UN
 255 | STOP   : UN
 256 | STX    : UN
 257 | SUB    : UN
 258 | SWI    : UN
 259 | TAP    : UN
 260 | TAX    : UN
 261 | TPA    : UN
 262 | TST    : UN
 263 | TSX    : UN
 264 | TXA    : UN
 265 | TXS    : UN
 266 | WAIT   : UN
 267 .
 268
 269 (* funzione di uguaglianza sugli atomi *)
 270 ndefinition eq_UN ≝
 271 λu1,u2.match u1 with
 272  [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ]
 273  | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ]
 274  | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ]
 275  | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ]
 276
 277  | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ]
 278  | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ]
 279  | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ]
 280  | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ]
 281  | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ]
 282  | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ]
 283  | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ]
 284  | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ]
 285
 286  | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ]
 287  | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ]
 288  | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ]
 289  | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ]
 290  | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ]
 291  | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ]
 292  | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ]
 293  | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ]
 294  | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ]
 295  | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ]
 296  | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ]
 297  | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ]
 298  | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ]
 299  | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ]
 300  | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ]
 301  | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ]
 302
 303  | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ]
 304  | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ]
 305  | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ]
 306  | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ]
 307  | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ]
 308  | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ]
 309  | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ]
 310  | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ]
 311  | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ]
 312  | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ]
 313  | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ]
 314  | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ]
 315  | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ]
 316  | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ]
 317  | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ]
 318  | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ]
 319  | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ]
 320  | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ]
 321  | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ]
 322  | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ]
 323  | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ]
 324  | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ]
 325  | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ]
 326  | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ]
 327  | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ]
 328  | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ]
 329  | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ]
 330  | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ]
 331  | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ]
 332  | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ]
 333  | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ]
 334  | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ]
 335
 336  | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ]
 337  | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ]
 338  | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ]
 339  | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ]
 340  | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ]
 341  | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ]
 342  | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ]
 343  | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ]
 344  | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ]
 345  | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ]
 346  | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ]
 347  | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ]
 348  | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ]
 349  | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ]
 350  | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ]
 351  | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ]
 352  | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ]
 353  | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ]
 354  | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ]
 355  | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ]
 356  | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ]
 357  | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ]
 358  | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ]
 359  | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ]
 360  | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ]
 361  | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ]
 362  | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ]
 363  | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ]
 364  | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ]
 365  | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ]
 366  | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ]
 367  | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ]
 368  | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ]
 369  | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ]
 370  | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ]
 371  | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ]
 372  | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ]
 373  | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ]
 374  | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ]
 375  | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ]
 376  | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ]
 377  | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ]
 378  | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ]
 379  | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ]
 380  | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ]
 381  | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ]
 382  | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ]
 383  | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ]
 384  | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ]
 385  | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ]
 386  | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ]
 387  | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ]
 388  | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ]
 389  | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ]
 390  | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ]
 391  | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ]
 392  | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ]
 393  | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ]
 394  | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ]
 395  | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ]
 396  | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ]
 397  | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ]
 398  | uch_z ⇒ match u2 with [ uch_z ⇒ true | _ ⇒ false ]
 399
 400  | ADC    ⇒ match u2 with [ ADC    ⇒ true | _ ⇒ false ]
 401  | ADD    ⇒ match u2 with [ ADD    ⇒ true | _ ⇒ false ]
 402  | AIS    ⇒ match u2 with [ AIS    ⇒ true | _ ⇒ false ]
 403  | AIX    ⇒ match u2 with [ AIX    ⇒ true | _ ⇒ false ]
 404  | AND    ⇒ match u2 with [ AND    ⇒ true | _ ⇒ false ]
 405  | ASL    ⇒ match u2 with [ ASL    ⇒ true | _ ⇒ false ]
 406  | ASR    ⇒ match u2 with [ ASR    ⇒ true | _ ⇒ false ]
 407  | BCC    ⇒ match u2 with [ BCC    ⇒ true | _ ⇒ false ]
 408  | BCLRn  ⇒ match u2 with [ BCLRn  ⇒ true | _ ⇒ false ]
 409  | BCS    ⇒ match u2 with [ BCS    ⇒ true | _ ⇒ false ]
 410  | BEQ    ⇒ match u2 with [ BEQ    ⇒ true | _ ⇒ false ]
 411  | BGE    ⇒ match u2 with [ BGE    ⇒ true | _ ⇒ false ]
 412  | BGND   ⇒ match u2 with [ BGND   ⇒ true | _ ⇒ false ]
 413  | BGT    ⇒ match u2 with [ BGT    ⇒ true | _ ⇒ false ]
 414  | BHCC   ⇒ match u2 with [ BHCC   ⇒ true | _ ⇒ false ]
 415  | BHCS   ⇒ match u2 with [ BHCS   ⇒ true | _ ⇒ false ]
 416  | BHI    ⇒ match u2 with [ BHI    ⇒ true | _ ⇒ false ]
 417  | BIH    ⇒ match u2 with [ BIH    ⇒ true | _ ⇒ false ]
 418  | BIL    ⇒ match u2 with [ BIL    ⇒ true | _ ⇒ false ]
 419  | BIT    ⇒ match u2 with [ BIT    ⇒ true | _ ⇒ false ]
 420  | BLE    ⇒ match u2 with [ BLE    ⇒ true | _ ⇒ false ]
 421  | BLS    ⇒ match u2 with [ BLS    ⇒ true | _ ⇒ false ]
 422  | BLT    ⇒ match u2 with [ BLT    ⇒ true | _ ⇒ false ]
 423  | BMC    ⇒ match u2 with [ BMC    ⇒ true | _ ⇒ false ]
 424  | BMI    ⇒ match u2 with [ BMI    ⇒ true | _ ⇒ false ]
 425  | BMS    ⇒ match u2 with [ BMS    ⇒ true | _ ⇒ false ]
 426  | BNE    ⇒ match u2 with [ BNE    ⇒ true | _ ⇒ false ]
 427  | BPL    ⇒ match u2 with [ BPL    ⇒ true | _ ⇒ false ]
 428  | BRA    ⇒ match u2 with [ BRA    ⇒ true | _ ⇒ false ]
 429  | BRCLRn ⇒ match u2 with [ BRCLRn ⇒ true | _ ⇒ false ]
 430  | BRN    ⇒ match u2 with [ BRN    ⇒ true | _ ⇒ false ]
 431  | BRSETn ⇒ match u2 with [ BRSETn ⇒ true | _ ⇒ false ]
 432  | BSETn  ⇒ match u2 with [ BSETn  ⇒ true | _ ⇒ false ]
 433  | BSR    ⇒ match u2 with [ BSR    ⇒ true | _ ⇒ false ]
 434  | CBEQA  ⇒ match u2 with [ CBEQA  ⇒ true | _ ⇒ false ]
 435  | CBEQX  ⇒ match u2 with [ CBEQX  ⇒ true | _ ⇒ false ]
 436  | CLC    ⇒ match u2 with [ CLC    ⇒ true | _ ⇒ false ]
 437  | CLI    ⇒ match u2 with [ CLI    ⇒ true | _ ⇒ false ]
 438  | CLR    ⇒ match u2 with [ CLR    ⇒ true | _ ⇒ false ]
 439  | CMP    ⇒ match u2 with [ CMP    ⇒ true | _ ⇒ false ]
 440  | COM    ⇒ match u2 with [ COM    ⇒ true | _ ⇒ false ]
 441  | CPHX   ⇒ match u2 with [ CPHX   ⇒ true | _ ⇒ false ]
 442  | CPX    ⇒ match u2 with [ CPX    ⇒ true | _ ⇒ false ]
 443  | DAA    ⇒ match u2 with [ DAA    ⇒ true | _ ⇒ false ]
 444  | DBNZ   ⇒ match u2 with [ DBNZ   ⇒ true | _ ⇒ false ]
 445  | DEC    ⇒ match u2 with [ DEC    ⇒ true | _ ⇒ false ]
 446  | DIV    ⇒ match u2 with [ DIV    ⇒ true | _ ⇒ false ]
 447  | EOR    ⇒ match u2 with [ EOR    ⇒ true | _ ⇒ false ]
 448  | INC    ⇒ match u2 with [ INC    ⇒ true | _ ⇒ false ]
 449  | JMP    ⇒ match u2 with [ JMP    ⇒ true | _ ⇒ false ]
 450  | JSR    ⇒ match u2 with [ JSR    ⇒ true | _ ⇒ false ]
 451  | LDA    ⇒ match u2 with [ LDA    ⇒ true | _ ⇒ false ]
 452  | LDHX   ⇒ match u2 with [ LDHX   ⇒ true | _ ⇒ false ]
 453  | LDX    ⇒ match u2 with [ LDX    ⇒ true | _ ⇒ false ]
 454  | LSR    ⇒ match u2 with [ LSR    ⇒ true | _ ⇒ false ]
 455  | MOV    ⇒ match u2 with [ MOV    ⇒ true | _ ⇒ false ]
 456  | MUL    ⇒ match u2 with [ MUL    ⇒ true | _ ⇒ false ]
 457  | NEG    ⇒ match u2 with [ NEG    ⇒ true | _ ⇒ false ]
 458  | NOP    ⇒ match u2 with [ NOP    ⇒ true | _ ⇒ false ]
 459  | NSA    ⇒ match u2 with [ NSA    ⇒ true | _ ⇒ false ]
 460  | ORA    ⇒ match u2 with [ ORA    ⇒ true | _ ⇒ false ]
 461  | PSHA   ⇒ match u2 with [ PSHA   ⇒ true | _ ⇒ false ]
 462  | PSHH   ⇒ match u2 with [ PSHH   ⇒ true | _ ⇒ false ]
 463  | PSHX   ⇒ match u2 with [ PSHX   ⇒ true | _ ⇒ false ]
 464  | PULA   ⇒ match u2 with [ PULA   ⇒ true | _ ⇒ false ]
 465  | PULH   ⇒ match u2 with [ PULH   ⇒ true | _ ⇒ false ]
 466  | PULX   ⇒ match u2 with [ PULX   ⇒ true | _ ⇒ false ]
 467  | ROL    ⇒ match u2 with [ ROL    ⇒ true | _ ⇒ false ]
 468  | ROR    ⇒ match u2 with [ ROR    ⇒ true | _ ⇒ false ]
 469  | RSP    ⇒ match u2 with [ RSP    ⇒ true | _ ⇒ false ]
 470  | RTI    ⇒ match u2 with [ RTI    ⇒ true | _ ⇒ false ]
 471  | RTS    ⇒ match u2 with [ RTS    ⇒ true | _ ⇒ false ]
 472  | SBC    ⇒ match u2 with [ SBC    ⇒ true | _ ⇒ false ]
 473  | SEC    ⇒ match u2 with [ SEC    ⇒ true | _ ⇒ false ]
 474  | SEI    ⇒ match u2 with [ SEI    ⇒ true | _ ⇒ false ]
 475  | SHA    ⇒ match u2 with [ SHA    ⇒ true | _ ⇒ false ]
 476  | SLA    ⇒ match u2 with [ SLA    ⇒ true | _ ⇒ false ]
 477  | STA    ⇒ match u2 with [ STA    ⇒ true | _ ⇒ false ]
 478  | STHX   ⇒ match u2 with [ STHX   ⇒ true | _ ⇒ false ]
 479  | STOP   ⇒ match u2 with [ STOP   ⇒ true | _ ⇒ false ]
 480  | STX    ⇒ match u2 with [ STX    ⇒ true | _ ⇒ false ]
 481  | SUB    ⇒ match u2 with [ SUB    ⇒ true | _ ⇒ false ]
 482  | SWI    ⇒ match u2 with [ SWI    ⇒ true | _ ⇒ false ]
 483  | TAP    ⇒ match u2 with [ TAP    ⇒ true | _ ⇒ false ]
 484  | TAX    ⇒ match u2 with [ TAX    ⇒ true | _ ⇒ false ]
 485  | TPA    ⇒ match u2 with [ TPA    ⇒ true | _ ⇒ false ]
 486  | TST    ⇒ match u2 with [ TST    ⇒ true | _ ⇒ false ]
 487  | TSX    ⇒ match u2 with [ TSX    ⇒ true | _ ⇒ false ]
 488  | TXA    ⇒ match u2 with [ TXA    ⇒ true | _ ⇒ false ]
 489  | TXS    ⇒ match u2 with [ TXS    ⇒ true | _ ⇒ false ]
 490  | WAIT   ⇒ match u2 with [ WAIT   ⇒ true | _ ⇒ false ]
 491
 492  ].
 493
 494 (* costruttore di un sottouniverso:
 495    S_EL cioe' uno qualsiasi degli elementi del sottouniverso
 496    S_KO cioe' il caso impossibile
 497 *)
 498 ninductive S_UN (l:list UN) : Type ≝
 499   S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l
 500 | S_KO : False → S_UN l.
 501
 502 ndefinition getelem : ∀l.∀e:S_UN l.UN.
 503  #l; #s; nelim s;
 504  ##[ ##1: #u; #dim1; #dim2; napply u
 505  ##| ##2: #F; nelim F
 506  ##]
 507 nqed.
 508
 509 ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y).
 510
 511 ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true.
 512  #l; #s; nelim s;
 513  ##[ ##2: #F; nelim F
 514  ##| ##1: #u; #dim1; #dim2; napply dim1
 515  ##]
 516 nqed.
 517
 518 ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y).
 519  #l; #s; nelim s;
 520  ##[ ##2: #F; nelim F
 521  ##| ##1: #u; #dim1; #dim2; napply dim2
 522  ##]
 523 nqed.
 524
 525 nlemma SUN_destruct_1
 526  : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2.
 527  #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H;
 528  nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]);
 529  nrewrite < H;
 530  nnormalize;
 531  napply refl_eq.
 532 nqed.
 533
 534 ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P  | false ⇒ P ].
 535  #x; #y; #P; #H;
 536  nrewrite > H;
 537  nelim y;
 538  nnormalize;
 539  napply (λx.x).
 540 nqed.
 541
 542 ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
 543  #l; #x; nelim x;
 544  ##[ ##2: #F; nelim F
 545  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 546           ##[ ##2: #F; nelim F
 547           ##| ##1: #u2; #dim21; #dim22; #P;
 548                    nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
 549                    #H; napply (UN_destruct u1 u2);
 550                    napply (SUN_destruct_1 l … H)
 551           ##]
 552  ##]
 553 nqed.
 554
 555 nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
 556  #e1; #e2; #H;
 557  nrewrite > H;
 558  nelim e2;
 559  nnormalize;
 560  napply refl_eq.
 561 nqed.
 562
 563 nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
 564  #l; #x; nelim x;
 565  ##[ ##2: #F; nelim F
 566  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 567           ##[ ##2: #F; nelim F
 568           ##| ##1: #u2; #dim21; #dim22;
 569                    nchange with (? → eq_UN u1 u2 = true);
 570                    #H; napply (eq_to_eqUN u1 u2);
 571                    napply (SUN_destruct_1 l … H)
 572           ##]
 573  ##]
 574 nqed.
 575
 576 nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
 577  #e1; #e2; #H;
 578  napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …);
 579  ##[ ##1: napply (eq_to_eqUN e1 e2)
 580  ##| ##2: napply (eqfalse_to_neqtrue … H)
 581  ##]
 582 nqed.
 583
 584 nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
 585  #l; #x; nelim x;
 586  ##[ ##2: #F; nelim F
 587  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 588           ##[ ##2: #F; nelim F
 589           ##| ##1: #u2; #dim21; #dim22;
 590                         nchange with ((eq_UN u1 u2 = false) → ?);
 591                         #H; nnormalize; #H1;
 592                         napply (neqUN_to_neq u1 u2 H);
 593                         napply (SUN_destruct_1 l … H1)
 594           ##]
 595  ##]
 596 nqed.
 597
 598 naxiom SUN_construct
 599  : ∀l.∀u.
 600    ∀dim11,dim21:(member_list UN u eq_UN l = true).
 601    ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)).
 602    ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)).
 603
 604 nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
 605  #l; #x; nelim x;
 606  ##[ ##2: #F; nelim F
 607  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 608           ##[ ##2: #F; nelim F
 609           ##| ##1: #u2; #dim21; #dim22;
 610                    nchange with (u1 = u2 → ?); #H;
 611                    nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12;
 612                    napply (SUN_construct l u2 dim11 dim21 dim12 dim22);
 613           ##]
 614  ##]
 615 nqed.
 616
 617 nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y).
 618  #l; #x; nelim x;
 619  ##[ ##2: #F; nelim F
 620  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 621           ##[ ##2: #F; nelim F
 622           ##| ##1: #u2; #dim21; #dim22; #H;
 623                    napply (not_to_not ((getelem l ?) = (getelem l ?))
 624                                       ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?);
 625                    ##[ ##1: napply H
 626                    ##| ##2: napply (eqgetelem_to_eq l …)
 627                    ##]
 628           ##]
 629  ##]
 630 nqed.
 631
 632 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
 633  #l; #x; nelim x;
 634  ##[ ##2: #F; nelim F
 635  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 636           ##[ ##2: #F; nelim F
 637           ##| ##1: #u2; #dim21; #dim22;
 638                    nchange with ((eq_UN u1 u2 = true) → ?); #H;
 639                    nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H));
 640                    napply refl_eq
 641           ##]
 642  ##]
 643 nqed.
 644
 645 nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
 646  #l; #x; nelim x;
 647  ##[ ##2: #F; nelim F
 648  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 649           ##[ ##2: #F; nelim F
 650           ##| ##1: #u2; #dim21; #dim22; #H;
 651                    napply neqtrue_to_eqfalse;
 652                    napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ;
 653                    napply H
 654           ##]
 655  ##]
 656 nqed.
 657
 658 nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
 659  #l; #x; nelim x;
 660  ##[ ##2: #F; nelim F
 661  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 662           ##[ ##2: #F; nelim F
 663           ##| ##1: #u2; #dim21; #dim22; nnormalize;
 664                    napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))));
 665  ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H))
 666  ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H))
 667  ##]
 668 nqed.
 669
 670 nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
 671  #l; #x; nelim x;
 672  ##[ ##2: #F; nelim F
 673  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 674           ##[ ##2: #F; nelim F
 675           ##| ##1: #u2; #dim21; #dim22;
 676                    napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)));
 677  ##[ ##1: #H; nrewrite > H; napply refl_eq
 678  ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H);
 679           napply (symmetric_eq ? (eq_SUN l ??) false);
 680           napply (neq_to_neqSUN l … (symmetric_neq … H))
 681  ##]
 682 nqed.
 683
 684 (*
 685 ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
 686
 687 ndefinition f1_EX_UN
 688  : ∀e:S_UN EX_UN.
 689    ∀f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN.
 690    S_UN EX_UN.
 691  #input; #f1; #f2; #f3; #f4; #f5; #f6; #f7; #f8; #f9; #f10; #f11; #f12; #f13; #f14; #f15; #f16;
 692  nelim input;
 693  ##[ ##2: #H; nelim H
 694  ##| ##1: #u; #H; nelim u in H:(%); #H;
 695           ##[ ##13: napply f1 ##| ##14: napply f2 ##| ##15: napply f3 ##| ##16: napply f4
 696           ##| ##17: napply f5 ##| ##18: napply f6 ##| ##19: napply f7 ##| ##20: napply f8
 697           ##| ##21: napply f9 ##| ##22: napply f10 ##| ##23: napply f11 ##| ##24: napply f12
 698           ##| ##25: napply f13 ##| ##26: napply f14 ##| ##27: napply f15 ##| ##28: napply f16
 699           ##| ##*: nnormalize in H:(%); napply (S_KO EX_UN (bool_destruct false true False H))
 700           ##]
 701  ##]
 702 nqed.
 703
 704 ndefinition succ_EX_UN ≝
 705 λe:S_UN EX_UN.f1_EX_UN
 706  (S_EL EX_UN ux1 (refl_eq …)) (S_EL EX_UN ux2 (refl_eq …))
 707  (S_EL EX_UN ux3 (refl_eq …)) (S_EL EX_UN ux4 (refl_eq …))
 708  (S_EL EX_UN ux5 (refl_eq …)) (S_EL EX_UN ux6 (refl_eq …))
 709  (S_EL EX_UN ux7 (refl_eq …)) (S_EL EX_UN ux8 (refl_eq …))
 710  (S_EL EX_UN ux9 (refl_eq …)) (S_EL EX_UN uxA (refl_eq …))
 711  (S_EL EX_UN uxB (refl_eq …)) (S_EL EX_UN uxC (refl_eq …))
 712  (S_EL EX_UN uxD (refl_eq …)) (S_EL EX_UN uxE (refl_eq …))
 713  (S_EL EX_UN uxF (refl_eq …)) (S_EL EX_UN ux0 (refl_eq …)).
 714 *)