]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_byte8.ml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
branch for universe
[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_freescale_byte8.ml
diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_byte8.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_byte8.ml
new file mode 100644 (file)
index 0000000..8c92bff
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_byte8.ml
@@ -0,0 +1,550 @@
+type byte8 =
+Mk_byte8 of Matita_freescale_exadecim.exadecim * Matita_freescale_exadecim.exadecim
+;;
+
+let byte8_rec =
+(function f -> (function b -> 
+(match b with 
+   Mk_byte8(e,e1) -> (f e e1))
+))
+;;
+
+let byte8_rect =
+(function f -> (function b -> 
+(match b with 
+   Mk_byte8(e,e1) -> (f e e1))
+))
+;;
+
+let b8h =
+(function w -> 
+(match w with 
+   Mk_byte8(b8h,b8l) -> b8h)
+)
+;;
+
+let b8l =
+(function w -> 
+(match w with 
+   Mk_byte8(b8h,b8l) -> b8l)
+)
+;;
+
+let eq_b8 =
+(function b1 -> (function b2 -> (Matita_freescale_extra.and_bool (Matita_freescale_exadecim.eq_ex (b8h b1) (b8h b2)) (Matita_freescale_exadecim.eq_ex (b8l b1) (b8l b2)))))
+;;
+
+let lt_b8 =
+(function b1 -> (function b2 -> 
+(match (Matita_freescale_exadecim.lt_ex (b8h b1) (b8h b2)) with 
+   Matita_datatypes_bool.True -> Matita_datatypes_bool.True
+ | Matita_datatypes_bool.False -> 
+(match (Matita_freescale_exadecim.gt_ex (b8h b1) (b8h b2)) with 
+   Matita_datatypes_bool.True -> Matita_datatypes_bool.False
+ | Matita_datatypes_bool.False -> (Matita_freescale_exadecim.lt_ex (b8l b1) (b8l b2)))
+)
+))
+;;
+
+let le_b8 =
+(function b1 -> (function b2 -> (Matita_freescale_extra.or_bool (eq_b8 b1 b2) (lt_b8 b1 b2))))
+;;
+
+let gt_b8 =
+(function b1 -> (function b2 -> (Matita_freescale_extra.not_bool (le_b8 b1 b2))))
+;;
+
+let ge_b8 =
+(function b1 -> (function b2 -> (Matita_freescale_extra.not_bool (lt_b8 b1 b2))))
+;;
+
+let and_b8 =
+(function b1 -> (function b2 -> (Mk_byte8((Matita_freescale_exadecim.and_ex (b8h b1) (b8h b2)),(Matita_freescale_exadecim.and_ex (b8l b1) (b8l b2))))))
+;;
+
+let or_b8 =
+(function b1 -> (function b2 -> (Mk_byte8((Matita_freescale_exadecim.or_ex (b8h b1) (b8h b2)),(Matita_freescale_exadecim.or_ex (b8l b1) (b8l b2))))))
+;;
+
+let xor_b8 =
+(function b1 -> (function b2 -> (Mk_byte8((Matita_freescale_exadecim.xor_ex (b8h b1) (b8h b2)),(Matita_freescale_exadecim.xor_ex (b8l b1) (b8l b2))))))
+;;
+
+let rcr_b8 =
+(function b -> (function c -> 
+(match (Matita_freescale_exadecim.rcr_ex (b8h b) c) with 
+   Matita_datatypes_constructors.Pair(bh',c') -> 
+(match (Matita_freescale_exadecim.rcr_ex (b8l b) c') with 
+   Matita_datatypes_constructors.Pair(bl',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
+)
+))
+;;
+
+let shr_b8 =
+(function b -> 
+(match (Matita_freescale_exadecim.rcr_ex (b8h b) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(bh',c') -> 
+(match (Matita_freescale_exadecim.rcr_ex (b8l b) c') with 
+   Matita_datatypes_constructors.Pair(bl',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
+)
+)
+;;
+
+let ror_b8 =
+(function b -> 
+(match (Matita_freescale_exadecim.rcr_ex (b8h b) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(bh',c') -> 
+(match (Matita_freescale_exadecim.rcr_ex (b8l b) c') with 
+   Matita_datatypes_constructors.Pair(bl',c'') -> 
+(match c'' with 
+   Matita_datatypes_bool.True -> (Mk_byte8((Matita_freescale_exadecim.or_ex Matita_freescale_exadecim.X8 bh'),bl'))
+ | Matita_datatypes_bool.False -> (Mk_byte8(bh',bl')))
+)
+)
+)
+;;
+
+let ror_b8_n =
+let rec ror_b8_n = 
+(function b -> (function n -> 
+(match n with 
+   Matita_nat_nat.O -> b
+ | Matita_nat_nat.S(n') -> (ror_b8_n (ror_b8 b) n'))
+)) in ror_b8_n
+;;
+
+let rcl_b8 =
+(function b -> (function c -> 
+(match (Matita_freescale_exadecim.rcl_ex (b8l b) c) with 
+   Matita_datatypes_constructors.Pair(bl',c') -> 
+(match (Matita_freescale_exadecim.rcl_ex (b8h b) c') with 
+   Matita_datatypes_constructors.Pair(bh',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
+)
+))
+;;
+
+let shl_b8 =
+(function b -> 
+(match (Matita_freescale_exadecim.rcl_ex (b8l b) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(bl',c') -> 
+(match (Matita_freescale_exadecim.rcl_ex (b8h b) c') with 
+   Matita_datatypes_constructors.Pair(bh',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
+)
+)
+;;
+
+let rol_b8 =
+(function b -> 
+(match (Matita_freescale_exadecim.rcl_ex (b8l b) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(bl',c') -> 
+(match (Matita_freescale_exadecim.rcl_ex (b8h b) c') with 
+   Matita_datatypes_constructors.Pair(bh',c'') -> 
+(match c'' with 
+   Matita_datatypes_bool.True -> (Mk_byte8(bh',(Matita_freescale_exadecim.or_ex Matita_freescale_exadecim.X1 bl')))
+ | Matita_datatypes_bool.False -> (Mk_byte8(bh',bl')))
+)
+)
+)
+;;
+
+let rol_b8_n =
+let rec rol_b8_n = 
+(function b -> (function n -> 
+(match n with 
+   Matita_nat_nat.O -> b
+ | Matita_nat_nat.S(n') -> (rol_b8_n (rol_b8 b) n'))
+)) in rol_b8_n
+;;
+
+let not_b8 =
+(function b -> (Mk_byte8((Matita_freescale_exadecim.not_ex (b8h b)),(Matita_freescale_exadecim.not_ex (b8l b)))))
+;;
+
+let plus_b8 =
+(function b1 -> (function b2 -> (function c -> 
+(match (Matita_freescale_exadecim.plus_ex (b8l b1) (b8l b2) c) with 
+   Matita_datatypes_constructors.Pair(l,c') -> 
+(match (Matita_freescale_exadecim.plus_ex (b8h b1) (b8h b2) c') with 
+   Matita_datatypes_constructors.Pair(h,c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(h,l)),c'')))
+)
+)))
+;;
+
+let plus_b8nc =
+(function b1 -> (function b2 -> (Matita_datatypes_constructors.fst (plus_b8 b1 b2 Matita_datatypes_bool.False))))
+;;
+
+let plus_b8c =
+(function b1 -> (function b2 -> (Matita_datatypes_constructors.snd (plus_b8 b1 b2 Matita_datatypes_bool.False))))
+;;
+
+let mSB_b8 =
+(function b -> (Matita_freescale_exadecim.eq_ex Matita_freescale_exadecim.X8 (Matita_freescale_exadecim.and_ex Matita_freescale_exadecim.X8 (b8h b))))
+;;
+
+let nat_of_byte8 =
+(function b -> (Matita_nat_plus.plus (Matita_nat_times.times (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))) (Matita_freescale_exadecim.nat_of_exadecim (b8h b))) (Matita_freescale_exadecim.nat_of_exadecim (b8l b))))
+;;
+
+let byte8_of_nat =
+(function n -> (Mk_byte8((Matita_freescale_exadecim.exadecim_of_nat (Matita_nat_div_and_mod.div n (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))),(Matita_freescale_exadecim.exadecim_of_nat n))))
+;;
+
+let pred_b8 =
+(function b -> 
+(match (Matita_freescale_exadecim.eq_ex (b8l b) Matita_freescale_exadecim.X0) with 
+   Matita_datatypes_bool.True -> (Mk_byte8((Matita_freescale_exadecim.pred_ex (b8h b)),(Matita_freescale_exadecim.pred_ex (b8l b))))
+ | Matita_datatypes_bool.False -> (Mk_byte8((b8h b),(Matita_freescale_exadecim.pred_ex (b8l b)))))
+)
+;;
+
+let succ_b8 =
+(function b -> 
+(match (Matita_freescale_exadecim.eq_ex (b8l b) Matita_freescale_exadecim.XF) with 
+   Matita_datatypes_bool.True -> (Mk_byte8((Matita_freescale_exadecim.succ_ex (b8h b)),(Matita_freescale_exadecim.succ_ex (b8l b))))
+ | Matita_datatypes_bool.False -> (Mk_byte8((b8h b),(Matita_freescale_exadecim.succ_ex (b8l b)))))
+)
+;;
+
+let compl_b8 =
+(function b -> 
+(match (mSB_b8 b) with 
+   Matita_datatypes_bool.True -> (succ_b8 (not_b8 b))
+ | Matita_datatypes_bool.False -> (not_b8 (pred_b8 b)))
+)
+;;
+
+let mul_ex =
+(function e1 -> (function e2 -> 
+(match e1 with 
+   Matita_freescale_exadecim.X0 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
+
+ | Matita_freescale_exadecim.X1 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF)))
+
+ | Matita_freescale_exadecim.X2 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE)))
+
+ | Matita_freescale_exadecim.X3 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X7))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD)))
+
+ | Matita_freescale_exadecim.X4 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC)))
+
+ | Matita_freescale_exadecim.X5 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X7))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X1))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB)))
+
+ | Matita_freescale_exadecim.X6 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA)))
+
+ | Matita_freescale_exadecim.X7 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X1))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XD))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XB))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X9)))
+
+ | Matita_freescale_exadecim.X8 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8)))
+
+ | Matita_freescale_exadecim.X9 -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X1))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X3))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X5))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X7)))
+
+ | Matita_freescale_exadecim.XA -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X6)))
+
+ | Matita_freescale_exadecim.XB -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X7))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XD))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X3))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X9))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XF))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X5)))
+
+ | Matita_freescale_exadecim.XC -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X4)))
+
+ | Matita_freescale_exadecim.XD -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X7))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X1))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XB))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X5))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XF))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X9))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X3)))
+
+ | Matita_freescale_exadecim.XE -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X2)))
+
+ | Matita_freescale_exadecim.XF -> 
+(match e2 with 
+   Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
+ | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
+ | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
+ | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD))
+ | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
+ | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB))
+ | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA))
+ | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X9))
+ | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8))
+ | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X7))
+ | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X6))
+ | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X5))
+ | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X4))
+ | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X3))
+ | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X2))
+ | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X1)))
+)
+))
+;;
+
+let daa_b8 =
+(function h -> (function c -> (function x -> 
+(match (lt_b8 x (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XA))) with 
+   Matita_datatypes_bool.True -> (let x' = 
+(match (Matita_freescale_extra.and_bool (Matita_freescale_exadecim.lt_ex (b8l x) Matita_freescale_exadecim.XA) (Matita_freescale_extra.not_bool h)) with 
+   Matita_datatypes_bool.True -> x
+ | Matita_datatypes_bool.False -> (plus_b8nc x (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))
+ in (let x'' = 
+(match c with 
+   Matita_datatypes_bool.True -> (plus_b8nc x' (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))
+ | Matita_datatypes_bool.False -> x')
+ in (Matita_datatypes_constructors.Pair(x'',c))))
+ | Matita_datatypes_bool.False -> (let x' = 
+(match (Matita_freescale_extra.and_bool (Matita_freescale_exadecim.lt_ex (b8l x) Matita_freescale_exadecim.XA) (Matita_freescale_extra.not_bool h)) with 
+   Matita_datatypes_bool.True -> x
+ | Matita_datatypes_bool.False -> (plus_b8nc x (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))
+ in (let x'' = (plus_b8nc x' (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0))) in (Matita_datatypes_constructors.Pair(x'',Matita_datatypes_bool.True)))))
+)))
+;;
+
+let forall_byte8 =
+(function p -> (Matita_freescale_exadecim.forall_exadecim (function bh -> (Matita_freescale_exadecim.forall_exadecim (function bl -> (p (Mk_byte8(bh,bl))))))))
+;;
+
Unnamed repository; edit this file 'description' to name the repository.