]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.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_word16.ml
diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml
new file mode 100644 (file)
index 0000000..069774a
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml
@@ -0,0 +1,271 @@
+type word16 =
+Mk_word16 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
+;;
+
+let word16_rec =
+(function f -> (function w -> 
+(match w with 
+   Mk_word16(b,b1) -> (f b b1))
+))
+;;
+
+let word16_rect =
+(function f -> (function w -> 
+(match w with 
+   Mk_word16(b,b1) -> (f b b1))
+))
+;;
+
+let w16h =
+(function w -> 
+(match w with 
+   Mk_word16(w16h,w16l) -> w16h)
+)
+;;
+
+let w16l =
+(function w -> 
+(match w with 
+   Mk_word16(w16h,w16l) -> w16l)
+)
+;;
+
+let eq_w16 =
+(function w1 -> (function w2 -> (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 (w16h w1) (w16h w2)) (Matita_freescale_byte8.eq_b8 (w16l w1) (w16l w2)))))
+;;
+
+let lt_w16 =
+(function w1 -> (function w2 -> 
+(match (Matita_freescale_byte8.lt_b8 (w16h w1) (w16h w2)) with 
+   Matita_datatypes_bool.True -> Matita_datatypes_bool.True
+ | Matita_datatypes_bool.False -> 
+(match (Matita_freescale_byte8.gt_b8 (w16h w1) (w16h w2)) with 
+   Matita_datatypes_bool.True -> Matita_datatypes_bool.False
+ | Matita_datatypes_bool.False -> (Matita_freescale_byte8.lt_b8 (w16l w1) (w16l w2)))
+)
+))
+;;
+
+let le_w16 =
+(function w1 -> (function w2 -> (Matita_freescale_extra.or_bool (eq_w16 w1 w2) (lt_w16 w1 w2))))
+;;
+
+let gt_w16 =
+(function w1 -> (function w2 -> (Matita_freescale_extra.not_bool (le_w16 w1 w2))))
+;;
+
+let ge_w16 =
+(function w1 -> (function w2 -> (Matita_freescale_extra.not_bool (lt_w16 w1 w2))))
+;;
+
+let and_w16 =
+(function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.and_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.and_b8 (w16l w1) (w16l w2))))))
+;;
+
+let or_w16 =
+(function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.or_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.or_b8 (w16l w1) (w16l w2))))))
+;;
+
+let xor_w16 =
+(function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.xor_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.xor_b8 (w16l w1) (w16l w2))))))
+;;
+
+let rcr_w16 =
+(function w -> (function c -> 
+(match (Matita_freescale_byte8.rcr_b8 (w16h w) c) with 
+   Matita_datatypes_constructors.Pair(wh',c') -> 
+(match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with 
+   Matita_datatypes_constructors.Pair(wl',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
+)
+))
+;;
+
+let shr_w16 =
+(function w -> 
+(match (Matita_freescale_byte8.rcr_b8 (w16h w) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(wh',c') -> 
+(match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with 
+   Matita_datatypes_constructors.Pair(wl',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
+)
+)
+;;
+
+let ror_w16 =
+(function w -> 
+(match (Matita_freescale_byte8.rcr_b8 (w16h w) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(wh',c') -> 
+(match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with 
+   Matita_datatypes_constructors.Pair(wl',c'') -> 
+(match c'' with 
+   Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.or_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) wh'),wl'))
+ | Matita_datatypes_bool.False -> (Mk_word16(wh',wl')))
+)
+)
+)
+;;
+
+let ror_w16_n =
+let rec ror_w16_n = 
+(function w -> (function n -> 
+(match n with 
+   Matita_nat_nat.O -> w
+ | Matita_nat_nat.S(n') -> (ror_w16_n (ror_w16 w) n'))
+)) in ror_w16_n
+;;
+
+let rcl_w16 =
+(function w -> (function c -> 
+(match (Matita_freescale_byte8.rcl_b8 (w16l w) c) with 
+   Matita_datatypes_constructors.Pair(wl',c') -> 
+(match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with 
+   Matita_datatypes_constructors.Pair(wh',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
+)
+))
+;;
+
+let shl_w16 =
+(function w -> 
+(match (Matita_freescale_byte8.rcl_b8 (w16l w) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(wl',c') -> 
+(match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with 
+   Matita_datatypes_constructors.Pair(wh',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
+)
+)
+;;
+
+let rol_w16 =
+(function w -> 
+(match (Matita_freescale_byte8.rcl_b8 (w16l w) Matita_datatypes_bool.False) with 
+   Matita_datatypes_constructors.Pair(wl',c') -> 
+(match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with 
+   Matita_datatypes_constructors.Pair(wh',c'') -> 
+(match c'' with 
+   Matita_datatypes_bool.True -> (Mk_word16(wh',(Matita_freescale_byte8.or_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)) wl')))
+ | Matita_datatypes_bool.False -> (Mk_word16(wh',wl')))
+)
+)
+)
+;;
+
+let rol_w16_n =
+let rec rol_w16_n = 
+(function w -> (function n -> 
+(match n with 
+   Matita_nat_nat.O -> w
+ | Matita_nat_nat.S(n') -> (rol_w16_n (rol_w16 w) n'))
+)) in rol_w16_n
+;;
+
+let not_w16 =
+(function w -> (Mk_word16((Matita_freescale_byte8.not_b8 (w16h w)),(Matita_freescale_byte8.not_b8 (w16l w)))))
+;;
+
+let plus_w16 =
+(function w1 -> (function w2 -> (function c -> 
+(match (Matita_freescale_byte8.plus_b8 (w16l w1) (w16l w2) c) with 
+   Matita_datatypes_constructors.Pair(l,c') -> 
+(match (Matita_freescale_byte8.plus_b8 (w16h w1) (w16h w2) c') with 
+   Matita_datatypes_constructors.Pair(h,c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(h,l)),c'')))
+)
+)))
+;;
+
+let plus_w16nc =
+(function w1 -> (function w2 -> (Matita_datatypes_constructors.fst (plus_w16 w1 w2 Matita_datatypes_bool.False))))
+;;
+
+let plus_w16c =
+(function w1 -> (function w2 -> (Matita_datatypes_constructors.snd (plus_w16 w1 w2 Matita_datatypes_bool.False))))
+;;
+
+let mSB_w16 =
+(function w -> (Matita_freescale_exadecim.eq_ex Matita_freescale_exadecim.X8 (Matita_freescale_exadecim.and_ex Matita_freescale_exadecim.X8 (Matita_freescale_byte8.b8h (w16h w)))))
+;;
+
+let nat_of_word16 =
+(function w -> (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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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_byte8.nat_of_byte8 (w16h w))) (Matita_freescale_byte8.nat_of_byte8 (w16l w))))
+;;
+
+let word16_of_nat =
+(function n -> (Mk_word16((Matita_freescale_byte8.byte8_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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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_byte8.byte8_of_nat n))))
+;;
+
+let pred_w16 =
+(function w -> 
+(match (Matita_freescale_byte8.eq_b8 (w16l w) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) with 
+   Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.pred_b8 (w16h w)),(Matita_freescale_byte8.pred_b8 (w16l w))))
+ | Matita_datatypes_bool.False -> (Mk_word16((w16h w),(Matita_freescale_byte8.pred_b8 (w16l w)))))
+)
+;;
+
+let succ_w16 =
+(function w -> 
+(match (Matita_freescale_byte8.eq_b8 (w16l w) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))) with 
+   Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.succ_b8 (w16h w)),(Matita_freescale_byte8.succ_b8 (w16l w))))
+ | Matita_datatypes_bool.False -> (Mk_word16((w16h w),(Matita_freescale_byte8.succ_b8 (w16l w)))))
+)
+;;
+
+let compl_w16 =
+(function w -> 
+(match (mSB_w16 w) with 
+   Matita_datatypes_bool.True -> (succ_w16 (not_w16 w))
+ | Matita_datatypes_bool.False -> (not_w16 (pred_w16 w)))
+)
+;;
+
+let mul_b8 =
+(function b1 -> (function b2 -> 
+(match b1 with 
+   Matita_freescale_byte8.Mk_byte8(b1h,b1l) -> 
+(match b2 with 
+   Matita_freescale_byte8.Mk_byte8(b2h,b2l) -> 
+(match (Matita_freescale_byte8.mul_ex b1l b2l) with 
+   Matita_freescale_byte8.Mk_byte8(t1_h,t1_l) -> 
+(match (Matita_freescale_byte8.mul_ex b1h b2l) with 
+   Matita_freescale_byte8.Mk_byte8(t2_h,t2_l) -> 
+(match (Matita_freescale_byte8.mul_ex b2h b1l) with 
+   Matita_freescale_byte8.Mk_byte8(t3_h,t3_l) -> 
+(match (Matita_freescale_byte8.mul_ex b1h b2h) with 
+   Matita_freescale_byte8.Mk_byte8(t4_h,t4_l) -> (plus_w16nc (plus_w16nc (plus_w16nc (Mk_word16((Matita_freescale_byte8.Mk_byte8(t4_h,t4_l)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,t3_h)),(Matita_freescale_byte8.Mk_byte8(t3_l,Matita_freescale_exadecim.X0))))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,t2_h)),(Matita_freescale_byte8.Mk_byte8(t2_l,Matita_freescale_exadecim.X0))))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(t1_h,t1_l))))))
+)
+)
+)
+)
+)
+))
+;;
+
+let div_b8 =
+(function w -> (function b -> 
+(match (Matita_freescale_byte8.eq_b8 b (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) with 
+   Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(w16l w),Matita_datatypes_bool.True))
+ | Matita_datatypes_bool.False -> 
+(match (eq_w16 w (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with 
+   Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),Matita_datatypes_bool.False))
+ | Matita_datatypes_bool.False -> (let rec aux = 
+(function divd -> (function divs -> (function molt -> (function q -> (function c -> (let w' = (plus_w16nc divd (compl_w16 divs)) in 
+(match c with 
+   Matita_nat_nat.O -> 
+(match (le_w16 divs divd) with 
+   Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.or_b8 molt q),(w16l w'),(Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 (w16h w') (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))
+ | Matita_datatypes_bool.False -> (Matita_freescale_extra.TripleT(q,(w16l divd),(Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 (w16h divd) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))
+
+ | Matita_nat_nat.S(c') -> 
+(match (le_w16 divs divd) with 
+   Matita_datatypes_bool.True -> (aux w' (ror_w16 divs) (Matita_freescale_byte8.ror_b8 molt) (Matita_freescale_byte8.or_b8 molt q) c')
+ | Matita_datatypes_bool.False -> (aux divd (ror_w16 divs) (Matita_freescale_byte8.ror_b8 molt) q c'))
+)
+)))))) in aux w (rol_w16_n (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),b)) (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_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (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))))))))))))))))
+)
+))
+;;
+
+let in_range =
+(function x -> (function inf -> (function sup -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (le_w16 inf sup) (ge_w16 x inf)) (le_w16 x sup)))))
+;;
+
+let forall_word16 =
+(function p -> (Matita_freescale_byte8.forall_byte8 (function bh -> (Matita_freescale_byte8.forall_byte8 (function bl -> (p (Mk_word16(bh,bl))))))))
+;;
+
Unnamed repository; edit this file 'description' to name the repository.