helm/software/matita/contribs/ng_assembly/universe/opcode.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 "universe/universe.ma".
  24
  25 ndefinition OP_UN ≝ [ uADC; uADD; uAIS; uAIX; uAND; uASL; uASR; uBCC; uBCLRn; uBCS;
  26                       uBEQ; uBGE; uBGND; uBGT; uBHCC; uBHCS; uBHI; uBIH; uBIL; uBIT;
  27                       uBLE; uBLS; uBLT; uBMC; uBMI; uBMS; uBNE; uBPL; uBRA; uBRCLRn;
  28                       uBRN; uBRSETn; uBSETn; uBSR; uCBEQA; uCBEQX; uCLC; uCLI; uCLR;
  29                       uCMP; uCOM; uCPHX; uCPX; uDAA; uDBNZ; uDEC; uDIV; uEOR; uINC;
  30                       uJMP; uJSR; uLDA; uLDHX; uLDX; uLSR; uMOV; uMUL; uNEG; uNOP;
  31                       uNSA; uORA; uPSHA; uPSHH; uPSHX; uPULA; uPULH; uPULX; uROL;
  32                       uROR; uRSP; uRTI; uRTS; uSBC; uSEC; uSEI; uSHA; uSLA; uSTA;
  33                       uSTHX; uSTOP; uSTX; uSUB; uSWI; uTAP; uTAX; uTPA; uTST; uTSX;
  34                       uTXA; uTXS; uWAIT ].
  35
  36 (* derivati dall'universo
  37   1) SUN_destruct OP_UN
  38   2) eq_to_eqSUN OP_UN
  39   3) neq_to_neqSUN OP_UN
  40   4) eqSUN_to_eq OP_UN
  41   5) neqSUN_to_neq OP_UN
  42   6) decidable_SUN OP_UN
  43   7) symmetric_eqSUN OP_UN
  44 *)
  45
  46 nlemma un_ADC : S_UN OP_UN. napply (S_EL OP_UN uADC (refl_eq …) ?); #y; nelim y; ##[ ##124: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  47 nlemma un_ADD : S_UN OP_UN. napply (S_EL OP_UN uADD (refl_eq …) ?); #y; nelim y; ##[ ##125: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  48 nlemma un_AIS : S_UN OP_UN. napply (S_EL OP_UN uAIS (refl_eq …) ?); #y; nelim y; ##[ ##126: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  49 nlemma un_AIX : S_UN OP_UN. napply (S_EL OP_UN uAIX (refl_eq …) ?); #y; nelim y; ##[ ##127: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  50 nlemma un_AND : S_UN OP_UN. napply (S_EL OP_UN uAND (refl_eq …) ?); #y; nelim y; ##[ ##128: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  51 nlemma un_ASL : S_UN OP_UN. napply (S_EL OP_UN uASL (refl_eq …) ?); #y; nelim y; ##[ ##129: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  52 nlemma un_ASR : S_UN OP_UN. napply (S_EL OP_UN uASR (refl_eq …) ?); #y; nelim y; ##[ ##130: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  53 nlemma un_BCC : S_UN OP_UN. napply (S_EL OP_UN uBCC (refl_eq …) ?); #y; nelim y; ##[ ##131: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  54 nlemma un_BCLRn : S_UN OP_UN. napply (S_EL OP_UN uBCLRn (refl_eq …) ?); #y; nelim y; ##[ ##132: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  55 nlemma un_BCS : S_UN OP_UN. napply (S_EL OP_UN uBCS (refl_eq …) ?); #y; nelim y; ##[ ##133: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  56 nlemma un_BEQ : S_UN OP_UN. napply (S_EL OP_UN uBEQ (refl_eq …) ?); #y; nelim y; ##[ ##134: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  57 nlemma un_BGE : S_UN OP_UN. napply (S_EL OP_UN uBGE (refl_eq …) ?); #y; nelim y; ##[ ##135: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  58 nlemma un_BGND : S_UN OP_UN. napply (S_EL OP_UN uBGND (refl_eq …) ?); #y; nelim y; ##[ ##136: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  59 nlemma un_BGT : S_UN OP_UN. napply (S_EL OP_UN uBGT (refl_eq …) ?); #y; nelim y; ##[ ##137: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  60 nlemma un_BHCC : S_UN OP_UN. napply (S_EL OP_UN uBHCC (refl_eq …) ?); #y; nelim y; ##[ ##138: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  61 nlemma un_BHCS : S_UN OP_UN. napply (S_EL OP_UN uBHCS (refl_eq …) ?); #y; nelim y; ##[ ##139: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  62 nlemma un_BHI : S_UN OP_UN. napply (S_EL OP_UN uBHI (refl_eq …) ?); #y; nelim y; ##[ ##140: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  63 nlemma un_BIH : S_UN OP_UN. napply (S_EL OP_UN uBIH (refl_eq …) ?); #y; nelim y; ##[ ##141: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  64 nlemma un_BIL : S_UN OP_UN. napply (S_EL OP_UN uBIL (refl_eq …) ?); #y; nelim y; ##[ ##142: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  65 nlemma un_BIT : S_UN OP_UN. napply (S_EL OP_UN uBIT (refl_eq …) ?); #y; nelim y; ##[ ##143: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  66 nlemma un_BLE : S_UN OP_UN. napply (S_EL OP_UN uBLE (refl_eq …) ?); #y; nelim y; ##[ ##144: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  67 nlemma un_BLS : S_UN OP_UN. napply (S_EL OP_UN uBLS (refl_eq …) ?); #y; nelim y; ##[ ##145: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  68 nlemma un_BLT : S_UN OP_UN. napply (S_EL OP_UN uBLT (refl_eq …) ?); #y; nelim y; ##[ ##146: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  69 nlemma un_BMC : S_UN OP_UN. napply (S_EL OP_UN uBMC (refl_eq …) ?); #y; nelim y; ##[ ##147: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  70 nlemma un_BMI : S_UN OP_UN. napply (S_EL OP_UN uBMI (refl_eq …) ?); #y; nelim y; ##[ ##148: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  71 nlemma un_BMS : S_UN OP_UN. napply (S_EL OP_UN uBMS (refl_eq …) ?); #y; nelim y; ##[ ##149: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  72 nlemma un_BNE : S_UN OP_UN. napply (S_EL OP_UN uBNE (refl_eq …) ?); #y; nelim y; ##[ ##150: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  73 nlemma un_BPL : S_UN OP_UN. napply (S_EL OP_UN uBPL (refl_eq …) ?); #y; nelim y; ##[ ##151: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  74 nlemma un_BRA : S_UN OP_UN. napply (S_EL OP_UN uBRA (refl_eq …) ?); #y; nelim y; ##[ ##152: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  75 nlemma un_BRCLRn : S_UN OP_UN. napply (S_EL OP_UN uBRCLRn (refl_eq …) ?); #y; nelim y; ##[ ##153: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  76 nlemma un_BRN : S_UN OP_UN. napply (S_EL OP_UN uBRN (refl_eq …) ?); #y; nelim y; ##[ ##154: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  77 nlemma un_BRSETn : S_UN OP_UN. napply (S_EL OP_UN uBRSETn (refl_eq …) ?); #y; nelim y; ##[ ##155: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  78 nlemma un_BSETn : S_UN OP_UN. napply (S_EL OP_UN uBSETn (refl_eq …) ?); #y; nelim y; ##[ ##156: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  79 nlemma un_BSR : S_UN OP_UN. napply (S_EL OP_UN uBSR (refl_eq …) ?); #y; nelim y; ##[ ##157: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  80 nlemma un_CBEQA : S_UN OP_UN. napply (S_EL OP_UN uCBEQA (refl_eq …) ?); #y; nelim y; ##[ ##158: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  81 nlemma un_CBEQX : S_UN OP_UN. napply (S_EL OP_UN uCBEQX (refl_eq …) ?); #y; nelim y; ##[ ##159: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  82 nlemma un_CLC : S_UN OP_UN. napply (S_EL OP_UN uCLC (refl_eq …) ?); #y; nelim y; ##[ ##160: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  83 nlemma un_CLI : S_UN OP_UN. napply (S_EL OP_UN uCLI (refl_eq …) ?); #y; nelim y; ##[ ##161: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  84 nlemma un_CLR : S_UN OP_UN. napply (S_EL OP_UN uCLR (refl_eq …) ?); #y; nelim y; ##[ ##162: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  85 nlemma un_CMP : S_UN OP_UN. napply (S_EL OP_UN uCMP (refl_eq …) ?); #y; nelim y; ##[ ##163: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  86 nlemma un_COM : S_UN OP_UN. napply (S_EL OP_UN uCOM (refl_eq …) ?); #y; nelim y; ##[ ##164: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  87 nlemma un_CPHX : S_UN OP_UN. napply (S_EL OP_UN uCPHX (refl_eq …) ?); #y; nelim y; ##[ ##165: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  88 nlemma un_CPX : S_UN OP_UN. napply (S_EL OP_UN uCPX (refl_eq …) ?); #y; nelim y; ##[ ##166: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  89 nlemma un_DAA : S_UN OP_UN. napply (S_EL OP_UN uDAA (refl_eq …) ?); #y; nelim y; ##[ ##167: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  90 nlemma un_DBNZ : S_UN OP_UN. napply (S_EL OP_UN uDBNZ (refl_eq …) ?); #y; nelim y; ##[ ##168: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  91 nlemma un_DEC : S_UN OP_UN. napply (S_EL OP_UN uDEC (refl_eq …) ?); #y; nelim y; ##[ ##169: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  92 nlemma un_DIV : S_UN OP_UN. napply (S_EL OP_UN uDIV (refl_eq …) ?); #y; nelim y; ##[ ##170: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  93 nlemma un_EOR : S_UN OP_UN. napply (S_EL OP_UN uEOR (refl_eq …) ?); #y; nelim y; ##[ ##171: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  94 nlemma un_INC : S_UN OP_UN. napply (S_EL OP_UN uINC (refl_eq …) ?); #y; nelim y; ##[ ##172: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  95 nlemma un_JMP : S_UN OP_UN. napply (S_EL OP_UN uJMP (refl_eq …) ?); #y; nelim y; ##[ ##173: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  96 nlemma un_JSR : S_UN OP_UN. napply (S_EL OP_UN uJSR (refl_eq …) ?); #y; nelim y; ##[ ##174: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  97 nlemma un_LDA : S_UN OP_UN. napply (S_EL OP_UN uLDA (refl_eq …) ?); #y; nelim y; ##[ ##175: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  98 nlemma un_LDHX : S_UN OP_UN. napply (S_EL OP_UN uLDHX (refl_eq …) ?); #y; nelim y; ##[ ##176: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
  99 nlemma un_LDX : S_UN OP_UN. napply (S_EL OP_UN uLDX (refl_eq …) ?); #y; nelim y; ##[ ##177: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 100 nlemma un_LSR : S_UN OP_UN. napply (S_EL OP_UN uLSR (refl_eq …) ?); #y; nelim y; ##[ ##178: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 101 nlemma un_MOV : S_UN OP_UN. napply (S_EL OP_UN uMOV (refl_eq …) ?); #y; nelim y; ##[ ##179: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 102 nlemma un_MUL : S_UN OP_UN. napply (S_EL OP_UN uMUL (refl_eq …) ?); #y; nelim y; ##[ ##180: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 103 nlemma un_NEG : S_UN OP_UN. napply (S_EL OP_UN uNEG (refl_eq …) ?); #y; nelim y; ##[ ##181: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 104 nlemma un_NOP : S_UN OP_UN. napply (S_EL OP_UN uNOP (refl_eq …) ?); #y; nelim y; ##[ ##182: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 105 nlemma un_NSA : S_UN OP_UN. napply (S_EL OP_UN uNSA (refl_eq …) ?); #y; nelim y; ##[ ##183: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 106 nlemma un_ORA : S_UN OP_UN. napply (S_EL OP_UN uORA (refl_eq …) ?); #y; nelim y; ##[ ##184: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 107 nlemma un_PSHA : S_UN OP_UN. napply (S_EL OP_UN uPSHA (refl_eq …) ?); #y; nelim y; ##[ ##185: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 108 nlemma un_PSHH : S_UN OP_UN. napply (S_EL OP_UN uPSHH (refl_eq …) ?); #y; nelim y; ##[ ##186: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 109 nlemma un_PSHX : S_UN OP_UN. napply (S_EL OP_UN uPSHX (refl_eq …) ?); #y; nelim y; ##[ ##187: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 110 nlemma un_PULA : S_UN OP_UN. napply (S_EL OP_UN uPULA (refl_eq …) ?); #y; nelim y; ##[ ##188: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 111 nlemma un_PULH : S_UN OP_UN. napply (S_EL OP_UN uPULH (refl_eq …) ?); #y; nelim y; ##[ ##189: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 112 nlemma un_PULX : S_UN OP_UN. napply (S_EL OP_UN uPULX (refl_eq …) ?); #y; nelim y; ##[ ##190: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 113 nlemma un_ROL : S_UN OP_UN. napply (S_EL OP_UN uROL (refl_eq …) ?); #y; nelim y; ##[ ##191: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 114 nlemma un_ROR : S_UN OP_UN. napply (S_EL OP_UN uROR (refl_eq …) ?); #y; nelim y; ##[ ##192: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 115 nlemma un_RSP : S_UN OP_UN. napply (S_EL OP_UN uRSP (refl_eq …) ?); #y; nelim y; ##[ ##193: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 116 nlemma un_RTI : S_UN OP_UN. napply (S_EL OP_UN uRTI (refl_eq …) ?); #y; nelim y; ##[ ##194: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 117 nlemma un_RTS : S_UN OP_UN. napply (S_EL OP_UN uRTS (refl_eq …) ?); #y; nelim y; ##[ ##195: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 118 nlemma un_SBC : S_UN OP_UN. napply (S_EL OP_UN uSBC (refl_eq …) ?); #y; nelim y; ##[ ##196: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 119 nlemma un_SEC : S_UN OP_UN. napply (S_EL OP_UN uSEC (refl_eq …) ?); #y; nelim y; ##[ ##197: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 120 nlemma un_SEI : S_UN OP_UN. napply (S_EL OP_UN uSEI (refl_eq …) ?); #y; nelim y; ##[ ##198: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 121 nlemma un_SHA : S_UN OP_UN. napply (S_EL OP_UN uSHA (refl_eq …) ?); #y; nelim y; ##[ ##199: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 122 nlemma un_SLA : S_UN OP_UN. napply (S_EL OP_UN uSLA (refl_eq …) ?); #y; nelim y; ##[ ##200: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 123 nlemma un_STA : S_UN OP_UN. napply (S_EL OP_UN uSTA (refl_eq …) ?); #y; nelim y; ##[ ##201: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 124 nlemma un_STHX : S_UN OP_UN. napply (S_EL OP_UN uSTHX (refl_eq …) ?); #y; nelim y; ##[ ##202: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 125 nlemma un_STOP : S_UN OP_UN. napply (S_EL OP_UN uSTOP (refl_eq …) ?); #y; nelim y; ##[ ##203: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 126 nlemma un_STX : S_UN OP_UN. napply (S_EL OP_UN uSTX (refl_eq …) ?); #y; nelim y; ##[ ##204: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 127 nlemma un_SUB : S_UN OP_UN. napply (S_EL OP_UN uSUB (refl_eq …) ?); #y; nelim y; ##[ ##205: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 128 nlemma un_SWI : S_UN OP_UN. napply (S_EL OP_UN uSWI (refl_eq …) ?); #y; nelim y; ##[ ##206: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 129 nlemma un_TAP : S_UN OP_UN. napply (S_EL OP_UN uTAP (refl_eq …) ?); #y; nelim y; ##[ ##207: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 130 nlemma un_TAX : S_UN OP_UN. napply (S_EL OP_UN uTAX (refl_eq …) ?); #y; nelim y; ##[ ##208: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 131 nlemma un_TPA : S_UN OP_UN. napply (S_EL OP_UN uTPA (refl_eq …) ?); #y; nelim y; ##[ ##209: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 132 nlemma un_TST : S_UN OP_UN. napply (S_EL OP_UN uTST (refl_eq …) ?); #y; nelim y; ##[ ##210: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 133 nlemma un_TSX : S_UN OP_UN. napply (S_EL OP_UN uTSX (refl_eq …) ?); #y; nelim y; ##[ ##211: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 134 nlemma un_TXA : S_UN OP_UN. napply (S_EL OP_UN uTXA (refl_eq …) ?); #y; nelim y; ##[ ##212: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 135 nlemma un_TXS : S_UN OP_UN. napply (S_EL OP_UN uTXS (refl_eq …) ?); #y; nelim y; ##[ ##213: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
 136 nlemma un_WAIT : S_UN OP_UN. napply (S_EL OP_UN uWAIT (refl_eq …) ?); #y; nelim y; ##[ ##214: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.