Library Coq.Init.Byte
Require Import Coq.Init.Ltac.
Require Import Coq.Init.Datatypes.
Require Import Coq.Init.Logic.
Require Import Coq.Init.Specif.
Require Coq.Init.Nat.
We define an inductive for use with the String Notation command
which contains all ascii characters. We use 256 constructors for
efficiency and ease of conversion.
Declare Scope byte_scope.
Delimit Scope byte_scope with byte.
Inductive byte :=
| x00
| x01
| x02
| x03
| x04
| x05
| x06
| x07
| x08
| x09
| x0a
| x0b
| x0c
| x0d
| x0e
| x0f
| x10
| x11
| x12
| x13
| x14
| x15
| x16
| x17
| x18
| x19
| x1a
| x1b
| x1c
| x1d
| x1e
| x1f
| x20
| x21
| x22
| x23
| x24
| x25
| x26
| x27
| x28
| x29
| x2a
| x2b
| x2c
| x2d
| x2e
| x2f
| x30
| x31
| x32
| x33
| x34
| x35
| x36
| x37
| x38
| x39
| x3a
| x3b
| x3c
| x3d
| x3e
| x3f
| x40
| x41
| x42
| x43
| x44
| x45
| x46
| x47
| x48
| x49
| x4a
| x4b
| x4c
| x4d
| x4e
| x4f
| x50
| x51
| x52
| x53
| x54
| x55
| x56
| x57
| x58
| x59
| x5a
| x5b
| x5c
| x5d
| x5e
| x5f
| x60
| x61
| x62
| x63
| x64
| x65
| x66
| x67
| x68
| x69
| x6a
| x6b
| x6c
| x6d
| x6e
| x6f
| x70
| x71
| x72
| x73
| x74
| x75
| x76
| x77
| x78
| x79
| x7a
| x7b
| x7c
| x7d
| x7e
| x7f
| x80
| x81
| x82
| x83
| x84
| x85
| x86
| x87
| x88
| x89
| x8a
| x8b
| x8c
| x8d
| x8e
| x8f
| x90
| x91
| x92
| x93
| x94
| x95
| x96
| x97
| x98
| x99
| x9a
| x9b
| x9c
| x9d
| x9e
| x9f
| xa0
| xa1
| xa2
| xa3
| xa4
| xa5
| xa6
| xa7
| xa8
| xa9
| xaa
| xab
| xac
| xad
| xae
| xaf
| xb0
| xb1
| xb2
| xb3
| xb4
| xb5
| xb6
| xb7
| xb8
| xb9
| xba
| xbb
| xbc
| xbd
| xbe
| xbf
| xc0
| xc1
| xc2
| xc3
| xc4
| xc5
| xc6
| xc7
| xc8
| xc9
| xca
| xcb
| xcc
| xcd
| xce
| xcf
| xd0
| xd1
| xd2
| xd3
| xd4
| xd5
| xd6
| xd7
| xd8
| xd9
| xda
| xdb
| xdc
| xdd
| xde
| xdf
| xe0
| xe1
| xe2
| xe3
| xe4
| xe5
| xe6
| xe7
| xe8
| xe9
| xea
| xeb
| xec
| xed
| xee
| xef
| xf0
| xf1
| xf2
| xf3
| xf4
| xf5
| xf6
| xf7
| xf8
| xf9
| xfa
| xfb
| xfc
| xfd
| xfe
| xff
.
Bind Scope byte_scope with byte.
Register byte as core.byte.type.
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
:= 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
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.
Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b.
Definition byte_of_byte (b : byte) : byte := b.
Module Export ByteSyntaxNotations.
String Notation byte byte_of_byte byte_of_byte : byte_scope.
End ByteSyntaxNotations.
:= 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
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.
Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b.
Definition byte_of_byte (b : byte) : byte := b.
Module Export ByteSyntaxNotations.
String Notation byte byte_of_byte byte_of_byte : byte_scope.
End ByteSyntaxNotations.