freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / byte8.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index 260e49ad05a78b0299149c18bae1d4c2cbcb402f..bc7e6f9ceaeb06ced915251f53fc2204695e6d0e 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -346,8 +346,12 @@ ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1
   | xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))
   ].
 
-ndefinition b8_to_recb8 ≝
-λn.b8_to_recb8_aux3 (b8h n) (b8l n) (b8_to_recb8_aux2 (b8h n) (ex_to_recex (b8h n))).
+ndefinition b8_to_recb8 : Πb.rec_byte8 b.
+ #b;
+ nletin K ≝ (b8_to_recb8_aux3 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
+ nelim b in K:(%) ⊢ %;
+ #e1; #e2; nnormalize; #H; napply H.
+nqed.
 
 (* ottali → esadecimali *)
 ndefinition b8_of_bit ≝