From e30e864d61431a0145853fcf90b5f16b781f4a46 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 7 Nov 2018 21:19:05 -0500 Subject: Add `String Notation` vernacular like `Numeral Notation` Users can now register string notations for custom inductives. Much of the code and documentation was copied from numeral notations. I chose to use a 256-constructor inductive for primitive string syntax because (a) it is easy to convert between character codes and constructors, and (b) it is more efficient than the existing `ascii` type. Some choices about proofs of the new `byte` type were made based on efficiency. For example, https://github.com/coq/coq/issues/8517 means that we cannot simply use `Scheme Equality` for this type, and I have taken some care to ensure that the proofs of decidable equality and conversion are fast. (Unfortunately, the `Init/Byte.v` file is the slowest one in the prelude (it takes a couple of seconds to build), and I'm not sure where the slowness is.) In String.v, some uses of `0` as a `nat` were replaced by `O`, because the file initially refused to check interactively otherwise (it complained that `0` could not be interpreted in `string_scope` before loading `Coq.Strings.String`). There is unfortunately a decent amount of code duplication between numeral notations and string notations. I have not put too much thought into chosing names; most names have been chosen to be similar to numeral notations, though I chose the name `byte` from https://github.com/coq/coq/issues/8483#issuecomment-421671785. Unfortunately, this feature does not support declaring string syntax for `list ascii`, unless that type is wrapped in a record or other inductive type. This is not a fundamental limitation; it should be relatively easy for someone who knows the API of the reduction machinery in Coq to extend both this and numeral notations to support any type whose hnf starts with an inductive type. (The reason for needing an inductive type to bottom out at is that this is how the plugin determines what constructors are the entry points for printing the given notation. However, see also https://github.com/coq/coq/issues/8964 for complications that are more likely to arise if inductive type families are supported.) N.B. I generated the long lists of constructors for the `byte` type with short python scripts. Closes #8853 --- theories/Init/Byte.v | 302 ++++++++++++++++++++++++++++++++++++++++++++++++ theories/Init/Prelude.v | 5 + 2 files changed, 307 insertions(+) create mode 100644 theories/Init/Byte.v (limited to 'theories/Init') diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v new file mode 100644 index 0000000000..2d8ee30a43 --- /dev/null +++ b/theories/Init/Byte.v @@ -0,0 +1,302 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* x00 + | (1,0,0,0,0,0,0,0) => x01 + | (0,1,0,0,0,0,0,0) => x02 + | (1,1,0,0,0,0,0,0) => x03 + | (0,0,1,0,0,0,0,0) => x04 + | (1,0,1,0,0,0,0,0) => x05 + | (0,1,1,0,0,0,0,0) => x06 + | (1,1,1,0,0,0,0,0) => x07 + | (0,0,0,1,0,0,0,0) => x08 + | (1,0,0,1,0,0,0,0) => x09 + | (0,1,0,1,0,0,0,0) => x0a + | (1,1,0,1,0,0,0,0) => x0b + | (0,0,1,1,0,0,0,0) => x0c + | (1,0,1,1,0,0,0,0) => x0d + | (0,1,1,1,0,0,0,0) => x0e + | (1,1,1,1,0,0,0,0) => x0f + | (0,0,0,0,1,0,0,0) => x10 + | (1,0,0,0,1,0,0,0) => x11 + | (0,1,0,0,1,0,0,0) => x12 + | (1,1,0,0,1,0,0,0) => x13 + | (0,0,1,0,1,0,0,0) => x14 + | (1,0,1,0,1,0,0,0) => x15 + | (0,1,1,0,1,0,0,0) => x16 + | (1,1,1,0,1,0,0,0) => x17 + | (0,0,0,1,1,0,0,0) => x18 + | (1,0,0,1,1,0,0,0) => x19 + | (0,1,0,1,1,0,0,0) => x1a + | (1,1,0,1,1,0,0,0) => x1b + | (0,0,1,1,1,0,0,0) => x1c + | (1,0,1,1,1,0,0,0) => x1d + | (0,1,1,1,1,0,0,0) => x1e + | (1,1,1,1,1,0,0,0) => x1f + | (0,0,0,0,0,1,0,0) => x20 + | (1,0,0,0,0,1,0,0) => x21 + | (0,1,0,0,0,1,0,0) => x22 + | (1,1,0,0,0,1,0,0) => x23 + | (0,0,1,0,0,1,0,0) => x24 + | (1,0,1,0,0,1,0,0) => x25 + | (0,1,1,0,0,1,0,0) => x26 + | (1,1,1,0,0,1,0,0) => x27 + | (0,0,0,1,0,1,0,0) => x28 + | (1,0,0,1,0,1,0,0) => x29 + | (0,1,0,1,0,1,0,0) => x2a + | (1,1,0,1,0,1,0,0) => x2b + | (0,0,1,1,0,1,0,0) => x2c + | (1,0,1,1,0,1,0,0) => x2d + | (0,1,1,1,0,1,0,0) => x2e + | (1,1,1,1,0,1,0,0) => x2f + | (0,0,0,0,1,1,0,0) => x30 + | (1,0,0,0,1,1,0,0) => x31 + | (0,1,0,0,1,1,0,0) => x32 + | (1,1,0,0,1,1,0,0) => x33 + | (0,0,1,0,1,1,0,0) => x34 + | (1,0,1,0,1,1,0,0) => x35 + | (0,1,1,0,1,1,0,0) => x36 + | (1,1,1,0,1,1,0,0) => x37 + | (0,0,0,1,1,1,0,0) => x38 + | (1,0,0,1,1,1,0,0) => x39 + | (0,1,0,1,1,1,0,0) => x3a + | (1,1,0,1,1,1,0,0) => x3b + | (0,0,1,1,1,1,0,0) => x3c + | (1,0,1,1,1,1,0,0) => x3d + | (0,1,1,1,1,1,0,0) => x3e + | (1,1,1,1,1,1,0,0) => x3f + | (0,0,0,0,0,0,1,0) => x40 + | (1,0,0,0,0,0,1,0) => x41 + | (0,1,0,0,0,0,1,0) => x42 + | (1,1,0,0,0,0,1,0) => x43 + | (0,0,1,0,0,0,1,0) => x44 + | (1,0,1,0,0,0,1,0) => x45 + | (0,1,1,0,0,0,1,0) => x46 + | (1,1,1,0,0,0,1,0) => x47 + | (0,0,0,1,0,0,1,0) => x48 + | (1,0,0,1,0,0,1,0) => x49 + | (0,1,0,1,0,0,1,0) => x4a + | (1,1,0,1,0,0,1,0) => x4b + | (0,0,1,1,0,0,1,0) => x4c + | (1,0,1,1,0,0,1,0) => x4d + | (0,1,1,1,0,0,1,0) => x4e + | (1,1,1,1,0,0,1,0) => x4f + | (0,0,0,0,1,0,1,0) => x50 + | (1,0,0,0,1,0,1,0) => x51 + | (0,1,0,0,1,0,1,0) => x52 + | (1,1,0,0,1,0,1,0) => x53 + | (0,0,1,0,1,0,1,0) => x54 + | (1,0,1,0,1,0,1,0) => x55 + | (0,1,1,0,1,0,1,0) => x56 + | (1,1,1,0,1,0,1,0) => x57 + | (0,0,0,1,1,0,1,0) => x58 + | (1,0,0,1,1,0,1,0) => x59 + | (0,1,0,1,1,0,1,0) => x5a + | (1,1,0,1,1,0,1,0) => x5b + | (0,0,1,1,1,0,1,0) => x5c + | (1,0,1,1,1,0,1,0) => x5d + | (0,1,1,1,1,0,1,0) => x5e + | (1,1,1,1,1,0,1,0) => x5f + | (0,0,0,0,0,1,1,0) => x60 + | (1,0,0,0,0,1,1,0) => x61 + | (0,1,0,0,0,1,1,0) => x62 + | (1,1,0,0,0,1,1,0) => x63 + | (0,0,1,0,0,1,1,0) => x64 + | (1,0,1,0,0,1,1,0) => x65 + | (0,1,1,0,0,1,1,0) => x66 + | (1,1,1,0,0,1,1,0) => x67 + | (0,0,0,1,0,1,1,0) => x68 + | (1,0,0,1,0,1,1,0) => x69 + | (0,1,0,1,0,1,1,0) => x6a + | (1,1,0,1,0,1,1,0) => x6b + | (0,0,1,1,0,1,1,0) => x6c + | (1,0,1,1,0,1,1,0) => x6d + | (0,1,1,1,0,1,1,0) => x6e + | (1,1,1,1,0,1,1,0) => x6f + | (0,0,0,0,1,1,1,0) => x70 + | (1,0,0,0,1,1,1,0) => x71 + | (0,1,0,0,1,1,1,0) => x72 + | (1,1,0,0,1,1,1,0) => x73 + | (0,0,1,0,1,1,1,0) => x74 + | (1,0,1,0,1,1,1,0) => x75 + | (0,1,1,0,1,1,1,0) => x76 + | (1,1,1,0,1,1,1,0) => x77 + | (0,0,0,1,1,1,1,0) => x78 + | (1,0,0,1,1,1,1,0) => x79 + | (0,1,0,1,1,1,1,0) => x7a + | (1,1,0,1,1,1,1,0) => x7b + | (0,0,1,1,1,1,1,0) => x7c + | (1,0,1,1,1,1,1,0) => x7d + | (0,1,1,1,1,1,1,0) => x7e + | (1,1,1,1,1,1,1,0) => x7f + | (0,0,0,0,0,0,0,1) => x80 + | (1,0,0,0,0,0,0,1) => x81 + | (0,1,0,0,0,0,0,1) => x82 + | (1,1,0,0,0,0,0,1) => x83 + | (0,0,1,0,0,0,0,1) => x84 + | (1,0,1,0,0,0,0,1) => x85 + | (0,1,1,0,0,0,0,1) => x86 + | (1,1,1,0,0,0,0,1) => x87 + | (0,0,0,1,0,0,0,1) => x88 + | (1,0,0,1,0,0,0,1) => x89 + | (0,1,0,1,0,0,0,1) => x8a + | (1,1,0,1,0,0,0,1) => x8b + | (0,0,1,1,0,0,0,1) => x8c + | (1,0,1,1,0,0,0,1) => x8d + | (0,1,1,1,0,0,0,1) => x8e + | (1,1,1,1,0,0,0,1) => x8f + | (0,0,0,0,1,0,0,1) => x90 + | (1,0,0,0,1,0,0,1) => x91 + | (0,1,0,0,1,0,0,1) => x92 + | (1,1,0,0,1,0,0,1) => x93 + | (0,0,1,0,1,0,0,1) => x94 + | (1,0,1,0,1,0,0,1) => x95 + | (0,1,1,0,1,0,0,1) => x96 + | (1,1,1,0,1,0,0,1) => x97 + | (0,0,0,1,1,0,0,1) => x98 + | (1,0,0,1,1,0,0,1) => x99 + | (0,1,0,1,1,0,0,1) => x9a + | (1,1,0,1,1,0,0,1) => x9b + | (0,0,1,1,1,0,0,1) => x9c + | (1,0,1,1,1,0,0,1) => x9d + | (0,1,1,1,1,0,0,1) => x9e + | (1,1,1,1,1,0,0,1) => x9f + | (0,0,0,0,0,1,0,1) => xa0 + | (1,0,0,0,0,1,0,1) => xa1 + | (0,1,0,0,0,1,0,1) => xa2 + | (1,1,0,0,0,1,0,1) => xa3 + | (0,0,1,0,0,1,0,1) => xa4 + | (1,0,1,0,0,1,0,1) => xa5 + | (0,1,1,0,0,1,0,1) => xa6 + | (1,1,1,0,0,1,0,1) => xa7 + | (0,0,0,1,0,1,0,1) => xa8 + | (1,0,0,1,0,1,0,1) => xa9 + | (0,1,0,1,0,1,0,1) => xaa + | (1,1,0,1,0,1,0,1) => xab + | (0,0,1,1,0,1,0,1) => xac + | (1,0,1,1,0,1,0,1) => xad + | (0,1,1,1,0,1,0,1) => xae + | (1,1,1,1,0,1,0,1) => xaf + | (0,0,0,0,1,1,0,1) => xb0 + | (1,0,0,0,1,1,0,1) => xb1 + | (0,1,0,0,1,1,0,1) => xb2 + | (1,1,0,0,1,1,0,1) => xb3 + | (0,0,1,0,1,1,0,1) => xb4 + | (1,0,1,0,1,1,0,1) => xb5 + | (0,1,1,0,1,1,0,1) => xb6 + | (1,1,1,0,1,1,0,1) => xb7 + | (0,0,0,1,1,1,0,1) => xb8 + | (1,0,0,1,1,1,0,1) => xb9 + | (0,1,0,1,1,1,0,1) => xba + | (1,1,0,1,1,1,0,1) => xbb + | (0,0,1,1,1,1,0,1) => xbc + | (1,0,1,1,1,1,0,1) => xbd + | (0,1,1,1,1,1,0,1) => xbe + | (1,1,1,1,1,1,0,1) => xbf + | (0,0,0,0,0,0,1,1) => xc0 + | (1,0,0,0,0,0,1,1) => xc1 + | (0,1,0,0,0,0,1,1) => xc2 + | (1,1,0,0,0,0,1,1) => xc3 + | (0,0,1,0,0,0,1,1) => xc4 + | (1,0,1,0,0,0,1,1) => xc5 + | (0,1,1,0,0,0,1,1) => xc6 + | (1,1,1,0,0,0,1,1) => xc7 + | (0,0,0,1,0,0,1,1) => xc8 + | (1,0,0,1,0,0,1,1) => xc9 + | (0,1,0,1,0,0,1,1) => xca + | (1,1,0,1,0,0,1,1) => xcb + | (0,0,1,1,0,0,1,1) => xcc + | (1,0,1,1,0,0,1,1) => xcd + | (0,1,1,1,0,0,1,1) => xce + | (1,1,1,1,0,0,1,1) => xcf + | (0,0,0,0,1,0,1,1) => xd0 + | (1,0,0,0,1,0,1,1) => xd1 + | (0,1,0,0,1,0,1,1) => xd2 + | (1,1,0,0,1,0,1,1) => xd3 + | (0,0,1,0,1,0,1,1) => xd4 + | (1,0,1,0,1,0,1,1) => xd5 + | (0,1,1,0,1,0,1,1) => xd6 + | (1,1,1,0,1,0,1,1) => xd7 + | (0,0,0,1,1,0,1,1) => xd8 + | (1,0,0,1,1,0,1,1) => xd9 + | (0,1,0,1,1,0,1,1) => xda + | (1,1,0,1,1,0,1,1) => xdb + | (0,0,1,1,1,0,1,1) => xdc + | (1,0,1,1,1,0,1,1) => xdd + | (0,1,1,1,1,0,1,1) => xde + | (1,1,1,1,1,0,1,1) => xdf + | (0,0,0,0,0,1,1,1) => xe0 + | (1,0,0,0,0,1,1,1) => xe1 + | (0,1,0,0,0,1,1,1) => xe2 + | (1,1,0,0,0,1,1,1) => xe3 + | (0,0,1,0,0,1,1,1) => xe4 + | (1,0,1,0,0,1,1,1) => xe5 + | (0,1,1,0,0,1,1,1) => xe6 + | (1,1,1,0,0,1,1,1) => xe7 + | (0,0,0,1,0,1,1,1) => xe8 + | (1,0,0,1,0,1,1,1) => xe9 + | (0,1,0,1,0,1,1,1) => xea + | (1,1,0,1,0,1,1,1) => xeb + | (0,0,1,1,0,1,1,1) => xec + | (1,0,1,1,0,1,1,1) => xed + | (0,1,1,1,0,1,1,1) => xee + | (1,1,1,1,0,1,1,1) => xef + | (0,0,0,0,1,1,1,1) => xf0 + | (1,0,0,0,1,1,1,1) => xf1 + | (0,1,0,0,1,1,1,1) => xf2 + | (1,1,0,0,1,1,1,1) => xf3 + | (0,0,1,0,1,1,1,1) => xf4 + | (1,0,1,0,1,1,1,1) => xf5 + | (0,1,1,0,1,1,1,1) => xf6 + | (1,1,1,0,1,1,1,1) => xf7 + | (0,0,0,1,1,1,1,1) => xf8 + | (1,0,0,1,1,1,1,1) => xf9 + | (0,1,0,1,1,1,1,1) => xfa + | (1,1,0,1,1,1,1,1) => xfb + | (0,0,1,1,1,1,1,1) => xfc + | (1,0,1,1,1,1,1,1) => xfd + | (0,1,1,1,1,1,1,1) => xfe + | (1,1,1,1,1,1,1,1) => xff + end. + +Definition to_bits (b : byte) : bool * bool * bool * bool * bool * bool * bool * bool + := match b with + | x00 => (0,0,0,0,0,0,0,0) + | x01 => (1,0,0,0,0,0,0,0) + | x02 => (0,1,0,0,0,0,0,0) + | x03 => (1,1,0,0,0,0,0,0) + | x04 => (0,0,1,0,0,0,0,0) + | x05 => (1,0,1,0,0,0,0,0) + | x06 => (0,1,1,0,0,0,0,0) + | x07 => (1,1,1,0,0,0,0,0) + | x08 => (0,0,0,1,0,0,0,0) + | x09 => (1,0,0,1,0,0,0,0) + | x0a => (0,1,0,1,0,0,0,0) + | x0b => (1,1,0,1,0,0,0,0) + | x0c => (0,0,1,1,0,0,0,0) + | x0d => (1,0,1,1,0,0,0,0) + | x0e => (0,1,1,1,0,0,0,0) + | x0f => (1,1,1,1,0,0,0,0) + | x10 => (0,0,0,0,1,0,0,0) + | x11 => (1,0,0,0,1,0,0,0) + | x12 => (0,1,0,0,1,0,0,0) + | x13 => (1,1,0,0,1,0,0,0) + | x14 => (0,0,1,0,1,0,0,0) + | x15 => (1,0,1,0,1,0,0,0) + | x16 => (0,1,1,0,1,0,0,0) + | x17 => (1,1,1,0,1,0,0,0) + | x18 => (0,0,0,1,1,0,0,0) + | x19 => (1,0,0,1,1,0,0,0) + | x1a => (0,1,0,1,1,0,0,0) + | x1b => (1,1,0,1,1,0,0,0) + | x1c => (0,0,1,1,1,0,0,0) + | x1d => (1,0,1,1,1,0,0,0) + | x1e => (0,1,1,1,1,0,0,0) + | x1f => (1,1,1,1,1,0,0,0) + | x20 => (0,0,0,0,0,1,0,0) + | x21 => (1,0,0,0,0,1,0,0) + | x22 => (0,1,0,0,0,1,0,0) + | x23 => (1,1,0,0,0,1,0,0) + | x24 => (0,0,1,0,0,1,0,0) + | x25 => (1,0,1,0,0,1,0,0) + | x26 => (0,1,1,0,0,1,0,0) + | x27 => (1,1,1,0,0,1,0,0) + | x28 => (0,0,0,1,0,1,0,0) + | x29 => (1,0,0,1,0,1,0,0) + | x2a => (0,1,0,1,0,1,0,0) + | x2b => (1,1,0,1,0,1,0,0) + | x2c => (0,0,1,1,0,1,0,0) + | x2d => (1,0,1,1,0,1,0,0) + | x2e => (0,1,1,1,0,1,0,0) + | x2f => (1,1,1,1,0,1,0,0) + | x30 => (0,0,0,0,1,1,0,0) + | x31 => (1,0,0,0,1,1,0,0) + | x32 => (0,1,0,0,1,1,0,0) + | x33 => (1,1,0,0,1,1,0,0) + | x34 => (0,0,1,0,1,1,0,0) + | x35 => (1,0,1,0,1,1,0,0) + | x36 => (0,1,1,0,1,1,0,0) + | x37 => (1,1,1,0,1,1,0,0) + | x38 => (0,0,0,1,1,1,0,0) + | x39 => (1,0,0,1,1,1,0,0) + | x3a => (0,1,0,1,1,1,0,0) + | x3b => (1,1,0,1,1,1,0,0) + | x3c => (0,0,1,1,1,1,0,0) + | x3d => (1,0,1,1,1,1,0,0) + | x3e => (0,1,1,1,1,1,0,0) + | x3f => (1,1,1,1,1,1,0,0) + | x40 => (0,0,0,0,0,0,1,0) + | x41 => (1,0,0,0,0,0,1,0) + | x42 => (0,1,0,0,0,0,1,0) + | x43 => (1,1,0,0,0,0,1,0) + | x44 => (0,0,1,0,0,0,1,0) + | x45 => (1,0,1,0,0,0,1,0) + | x46 => (0,1,1,0,0,0,1,0) + | x47 => (1,1,1,0,0,0,1,0) + | x48 => (0,0,0,1,0,0,1,0) + | x49 => (1,0,0,1,0,0,1,0) + | x4a => (0,1,0,1,0,0,1,0) + | x4b => (1,1,0,1,0,0,1,0) + | x4c => (0,0,1,1,0,0,1,0) + | x4d => (1,0,1,1,0,0,1,0) + | x4e => (0,1,1,1,0,0,1,0) + | x4f => (1,1,1,1,0,0,1,0) + | x50 => (0,0,0,0,1,0,1,0) + | x51 => (1,0,0,0,1,0,1,0) + | x52 => (0,1,0,0,1,0,1,0) + | x53 => (1,1,0,0,1,0,1,0) + | x54 => (0,0,1,0,1,0,1,0) + | x55 => (1,0,1,0,1,0,1,0) + | x56 => (0,1,1,0,1,0,1,0) + | x57 => (1,1,1,0,1,0,1,0) + | x58 => (0,0,0,1,1,0,1,0) + | x59 => (1,0,0,1,1,0,1,0) + | x5a => (0,1,0,1,1,0,1,0) + | x5b => (1,1,0,1,1,0,1,0) + | x5c => (0,0,1,1,1,0,1,0) + | x5d => (1,0,1,1,1,0,1,0) + | x5e => (0,1,1,1,1,0,1,0) + | x5f => (1,1,1,1,1,0,1,0) + | x60 => (0,0,0,0,0,1,1,0) + | x61 => (1,0,0,0,0,1,1,0) + | x62 => (0,1,0,0,0,1,1,0) + | x63 => (1,1,0,0,0,1,1,0) + | x64 => (0,0,1,0,0,1,1,0) + | x65 => (1,0,1,0,0,1,1,0) + | x66 => (0,1,1,0,0,1,1,0) + | x67 => (1,1,1,0,0,1,1,0) + | x68 => (0,0,0,1,0,1,1,0) + | x69 => (1,0,0,1,0,1,1,0) + | x6a => (0,1,0,1,0,1,1,0) + | x6b => (1,1,0,1,0,1,1,0) + | x6c => (0,0,1,1,0,1,1,0) + | x6d => (1,0,1,1,0,1,1,0) + | x6e => (0,1,1,1,0,1,1,0) + | x6f => (1,1,1,1,0,1,1,0) + | x70 => (0,0,0,0,1,1,1,0) + | x71 => (1,0,0,0,1,1,1,0) + | x72 => (0,1,0,0,1,1,1,0) + | x73 => (1,1,0,0,1,1,1,0) + | x74 => (0,0,1,0,1,1,1,0) + | x75 => (1,0,1,0,1,1,1,0) + | x76 => (0,1,1,0,1,1,1,0) + | x77 => (1,1,1,0,1,1,1,0) + | x78 => (0,0,0,1,1,1,1,0) + | x79 => (1,0,0,1,1,1,1,0) + | x7a => (0,1,0,1,1,1,1,0) + | x7b => (1,1,0,1,1,1,1,0) + | x7c => (0,0,1,1,1,1,1,0) + | x7d => (1,0,1,1,1,1,1,0) + | x7e => (0,1,1,1,1,1,1,0) + | x7f => (1,1,1,1,1,1,1,0) + | x80 => (0,0,0,0,0,0,0,1) + | x81 => (1,0,0,0,0,0,0,1) + | x82 => (0,1,0,0,0,0,0,1) + | x83 => (1,1,0,0,0,0,0,1) + | x84 => (0,0,1,0,0,0,0,1) + | x85 => (1,0,1,0,0,0,0,1) + | x86 => (0,1,1,0,0,0,0,1) + | x87 => (1,1,1,0,0,0,0,1) + | x88 => (0,0,0,1,0,0,0,1) + | x89 => (1,0,0,1,0,0,0,1) + | x8a => (0,1,0,1,0,0,0,1) + | x8b => (1,1,0,1,0,0,0,1) + | x8c => (0,0,1,1,0,0,0,1) + | x8d => (1,0,1,1,0,0,0,1) + | x8e => (0,1,1,1,0,0,0,1) + | x8f => (1,1,1,1,0,0,0,1) + | x90 => (0,0,0,0,1,0,0,1) + | x91 => (1,0,0,0,1,0,0,1) + | x92 => (0,1,0,0,1,0,0,1) + | x93 => (1,1,0,0,1,0,0,1) + | x94 => (0,0,1,0,1,0,0,1) + | x95 => (1,0,1,0,1,0,0,1) + | x96 => (0,1,1,0,1,0,0,1) + | x97 => (1,1,1,0,1,0,0,1) + | x98 => (0,0,0,1,1,0,0,1) + | x99 => (1,0,0,1,1,0,0,1) + | x9a => (0,1,0,1,1,0,0,1) + | x9b => (1,1,0,1,1,0,0,1) + | x9c => (0,0,1,1,1,0,0,1) + | x9d => (1,0,1,1,1,0,0,1) + | x9e => (0,1,1,1,1,0,0,1) + | x9f => (1,1,1,1,1,0,0,1) + | xa0 => (0,0,0,0,0,1,0,1) + | xa1 => (1,0,0,0,0,1,0,1) + | xa2 => (0,1,0,0,0,1,0,1) + | xa3 => (1,1,0,0,0,1,0,1) + | xa4 => (0,0,1,0,0,1,0,1) + | xa5 => (1,0,1,0,0,1,0,1) + | xa6 => (0,1,1,0,0,1,0,1) + | xa7 => (1,1,1,0,0,1,0,1) + | xa8 => (0,0,0,1,0,1,0,1) + | xa9 => (1,0,0,1,0,1,0,1) + | xaa => (0,1,0,1,0,1,0,1) + | xab => (1,1,0,1,0,1,0,1) + | xac => (0,0,1,1,0,1,0,1) + | xad => (1,0,1,1,0,1,0,1) + | xae => (0,1,1,1,0,1,0,1) + | xaf => (1,1,1,1,0,1,0,1) + | xb0 => (0,0,0,0,1,1,0,1) + | xb1 => (1,0,0,0,1,1,0,1) + | xb2 => (0,1,0,0,1,1,0,1) + | xb3 => (1,1,0,0,1,1,0,1) + | xb4 => (0,0,1,0,1,1,0,1) + | xb5 => (1,0,1,0,1,1,0,1) + | xb6 => (0,1,1,0,1,1,0,1) + | xb7 => (1,1,1,0,1,1,0,1) + | xb8 => (0,0,0,1,1,1,0,1) + | xb9 => (1,0,0,1,1,1,0,1) + | xba => (0,1,0,1,1,1,0,1) + | xbb => (1,1,0,1,1,1,0,1) + | xbc => (0,0,1,1,1,1,0,1) + | xbd => (1,0,1,1,1,1,0,1) + | xbe => (0,1,1,1,1,1,0,1) + | xbf => (1,1,1,1,1,1,0,1) + | xc0 => (0,0,0,0,0,0,1,1) + | xc1 => (1,0,0,0,0,0,1,1) + | xc2 => (0,1,0,0,0,0,1,1) + | xc3 => (1,1,0,0,0,0,1,1) + | xc4 => (0,0,1,0,0,0,1,1) + | xc5 => (1,0,1,0,0,0,1,1) + | xc6 => (0,1,1,0,0,0,1,1) + | xc7 => (1,1,1,0,0,0,1,1) + | xc8 => (0,0,0,1,0,0,1,1) + | xc9 => (1,0,0,1,0,0,1,1) + | xca => (0,1,0,1,0,0,1,1) + | xcb => (1,1,0,1,0,0,1,1) + | xcc => (0,0,1,1,0,0,1,1) + | xcd => (1,0,1,1,0,0,1,1) + | xce => (0,1,1,1,0,0,1,1) + | xcf => (1,1,1,1,0,0,1,1) + | xd0 => (0,0,0,0,1,0,1,1) + | xd1 => (1,0,0,0,1,0,1,1) + | xd2 => (0,1,0,0,1,0,1,1) + | xd3 => (1,1,0,0,1,0,1,1) + | xd4 => (0,0,1,0,1,0,1,1) + | xd5 => (1,0,1,0,1,0,1,1) + | xd6 => (0,1,1,0,1,0,1,1) + | xd7 => (1,1,1,0,1,0,1,1) + | xd8 => (0,0,0,1,1,0,1,1) + | xd9 => (1,0,0,1,1,0,1,1) + | xda => (0,1,0,1,1,0,1,1) + | xdb => (1,1,0,1,1,0,1,1) + | xdc => (0,0,1,1,1,0,1,1) + | xdd => (1,0,1,1,1,0,1,1) + | xde => (0,1,1,1,1,0,1,1) + | xdf => (1,1,1,1,1,0,1,1) + | xe0 => (0,0,0,0,0,1,1,1) + | xe1 => (1,0,0,0,0,1,1,1) + | xe2 => (0,1,0,0,0,1,1,1) + | xe3 => (1,1,0,0,0,1,1,1) + | xe4 => (0,0,1,0,0,1,1,1) + | xe5 => (1,0,1,0,0,1,1,1) + | xe6 => (0,1,1,0,0,1,1,1) + | xe7 => (1,1,1,0,0,1,1,1) + | xe8 => (0,0,0,1,0,1,1,1) + | xe9 => (1,0,0,1,0,1,1,1) + | xea => (0,1,0,1,0,1,1,1) + | xeb => (1,1,0,1,0,1,1,1) + | xec => (0,0,1,1,0,1,1,1) + | xed => (1,0,1,1,0,1,1,1) + | xee => (0,1,1,1,0,1,1,1) + | xef => (1,1,1,1,0,1,1,1) + | xf0 => (0,0,0,0,1,1,1,1) + | xf1 => (1,0,0,0,1,1,1,1) + | xf2 => (0,1,0,0,1,1,1,1) + | xf3 => (1,1,0,0,1,1,1,1) + | xf4 => (0,0,1,0,1,1,1,1) + | xf5 => (1,0,1,0,1,1,1,1) + | xf6 => (0,1,1,0,1,1,1,1) + | xf7 => (1,1,1,0,1,1,1,1) + | xf8 => (0,0,0,1,1,1,1,1) + | xf9 => (1,0,0,1,1,1,1,1) + | xfa => (0,1,0,1,1,1,1,1) + | xfb => (1,1,0,1,1,1,1,1) + | xfc => (0,0,1,1,1,1,1,1) + | xfd => (1,0,1,1,1,1,1,1) + | xfe => (0,1,1,1,1,1,1,1) + | xff => (1,1,1,1,1,1,1,1) + end. + +Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b. +Proof. destruct b; exact eq_refl. Qed. + +Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b. +Proof. + repeat match goal with + | p : prod _ _ |- _ => destruct p + | b : bool |- _ => destruct b + end; + exact eq_refl. +Qed. Definition byte_of_byte (b : byte) : byte := b. Module Export ByteSyntaxNotations. String Notation byte byte_of_byte byte_of_byte : byte_scope. End ByteSyntaxNotations. - -Module Export ByteNotations. - Export ByteSyntaxNotations. - Infix "=?" := eqb (at level 70) : byte_scope. -End ByteNotations. -- cgit v1.2.3 From f5e3d9e29f030a86433bb2700e55c4c183593163 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Nov 2018 15:16:31 -0500 Subject: Byte.v: use right-associative tuples in bits We encode the conversion to bits with little-endian right-associative tuples to ensure that the head of the tuple (the `fst` element) is the least significant bit. We still enforce that the ordering of bits matches the order of the `bool`s in the `ascii` inductive type. --- theories/Init/Byte.v | 1028 +++++++++++++++++++++++++------------------------- 1 file changed, 514 insertions(+), 514 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index 59b5f5ebe3..eede9d5028 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -291,524 +291,524 @@ Local Notation "0" := false. Local Notation "1" := true. (** We pick a definition that matches with [Ascii.ascii] *) -Definition of_bits (b : bool * bool * bool * bool * bool * bool * bool * bool) : byte +Definition of_bits (b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))) : byte := match b with - | (0,0,0,0,0,0,0,0) => x00 - | (1,0,0,0,0,0,0,0) => x01 - | (0,1,0,0,0,0,0,0) => x02 - | (1,1,0,0,0,0,0,0) => x03 - | (0,0,1,0,0,0,0,0) => x04 - | (1,0,1,0,0,0,0,0) => x05 - | (0,1,1,0,0,0,0,0) => x06 - | (1,1,1,0,0,0,0,0) => x07 - | (0,0,0,1,0,0,0,0) => x08 - | (1,0,0,1,0,0,0,0) => x09 - | (0,1,0,1,0,0,0,0) => x0a - | (1,1,0,1,0,0,0,0) => x0b - | (0,0,1,1,0,0,0,0) => x0c - | (1,0,1,1,0,0,0,0) => x0d - | (0,1,1,1,0,0,0,0) => x0e - | (1,1,1,1,0,0,0,0) => x0f - | (0,0,0,0,1,0,0,0) => x10 - | (1,0,0,0,1,0,0,0) => x11 - | (0,1,0,0,1,0,0,0) => x12 - | (1,1,0,0,1,0,0,0) => x13 - | (0,0,1,0,1,0,0,0) => x14 - | (1,0,1,0,1,0,0,0) => x15 - | (0,1,1,0,1,0,0,0) => x16 - | (1,1,1,0,1,0,0,0) => x17 - | (0,0,0,1,1,0,0,0) => x18 - | (1,0,0,1,1,0,0,0) => x19 - | (0,1,0,1,1,0,0,0) => x1a - | (1,1,0,1,1,0,0,0) => x1b - | (0,0,1,1,1,0,0,0) => x1c - | (1,0,1,1,1,0,0,0) => x1d - | (0,1,1,1,1,0,0,0) => x1e - | (1,1,1,1,1,0,0,0) => x1f - | (0,0,0,0,0,1,0,0) => x20 - | (1,0,0,0,0,1,0,0) => x21 - | (0,1,0,0,0,1,0,0) => x22 - | (1,1,0,0,0,1,0,0) => x23 - | (0,0,1,0,0,1,0,0) => x24 - | (1,0,1,0,0,1,0,0) => x25 - | (0,1,1,0,0,1,0,0) => x26 - | (1,1,1,0,0,1,0,0) => x27 - | (0,0,0,1,0,1,0,0) => x28 - | (1,0,0,1,0,1,0,0) => x29 - | (0,1,0,1,0,1,0,0) => x2a - | (1,1,0,1,0,1,0,0) => x2b - | (0,0,1,1,0,1,0,0) => x2c - | (1,0,1,1,0,1,0,0) => x2d - | (0,1,1,1,0,1,0,0) => x2e - | (1,1,1,1,0,1,0,0) => x2f - | (0,0,0,0,1,1,0,0) => x30 - | (1,0,0,0,1,1,0,0) => x31 - | (0,1,0,0,1,1,0,0) => x32 - | (1,1,0,0,1,1,0,0) => x33 - | (0,0,1,0,1,1,0,0) => x34 - | (1,0,1,0,1,1,0,0) => x35 - | (0,1,1,0,1,1,0,0) => x36 - | (1,1,1,0,1,1,0,0) => x37 - | (0,0,0,1,1,1,0,0) => x38 - | (1,0,0,1,1,1,0,0) => x39 - | (0,1,0,1,1,1,0,0) => x3a - | (1,1,0,1,1,1,0,0) => x3b - | (0,0,1,1,1,1,0,0) => x3c - | (1,0,1,1,1,1,0,0) => x3d - | (0,1,1,1,1,1,0,0) => x3e - | (1,1,1,1,1,1,0,0) => x3f - | (0,0,0,0,0,0,1,0) => x40 - | (1,0,0,0,0,0,1,0) => x41 - | (0,1,0,0,0,0,1,0) => x42 - | (1,1,0,0,0,0,1,0) => x43 - | (0,0,1,0,0,0,1,0) => x44 - | (1,0,1,0,0,0,1,0) => x45 - | (0,1,1,0,0,0,1,0) => x46 - | (1,1,1,0,0,0,1,0) => x47 - | (0,0,0,1,0,0,1,0) => x48 - | (1,0,0,1,0,0,1,0) => x49 - | (0,1,0,1,0,0,1,0) => x4a - | (1,1,0,1,0,0,1,0) => x4b - | (0,0,1,1,0,0,1,0) => x4c - | (1,0,1,1,0,0,1,0) => x4d - | (0,1,1,1,0,0,1,0) => x4e - | (1,1,1,1,0,0,1,0) => x4f - | (0,0,0,0,1,0,1,0) => x50 - | (1,0,0,0,1,0,1,0) => x51 - | (0,1,0,0,1,0,1,0) => x52 - | (1,1,0,0,1,0,1,0) => x53 - | (0,0,1,0,1,0,1,0) => x54 - | (1,0,1,0,1,0,1,0) => x55 - | (0,1,1,0,1,0,1,0) => x56 - | (1,1,1,0,1,0,1,0) => x57 - | (0,0,0,1,1,0,1,0) => x58 - | (1,0,0,1,1,0,1,0) => x59 - | (0,1,0,1,1,0,1,0) => x5a - | (1,1,0,1,1,0,1,0) => x5b - | (0,0,1,1,1,0,1,0) => x5c - | (1,0,1,1,1,0,1,0) => x5d - | (0,1,1,1,1,0,1,0) => x5e - | (1,1,1,1,1,0,1,0) => x5f - | (0,0,0,0,0,1,1,0) => x60 - | (1,0,0,0,0,1,1,0) => x61 - | (0,1,0,0,0,1,1,0) => x62 - | (1,1,0,0,0,1,1,0) => x63 - | (0,0,1,0,0,1,1,0) => x64 - | (1,0,1,0,0,1,1,0) => x65 - | (0,1,1,0,0,1,1,0) => x66 - | (1,1,1,0,0,1,1,0) => x67 - | (0,0,0,1,0,1,1,0) => x68 - | (1,0,0,1,0,1,1,0) => x69 - | (0,1,0,1,0,1,1,0) => x6a - | (1,1,0,1,0,1,1,0) => x6b - | (0,0,1,1,0,1,1,0) => x6c - | (1,0,1,1,0,1,1,0) => x6d - | (0,1,1,1,0,1,1,0) => x6e - | (1,1,1,1,0,1,1,0) => x6f - | (0,0,0,0,1,1,1,0) => x70 - | (1,0,0,0,1,1,1,0) => x71 - | (0,1,0,0,1,1,1,0) => x72 - | (1,1,0,0,1,1,1,0) => x73 - | (0,0,1,0,1,1,1,0) => x74 - | (1,0,1,0,1,1,1,0) => x75 - | (0,1,1,0,1,1,1,0) => x76 - | (1,1,1,0,1,1,1,0) => x77 - | (0,0,0,1,1,1,1,0) => x78 - | (1,0,0,1,1,1,1,0) => x79 - | (0,1,0,1,1,1,1,0) => x7a - | (1,1,0,1,1,1,1,0) => x7b - | (0,0,1,1,1,1,1,0) => x7c - | (1,0,1,1,1,1,1,0) => x7d - | (0,1,1,1,1,1,1,0) => x7e - | (1,1,1,1,1,1,1,0) => x7f - | (0,0,0,0,0,0,0,1) => x80 - | (1,0,0,0,0,0,0,1) => x81 - | (0,1,0,0,0,0,0,1) => x82 - | (1,1,0,0,0,0,0,1) => x83 - | (0,0,1,0,0,0,0,1) => x84 - | (1,0,1,0,0,0,0,1) => x85 - | (0,1,1,0,0,0,0,1) => x86 - | (1,1,1,0,0,0,0,1) => x87 - | (0,0,0,1,0,0,0,1) => x88 - | (1,0,0,1,0,0,0,1) => x89 - | (0,1,0,1,0,0,0,1) => x8a - | (1,1,0,1,0,0,0,1) => x8b - | (0,0,1,1,0,0,0,1) => x8c - | (1,0,1,1,0,0,0,1) => x8d - | (0,1,1,1,0,0,0,1) => x8e - | (1,1,1,1,0,0,0,1) => x8f - | (0,0,0,0,1,0,0,1) => x90 - | (1,0,0,0,1,0,0,1) => x91 - | (0,1,0,0,1,0,0,1) => x92 - | (1,1,0,0,1,0,0,1) => x93 - | (0,0,1,0,1,0,0,1) => x94 - | (1,0,1,0,1,0,0,1) => x95 - | (0,1,1,0,1,0,0,1) => x96 - | (1,1,1,0,1,0,0,1) => x97 - | (0,0,0,1,1,0,0,1) => x98 - | (1,0,0,1,1,0,0,1) => x99 - | (0,1,0,1,1,0,0,1) => x9a - | (1,1,0,1,1,0,0,1) => x9b - | (0,0,1,1,1,0,0,1) => x9c - | (1,0,1,1,1,0,0,1) => x9d - | (0,1,1,1,1,0,0,1) => x9e - | (1,1,1,1,1,0,0,1) => x9f - | (0,0,0,0,0,1,0,1) => xa0 - | (1,0,0,0,0,1,0,1) => xa1 - | (0,1,0,0,0,1,0,1) => xa2 - | (1,1,0,0,0,1,0,1) => xa3 - | (0,0,1,0,0,1,0,1) => xa4 - | (1,0,1,0,0,1,0,1) => xa5 - | (0,1,1,0,0,1,0,1) => xa6 - | (1,1,1,0,0,1,0,1) => xa7 - | (0,0,0,1,0,1,0,1) => xa8 - | (1,0,0,1,0,1,0,1) => xa9 - | (0,1,0,1,0,1,0,1) => xaa - | (1,1,0,1,0,1,0,1) => xab - | (0,0,1,1,0,1,0,1) => xac - | (1,0,1,1,0,1,0,1) => xad - | (0,1,1,1,0,1,0,1) => xae - | (1,1,1,1,0,1,0,1) => xaf - | (0,0,0,0,1,1,0,1) => xb0 - | (1,0,0,0,1,1,0,1) => xb1 - | (0,1,0,0,1,1,0,1) => xb2 - | (1,1,0,0,1,1,0,1) => xb3 - | (0,0,1,0,1,1,0,1) => xb4 - | (1,0,1,0,1,1,0,1) => xb5 - | (0,1,1,0,1,1,0,1) => xb6 - | (1,1,1,0,1,1,0,1) => xb7 - | (0,0,0,1,1,1,0,1) => xb8 - | (1,0,0,1,1,1,0,1) => xb9 - | (0,1,0,1,1,1,0,1) => xba - | (1,1,0,1,1,1,0,1) => xbb - | (0,0,1,1,1,1,0,1) => xbc - | (1,0,1,1,1,1,0,1) => xbd - | (0,1,1,1,1,1,0,1) => xbe - | (1,1,1,1,1,1,0,1) => xbf - | (0,0,0,0,0,0,1,1) => xc0 - | (1,0,0,0,0,0,1,1) => xc1 - | (0,1,0,0,0,0,1,1) => xc2 - | (1,1,0,0,0,0,1,1) => xc3 - | (0,0,1,0,0,0,1,1) => xc4 - | (1,0,1,0,0,0,1,1) => xc5 - | (0,1,1,0,0,0,1,1) => xc6 - | (1,1,1,0,0,0,1,1) => xc7 - | (0,0,0,1,0,0,1,1) => xc8 - | (1,0,0,1,0,0,1,1) => xc9 - | (0,1,0,1,0,0,1,1) => xca - | (1,1,0,1,0,0,1,1) => xcb - | (0,0,1,1,0,0,1,1) => xcc - | (1,0,1,1,0,0,1,1) => xcd - | (0,1,1,1,0,0,1,1) => xce - | (1,1,1,1,0,0,1,1) => xcf - | (0,0,0,0,1,0,1,1) => xd0 - | (1,0,0,0,1,0,1,1) => xd1 - | (0,1,0,0,1,0,1,1) => xd2 - | (1,1,0,0,1,0,1,1) => xd3 - | (0,0,1,0,1,0,1,1) => xd4 - | (1,0,1,0,1,0,1,1) => xd5 - | (0,1,1,0,1,0,1,1) => xd6 - | (1,1,1,0,1,0,1,1) => xd7 - | (0,0,0,1,1,0,1,1) => xd8 - | (1,0,0,1,1,0,1,1) => xd9 - | (0,1,0,1,1,0,1,1) => xda - | (1,1,0,1,1,0,1,1) => xdb - | (0,0,1,1,1,0,1,1) => xdc - | (1,0,1,1,1,0,1,1) => xdd - | (0,1,1,1,1,0,1,1) => xde - | (1,1,1,1,1,0,1,1) => xdf - | (0,0,0,0,0,1,1,1) => xe0 - | (1,0,0,0,0,1,1,1) => xe1 - | (0,1,0,0,0,1,1,1) => xe2 - | (1,1,0,0,0,1,1,1) => xe3 - | (0,0,1,0,0,1,1,1) => xe4 - | (1,0,1,0,0,1,1,1) => xe5 - | (0,1,1,0,0,1,1,1) => xe6 - | (1,1,1,0,0,1,1,1) => xe7 - | (0,0,0,1,0,1,1,1) => xe8 - | (1,0,0,1,0,1,1,1) => xe9 - | (0,1,0,1,0,1,1,1) => xea - | (1,1,0,1,0,1,1,1) => xeb - | (0,0,1,1,0,1,1,1) => xec - | (1,0,1,1,0,1,1,1) => xed - | (0,1,1,1,0,1,1,1) => xee - | (1,1,1,1,0,1,1,1) => xef - | (0,0,0,0,1,1,1,1) => xf0 - | (1,0,0,0,1,1,1,1) => xf1 - | (0,1,0,0,1,1,1,1) => xf2 - | (1,1,0,0,1,1,1,1) => xf3 - | (0,0,1,0,1,1,1,1) => xf4 - | (1,0,1,0,1,1,1,1) => xf5 - | (0,1,1,0,1,1,1,1) => xf6 - | (1,1,1,0,1,1,1,1) => xf7 - | (0,0,0,1,1,1,1,1) => xf8 - | (1,0,0,1,1,1,1,1) => xf9 - | (0,1,0,1,1,1,1,1) => xfa - | (1,1,0,1,1,1,1,1) => xfb - | (0,0,1,1,1,1,1,1) => xfc - | (1,0,1,1,1,1,1,1) => xfd - | (0,1,1,1,1,1,1,1) => xfe - | (1,1,1,1,1,1,1,1) => xff + | (0,(0,(0,(0,(0,(0,(0,0))))))) => x00 + | (1,(0,(0,(0,(0,(0,(0,0))))))) => x01 + | (0,(1,(0,(0,(0,(0,(0,0))))))) => x02 + | (1,(1,(0,(0,(0,(0,(0,0))))))) => x03 + | (0,(0,(1,(0,(0,(0,(0,0))))))) => x04 + | (1,(0,(1,(0,(0,(0,(0,0))))))) => x05 + | (0,(1,(1,(0,(0,(0,(0,0))))))) => x06 + | (1,(1,(1,(0,(0,(0,(0,0))))))) => x07 + | (0,(0,(0,(1,(0,(0,(0,0))))))) => x08 + | (1,(0,(0,(1,(0,(0,(0,0))))))) => x09 + | (0,(1,(0,(1,(0,(0,(0,0))))))) => x0a + | (1,(1,(0,(1,(0,(0,(0,0))))))) => x0b + | (0,(0,(1,(1,(0,(0,(0,0))))))) => x0c + | (1,(0,(1,(1,(0,(0,(0,0))))))) => x0d + | (0,(1,(1,(1,(0,(0,(0,0))))))) => x0e + | (1,(1,(1,(1,(0,(0,(0,0))))))) => x0f + | (0,(0,(0,(0,(1,(0,(0,0))))))) => x10 + | (1,(0,(0,(0,(1,(0,(0,0))))))) => x11 + | (0,(1,(0,(0,(1,(0,(0,0))))))) => x12 + | (1,(1,(0,(0,(1,(0,(0,0))))))) => x13 + | (0,(0,(1,(0,(1,(0,(0,0))))))) => x14 + | (1,(0,(1,(0,(1,(0,(0,0))))))) => x15 + | (0,(1,(1,(0,(1,(0,(0,0))))))) => x16 + | (1,(1,(1,(0,(1,(0,(0,0))))))) => x17 + | (0,(0,(0,(1,(1,(0,(0,0))))))) => x18 + | (1,(0,(0,(1,(1,(0,(0,0))))))) => x19 + | (0,(1,(0,(1,(1,(0,(0,0))))))) => x1a + | (1,(1,(0,(1,(1,(0,(0,0))))))) => x1b + | (0,(0,(1,(1,(1,(0,(0,0))))))) => x1c + | (1,(0,(1,(1,(1,(0,(0,0))))))) => x1d + | (0,(1,(1,(1,(1,(0,(0,0))))))) => x1e + | (1,(1,(1,(1,(1,(0,(0,0))))))) => x1f + | (0,(0,(0,(0,(0,(1,(0,0))))))) => x20 + | (1,(0,(0,(0,(0,(1,(0,0))))))) => x21 + | (0,(1,(0,(0,(0,(1,(0,0))))))) => x22 + | (1,(1,(0,(0,(0,(1,(0,0))))))) => x23 + | (0,(0,(1,(0,(0,(1,(0,0))))))) => x24 + | (1,(0,(1,(0,(0,(1,(0,0))))))) => x25 + | (0,(1,(1,(0,(0,(1,(0,0))))))) => x26 + | (1,(1,(1,(0,(0,(1,(0,0))))))) => x27 + | (0,(0,(0,(1,(0,(1,(0,0))))))) => x28 + | (1,(0,(0,(1,(0,(1,(0,0))))))) => x29 + | (0,(1,(0,(1,(0,(1,(0,0))))))) => x2a + | (1,(1,(0,(1,(0,(1,(0,0))))))) => x2b + | (0,(0,(1,(1,(0,(1,(0,0))))))) => x2c + | (1,(0,(1,(1,(0,(1,(0,0))))))) => x2d + | (0,(1,(1,(1,(0,(1,(0,0))))))) => x2e + | (1,(1,(1,(1,(0,(1,(0,0))))))) => x2f + | (0,(0,(0,(0,(1,(1,(0,0))))))) => x30 + | (1,(0,(0,(0,(1,(1,(0,0))))))) => x31 + | (0,(1,(0,(0,(1,(1,(0,0))))))) => x32 + | (1,(1,(0,(0,(1,(1,(0,0))))))) => x33 + | (0,(0,(1,(0,(1,(1,(0,0))))))) => x34 + | (1,(0,(1,(0,(1,(1,(0,0))))))) => x35 + | (0,(1,(1,(0,(1,(1,(0,0))))))) => x36 + | (1,(1,(1,(0,(1,(1,(0,0))))))) => x37 + | (0,(0,(0,(1,(1,(1,(0,0))))))) => x38 + | (1,(0,(0,(1,(1,(1,(0,0))))))) => x39 + | (0,(1,(0,(1,(1,(1,(0,0))))))) => x3a + | (1,(1,(0,(1,(1,(1,(0,0))))))) => x3b + | (0,(0,(1,(1,(1,(1,(0,0))))))) => x3c + | (1,(0,(1,(1,(1,(1,(0,0))))))) => x3d + | (0,(1,(1,(1,(1,(1,(0,0))))))) => x3e + | (1,(1,(1,(1,(1,(1,(0,0))))))) => x3f + | (0,(0,(0,(0,(0,(0,(1,0))))))) => x40 + | (1,(0,(0,(0,(0,(0,(1,0))))))) => x41 + | (0,(1,(0,(0,(0,(0,(1,0))))))) => x42 + | (1,(1,(0,(0,(0,(0,(1,0))))))) => x43 + | (0,(0,(1,(0,(0,(0,(1,0))))))) => x44 + | (1,(0,(1,(0,(0,(0,(1,0))))))) => x45 + | (0,(1,(1,(0,(0,(0,(1,0))))))) => x46 + | (1,(1,(1,(0,(0,(0,(1,0))))))) => x47 + | (0,(0,(0,(1,(0,(0,(1,0))))))) => x48 + | (1,(0,(0,(1,(0,(0,(1,0))))))) => x49 + | (0,(1,(0,(1,(0,(0,(1,0))))))) => x4a + | (1,(1,(0,(1,(0,(0,(1,0))))))) => x4b + | (0,(0,(1,(1,(0,(0,(1,0))))))) => x4c + | (1,(0,(1,(1,(0,(0,(1,0))))))) => x4d + | (0,(1,(1,(1,(0,(0,(1,0))))))) => x4e + | (1,(1,(1,(1,(0,(0,(1,0))))))) => x4f + | (0,(0,(0,(0,(1,(0,(1,0))))))) => x50 + | (1,(0,(0,(0,(1,(0,(1,0))))))) => x51 + | (0,(1,(0,(0,(1,(0,(1,0))))))) => x52 + | (1,(1,(0,(0,(1,(0,(1,0))))))) => x53 + | (0,(0,(1,(0,(1,(0,(1,0))))))) => x54 + | (1,(0,(1,(0,(1,(0,(1,0))))))) => x55 + | (0,(1,(1,(0,(1,(0,(1,0))))))) => x56 + | (1,(1,(1,(0,(1,(0,(1,0))))))) => x57 + | (0,(0,(0,(1,(1,(0,(1,0))))))) => x58 + | (1,(0,(0,(1,(1,(0,(1,0))))))) => x59 + | (0,(1,(0,(1,(1,(0,(1,0))))))) => x5a + | (1,(1,(0,(1,(1,(0,(1,0))))))) => x5b + | (0,(0,(1,(1,(1,(0,(1,0))))))) => x5c + | (1,(0,(1,(1,(1,(0,(1,0))))))) => x5d + | (0,(1,(1,(1,(1,(0,(1,0))))))) => x5e + | (1,(1,(1,(1,(1,(0,(1,0))))))) => x5f + | (0,(0,(0,(0,(0,(1,(1,0))))))) => x60 + | (1,(0,(0,(0,(0,(1,(1,0))))))) => x61 + | (0,(1,(0,(0,(0,(1,(1,0))))))) => x62 + | (1,(1,(0,(0,(0,(1,(1,0))))))) => x63 + | (0,(0,(1,(0,(0,(1,(1,0))))))) => x64 + | (1,(0,(1,(0,(0,(1,(1,0))))))) => x65 + | (0,(1,(1,(0,(0,(1,(1,0))))))) => x66 + | (1,(1,(1,(0,(0,(1,(1,0))))))) => x67 + | (0,(0,(0,(1,(0,(1,(1,0))))))) => x68 + | (1,(0,(0,(1,(0,(1,(1,0))))))) => x69 + | (0,(1,(0,(1,(0,(1,(1,0))))))) => x6a + | (1,(1,(0,(1,(0,(1,(1,0))))))) => x6b + | (0,(0,(1,(1,(0,(1,(1,0))))))) => x6c + | (1,(0,(1,(1,(0,(1,(1,0))))))) => x6d + | (0,(1,(1,(1,(0,(1,(1,0))))))) => x6e + | (1,(1,(1,(1,(0,(1,(1,0))))))) => x6f + | (0,(0,(0,(0,(1,(1,(1,0))))))) => x70 + | (1,(0,(0,(0,(1,(1,(1,0))))))) => x71 + | (0,(1,(0,(0,(1,(1,(1,0))))))) => x72 + | (1,(1,(0,(0,(1,(1,(1,0))))))) => x73 + | (0,(0,(1,(0,(1,(1,(1,0))))))) => x74 + | (1,(0,(1,(0,(1,(1,(1,0))))))) => x75 + | (0,(1,(1,(0,(1,(1,(1,0))))))) => x76 + | (1,(1,(1,(0,(1,(1,(1,0))))))) => x77 + | (0,(0,(0,(1,(1,(1,(1,0))))))) => x78 + | (1,(0,(0,(1,(1,(1,(1,0))))))) => x79 + | (0,(1,(0,(1,(1,(1,(1,0))))))) => x7a + | (1,(1,(0,(1,(1,(1,(1,0))))))) => x7b + | (0,(0,(1,(1,(1,(1,(1,0))))))) => x7c + | (1,(0,(1,(1,(1,(1,(1,0))))))) => x7d + | (0,(1,(1,(1,(1,(1,(1,0))))))) => x7e + | (1,(1,(1,(1,(1,(1,(1,0))))))) => x7f + | (0,(0,(0,(0,(0,(0,(0,1))))))) => x80 + | (1,(0,(0,(0,(0,(0,(0,1))))))) => x81 + | (0,(1,(0,(0,(0,(0,(0,1))))))) => x82 + | (1,(1,(0,(0,(0,(0,(0,1))))))) => x83 + | (0,(0,(1,(0,(0,(0,(0,1))))))) => x84 + | (1,(0,(1,(0,(0,(0,(0,1))))))) => x85 + | (0,(1,(1,(0,(0,(0,(0,1))))))) => x86 + | (1,(1,(1,(0,(0,(0,(0,1))))))) => x87 + | (0,(0,(0,(1,(0,(0,(0,1))))))) => x88 + | (1,(0,(0,(1,(0,(0,(0,1))))))) => x89 + | (0,(1,(0,(1,(0,(0,(0,1))))))) => x8a + | (1,(1,(0,(1,(0,(0,(0,1))))))) => x8b + | (0,(0,(1,(1,(0,(0,(0,1))))))) => x8c + | (1,(0,(1,(1,(0,(0,(0,1))))))) => x8d + | (0,(1,(1,(1,(0,(0,(0,1))))))) => x8e + | (1,(1,(1,(1,(0,(0,(0,1))))))) => x8f + | (0,(0,(0,(0,(1,(0,(0,1))))))) => x90 + | (1,(0,(0,(0,(1,(0,(0,1))))))) => x91 + | (0,(1,(0,(0,(1,(0,(0,1))))))) => x92 + | (1,(1,(0,(0,(1,(0,(0,1))))))) => x93 + | (0,(0,(1,(0,(1,(0,(0,1))))))) => x94 + | (1,(0,(1,(0,(1,(0,(0,1))))))) => x95 + | (0,(1,(1,(0,(1,(0,(0,1))))))) => x96 + | (1,(1,(1,(0,(1,(0,(0,1))))))) => x97 + | (0,(0,(0,(1,(1,(0,(0,1))))))) => x98 + | (1,(0,(0,(1,(1,(0,(0,1))))))) => x99 + | (0,(1,(0,(1,(1,(0,(0,1))))))) => x9a + | (1,(1,(0,(1,(1,(0,(0,1))))))) => x9b + | (0,(0,(1,(1,(1,(0,(0,1))))))) => x9c + | (1,(0,(1,(1,(1,(0,(0,1))))))) => x9d + | (0,(1,(1,(1,(1,(0,(0,1))))))) => x9e + | (1,(1,(1,(1,(1,(0,(0,1))))))) => x9f + | (0,(0,(0,(0,(0,(1,(0,1))))))) => xa0 + | (1,(0,(0,(0,(0,(1,(0,1))))))) => xa1 + | (0,(1,(0,(0,(0,(1,(0,1))))))) => xa2 + | (1,(1,(0,(0,(0,(1,(0,1))))))) => xa3 + | (0,(0,(1,(0,(0,(1,(0,1))))))) => xa4 + | (1,(0,(1,(0,(0,(1,(0,1))))))) => xa5 + | (0,(1,(1,(0,(0,(1,(0,1))))))) => xa6 + | (1,(1,(1,(0,(0,(1,(0,1))))))) => xa7 + | (0,(0,(0,(1,(0,(1,(0,1))))))) => xa8 + | (1,(0,(0,(1,(0,(1,(0,1))))))) => xa9 + | (0,(1,(0,(1,(0,(1,(0,1))))))) => xaa + | (1,(1,(0,(1,(0,(1,(0,1))))))) => xab + | (0,(0,(1,(1,(0,(1,(0,1))))))) => xac + | (1,(0,(1,(1,(0,(1,(0,1))))))) => xad + | (0,(1,(1,(1,(0,(1,(0,1))))))) => xae + | (1,(1,(1,(1,(0,(1,(0,1))))))) => xaf + | (0,(0,(0,(0,(1,(1,(0,1))))))) => xb0 + | (1,(0,(0,(0,(1,(1,(0,1))))))) => xb1 + | (0,(1,(0,(0,(1,(1,(0,1))))))) => xb2 + | (1,(1,(0,(0,(1,(1,(0,1))))))) => xb3 + | (0,(0,(1,(0,(1,(1,(0,1))))))) => xb4 + | (1,(0,(1,(0,(1,(1,(0,1))))))) => xb5 + | (0,(1,(1,(0,(1,(1,(0,1))))))) => xb6 + | (1,(1,(1,(0,(1,(1,(0,1))))))) => xb7 + | (0,(0,(0,(1,(1,(1,(0,1))))))) => xb8 + | (1,(0,(0,(1,(1,(1,(0,1))))))) => xb9 + | (0,(1,(0,(1,(1,(1,(0,1))))))) => xba + | (1,(1,(0,(1,(1,(1,(0,1))))))) => xbb + | (0,(0,(1,(1,(1,(1,(0,1))))))) => xbc + | (1,(0,(1,(1,(1,(1,(0,1))))))) => xbd + | (0,(1,(1,(1,(1,(1,(0,1))))))) => xbe + | (1,(1,(1,(1,(1,(1,(0,1))))))) => xbf + | (0,(0,(0,(0,(0,(0,(1,1))))))) => xc0 + | (1,(0,(0,(0,(0,(0,(1,1))))))) => xc1 + | (0,(1,(0,(0,(0,(0,(1,1))))))) => xc2 + | (1,(1,(0,(0,(0,(0,(1,1))))))) => xc3 + | (0,(0,(1,(0,(0,(0,(1,1))))))) => xc4 + | (1,(0,(1,(0,(0,(0,(1,1))))))) => xc5 + | (0,(1,(1,(0,(0,(0,(1,1))))))) => xc6 + | (1,(1,(1,(0,(0,(0,(1,1))))))) => xc7 + | (0,(0,(0,(1,(0,(0,(1,1))))))) => xc8 + | (1,(0,(0,(1,(0,(0,(1,1))))))) => xc9 + | (0,(1,(0,(1,(0,(0,(1,1))))))) => xca + | (1,(1,(0,(1,(0,(0,(1,1))))))) => xcb + | (0,(0,(1,(1,(0,(0,(1,1))))))) => xcc + | (1,(0,(1,(1,(0,(0,(1,1))))))) => xcd + | (0,(1,(1,(1,(0,(0,(1,1))))))) => xce + | (1,(1,(1,(1,(0,(0,(1,1))))))) => xcf + | (0,(0,(0,(0,(1,(0,(1,1))))))) => xd0 + | (1,(0,(0,(0,(1,(0,(1,1))))))) => xd1 + | (0,(1,(0,(0,(1,(0,(1,1))))))) => xd2 + | (1,(1,(0,(0,(1,(0,(1,1))))))) => xd3 + | (0,(0,(1,(0,(1,(0,(1,1))))))) => xd4 + | (1,(0,(1,(0,(1,(0,(1,1))))))) => xd5 + | (0,(1,(1,(0,(1,(0,(1,1))))))) => xd6 + | (1,(1,(1,(0,(1,(0,(1,1))))))) => xd7 + | (0,(0,(0,(1,(1,(0,(1,1))))))) => xd8 + | (1,(0,(0,(1,(1,(0,(1,1))))))) => xd9 + | (0,(1,(0,(1,(1,(0,(1,1))))))) => xda + | (1,(1,(0,(1,(1,(0,(1,1))))))) => xdb + | (0,(0,(1,(1,(1,(0,(1,1))))))) => xdc + | (1,(0,(1,(1,(1,(0,(1,1))))))) => xdd + | (0,(1,(1,(1,(1,(0,(1,1))))))) => xde + | (1,(1,(1,(1,(1,(0,(1,1))))))) => xdf + | (0,(0,(0,(0,(0,(1,(1,1))))))) => xe0 + | (1,(0,(0,(0,(0,(1,(1,1))))))) => xe1 + | (0,(1,(0,(0,(0,(1,(1,1))))))) => xe2 + | (1,(1,(0,(0,(0,(1,(1,1))))))) => xe3 + | (0,(0,(1,(0,(0,(1,(1,1))))))) => xe4 + | (1,(0,(1,(0,(0,(1,(1,1))))))) => xe5 + | (0,(1,(1,(0,(0,(1,(1,1))))))) => xe6 + | (1,(1,(1,(0,(0,(1,(1,1))))))) => xe7 + | (0,(0,(0,(1,(0,(1,(1,1))))))) => xe8 + | (1,(0,(0,(1,(0,(1,(1,1))))))) => xe9 + | (0,(1,(0,(1,(0,(1,(1,1))))))) => xea + | (1,(1,(0,(1,(0,(1,(1,1))))))) => xeb + | (0,(0,(1,(1,(0,(1,(1,1))))))) => xec + | (1,(0,(1,(1,(0,(1,(1,1))))))) => xed + | (0,(1,(1,(1,(0,(1,(1,1))))))) => xee + | (1,(1,(1,(1,(0,(1,(1,1))))))) => xef + | (0,(0,(0,(0,(1,(1,(1,1))))))) => xf0 + | (1,(0,(0,(0,(1,(1,(1,1))))))) => xf1 + | (0,(1,(0,(0,(1,(1,(1,1))))))) => xf2 + | (1,(1,(0,(0,(1,(1,(1,1))))))) => xf3 + | (0,(0,(1,(0,(1,(1,(1,1))))))) => xf4 + | (1,(0,(1,(0,(1,(1,(1,1))))))) => xf5 + | (0,(1,(1,(0,(1,(1,(1,1))))))) => xf6 + | (1,(1,(1,(0,(1,(1,(1,1))))))) => xf7 + | (0,(0,(0,(1,(1,(1,(1,1))))))) => xf8 + | (1,(0,(0,(1,(1,(1,(1,1))))))) => xf9 + | (0,(1,(0,(1,(1,(1,(1,1))))))) => xfa + | (1,(1,(0,(1,(1,(1,(1,1))))))) => xfb + | (0,(0,(1,(1,(1,(1,(1,1))))))) => xfc + | (1,(0,(1,(1,(1,(1,(1,1))))))) => xfd + | (0,(1,(1,(1,(1,(1,(1,1))))))) => xfe + | (1,(1,(1,(1,(1,(1,(1,1))))))) => xff end. -Definition to_bits (b : byte) : bool * bool * bool * bool * bool * bool * bool * bool +Definition to_bits (b : byte) : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) := match b with - | x00 => (0,0,0,0,0,0,0,0) - | x01 => (1,0,0,0,0,0,0,0) - | x02 => (0,1,0,0,0,0,0,0) - | x03 => (1,1,0,0,0,0,0,0) - | x04 => (0,0,1,0,0,0,0,0) - | x05 => (1,0,1,0,0,0,0,0) - | x06 => (0,1,1,0,0,0,0,0) - | x07 => (1,1,1,0,0,0,0,0) - | x08 => (0,0,0,1,0,0,0,0) - | x09 => (1,0,0,1,0,0,0,0) - | x0a => (0,1,0,1,0,0,0,0) - | x0b => (1,1,0,1,0,0,0,0) - | x0c => (0,0,1,1,0,0,0,0) - | x0d => (1,0,1,1,0,0,0,0) - | x0e => (0,1,1,1,0,0,0,0) - | x0f => (1,1,1,1,0,0,0,0) - | x10 => (0,0,0,0,1,0,0,0) - | x11 => (1,0,0,0,1,0,0,0) - | x12 => (0,1,0,0,1,0,0,0) - | x13 => (1,1,0,0,1,0,0,0) - | x14 => (0,0,1,0,1,0,0,0) - | x15 => (1,0,1,0,1,0,0,0) - | x16 => (0,1,1,0,1,0,0,0) - | x17 => (1,1,1,0,1,0,0,0) - | x18 => (0,0,0,1,1,0,0,0) - | x19 => (1,0,0,1,1,0,0,0) - | x1a => (0,1,0,1,1,0,0,0) - | x1b => (1,1,0,1,1,0,0,0) - | x1c => (0,0,1,1,1,0,0,0) - | x1d => (1,0,1,1,1,0,0,0) - | x1e => (0,1,1,1,1,0,0,0) - | x1f => (1,1,1,1,1,0,0,0) - | x20 => (0,0,0,0,0,1,0,0) - | x21 => (1,0,0,0,0,1,0,0) - | x22 => (0,1,0,0,0,1,0,0) - | x23 => (1,1,0,0,0,1,0,0) - | x24 => (0,0,1,0,0,1,0,0) - | x25 => (1,0,1,0,0,1,0,0) - | x26 => (0,1,1,0,0,1,0,0) - | x27 => (1,1,1,0,0,1,0,0) - | x28 => (0,0,0,1,0,1,0,0) - | x29 => (1,0,0,1,0,1,0,0) - | x2a => (0,1,0,1,0,1,0,0) - | x2b => (1,1,0,1,0,1,0,0) - | x2c => (0,0,1,1,0,1,0,0) - | x2d => (1,0,1,1,0,1,0,0) - | x2e => (0,1,1,1,0,1,0,0) - | x2f => (1,1,1,1,0,1,0,0) - | x30 => (0,0,0,0,1,1,0,0) - | x31 => (1,0,0,0,1,1,0,0) - | x32 => (0,1,0,0,1,1,0,0) - | x33 => (1,1,0,0,1,1,0,0) - | x34 => (0,0,1,0,1,1,0,0) - | x35 => (1,0,1,0,1,1,0,0) - | x36 => (0,1,1,0,1,1,0,0) - | x37 => (1,1,1,0,1,1,0,0) - | x38 => (0,0,0,1,1,1,0,0) - | x39 => (1,0,0,1,1,1,0,0) - | x3a => (0,1,0,1,1,1,0,0) - | x3b => (1,1,0,1,1,1,0,0) - | x3c => (0,0,1,1,1,1,0,0) - | x3d => (1,0,1,1,1,1,0,0) - | x3e => (0,1,1,1,1,1,0,0) - | x3f => (1,1,1,1,1,1,0,0) - | x40 => (0,0,0,0,0,0,1,0) - | x41 => (1,0,0,0,0,0,1,0) - | x42 => (0,1,0,0,0,0,1,0) - | x43 => (1,1,0,0,0,0,1,0) - | x44 => (0,0,1,0,0,0,1,0) - | x45 => (1,0,1,0,0,0,1,0) - | x46 => (0,1,1,0,0,0,1,0) - | x47 => (1,1,1,0,0,0,1,0) - | x48 => (0,0,0,1,0,0,1,0) - | x49 => (1,0,0,1,0,0,1,0) - | x4a => (0,1,0,1,0,0,1,0) - | x4b => (1,1,0,1,0,0,1,0) - | x4c => (0,0,1,1,0,0,1,0) - | x4d => (1,0,1,1,0,0,1,0) - | x4e => (0,1,1,1,0,0,1,0) - | x4f => (1,1,1,1,0,0,1,0) - | x50 => (0,0,0,0,1,0,1,0) - | x51 => (1,0,0,0,1,0,1,0) - | x52 => (0,1,0,0,1,0,1,0) - | x53 => (1,1,0,0,1,0,1,0) - | x54 => (0,0,1,0,1,0,1,0) - | x55 => (1,0,1,0,1,0,1,0) - | x56 => (0,1,1,0,1,0,1,0) - | x57 => (1,1,1,0,1,0,1,0) - | x58 => (0,0,0,1,1,0,1,0) - | x59 => (1,0,0,1,1,0,1,0) - | x5a => (0,1,0,1,1,0,1,0) - | x5b => (1,1,0,1,1,0,1,0) - | x5c => (0,0,1,1,1,0,1,0) - | x5d => (1,0,1,1,1,0,1,0) - | x5e => (0,1,1,1,1,0,1,0) - | x5f => (1,1,1,1,1,0,1,0) - | x60 => (0,0,0,0,0,1,1,0) - | x61 => (1,0,0,0,0,1,1,0) - | x62 => (0,1,0,0,0,1,1,0) - | x63 => (1,1,0,0,0,1,1,0) - | x64 => (0,0,1,0,0,1,1,0) - | x65 => (1,0,1,0,0,1,1,0) - | x66 => (0,1,1,0,0,1,1,0) - | x67 => (1,1,1,0,0,1,1,0) - | x68 => (0,0,0,1,0,1,1,0) - | x69 => (1,0,0,1,0,1,1,0) - | x6a => (0,1,0,1,0,1,1,0) - | x6b => (1,1,0,1,0,1,1,0) - | x6c => (0,0,1,1,0,1,1,0) - | x6d => (1,0,1,1,0,1,1,0) - | x6e => (0,1,1,1,0,1,1,0) - | x6f => (1,1,1,1,0,1,1,0) - | x70 => (0,0,0,0,1,1,1,0) - | x71 => (1,0,0,0,1,1,1,0) - | x72 => (0,1,0,0,1,1,1,0) - | x73 => (1,1,0,0,1,1,1,0) - | x74 => (0,0,1,0,1,1,1,0) - | x75 => (1,0,1,0,1,1,1,0) - | x76 => (0,1,1,0,1,1,1,0) - | x77 => (1,1,1,0,1,1,1,0) - | x78 => (0,0,0,1,1,1,1,0) - | x79 => (1,0,0,1,1,1,1,0) - | x7a => (0,1,0,1,1,1,1,0) - | x7b => (1,1,0,1,1,1,1,0) - | x7c => (0,0,1,1,1,1,1,0) - | x7d => (1,0,1,1,1,1,1,0) - | x7e => (0,1,1,1,1,1,1,0) - | x7f => (1,1,1,1,1,1,1,0) - | x80 => (0,0,0,0,0,0,0,1) - | x81 => (1,0,0,0,0,0,0,1) - | x82 => (0,1,0,0,0,0,0,1) - | x83 => (1,1,0,0,0,0,0,1) - | x84 => (0,0,1,0,0,0,0,1) - | x85 => (1,0,1,0,0,0,0,1) - | x86 => (0,1,1,0,0,0,0,1) - | x87 => (1,1,1,0,0,0,0,1) - | x88 => (0,0,0,1,0,0,0,1) - | x89 => (1,0,0,1,0,0,0,1) - | x8a => (0,1,0,1,0,0,0,1) - | x8b => (1,1,0,1,0,0,0,1) - | x8c => (0,0,1,1,0,0,0,1) - | x8d => (1,0,1,1,0,0,0,1) - | x8e => (0,1,1,1,0,0,0,1) - | x8f => (1,1,1,1,0,0,0,1) - | x90 => (0,0,0,0,1,0,0,1) - | x91 => (1,0,0,0,1,0,0,1) - | x92 => (0,1,0,0,1,0,0,1) - | x93 => (1,1,0,0,1,0,0,1) - | x94 => (0,0,1,0,1,0,0,1) - | x95 => (1,0,1,0,1,0,0,1) - | x96 => (0,1,1,0,1,0,0,1) - | x97 => (1,1,1,0,1,0,0,1) - | x98 => (0,0,0,1,1,0,0,1) - | x99 => (1,0,0,1,1,0,0,1) - | x9a => (0,1,0,1,1,0,0,1) - | x9b => (1,1,0,1,1,0,0,1) - | x9c => (0,0,1,1,1,0,0,1) - | x9d => (1,0,1,1,1,0,0,1) - | x9e => (0,1,1,1,1,0,0,1) - | x9f => (1,1,1,1,1,0,0,1) - | xa0 => (0,0,0,0,0,1,0,1) - | xa1 => (1,0,0,0,0,1,0,1) - | xa2 => (0,1,0,0,0,1,0,1) - | xa3 => (1,1,0,0,0,1,0,1) - | xa4 => (0,0,1,0,0,1,0,1) - | xa5 => (1,0,1,0,0,1,0,1) - | xa6 => (0,1,1,0,0,1,0,1) - | xa7 => (1,1,1,0,0,1,0,1) - | xa8 => (0,0,0,1,0,1,0,1) - | xa9 => (1,0,0,1,0,1,0,1) - | xaa => (0,1,0,1,0,1,0,1) - | xab => (1,1,0,1,0,1,0,1) - | xac => (0,0,1,1,0,1,0,1) - | xad => (1,0,1,1,0,1,0,1) - | xae => (0,1,1,1,0,1,0,1) - | xaf => (1,1,1,1,0,1,0,1) - | xb0 => (0,0,0,0,1,1,0,1) - | xb1 => (1,0,0,0,1,1,0,1) - | xb2 => (0,1,0,0,1,1,0,1) - | xb3 => (1,1,0,0,1,1,0,1) - | xb4 => (0,0,1,0,1,1,0,1) - | xb5 => (1,0,1,0,1,1,0,1) - | xb6 => (0,1,1,0,1,1,0,1) - | xb7 => (1,1,1,0,1,1,0,1) - | xb8 => (0,0,0,1,1,1,0,1) - | xb9 => (1,0,0,1,1,1,0,1) - | xba => (0,1,0,1,1,1,0,1) - | xbb => (1,1,0,1,1,1,0,1) - | xbc => (0,0,1,1,1,1,0,1) - | xbd => (1,0,1,1,1,1,0,1) - | xbe => (0,1,1,1,1,1,0,1) - | xbf => (1,1,1,1,1,1,0,1) - | xc0 => (0,0,0,0,0,0,1,1) - | xc1 => (1,0,0,0,0,0,1,1) - | xc2 => (0,1,0,0,0,0,1,1) - | xc3 => (1,1,0,0,0,0,1,1) - | xc4 => (0,0,1,0,0,0,1,1) - | xc5 => (1,0,1,0,0,0,1,1) - | xc6 => (0,1,1,0,0,0,1,1) - | xc7 => (1,1,1,0,0,0,1,1) - | xc8 => (0,0,0,1,0,0,1,1) - | xc9 => (1,0,0,1,0,0,1,1) - | xca => (0,1,0,1,0,0,1,1) - | xcb => (1,1,0,1,0,0,1,1) - | xcc => (0,0,1,1,0,0,1,1) - | xcd => (1,0,1,1,0,0,1,1) - | xce => (0,1,1,1,0,0,1,1) - | xcf => (1,1,1,1,0,0,1,1) - | xd0 => (0,0,0,0,1,0,1,1) - | xd1 => (1,0,0,0,1,0,1,1) - | xd2 => (0,1,0,0,1,0,1,1) - | xd3 => (1,1,0,0,1,0,1,1) - | xd4 => (0,0,1,0,1,0,1,1) - | xd5 => (1,0,1,0,1,0,1,1) - | xd6 => (0,1,1,0,1,0,1,1) - | xd7 => (1,1,1,0,1,0,1,1) - | xd8 => (0,0,0,1,1,0,1,1) - | xd9 => (1,0,0,1,1,0,1,1) - | xda => (0,1,0,1,1,0,1,1) - | xdb => (1,1,0,1,1,0,1,1) - | xdc => (0,0,1,1,1,0,1,1) - | xdd => (1,0,1,1,1,0,1,1) - | xde => (0,1,1,1,1,0,1,1) - | xdf => (1,1,1,1,1,0,1,1) - | xe0 => (0,0,0,0,0,1,1,1) - | xe1 => (1,0,0,0,0,1,1,1) - | xe2 => (0,1,0,0,0,1,1,1) - | xe3 => (1,1,0,0,0,1,1,1) - | xe4 => (0,0,1,0,0,1,1,1) - | xe5 => (1,0,1,0,0,1,1,1) - | xe6 => (0,1,1,0,0,1,1,1) - | xe7 => (1,1,1,0,0,1,1,1) - | xe8 => (0,0,0,1,0,1,1,1) - | xe9 => (1,0,0,1,0,1,1,1) - | xea => (0,1,0,1,0,1,1,1) - | xeb => (1,1,0,1,0,1,1,1) - | xec => (0,0,1,1,0,1,1,1) - | xed => (1,0,1,1,0,1,1,1) - | xee => (0,1,1,1,0,1,1,1) - | xef => (1,1,1,1,0,1,1,1) - | xf0 => (0,0,0,0,1,1,1,1) - | xf1 => (1,0,0,0,1,1,1,1) - | xf2 => (0,1,0,0,1,1,1,1) - | xf3 => (1,1,0,0,1,1,1,1) - | xf4 => (0,0,1,0,1,1,1,1) - | xf5 => (1,0,1,0,1,1,1,1) - | xf6 => (0,1,1,0,1,1,1,1) - | xf7 => (1,1,1,0,1,1,1,1) - | xf8 => (0,0,0,1,1,1,1,1) - | xf9 => (1,0,0,1,1,1,1,1) - | xfa => (0,1,0,1,1,1,1,1) - | xfb => (1,1,0,1,1,1,1,1) - | xfc => (0,0,1,1,1,1,1,1) - | xfd => (1,0,1,1,1,1,1,1) - | xfe => (0,1,1,1,1,1,1,1) - | xff => (1,1,1,1,1,1,1,1) + | x00 => (0,(0,(0,(0,(0,(0,(0,0))))))) + | x01 => (1,(0,(0,(0,(0,(0,(0,0))))))) + | x02 => (0,(1,(0,(0,(0,(0,(0,0))))))) + | x03 => (1,(1,(0,(0,(0,(0,(0,0))))))) + | x04 => (0,(0,(1,(0,(0,(0,(0,0))))))) + | x05 => (1,(0,(1,(0,(0,(0,(0,0))))))) + | x06 => (0,(1,(1,(0,(0,(0,(0,0))))))) + | x07 => (1,(1,(1,(0,(0,(0,(0,0))))))) + | x08 => (0,(0,(0,(1,(0,(0,(0,0))))))) + | x09 => (1,(0,(0,(1,(0,(0,(0,0))))))) + | x0a => (0,(1,(0,(1,(0,(0,(0,0))))))) + | x0b => (1,(1,(0,(1,(0,(0,(0,0))))))) + | x0c => (0,(0,(1,(1,(0,(0,(0,0))))))) + | x0d => (1,(0,(1,(1,(0,(0,(0,0))))))) + | x0e => (0,(1,(1,(1,(0,(0,(0,0))))))) + | x0f => (1,(1,(1,(1,(0,(0,(0,0))))))) + | x10 => (0,(0,(0,(0,(1,(0,(0,0))))))) + | x11 => (1,(0,(0,(0,(1,(0,(0,0))))))) + | x12 => (0,(1,(0,(0,(1,(0,(0,0))))))) + | x13 => (1,(1,(0,(0,(1,(0,(0,0))))))) + | x14 => (0,(0,(1,(0,(1,(0,(0,0))))))) + | x15 => (1,(0,(1,(0,(1,(0,(0,0))))))) + | x16 => (0,(1,(1,(0,(1,(0,(0,0))))))) + | x17 => (1,(1,(1,(0,(1,(0,(0,0))))))) + | x18 => (0,(0,(0,(1,(1,(0,(0,0))))))) + | x19 => (1,(0,(0,(1,(1,(0,(0,0))))))) + | x1a => (0,(1,(0,(1,(1,(0,(0,0))))))) + | x1b => (1,(1,(0,(1,(1,(0,(0,0))))))) + | x1c => (0,(0,(1,(1,(1,(0,(0,0))))))) + | x1d => (1,(0,(1,(1,(1,(0,(0,0))))))) + | x1e => (0,(1,(1,(1,(1,(0,(0,0))))))) + | x1f => (1,(1,(1,(1,(1,(0,(0,0))))))) + | x20 => (0,(0,(0,(0,(0,(1,(0,0))))))) + | x21 => (1,(0,(0,(0,(0,(1,(0,0))))))) + | x22 => (0,(1,(0,(0,(0,(1,(0,0))))))) + | x23 => (1,(1,(0,(0,(0,(1,(0,0))))))) + | x24 => (0,(0,(1,(0,(0,(1,(0,0))))))) + | x25 => (1,(0,(1,(0,(0,(1,(0,0))))))) + | x26 => (0,(1,(1,(0,(0,(1,(0,0))))))) + | x27 => (1,(1,(1,(0,(0,(1,(0,0))))))) + | x28 => (0,(0,(0,(1,(0,(1,(0,0))))))) + | x29 => (1,(0,(0,(1,(0,(1,(0,0))))))) + | x2a => (0,(1,(0,(1,(0,(1,(0,0))))))) + | x2b => (1,(1,(0,(1,(0,(1,(0,0))))))) + | x2c => (0,(0,(1,(1,(0,(1,(0,0))))))) + | x2d => (1,(0,(1,(1,(0,(1,(0,0))))))) + | x2e => (0,(1,(1,(1,(0,(1,(0,0))))))) + | x2f => (1,(1,(1,(1,(0,(1,(0,0))))))) + | x30 => (0,(0,(0,(0,(1,(1,(0,0))))))) + | x31 => (1,(0,(0,(0,(1,(1,(0,0))))))) + | x32 => (0,(1,(0,(0,(1,(1,(0,0))))))) + | x33 => (1,(1,(0,(0,(1,(1,(0,0))))))) + | x34 => (0,(0,(1,(0,(1,(1,(0,0))))))) + | x35 => (1,(0,(1,(0,(1,(1,(0,0))))))) + | x36 => (0,(1,(1,(0,(1,(1,(0,0))))))) + | x37 => (1,(1,(1,(0,(1,(1,(0,0))))))) + | x38 => (0,(0,(0,(1,(1,(1,(0,0))))))) + | x39 => (1,(0,(0,(1,(1,(1,(0,0))))))) + | x3a => (0,(1,(0,(1,(1,(1,(0,0))))))) + | x3b => (1,(1,(0,(1,(1,(1,(0,0))))))) + | x3c => (0,(0,(1,(1,(1,(1,(0,0))))))) + | x3d => (1,(0,(1,(1,(1,(1,(0,0))))))) + | x3e => (0,(1,(1,(1,(1,(1,(0,0))))))) + | x3f => (1,(1,(1,(1,(1,(1,(0,0))))))) + | x40 => (0,(0,(0,(0,(0,(0,(1,0))))))) + | x41 => (1,(0,(0,(0,(0,(0,(1,0))))))) + | x42 => (0,(1,(0,(0,(0,(0,(1,0))))))) + | x43 => (1,(1,(0,(0,(0,(0,(1,0))))))) + | x44 => (0,(0,(1,(0,(0,(0,(1,0))))))) + | x45 => (1,(0,(1,(0,(0,(0,(1,0))))))) + | x46 => (0,(1,(1,(0,(0,(0,(1,0))))))) + | x47 => (1,(1,(1,(0,(0,(0,(1,0))))))) + | x48 => (0,(0,(0,(1,(0,(0,(1,0))))))) + | x49 => (1,(0,(0,(1,(0,(0,(1,0))))))) + | x4a => (0,(1,(0,(1,(0,(0,(1,0))))))) + | x4b => (1,(1,(0,(1,(0,(0,(1,0))))))) + | x4c => (0,(0,(1,(1,(0,(0,(1,0))))))) + | x4d => (1,(0,(1,(1,(0,(0,(1,0))))))) + | x4e => (0,(1,(1,(1,(0,(0,(1,0))))))) + | x4f => (1,(1,(1,(1,(0,(0,(1,0))))))) + | x50 => (0,(0,(0,(0,(1,(0,(1,0))))))) + | x51 => (1,(0,(0,(0,(1,(0,(1,0))))))) + | x52 => (0,(1,(0,(0,(1,(0,(1,0))))))) + | x53 => (1,(1,(0,(0,(1,(0,(1,0))))))) + | x54 => (0,(0,(1,(0,(1,(0,(1,0))))))) + | x55 => (1,(0,(1,(0,(1,(0,(1,0))))))) + | x56 => (0,(1,(1,(0,(1,(0,(1,0))))))) + | x57 => (1,(1,(1,(0,(1,(0,(1,0))))))) + | x58 => (0,(0,(0,(1,(1,(0,(1,0))))))) + | x59 => (1,(0,(0,(1,(1,(0,(1,0))))))) + | x5a => (0,(1,(0,(1,(1,(0,(1,0))))))) + | x5b => (1,(1,(0,(1,(1,(0,(1,0))))))) + | x5c => (0,(0,(1,(1,(1,(0,(1,0))))))) + | x5d => (1,(0,(1,(1,(1,(0,(1,0))))))) + | x5e => (0,(1,(1,(1,(1,(0,(1,0))))))) + | x5f => (1,(1,(1,(1,(1,(0,(1,0))))))) + | x60 => (0,(0,(0,(0,(0,(1,(1,0))))))) + | x61 => (1,(0,(0,(0,(0,(1,(1,0))))))) + | x62 => (0,(1,(0,(0,(0,(1,(1,0))))))) + | x63 => (1,(1,(0,(0,(0,(1,(1,0))))))) + | x64 => (0,(0,(1,(0,(0,(1,(1,0))))))) + | x65 => (1,(0,(1,(0,(0,(1,(1,0))))))) + | x66 => (0,(1,(1,(0,(0,(1,(1,0))))))) + | x67 => (1,(1,(1,(0,(0,(1,(1,0))))))) + | x68 => (0,(0,(0,(1,(0,(1,(1,0))))))) + | x69 => (1,(0,(0,(1,(0,(1,(1,0))))))) + | x6a => (0,(1,(0,(1,(0,(1,(1,0))))))) + | x6b => (1,(1,(0,(1,(0,(1,(1,0))))))) + | x6c => (0,(0,(1,(1,(0,(1,(1,0))))))) + | x6d => (1,(0,(1,(1,(0,(1,(1,0))))))) + | x6e => (0,(1,(1,(1,(0,(1,(1,0))))))) + | x6f => (1,(1,(1,(1,(0,(1,(1,0))))))) + | x70 => (0,(0,(0,(0,(1,(1,(1,0))))))) + | x71 => (1,(0,(0,(0,(1,(1,(1,0))))))) + | x72 => (0,(1,(0,(0,(1,(1,(1,0))))))) + | x73 => (1,(1,(0,(0,(1,(1,(1,0))))))) + | x74 => (0,(0,(1,(0,(1,(1,(1,0))))))) + | x75 => (1,(0,(1,(0,(1,(1,(1,0))))))) + | x76 => (0,(1,(1,(0,(1,(1,(1,0))))))) + | x77 => (1,(1,(1,(0,(1,(1,(1,0))))))) + | x78 => (0,(0,(0,(1,(1,(1,(1,0))))))) + | x79 => (1,(0,(0,(1,(1,(1,(1,0))))))) + | x7a => (0,(1,(0,(1,(1,(1,(1,0))))))) + | x7b => (1,(1,(0,(1,(1,(1,(1,0))))))) + | x7c => (0,(0,(1,(1,(1,(1,(1,0))))))) + | x7d => (1,(0,(1,(1,(1,(1,(1,0))))))) + | x7e => (0,(1,(1,(1,(1,(1,(1,0))))))) + | x7f => (1,(1,(1,(1,(1,(1,(1,0))))))) + | x80 => (0,(0,(0,(0,(0,(0,(0,1))))))) + | x81 => (1,(0,(0,(0,(0,(0,(0,1))))))) + | x82 => (0,(1,(0,(0,(0,(0,(0,1))))))) + | x83 => (1,(1,(0,(0,(0,(0,(0,1))))))) + | x84 => (0,(0,(1,(0,(0,(0,(0,1))))))) + | x85 => (1,(0,(1,(0,(0,(0,(0,1))))))) + | x86 => (0,(1,(1,(0,(0,(0,(0,1))))))) + | x87 => (1,(1,(1,(0,(0,(0,(0,1))))))) + | x88 => (0,(0,(0,(1,(0,(0,(0,1))))))) + | x89 => (1,(0,(0,(1,(0,(0,(0,1))))))) + | x8a => (0,(1,(0,(1,(0,(0,(0,1))))))) + | x8b => (1,(1,(0,(1,(0,(0,(0,1))))))) + | x8c => (0,(0,(1,(1,(0,(0,(0,1))))))) + | x8d => (1,(0,(1,(1,(0,(0,(0,1))))))) + | x8e => (0,(1,(1,(1,(0,(0,(0,1))))))) + | x8f => (1,(1,(1,(1,(0,(0,(0,1))))))) + | x90 => (0,(0,(0,(0,(1,(0,(0,1))))))) + | x91 => (1,(0,(0,(0,(1,(0,(0,1))))))) + | x92 => (0,(1,(0,(0,(1,(0,(0,1))))))) + | x93 => (1,(1,(0,(0,(1,(0,(0,1))))))) + | x94 => (0,(0,(1,(0,(1,(0,(0,1))))))) + | x95 => (1,(0,(1,(0,(1,(0,(0,1))))))) + | x96 => (0,(1,(1,(0,(1,(0,(0,1))))))) + | x97 => (1,(1,(1,(0,(1,(0,(0,1))))))) + | x98 => (0,(0,(0,(1,(1,(0,(0,1))))))) + | x99 => (1,(0,(0,(1,(1,(0,(0,1))))))) + | x9a => (0,(1,(0,(1,(1,(0,(0,1))))))) + | x9b => (1,(1,(0,(1,(1,(0,(0,1))))))) + | x9c => (0,(0,(1,(1,(1,(0,(0,1))))))) + | x9d => (1,(0,(1,(1,(1,(0,(0,1))))))) + | x9e => (0,(1,(1,(1,(1,(0,(0,1))))))) + | x9f => (1,(1,(1,(1,(1,(0,(0,1))))))) + | xa0 => (0,(0,(0,(0,(0,(1,(0,1))))))) + | xa1 => (1,(0,(0,(0,(0,(1,(0,1))))))) + | xa2 => (0,(1,(0,(0,(0,(1,(0,1))))))) + | xa3 => (1,(1,(0,(0,(0,(1,(0,1))))))) + | xa4 => (0,(0,(1,(0,(0,(1,(0,1))))))) + | xa5 => (1,(0,(1,(0,(0,(1,(0,1))))))) + | xa6 => (0,(1,(1,(0,(0,(1,(0,1))))))) + | xa7 => (1,(1,(1,(0,(0,(1,(0,1))))))) + | xa8 => (0,(0,(0,(1,(0,(1,(0,1))))))) + | xa9 => (1,(0,(0,(1,(0,(1,(0,1))))))) + | xaa => (0,(1,(0,(1,(0,(1,(0,1))))))) + | xab => (1,(1,(0,(1,(0,(1,(0,1))))))) + | xac => (0,(0,(1,(1,(0,(1,(0,1))))))) + | xad => (1,(0,(1,(1,(0,(1,(0,1))))))) + | xae => (0,(1,(1,(1,(0,(1,(0,1))))))) + | xaf => (1,(1,(1,(1,(0,(1,(0,1))))))) + | xb0 => (0,(0,(0,(0,(1,(1,(0,1))))))) + | xb1 => (1,(0,(0,(0,(1,(1,(0,1))))))) + | xb2 => (0,(1,(0,(0,(1,(1,(0,1))))))) + | xb3 => (1,(1,(0,(0,(1,(1,(0,1))))))) + | xb4 => (0,(0,(1,(0,(1,(1,(0,1))))))) + | xb5 => (1,(0,(1,(0,(1,(1,(0,1))))))) + | xb6 => (0,(1,(1,(0,(1,(1,(0,1))))))) + | xb7 => (1,(1,(1,(0,(1,(1,(0,1))))))) + | xb8 => (0,(0,(0,(1,(1,(1,(0,1))))))) + | xb9 => (1,(0,(0,(1,(1,(1,(0,1))))))) + | xba => (0,(1,(0,(1,(1,(1,(0,1))))))) + | xbb => (1,(1,(0,(1,(1,(1,(0,1))))))) + | xbc => (0,(0,(1,(1,(1,(1,(0,1))))))) + | xbd => (1,(0,(1,(1,(1,(1,(0,1))))))) + | xbe => (0,(1,(1,(1,(1,(1,(0,1))))))) + | xbf => (1,(1,(1,(1,(1,(1,(0,1))))))) + | xc0 => (0,(0,(0,(0,(0,(0,(1,1))))))) + | xc1 => (1,(0,(0,(0,(0,(0,(1,1))))))) + | xc2 => (0,(1,(0,(0,(0,(0,(1,1))))))) + | xc3 => (1,(1,(0,(0,(0,(0,(1,1))))))) + | xc4 => (0,(0,(1,(0,(0,(0,(1,1))))))) + | xc5 => (1,(0,(1,(0,(0,(0,(1,1))))))) + | xc6 => (0,(1,(1,(0,(0,(0,(1,1))))))) + | xc7 => (1,(1,(1,(0,(0,(0,(1,1))))))) + | xc8 => (0,(0,(0,(1,(0,(0,(1,1))))))) + | xc9 => (1,(0,(0,(1,(0,(0,(1,1))))))) + | xca => (0,(1,(0,(1,(0,(0,(1,1))))))) + | xcb => (1,(1,(0,(1,(0,(0,(1,1))))))) + | xcc => (0,(0,(1,(1,(0,(0,(1,1))))))) + | xcd => (1,(0,(1,(1,(0,(0,(1,1))))))) + | xce => (0,(1,(1,(1,(0,(0,(1,1))))))) + | xcf => (1,(1,(1,(1,(0,(0,(1,1))))))) + | xd0 => (0,(0,(0,(0,(1,(0,(1,1))))))) + | xd1 => (1,(0,(0,(0,(1,(0,(1,1))))))) + | xd2 => (0,(1,(0,(0,(1,(0,(1,1))))))) + | xd3 => (1,(1,(0,(0,(1,(0,(1,1))))))) + | xd4 => (0,(0,(1,(0,(1,(0,(1,1))))))) + | xd5 => (1,(0,(1,(0,(1,(0,(1,1))))))) + | xd6 => (0,(1,(1,(0,(1,(0,(1,1))))))) + | xd7 => (1,(1,(1,(0,(1,(0,(1,1))))))) + | xd8 => (0,(0,(0,(1,(1,(0,(1,1))))))) + | xd9 => (1,(0,(0,(1,(1,(0,(1,1))))))) + | xda => (0,(1,(0,(1,(1,(0,(1,1))))))) + | xdb => (1,(1,(0,(1,(1,(0,(1,1))))))) + | xdc => (0,(0,(1,(1,(1,(0,(1,1))))))) + | xdd => (1,(0,(1,(1,(1,(0,(1,1))))))) + | xde => (0,(1,(1,(1,(1,(0,(1,1))))))) + | xdf => (1,(1,(1,(1,(1,(0,(1,1))))))) + | xe0 => (0,(0,(0,(0,(0,(1,(1,1))))))) + | xe1 => (1,(0,(0,(0,(0,(1,(1,1))))))) + | xe2 => (0,(1,(0,(0,(0,(1,(1,1))))))) + | xe3 => (1,(1,(0,(0,(0,(1,(1,1))))))) + | xe4 => (0,(0,(1,(0,(0,(1,(1,1))))))) + | xe5 => (1,(0,(1,(0,(0,(1,(1,1))))))) + | xe6 => (0,(1,(1,(0,(0,(1,(1,1))))))) + | xe7 => (1,(1,(1,(0,(0,(1,(1,1))))))) + | xe8 => (0,(0,(0,(1,(0,(1,(1,1))))))) + | xe9 => (1,(0,(0,(1,(0,(1,(1,1))))))) + | xea => (0,(1,(0,(1,(0,(1,(1,1))))))) + | xeb => (1,(1,(0,(1,(0,(1,(1,1))))))) + | xec => (0,(0,(1,(1,(0,(1,(1,1))))))) + | xed => (1,(0,(1,(1,(0,(1,(1,1))))))) + | xee => (0,(1,(1,(1,(0,(1,(1,1))))))) + | xef => (1,(1,(1,(1,(0,(1,(1,1))))))) + | xf0 => (0,(0,(0,(0,(1,(1,(1,1))))))) + | xf1 => (1,(0,(0,(0,(1,(1,(1,1))))))) + | xf2 => (0,(1,(0,(0,(1,(1,(1,1))))))) + | xf3 => (1,(1,(0,(0,(1,(1,(1,1))))))) + | xf4 => (0,(0,(1,(0,(1,(1,(1,1))))))) + | xf5 => (1,(0,(1,(0,(1,(1,(1,1))))))) + | xf6 => (0,(1,(1,(0,(1,(1,(1,1))))))) + | xf7 => (1,(1,(1,(0,(1,(1,(1,1))))))) + | xf8 => (0,(0,(0,(1,(1,(1,(1,1))))))) + | xf9 => (1,(0,(0,(1,(1,(1,(1,1))))))) + | xfa => (0,(1,(0,(1,(1,(1,(1,1))))))) + | xfb => (1,(1,(0,(1,(1,(1,(1,1))))))) + | xfc => (0,(0,(1,(1,(1,(1,(1,1))))))) + | xfd => (1,(0,(1,(1,(1,(1,(1,1))))))) + | xfe => (0,(1,(1,(1,(1,(1,(1,1))))))) + | xff => (1,(1,(1,(1,(1,(1,(1,1))))))) end. Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b. -- cgit v1.2.3