| xE ⇒ quadruple … true true true false
| xF ⇒ quadruple … true true true true
].
+
ndefinition bits_of_byte8 ≝
λb:byte8.
- mk_Array8T ? (fst4T … (bits_of_exadecim (b8h b)))
- (snd4T … (bits_of_exadecim (b8h b)))
- (thd4T … (bits_of_exadecim (b8h b)))
- (fth4T … (bits_of_exadecim (b8h b)))
- (fst4T … (bits_of_exadecim (b8l b)))
- (snd4T … (bits_of_exadecim (b8l b)))
- (thd4T … (bits_of_exadecim (b8l b)))
- (fth4T … (bits_of_exadecim (b8l b))).
+ mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b)))
+ (snd4T … (bits_of_exadecim (cnH ? b)))
+ (thd4T … (bits_of_exadecim (cnH ? b)))
+ (fth4T … (bits_of_exadecim (cnH ? b)))
+ (fst4T … (bits_of_exadecim (cnL ? b)))
+ (snd4T … (bits_of_exadecim (cnL ? b)))
+ (thd4T … (bits_of_exadecim (cnL ? b)))
+ (fth4T … (bits_of_exadecim (cnL ? b))).