X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Faux_bases.ma;h=262a52868ccb6966b4917d5ed7f2619d4cb9f367;hb=9f580d9bf8f6ba6950b252f587166e95bc8fb1a8;hp=2e71ab1b7d48afca01da193adc03865157286a87;hpb=f8830ea7f8b308241d73e558092089a24ab2f867;p=helm.git

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 2e71ab1b7..262a52868 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
@@ -24,7 +24,7 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-include "freescale/bool.ma".
+include "freescale/byte8.ma".
 include "freescale/nat.ma".
 
 (* ****** *)
@@ -363,6 +363,18 @@ ndefinition nat_of_bitrigesim ≝
   | t10 ⇒ 16 | t11 ⇒ 17 | t12 ⇒ 18 | t13 ⇒ 19 | t14 ⇒ 20 | t15 ⇒ 21 | t16 ⇒ 22 | t17 ⇒ 23
   | t18 ⇒ 24 | t19 ⇒ 25 | t1A ⇒ 26 | t1B ⇒ 27 | t1C ⇒ 28 | t1D ⇒ 29 | t1E ⇒ 30 | t1F ⇒ 31 ].
 
+ndefinition byte8_of_bitrigesim ≝
+λt:bitrigesim.
+ match t with
+  [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
+  | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
+  | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
+  | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
+  | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
+  | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
+  | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
+  | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉 ].
+
 (* iteratore sui bitrigesimali *)
 ndefinition forall_bitrigesim ≝ λP.
  P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗