Library Coq.Init.Byte
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.
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.
End ByteSyntaxNotations.