Elimination principles are now processed in O(1) again

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
index add19cb99f174e0f3faf2112c27d680906ff6836..a92c4a6e0ef7ee72bc669ba39403337a95e570b4 100755 (executable)
--- 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 }.