helm/software/matita/contribs/ng_assembly/universe/universe.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.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  27  match l with
  28   [ nil ⇒ true
  29   | cons h t ⇒ match f elem h with
  30    [ true ⇒ false | false ⇒ nmember_list T elem f t ]
  31   ].
  32
  33 (* elem presente una ed una sola volta in l *)
  34 nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  35  match l with
  36   [ nil ⇒ false
  37   | cons h t ⇒ match f elem h with
  38     [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ]
  39   ].
  40
  41 (* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
  42 ninductive UN : Type ≝
  43 (* quaternari[4] 1-4 *)
  44   uq0 : UN
  45 | uq1 : UN
  46 | uq2 : UN
  47 | uq3 : UN
  48
  49 (* ottali[8] 5-12 *)
  50 | uo0 : UN
  51 | uo1 : UN
  52 | uo2 : UN
  53 | uo3 : UN
  54 | uo4 : UN
  55 | uo5 : UN
  56 | uo6 : UN
  57 | uo7 : UN
  58
  59 (* esadecimali[16] 13-28 *)
  60 | ux0 : UN
  61 | ux1 : UN
  62 | ux2 : UN
  63 | ux3 : UN
  64 | ux4 : UN
  65 | ux5 : UN
  66 | ux6 : UN
  67 | ux7 : UN
  68 | ux8 : UN
  69 | ux9 : UN
  70 | uxA : UN
  71 | uxB : UN
  72 | uxC : UN
  73 | uxD : UN
  74 | uxE : UN
  75 | uxF : UN
  76
  77 (* bitrigesimali[32] 29-60 *)
  78 | ut00 : UN
  79 | ut01 : UN
  80 | ut02 : UN
  81 | ut03 : UN
  82 | ut04 : UN
  83 | ut05 : UN
  84 | ut06 : UN
  85 | ut07 : UN
  86 | ut08 : UN
  87 | ut09 : UN
  88 | ut0A : UN
  89 | ut0B : UN
  90 | ut0C : UN
  91 | ut0D : UN
  92 | ut0E : UN
  93 | ut0F : UN
  94 | ut10 : UN
  95 | ut11 : UN
  96 | ut12 : UN
  97 | ut13 : UN
  98 | ut14 : UN
  99 | ut15 : UN
 100 | ut16 : UN
 101 | ut17 : UN
 102 | ut18 : UN
 103 | ut19 : UN
 104 | ut1A : UN
 105 | ut1B : UN
 106 | ut1C : UN
 107 | ut1D : UN
 108 | ut1E : UN
 109 | ut1F : UN
 110
 111 (* ascii[63] 61-123 *)
 112 | uch_0 : UN
 113 | uch_1 : UN
 114 | uch_2 : UN
 115 | uch_3 : UN
 116 | uch_4 : UN
 117 | uch_5 : UN
 118 | uch_6 : UN
 119 | uch_7 : UN
 120 | uch_8 : UN
 121 | uch_9 : UN
 122 | uch__ : UN
 123 | uch_A : UN
 124 | uch_B : UN
 125 | uch_C : UN
 126 | uch_D : UN
 127 | uch_E : UN
 128 | uch_F : UN
 129 | uch_G : UN
 130 | uch_H : UN
 131 | uch_I : UN
 132 | uch_J : UN
 133 | uch_K : UN
 134 | uch_L : UN
 135 | uch_M : UN
 136 | uch_N : UN
 137 | uch_O : UN
 138 | uch_P : UN
 139 | uch_Q : UN
 140 | uch_R : UN
 141 | uch_S : UN
 142 | uch_T : UN
 143 | uch_U : UN
 144 | uch_V : UN
 145 | uch_W : UN
 146 | uch_X : UN
 147 | uch_Y : UN
 148 | uch_Z : UN
 149 | uch_a : UN
 150 | uch_b : UN
 151 | uch_c : UN
 152 | uch_d : UN
 153 | uch_e : UN
 154 | uch_f : UN
 155 | uch_g : UN
 156 | uch_h : UN
 157 | uch_i : UN
 158 | uch_j : UN
 159 | uch_k : UN
 160 | uch_l : UN
 161 | uch_m : UN
 162 | uch_n : UN
 163 | uch_o : UN
 164 | uch_p : UN
 165 | uch_q : UN
 166 | uch_r : UN
 167 | uch_s : UN
 168 | uch_t : UN
 169 | uch_u : UN
 170 | uch_v : UN
 171 | uch_w : UN
 172 | uch_x : UN
 173 | uch_y : UN
 174 | uch_z : UN
 175
 176 (* opcode[91] 124-214 *)
 177 | uADC    : UN
 178 | uADD    : UN
 179 | uAIS    : UN
 180 | uAIX    : UN
 181 | uAND    : UN
 182 | uASL    : UN
 183 | uASR    : UN
 184 | uBCC    : UN
 185 | uBCLRn  : UN
 186 | uBCS    : UN
 187 | uBEQ    : UN
 188 | uBGE    : UN
 189 | uBGND   : UN
 190 | uBGT    : UN
 191 | uBHCC   : UN
 192 | uBHCS   : UN
 193 | uBHI    : UN
 194 | uBIH    : UN
 195 | uBIL    : UN
 196 | uBIT    : UN
 197 | uBLE    : UN
 198 | uBLS    : UN
 199 | uBLT    : UN
 200 | uBMC    : UN
 201 | uBMI    : UN
 202 | uBMS    : UN
 203 | uBNE    : UN
 204 | uBPL    : UN
 205 | uBRA    : UN
 206 | uBRCLRn : UN
 207 | uBRN    : UN
 208 | uBRSETn : UN
 209 | uBSETn  : UN
 210 | uBSR    : UN
 211 | uCBEQA  : UN
 212 | uCBEQX  : UN
 213 | uCLC    : UN
 214 | uCLI    : UN
 215 | uCLR    : UN
 216 | uCMP    : UN
 217 | uCOM    : UN
 218 | uCPHX   : UN
 219 | uCPX    : UN
 220 | uDAA    : UN
 221 | uDBNZ   : UN
 222 | uDEC    : UN
 223 | uDIV    : UN
 224 | uEOR    : UN
 225 | uINC    : UN
 226 | uJMP    : UN
 227 | uJSR    : UN
 228 | uLDA    : UN
 229 | uLDHX   : UN
 230 | uLDX    : UN
 231 | uLSR    : UN
 232 | uMOV    : UN
 233 | uMUL    : UN
 234 | uNEG    : UN
 235 | uNOP    : UN
 236 | uNSA    : UN
 237 | uORA    : UN
 238 | uPSHA   : UN
 239 | uPSHH   : UN
 240 | uPSHX   : UN
 241 | uPULA   : UN
 242 | uPULH   : UN
 243 | uPULX   : UN
 244 | uROL    : UN
 245 | uROR    : UN
 246 | uRSP    : UN
 247 | uRTI    : UN
 248 | uRTS    : UN
 249 | uSBC    : UN
 250 | uSEC    : UN
 251 | uSEI    : UN
 252 | uSHA    : UN
 253 | uSLA    : UN
 254 | uSTA    : UN
 255 | uSTHX   : UN
 256 | uSTOP   : UN
 257 | uSTX    : UN
 258 | uSUB    : UN
 259 | uSWI    : UN
 260 | uTAP    : UN
 261 | uTAX    : UN
 262 | uTPA    : UN
 263 | uTST    : UN
 264 | uTSX    : UN
 265 | uTXA    : UN
 266 | uTXS    : UN
 267 | uWAIT   : UN
 268 .
 269
 270 (* funzione di uguaglianza sugli atomi *)
 271 ndefinition eq_UN ≝
 272 λu1,u2.match u1 with
 273  [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ]
 274  | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ]
 275  | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ]
 276  | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ]
 277
 278  | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ]
 279  | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ]
 280  | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ]
 281  | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ]
 282  | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ]
 283  | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ]
 284  | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ]
 285  | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ]
 286
 287  | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ]
 288  | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ]
 289  | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ]
 290  | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ]
 291  | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ]
 292  | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ]
 293  | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ]
 294  | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ]
 295  | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ]
 296  | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ]
 297  | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ]
 298  | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ]
 299  | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ]
 300  | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ]
 301  | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ]
 302  | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ]
 303
 304  | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ]
 305  | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ]
 306  | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ]
 307  | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ]
 308  | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ]
 309  | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ]
 310  | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ]
 311  | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ]
 312  | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ]
 313  | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ]
 314  | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ]
 315  | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ]
 316  | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ]
 317  | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ]
 318  | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ]
 319  | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ]
 320  | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ]
 321  | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ]
 322  | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ]
 323  | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ]
 324  | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ]
 325  | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ]
 326  | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ]
 327  | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ]
 328  | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ]
 329  | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ]
 330  | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ]
 331  | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ]
 332  | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ]
 333  | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ]
 334  | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ]
 335  | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ]
 336
 337  | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ]
 338  | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ]
 339  | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ]
 340  | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ]
 341  | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ]
 342  | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ]
 343  | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ]
 344  | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ]
 345  | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ]
 346  | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ]
 347  | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ]
 348  | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ]
 349  | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ]
 350  | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ]
 351  | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ]
 352  | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ]
 353  | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ]
 354  | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ]
 355  | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ]
 356  | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ]
 357  | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ]
 358  | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ]
 359  | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ]
 360  | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ]
 361  | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ]
 362  | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ]
 363  | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ]
 364  | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ]
 365  | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ]
 366  | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ]
 367  | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ]
 368  | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ]
 369  | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ]
 370  | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ]
 371  | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ]
 372  | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ]
 373  | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ]
 374  | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ]
 375  | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ]
 376  | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ]
 377  | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ]
 378  | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ]
 379  | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ]
 380  | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ]
 381  | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ]
 382  | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ]
 383  | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ]
 384  | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ]
 385  | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ]
 386  | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ]
 387  | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ]
 388  | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ]
 389  | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ]
 390  | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ]
 391  | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ]
 392  | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ]
 393  | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ]
 394  | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ]
 395  | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ]
 396  | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ]
 397  | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ]
 398  | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ]
 399  | uch_z ⇒ match u2 with [ uch_z ⇒ true | _ ⇒ false ]
 400
 401  | uADC    ⇒ match u2 with [ uADC    ⇒ true | _ ⇒ false ]
 402  | uADD    ⇒ match u2 with [ uADD    ⇒ true | _ ⇒ false ]
 403  | uAIS    ⇒ match u2 with [ uAIS    ⇒ true | _ ⇒ false ]
 404  | uAIX    ⇒ match u2 with [ uAIX    ⇒ true | _ ⇒ false ]
 405  | uAND    ⇒ match u2 with [ uAND    ⇒ true | _ ⇒ false ]
 406  | uASL    ⇒ match u2 with [ uASL    ⇒ true | _ ⇒ false ]
 407  | uASR    ⇒ match u2 with [ uASR    ⇒ true | _ ⇒ false ]
 408  | uBCC    ⇒ match u2 with [ uBCC    ⇒ true | _ ⇒ false ]
 409  | uBCLRn  ⇒ match u2 with [ uBCLRn  ⇒ true | _ ⇒ false ]
 410  | uBCS    ⇒ match u2 with [ uBCS    ⇒ true | _ ⇒ false ]
 411  | uBEQ    ⇒ match u2 with [ uBEQ    ⇒ true | _ ⇒ false ]
 412  | uBGE    ⇒ match u2 with [ uBGE    ⇒ true | _ ⇒ false ]
 413  | uBGND   ⇒ match u2 with [ uBGND   ⇒ true | _ ⇒ false ]
 414  | uBGT    ⇒ match u2 with [ uBGT    ⇒ true | _ ⇒ false ]
 415  | uBHCC   ⇒ match u2 with [ uBHCC   ⇒ true | _ ⇒ false ]
 416  | uBHCS   ⇒ match u2 with [ uBHCS   ⇒ true | _ ⇒ false ]
 417  | uBHI    ⇒ match u2 with [ uBHI    ⇒ true | _ ⇒ false ]
 418  | uBIH    ⇒ match u2 with [ uBIH    ⇒ true | _ ⇒ false ]
 419  | uBIL    ⇒ match u2 with [ uBIL    ⇒ true | _ ⇒ false ]
 420  | uBIT    ⇒ match u2 with [ uBIT    ⇒ true | _ ⇒ false ]
 421  | uBLE    ⇒ match u2 with [ uBLE    ⇒ true | _ ⇒ false ]
 422  | uBLS    ⇒ match u2 with [ uBLS    ⇒ true | _ ⇒ false ]
 423  | uBLT    ⇒ match u2 with [ uBLT    ⇒ true | _ ⇒ false ]
 424  | uBMC    ⇒ match u2 with [ uBMC    ⇒ true | _ ⇒ false ]
 425  | uBMI    ⇒ match u2 with [ uBMI    ⇒ true | _ ⇒ false ]
 426  | uBMS    ⇒ match u2 with [ uBMS    ⇒ true | _ ⇒ false ]
 427  | uBNE    ⇒ match u2 with [ uBNE    ⇒ true | _ ⇒ false ]
 428  | uBPL    ⇒ match u2 with [ uBPL    ⇒ true | _ ⇒ false ]
 429  | uBRA    ⇒ match u2 with [ uBRA    ⇒ true | _ ⇒ false ]
 430  | uBRCLRn ⇒ match u2 with [ uBRCLRn ⇒ true | _ ⇒ false ]
 431  | uBRN    ⇒ match u2 with [ uBRN    ⇒ true | _ ⇒ false ]
 432  | uBRSETn ⇒ match u2 with [ uBRSETn ⇒ true | _ ⇒ false ]
 433  | uBSETn  ⇒ match u2 with [ uBSETn  ⇒ true | _ ⇒ false ]
 434  | uBSR    ⇒ match u2 with [ uBSR    ⇒ true | _ ⇒ false ]
 435  | uCBEQA  ⇒ match u2 with [ uCBEQA  ⇒ true | _ ⇒ false ]
 436  | uCBEQX  ⇒ match u2 with [ uCBEQX  ⇒ true | _ ⇒ false ]
 437  | uCLC    ⇒ match u2 with [ uCLC    ⇒ true | _ ⇒ false ]
 438  | uCLI    ⇒ match u2 with [ uCLI    ⇒ true | _ ⇒ false ]
 439  | uCLR    ⇒ match u2 with [ uCLR    ⇒ true | _ ⇒ false ]
 440  | uCMP    ⇒ match u2 with [ uCMP    ⇒ true | _ ⇒ false ]
 441  | uCOM    ⇒ match u2 with [ uCOM    ⇒ true | _ ⇒ false ]
 442  | uCPHX   ⇒ match u2 with [ uCPHX   ⇒ true | _ ⇒ false ]
 443  | uCPX    ⇒ match u2 with [ uCPX    ⇒ true | _ ⇒ false ]
 444  | uDAA    ⇒ match u2 with [ uDAA    ⇒ true | _ ⇒ false ]
 445  | uDBNZ   ⇒ match u2 with [ uDBNZ   ⇒ true | _ ⇒ false ]
 446  | uDEC    ⇒ match u2 with [ uDEC    ⇒ true | _ ⇒ false ]
 447  | uDIV    ⇒ match u2 with [ uDIV    ⇒ true | _ ⇒ false ]
 448  | uEOR    ⇒ match u2 with [ uEOR    ⇒ true | _ ⇒ false ]
 449  | uINC    ⇒ match u2 with [ uINC    ⇒ true | _ ⇒ false ]
 450  | uJMP    ⇒ match u2 with [ uJMP    ⇒ true | _ ⇒ false ]
 451  | uJSR    ⇒ match u2 with [ uJSR    ⇒ true | _ ⇒ false ]
 452  | uLDA    ⇒ match u2 with [ uLDA    ⇒ true | _ ⇒ false ]
 453  | uLDHX   ⇒ match u2 with [ uLDHX   ⇒ true | _ ⇒ false ]
 454  | uLDX    ⇒ match u2 with [ uLDX    ⇒ true | _ ⇒ false ]
 455  | uLSR    ⇒ match u2 with [ uLSR    ⇒ true | _ ⇒ false ]
 456  | uMOV    ⇒ match u2 with [ uMOV    ⇒ true | _ ⇒ false ]
 457  | uMUL    ⇒ match u2 with [ uMUL    ⇒ true | _ ⇒ false ]
 458  | uNEG    ⇒ match u2 with [ uNEG    ⇒ true | _ ⇒ false ]
 459  | uNOP    ⇒ match u2 with [ uNOP    ⇒ true | _ ⇒ false ]
 460  | uNSA    ⇒ match u2 with [ uNSA    ⇒ true | _ ⇒ false ]
 461  | uORA    ⇒ match u2 with [ uORA    ⇒ true | _ ⇒ false ]
 462  | uPSHA   ⇒ match u2 with [ uPSHA   ⇒ true | _ ⇒ false ]
 463  | uPSHH   ⇒ match u2 with [ uPSHH   ⇒ true | _ ⇒ false ]
 464  | uPSHX   ⇒ match u2 with [ uPSHX   ⇒ true | _ ⇒ false ]
 465  | uPULA   ⇒ match u2 with [ uPULA   ⇒ true | _ ⇒ false ]
 466  | uPULH   ⇒ match u2 with [ uPULH   ⇒ true | _ ⇒ false ]
 467  | uPULX   ⇒ match u2 with [ uPULX   ⇒ true | _ ⇒ false ]
 468  | uROL    ⇒ match u2 with [ uROL    ⇒ true | _ ⇒ false ]
 469  | uROR    ⇒ match u2 with [ uROR    ⇒ true | _ ⇒ false ]
 470  | uRSP    ⇒ match u2 with [ uRSP    ⇒ true | _ ⇒ false ]
 471  | uRTI    ⇒ match u2 with [ uRTI    ⇒ true | _ ⇒ false ]
 472  | uRTS    ⇒ match u2 with [ uRTS    ⇒ true | _ ⇒ false ]
 473  | uSBC    ⇒ match u2 with [ uSBC    ⇒ true | _ ⇒ false ]
 474  | uSEC    ⇒ match u2 with [ uSEC    ⇒ true | _ ⇒ false ]
 475  | uSEI    ⇒ match u2 with [ uSEI    ⇒ true | _ ⇒ false ]
 476  | uSHA    ⇒ match u2 with [ uSHA    ⇒ true | _ ⇒ false ]
 477  | uSLA    ⇒ match u2 with [ uSLA    ⇒ true | _ ⇒ false ]
 478  | uSTA    ⇒ match u2 with [ uSTA    ⇒ true | _ ⇒ false ]
 479  | uSTHX   ⇒ match u2 with [ uSTHX   ⇒ true | _ ⇒ false ]
 480  | uSTOP   ⇒ match u2 with [ uSTOP   ⇒ true | _ ⇒ false ]
 481  | uSTX    ⇒ match u2 with [ uSTX    ⇒ true | _ ⇒ false ]
 482  | uSUB    ⇒ match u2 with [ uSUB    ⇒ true | _ ⇒ false ]
 483  | uSWI    ⇒ match u2 with [ uSWI    ⇒ true | _ ⇒ false ]
 484  | uTAP    ⇒ match u2 with [ uTAP    ⇒ true | _ ⇒ false ]
 485  | uTAX    ⇒ match u2 with [ uTAX    ⇒ true | _ ⇒ false ]
 486  | uTPA    ⇒ match u2 with [ uTPA    ⇒ true | _ ⇒ false ]
 487  | uTST    ⇒ match u2 with [ uTST    ⇒ true | _ ⇒ false ]
 488  | uTSX    ⇒ match u2 with [ uTSX    ⇒ true | _ ⇒ false ]
 489  | uTXA    ⇒ match u2 with [ uTXA    ⇒ true | _ ⇒ false ]
 490  | uTXS    ⇒ match u2 with [ uTXS    ⇒ true | _ ⇒ false ]
 491  | uWAIT   ⇒ match u2 with [ uWAIT   ⇒ true | _ ⇒ false ]
 492
 493  ].
 494
 495 (* costruttore di un sottouniverso:
 496    S_EL cioe' uno qualsiasi degli elementi del sottouniverso
 497    S_KO cioe' il caso impossibile
 498 *)
 499 ninductive S_UN (l:list UN) : Type ≝
 500   S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l
 501 | S_KO : False → S_UN l.
 502
 503 ndefinition getelem : ∀l.∀e:S_UN l.UN.
 504  #l; #s; nelim s;
 505  ##[ ##1: #u; #dim1; #dim2; napply u
 506  ##| ##2: #F; nelim F
 507  ##]
 508 nqed.
 509
 510 ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y).
 511
 512 ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true.
 513  #l; #s; nelim s;
 514  ##[ ##2: #F; nelim F
 515  ##| ##1: #u; #dim1; #dim2; napply dim1
 516  ##]
 517 nqed.
 518
 519 ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y).
 520  #l; #s; nelim s;
 521  ##[ ##2: #F; nelim F
 522  ##| ##1: #u; #dim1; #dim2; napply dim2
 523  ##]
 524 nqed.
 525
 526 nlemma SUN_destruct_1
 527  : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2.
 528  #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H;
 529  nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]);
 530  nrewrite < H;
 531  nnormalize;
 532  napply refl_eq.
 533 nqed.
 534
 535 ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P  | false ⇒ P ].
 536  #x; #y; #P; #H;
 537  nrewrite > H;
 538  nelim y;
 539  nnormalize;
 540  napply (λx.x).
 541 nqed.
 542
 543 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 ].
 544  #l; #x; nelim x;
 545  ##[ ##2: #F; nelim F
 546  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 547           ##[ ##2: #F; nelim F
 548           ##| ##1: #u2; #dim21; #dim22; #P;
 549                    nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
 550                    #H; napply (UN_destruct u1 u2);
 551                    napply (SUN_destruct_1 l … H)
 552           ##]
 553  ##]
 554 nqed.
 555
 556 nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
 557  #e1; #e2; #H;
 558  nrewrite > H;
 559  nelim e2;
 560  nnormalize;
 561  napply refl_eq.
 562 nqed.
 563
 564 nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
 565  #l; #x; nelim x;
 566  ##[ ##2: #F; nelim F
 567  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 568           ##[ ##2: #F; nelim F
 569           ##| ##1: #u2; #dim21; #dim22;
 570                    nchange with (? → eq_UN u1 u2 = true);
 571                    #H; napply (eq_to_eqUN u1 u2);
 572                    napply (SUN_destruct_1 l … H)
 573           ##]
 574  ##]
 575 nqed.
 576
 577 nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
 578  #e1; #e2; #H;
 579  napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …);
 580  ##[ ##1: napply (eq_to_eqUN e1 e2)
 581  ##| ##2: napply (eqfalse_to_neqtrue … H)
 582  ##]
 583 nqed.
 584
 585 nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
 586  #l; #x; nelim x;
 587  ##[ ##2: #F; nelim F
 588  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 589           ##[ ##2: #F; nelim F
 590           ##| ##1: #u2; #dim21; #dim22;
 591                         nchange with ((eq_UN u1 u2 = false) → ?);
 592                         #H; nnormalize; #H1;
 593                         napply (neqUN_to_neq u1 u2 H);
 594                         napply (SUN_destruct_1 l … H1)
 595           ##]
 596  ##]
 597 nqed.
 598
 599 naxiom SUN_construct
 600  : ∀l.∀u.
 601    ∀dim11,dim21:(member_list UN u eq_UN l = true).
 602    ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)).
 603    ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)).
 604
 605 nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
 606  #l; #x; nelim x;
 607  ##[ ##2: #F; nelim F
 608  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 609           ##[ ##2: #F; nelim F
 610           ##| ##1: #u2; #dim21; #dim22;
 611                    nchange with (u1 = u2 → ?); #H;
 612                    nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12;
 613                    napply (SUN_construct l u2 dim11 dim21 dim12 dim22);
 614           ##]
 615  ##]
 616 nqed.
 617
 618 nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y).
 619  #l; #x; nelim x;
 620  ##[ ##2: #F; nelim F
 621  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 622           ##[ ##2: #F; nelim F
 623           ##| ##1: #u2; #dim21; #dim22; #H;
 624                    napply (not_to_not ((getelem l ?) = (getelem l ?))
 625                                       ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?);
 626                    ##[ ##1: napply H
 627                    ##| ##2: napply (eqgetelem_to_eq l …)
 628                    ##]
 629           ##]
 630  ##]
 631 nqed.
 632
 633 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
 634  #l; #x; nelim x;
 635  ##[ ##2: #F; nelim F
 636  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 637           ##[ ##2: #F; nelim F
 638           ##| ##1: #u2; #dim21; #dim22;
 639                    nchange with ((eq_UN u1 u2 = true) → ?); #H;
 640                    nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H));
 641                    napply refl_eq
 642           ##]
 643  ##]
 644 nqed.
 645
 646 nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
 647  #l; #x; nelim x;
 648  ##[ ##2: #F; nelim F
 649  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 650           ##[ ##2: #F; nelim F
 651           ##| ##1: #u2; #dim21; #dim22; #H;
 652                    napply neqtrue_to_eqfalse;
 653                    napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ;
 654                    napply H
 655           ##]
 656  ##]
 657 nqed.
 658
 659 nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
 660  #l; #x; nelim x;
 661  ##[ ##2: #F; nelim F
 662  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 663           ##[ ##2: #F; nelim F
 664           ##| ##1: #u2; #dim21; #dim22; nnormalize;
 665                    napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))));
 666  ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H))
 667  ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H))
 668  ##]
 669 nqed.
 670
 671 nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
 672  #l; #x; nelim x;
 673  ##[ ##2: #F; nelim F
 674  ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
 675           ##[ ##2: #F; nelim F
 676           ##| ##1: #u2; #dim21; #dim22;
 677                    napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)));
 678  ##[ ##1: #H; nrewrite > H; napply refl_eq
 679  ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H);
 680           napply (symmetric_eq ? (eq_SUN l ??) false);
 681           napply (neq_to_neqSUN l … (symmetric_neq … H))
 682  ##]
 683 nqed.