Elimination principles are now processed in O(1) again

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / opcode_base.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
index 85879bf4aacbda15ab313923b91183c67a81f779..41de61f29ca459e8113da7beb73b9a74a31ad994 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
@@ -35,7 +35,7 @@ ninductive mcu_type: Type ≝
 | HCS08 : mcu_type
 | RS08  : mcu_type.
 
-ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
+(*ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
 λP:mcu_type → Prop.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
  match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
 
@@ -45,7 +45,7 @@ ndefinition mcu_type_rec : ΠP:mcu_type → Set.P HC05 → P HC08 → P HCS08 
 
 ndefinition mcu_type_rect : ΠP:mcu_type → Type.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
 λP:mcu_type → Type.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
- match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
+ match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].*)
 
 ndefinition eq_mcutype ≝
 λm1,m2:mcu_type.
@@ -136,7 +136,7 @@ ninductive instr_mode: Type ≝
 | MODE_SRT           : bitrigesim → instr_mode
 .
 
-ndefinition instr_mode_ind
+(*ndefinition instr_mode_ind
  : ΠP:instr_mode → Prop.
    P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
    P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
@@ -227,7 +227,7 @@ ndefinition instr_mode_rect
   | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
   | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
   | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
-  | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
+  | MODE_SRT (d:bitrigesim) ⇒ f3 d ].*)
 
 ndefinition eq_instrmode ≝
 λi1,i2:instr_mode.
@@ -363,7 +363,7 @@ ninductive opcode: Type ≝
 | WAIT   : opcode (* !!wait mode!! *)
 .
 
-ndefinition opcode_ind
+(*ndefinition opcode_ind
  : ΠP:opcode → Prop.
    P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
    P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
@@ -472,7 +472,7 @@ ndefinition opcode_rect
   | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
   | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
   | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
-  | TXS ⇒ p89 | WAIT ⇒ p90 ].
+  | TXS ⇒ p89 | WAIT ⇒ p90 ].*)
 
 ndefinition eq_op ≝
 λop1,op2:opcode.
@@ -529,7 +529,7 @@ ndefinition eq_op ≝
 ninductive any_opcode (m:mcu_type) : Type ≝
  anyOP : opcode → any_opcode m.
 
-ndefinition any_opcode_ind
+(*ndefinition any_opcode_ind
  : Πm:mcu_type.ΠP:any_opcode m → Prop.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
 λm:mcu_type.λP:any_opcode m → Prop.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
  match a with [ anyOP (o:opcode) ⇒ f o ].
@@ -542,7 +542,7 @@ ndefinition any_opcode_rec
 ndefinition any_opcode_rect
  : Πm:mcu_type.ΠP:any_opcode m → Type.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
 λm:mcu_type.λP:any_opcode m → Type.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
- match a with [ anyOP (o:opcode) ⇒ f o ].
+ match a with [ anyOP (o:opcode) ⇒ f o ].*)
 
 ndefinition eq_anyop ≝
 λm:mcu_type.λop1,op2:any_opcode m.
@@ -555,7 +555,7 @@ ninductive byte8_or_word16 : Type ≝
   Byte: byte8  → byte8_or_word16
 | Word: word16 → byte8_or_word16.
 
-ndefinition byte8_or_word16_ind
+(*ndefinition byte8_or_word16_ind
  : ΠP:byte8_or_word16 → Prop.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
 λP:byte8_or_word16 → Prop.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
  match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
@@ -568,7 +568,7 @@ ndefinition byte8_or_word16_rec
 ndefinition byte8_or_word16_rect
  : ΠP:byte8_or_word16 → Type.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
 λP:byte8_or_word16 → Type.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
- match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
+ match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].*)
 
 ndefinition eq_b8w16 ≝
 λbw1,bw2:byte8_or_word16.