freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
index 0c8c6e6339f8e8cb932b90277a73b39e1b27b030..02bd4e1384cafeec5c116a5301ef0c93b4e12886 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/bool_lemmas.ma".
@@ -51,7 +47,7 @@ nlemma pair_destruct_2 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqpair :
+nlemma symmetric_eqpair :
 ∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  (symmetricT T1 bool f1) →
@@ -142,7 +138,7 @@ nlemma triple_destruct_3 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqtriple :
+nlemma symmetric_eqtriple :
 ∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
  (symmetricT T1 bool f1) →
@@ -257,7 +253,7 @@ nlemma quadruple_destruct_4 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqquadruple :
+nlemma symmetric_eqquadruple :
 ∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
  (symmetricT T1 bool f1) →
@@ -397,7 +393,7 @@ nlemma quintuple_destruct_5 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqquintuple :
+nlemma symmetric_eqquintuple :
 ∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
  (symmetricT T1 bool f1) →