From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Jul 2009 16:46:04 +0000 (+0000)
Subject: Elimination principles are now processed in O(1) again
X-Git-Tag: make_still_working~3629
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7b60729bcdcdd820ae78e32a68b59e56e11f1c02;p=helm.git

Elimination principles are now processed in O(1) again
---

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
index 8f6de6f47..d972fe0ba 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
@@ -33,7 +33,7 @@ ninductive ast_base_type : Type ≝
 | AST_BASE_TYPE_WORD16: ast_base_type
 | AST_BASE_TYPE_WORD32: ast_base_type.
 
-ndefinition ast_base_type_ind
+(*ndefinition ast_base_type_ind
  : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
    Πa:ast_base_type.P a ≝
 λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
@@ -53,7 +53,7 @@ ndefinition ast_base_type_rect
 λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
 λa:ast_base_type.
  match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-
+*)
 ninductive ast_type : Type ≝
   AST_TYPE_BASE: ast_base_type → ast_type
 | AST_TYPE_ARRAY: ast_type → nat → ast_type
@@ -69,7 +69,7 @@ nlet rec ast_type_ind_aux (P:ast_type → Prop)
   | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t)
   ].
 
-nlet rec ast_type_ind (P:ast_type → Prop)
+(*nlet rec ast_type_ind (P:ast_type → Prop)
                       (f:Πb.P (AST_TYPE_BASE b))
                       (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
                       (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
@@ -84,7 +84,7 @@ nlet rec ast_type_ind (P:ast_type → Prop)
    ]
   ]. 
 
-nlet rec ast_type_rec_aux (P:ast_type → Set)
+nlet rec ast_type_rec_aux (P:ast_type → Type[0])
                           (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
                           (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
                           (f2:Πt.P t)
@@ -133,7 +133,7 @@ nlet rec ast_type_rect (P:ast_type → Type)
    | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t)
    ]
   ]. 
-
+*)
 ndefinition eq_ast_base_type ≝
 λt1,t2:ast_base_type.match t1 with
  [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
index a4707a5d5..58898142d 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
@@ -37,7 +37,7 @@ ninductive oct : Type ≝
 | o6: oct
 | o7: oct.
 
-ndefinition oct_ind :
+(*ndefinition oct_ind :
  ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
 λP:oct → Prop.
 λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
@@ -57,7 +57,7 @@ ndefinition oct_rect :
 λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
  match n with
   [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
-
+*)
 (* operatore = *)
 ndefinition eq_oct ≝
 λn1,n2:oct.
@@ -136,7 +136,7 @@ ninductive bitrigesim : Type ≝
 | t1E: bitrigesim
 | t1F: bitrigesim.
 
-ndefinition bitrigesim_ind :
+(*ndefinition bitrigesim_ind :
  ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
                       P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
                       P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
@@ -183,7 +183,7 @@ ndefinition bitrigesim_rect :
   | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
   | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
   | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].  
-
+*)
 (* operatore = *)
 ndefinition eq_bitrig ≝
 λt1,t2:bitrigesim.
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
index a93e38947..8e9f08c05 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
@@ -34,7 +34,7 @@ ninductive memory_impl : Type ≝
 | MEM_TREE: memory_impl
 | MEM_BITS: memory_impl.
 
-ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
+(*ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
 λP:memory_impl → Prop.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
  match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
 
@@ -44,7 +44,7 @@ ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE
 
 ndefinition memory_impl_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
 λP:memory_impl → Type.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
- match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
+ match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].*)
 
 (* ausiliario per il tipo della memoria *)
 ndefinition aux_mem_type ≝
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma
index d256fefd8..0ba7735af 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma
@@ -33,7 +33,7 @@ ninductive memory_type : Type ≝
 | MEM_READ_WRITE: memory_type
 | MEM_OUT_OF_BOUND: memory_type.
 
-ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝
+(*ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝
 λP:memory_type → Prop.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type.
  match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ].
 
@@ -44,7 +44,7 @@ ndefinition memory_type_rec : ΠP:memory_type → Set.P MEM_READ_ONLY → P MEM_
 ndefinition memory_type_rect : ΠP:memory_type → Type.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝
 λP:memory_type → Type.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type.
  match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ].
-
+*)
 (* **************** *)
 (* TIPO ARRAY DA 16 *)
 (* **************** *)
@@ -55,7 +55,7 @@ array_16T : T → T → T → T → T → T → T → T →
             T → T → T → T → T → T → T → T →
             Array16T T.
 
-ndefinition Array16T_ind
+(*ndefinition Array16T_ind
  : ΠT:Type.ΠP:Array16T T → Prop.
    (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝
 λT:Type.λP:Array16T T → Prop.
@@ -75,7 +75,7 @@ ndefinition Array16T_rect
 λT:Type.λP:Array16T T → Type.
 λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T.
  match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ].
-
+*)
 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 (* posso definire un getter a matrice sull'array *)
 ndefinition getn_array16T ≝
@@ -337,7 +337,7 @@ ninductive Array8T (T:Type) : Type ≝
 array_8T : T → T → T → T → T → T → T → T →
            Array8T T.
 
-ndefinition Array8T_ind
+(*ndefinition Array8T_ind
  : ΠT:Type.ΠP:Array8T T → Prop.
    (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝
 λT:Type.λP:Array8T T → Prop.
@@ -357,7 +357,7 @@ ndefinition Array8T_rect
 λT:Type.λP:Array8T T → Type.
 λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T.
  match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ].
-
+*)
 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 (* posso definire un getter a matrice sull'array *)
 ndefinition getn_array8T ≝
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 85879bf4a..41de61f29 100755
--- 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.
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
index add19cb99..a92c4a6e0 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
@@ -64,7 +64,7 @@ nrecord alu_HC05: Type ≝
  irq_flag_HC05 : bool
  }.
 
-ndefinition alu_HC05_ind :
+(*ndefinition alu_HC05_ind :
  ΠP:alu_HC05 → Prop.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
 λP:alu_HC05 → Prop.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
  match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
@@ -92,7 +92,7 @@ ndefinition n_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _
 ndefinition z_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
 ndefinition c_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
 ndefinition irq_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
-
+*)
 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
  non associative with precedence 80 for
  @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
@@ -130,7 +130,7 @@ nrecord alu_HC08: Type ≝
  irq_flag_HC08 : bool
  }.
 
-ndefinition alu_HC08_ind :
+(*ndefinition alu_HC08_ind :
  ΠP:alu_HC08 → Prop.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
 λP:alu_HC08 → Prop.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
  match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
@@ -157,7 +157,7 @@ ndefinition n_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _
 ndefinition z_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
 ndefinition c_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
 ndefinition irq_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
-
+*)
 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
  non associative with precedence 80 for
  @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
@@ -200,7 +200,7 @@ nrecord alu_RS08: Type ≝
  c_flag_RS08 : bool
  }.
 
-ndefinition alu_RS08_ind :
+(*ndefinition alu_RS08_ind :
  ΠP:alu_RS08 → Prop.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
 λP:alu_RS08 → Prop.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
  match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
@@ -223,7 +223,7 @@ ndefinition x_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ x _ _ _
 ndefinition ps_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ x _ _ ⇒ x ].
 ndefinition z_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ x _ ⇒ x ].
 ndefinition c_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ _ x ⇒ x ].
-
+*)
 notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}"
  non associative with precedence 80 for
  @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
index 7cb39cd91..8ef0d5234 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -76,7 +76,7 @@ full_info_of_word16_aux m borw (opcode_table m).
 ninductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
-ndefinition t_byte8_ind
+(*ndefinition t_byte8_ind
  : Πm:mcu_type.ΠP:t_byte8 m → Prop.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
 λm:mcu_type.λP:t_byte8 m → Prop.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
  match t with [ TByte (b:byte8) ⇒ f b ].
@@ -89,7 +89,7 @@ ndefinition t_byte8_rec
 ndefinition t_byte8_rect
  : Πm:mcu_type.ΠP:t_byte8 m → Type.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
 λm:mcu_type.λP:t_byte8 m → Type.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
- match t with [ TByte (b:byte8) ⇒ f b ].
+ match t with [ TByte (b:byte8) ⇒ f b ].*)
 
 nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
  #m; #b1; #b2; #H;
@@ -173,7 +173,7 @@ ndefinition instr_mode_ind
   | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
   | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
 
-ndefinition instr_mode_rec
+(*ndefinition instr_mode_rec
  : Πi:instr_mode.ΠP:Πj.MA_check j → Set.
    P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
    (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
@@ -244,7 +244,7 @@ ndefinition instr_mode_rect
   | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
   | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
   | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
-
+*)
 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
    MA_check i → list (t_byte8 m) *)
 ndefinition args_picker ≝
diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
index 35894f570..38d2e7f53 100755
--- a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
@@ -98,7 +98,7 @@ ninductive ascii : Type ≝
 | ch_y: ascii
 | ch_z: ascii.
 
-ndefinition ascii_ind
+(*ndefinition ascii_ind
  : ΠP:ascii → Prop.
    P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
    P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
@@ -149,7 +149,7 @@ ndefinition ascii_rect
   | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
   | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
   | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
-
+*)
 (* confronto fra ascii *)
 ndefinition eq_ascii ≝
 λc,c':ascii.match c with