reference documentation

Article hardware-wire-def.art

path: "vendor/opentheory/data/theories/hardware-wire-def/hardware-wire-def.art"

26317 bytes
6
version
nil
"P"
"->"
typeOp
0
def
"Hardware.wire"
typeOp
nil
opType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
var
5
def
"x"
1
ref
var
6
def
"Data.Bool.!"
const
7
def
0
ref
4
ref
3
ref
cons
opType
8
def
constTerm
9
def
"y"
1
ref
var
10
def
"="
const
11
def
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
12
def
nil
cons
cons
opType
13
def
constTerm
14
def
"Hardware.connect"
"_33607"
1
ref
var
15
def
"_33608"
1
ref
var
16
def
7
ref
0
ref
0
ref
"Number.Natural.natural"
typeOp
nil
opType
17
def
3
ref
cons
opType
18
def
3
ref
cons
opType
constTerm
19
def
"t"
17
ref
var
20
def
14
ref
"Hardware.signal"
const
0
ref
1
ref
18
remove
nil
cons
cons
opType
constTerm
21
def
16
ref
varTerm
22
def
appTerm
20
ref
varTerm
23
def
appTerm
appTerm
21
ref
15
ref
varTerm
24
def
appTerm
23
ref
appTerm
appTerm
absTerm
appTerm
25
def
absTerm
26
def
absTerm
27
def
defineConst
28
def
pop
0
ref
1
ref
4
remove
nil
cons
cons
opType
29
def
constTerm
30
def
6
ref
varTerm
31
def
appTerm
10
ref
varTerm
32
def
appTerm
appTerm
19
ref
20
ref
14
ref
21
ref
32
ref
appTerm
33
def
23
ref
appTerm
34
def
appTerm
35
def
21
ref
31
ref
appTerm
23
ref
appTerm
36
def
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
37
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
1
ref
nil
cons
cons
nil
cons
nil
nil
cons
cons
14
ref
7
remove
0
ref
0
ref
"A"
varType
38
def
3
ref
cons
opType
39
def
3
ref
cons
opType
40
def
constTerm
41
def
"P"
39
ref
var
varTerm
42
def
appTerm
appTerm
refl
"p"
39
ref
var
43
def
11
ref
0
ref
39
remove
40
ref
nil
cons
cons
opType
constTerm
43
remove
varTerm
appTerm
"x"
38
remove
var
"Data.Bool.T"
const
2
ref
constTerm
44
def
absTerm
appTerm
absTerm
45
def
42
ref
appTerm
betaConv
appThm
nil
11
remove
0
ref
40
ref
0
ref
40
remove
3
remove
cons
opType
nil
cons
cons
opType
constTerm
41
remove
appTerm
45
remove
appTerm
axiom
42
remove
refl
appThm
eqMp
sym
subst
46
def
subst
15
remove
nil
"t"
2
ref
var
47
def
9
ref
16
ref
14
ref
30
ref
24
ref
appTerm
22
ref
appTerm
appTerm
25
remove
appTerm
48
def
absTerm
49
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
14
ref
47
ref
varTerm
50
def
appTerm
44
ref
appTerm
assume
sym
nil
44
remove
axiom
51
def
eqMp
50
remove
assume
51
remove
deductAntisym
deductAntisym
52
def
subst
nil
5
ref
49
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
16
remove
nil
47
ref
48
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
28
remove
24
ref
refl
appThm
27
remove
24
remove
appTerm
betaConv
trans
22
ref
refl
appThm
26
remove
22
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
37
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
14
ref
"Hardware.not"
"_33631"
1
ref
var
53
def
"_33632"
1
ref
var
54
def
19
ref
20
ref
14
ref
21
ref
54
ref
varTerm
55
def
appTerm
23
ref
appTerm
appTerm
"Data.Bool.~"
const
12
remove
constTerm
56
def
21
ref
53
ref
varTerm
57
def
appTerm
23
ref
appTerm
appTerm
appTerm
absTerm
appTerm
58
def
absTerm
59
def
absTerm
60
def
defineConst
61
def
pop
29
ref
constTerm
62
def
31
ref
appTerm
32
ref
appTerm
appTerm
19
ref
20
ref
35
remove
56
ref
36
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
63
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
53
remove
nil
47
ref
9
ref
54
ref
14
ref
62
ref
57
ref
appTerm
55
ref
appTerm
appTerm
58
remove
appTerm
64
def
absTerm
65
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
65
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
54
remove
nil
47
ref
64
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
61
remove
57
ref
refl
appThm
60
remove
57
remove
appTerm
betaConv
trans
55
ref
refl
appThm
59
remove
55
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
63
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
14
ref
"Hardware.delay"
"_33619"
1
ref
var
66
def
"_33620"
1
ref
var
67
def
19
ref
20
ref
14
ref
21
ref
67
ref
varTerm
68
def
appTerm
"Number.Natural.+"
const
0
ref
17
ref
0
ref
17
ref
17
ref
nil
cons
cons
opType
69
def
nil
cons
cons
opType
constTerm
23
ref
appTerm
"Number.Natural.bit1"
const
69
remove
constTerm
"Number.Natural.zero"
const
17
remove
constTerm
appTerm
appTerm
70
def
appTerm
appTerm
21
ref
66
ref
varTerm
71
def
appTerm
23
ref
appTerm
appTerm
absTerm
appTerm
72
def
absTerm
73
def
absTerm
74
def
defineConst
75
def
pop
29
ref
constTerm
76
def
31
ref
appTerm
77
def
32
ref
appTerm
appTerm
19
ref
20
ref
14
ref
33
remove
70
remove
appTerm
appTerm
36
ref
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
78
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
66
remove
nil
47
ref
9
ref
67
ref
14
ref
76
ref
71
ref
appTerm
68
ref
appTerm
appTerm
72
remove
appTerm
79
def
absTerm
80
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
80
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
67
remove
nil
47
ref
79
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
75
remove
71
ref
refl
appThm
74
remove
71
remove
appTerm
betaConv
trans
68
ref
refl
appThm
73
remove
68
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
78
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
"z"
1
ref
var
81
def
14
ref
"Hardware.nor2"
"_33750"
1
ref
var
82
def
"_33751"
1
ref
var
83
def
"_33752"
1
ref
var
84
def
"Data.Bool.?"
const
8
remove
constTerm
85
def
"zn"
1
ref
var
86
def
"Data.Bool./\\"
const
13
ref
constTerm
87
def
"Hardware.or2"
"_33664"
1
ref
var
88
def
"_33665"
1
ref
var
89
def
"_33666"
1
ref
var
90
def
19
ref
20
ref
14
ref
21
ref
90
ref
varTerm
91
def
appTerm
23
ref
appTerm
appTerm
"Data.Bool.\\/"
const
13
ref
constTerm
92
def
21
ref
88
ref
varTerm
93
def
appTerm
23
ref
appTerm
appTerm
21
ref
89
ref
varTerm
94
def
appTerm
23
ref
appTerm
appTerm
appTerm
absTerm
appTerm
95
def
absTerm
96
def
absTerm
97
def
absTerm
98
def
defineConst
99
def
pop
0
ref
1
ref
29
ref
nil
cons
cons
opType
100
def
constTerm
101
def
82
ref
varTerm
102
def
appTerm
83
ref
varTerm
103
def
appTerm
86
ref
varTerm
104
def
appTerm
appTerm
62
ref
104
ref
appTerm
105
def
84
ref
varTerm
106
def
appTerm
appTerm
absTerm
appTerm
107
def
absTerm
108
def
absTerm
109
def
absTerm
110
def
defineConst
111
def
pop
100
ref
constTerm
112
def
31
ref
appTerm
32
ref
appTerm
81
ref
varTerm
113
def
appTerm
appTerm
85
ref
86
remove
87
ref
101
ref
31
ref
appTerm
32
ref
appTerm
114
def
104
remove
appTerm
appTerm
105
remove
113
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
115
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
82
remove
nil
47
ref
9
ref
83
ref
9
ref
84
ref
14
ref
112
remove
102
ref
appTerm
103
ref
appTerm
106
ref
appTerm
appTerm
107
remove
appTerm
116
def
absTerm
117
def
appTerm
118
def
absTerm
119
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
119
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
83
remove
nil
47
ref
118
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
117
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
84
remove
nil
47
ref
116
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
111
remove
102
ref
refl
appThm
110
remove
102
remove
appTerm
betaConv
trans
103
ref
refl
appThm
109
remove
103
remove
appTerm
betaConv
trans
106
ref
refl
appThm
108
remove
106
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
115
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
81
ref
14
ref
"Hardware.and2"
"_33643"
1
ref
var
120
def
"_33644"
1
ref
var
121
def
"_33645"
1
ref
var
122
def
19
ref
20
ref
14
ref
21
ref
122
ref
varTerm
123
def
appTerm
23
ref
appTerm
appTerm
87
ref
21
ref
120
ref
varTerm
124
def
appTerm
23
ref
appTerm
appTerm
21
ref
121
ref
varTerm
125
def
appTerm
23
ref
appTerm
appTerm
appTerm
absTerm
appTerm
126
def
absTerm
127
def
absTerm
128
def
absTerm
129
def
defineConst
130
def
pop
100
ref
constTerm
131
def
31
ref
appTerm
132
def
32
ref
appTerm
133
def
113
ref
appTerm
appTerm
19
ref
20
ref
14
ref
21
ref
113
ref
appTerm
23
ref
appTerm
appTerm
134
def
87
ref
36
ref
appTerm
34
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
135
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
120
remove
nil
47
ref
9
ref
121
ref
9
ref
122
ref
14
ref
131
ref
124
ref
appTerm
125
ref
appTerm
123
ref
appTerm
appTerm
126
remove
appTerm
136
def
absTerm
137
def
appTerm
138
def
absTerm
139
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
139
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
121
remove
nil
47
ref
138
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
137
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
122
remove
nil
47
ref
136
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
130
remove
124
ref
refl
appThm
129
remove
124
remove
appTerm
betaConv
trans
125
ref
refl
appThm
128
remove
125
remove
appTerm
betaConv
trans
123
ref
refl
appThm
127
remove
123
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
135
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
81
ref
14
ref
114
remove
113
ref
appTerm
appTerm
19
ref
20
ref
134
ref
92
remove
36
ref
appTerm
34
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
140
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
88
remove
nil
47
ref
9
ref
89
ref
9
ref
90
ref
14
ref
101
ref
93
ref
appTerm
94
ref
appTerm
91
ref
appTerm
appTerm
95
remove
appTerm
141
def
absTerm
142
def
appTerm
143
def
absTerm
144
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
144
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
89
remove
nil
47
ref
143
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
142
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
90
remove
nil
47
ref
141
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
99
remove
93
ref
refl
appThm
98
remove
93
remove
appTerm
betaConv
trans
94
ref
refl
appThm
97
remove
94
remove
appTerm
betaConv
trans
91
ref
refl
appThm
96
remove
91
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
140
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
14
ref
"Hardware.pulse"
"_33738"
1
ref
var
145
def
"_33739"
1
ref
var
146
def
85
ref
"xd"
1
ref
var
147
def
85
ref
"xn"
1
ref
var
148
def
87
ref
76
ref
145
ref
varTerm
149
def
appTerm
147
ref
varTerm
150
def
appTerm
appTerm
87
ref
62
remove
150
ref
appTerm
148
ref
varTerm
151
def
appTerm
appTerm
152
def
131
ref
149
ref
appTerm
151
ref
appTerm
146
ref
varTerm
153
def
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
154
def
absTerm
155
def
absTerm
156
def
defineConst
157
def
pop
29
remove
constTerm
158
def
31
ref
appTerm
32
ref
appTerm
appTerm
85
ref
147
remove
85
ref
148
remove
87
ref
77
remove
150
remove
appTerm
appTerm
152
remove
132
remove
151
remove
appTerm
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
159
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
145
remove
nil
47
ref
9
ref
146
ref
14
ref
158
remove
149
ref
appTerm
153
ref
appTerm
appTerm
154
remove
appTerm
160
def
absTerm
161
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
161
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
146
remove
nil
47
ref
160
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
157
remove
149
ref
refl
appThm
156
remove
149
remove
appTerm
betaConv
trans
153
ref
refl
appThm
155
remove
153
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
159
remove
appTerm
thm
nil
5
ref
"w"
1
ref
var
162
def
9
ref
6
ref
9
ref
10
ref
9
ref
81
ref
14
ref
"Hardware.and3"
"_33771"
1
ref
var
163
def
"_33772"
1
ref
var
164
def
"_33773"
1
ref
var
165
def
"_33774"
1
ref
var
166
def
85
ref
"wx"
1
ref
var
167
def
87
ref
131
ref
163
ref
varTerm
168
def
appTerm
164
ref
varTerm
169
def
appTerm
167
ref
varTerm
170
def
appTerm
appTerm
131
ref
170
ref
appTerm
171
def
165
ref
varTerm
172
def
appTerm
166
ref
varTerm
173
def
appTerm
appTerm
absTerm
appTerm
174
def
absTerm
175
def
absTerm
176
def
absTerm
177
def
absTerm
178
def
defineConst
179
def
pop
0
ref
1
ref
100
ref
nil
cons
cons
opType
180
def
constTerm
181
def
162
ref
varTerm
182
def
appTerm
31
ref
appTerm
32
ref
appTerm
113
ref
appTerm
appTerm
85
ref
167
ref
87
ref
131
ref
182
ref
appTerm
183
def
31
ref
appTerm
170
ref
appTerm
appTerm
184
def
171
remove
32
ref
appTerm
113
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
185
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
163
remove
nil
47
ref
9
ref
164
ref
9
ref
165
ref
9
ref
166
ref
14
ref
181
remove
168
ref
appTerm
169
ref
appTerm
172
ref
appTerm
173
ref
appTerm
appTerm
174
remove
appTerm
186
def
absTerm
187
def
appTerm
188
def
absTerm
189
def
appTerm
190
def
absTerm
191
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
191
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
164
remove
nil
47
ref
190
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
189
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
165
remove
nil
47
ref
188
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
187
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
166
remove
nil
47
ref
186
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
179
remove
168
ref
refl
appThm
178
remove
168
remove
appTerm
betaConv
trans
169
ref
refl
appThm
177
remove
169
remove
appTerm
betaConv
trans
172
ref
refl
appThm
176
remove
172
remove
appTerm
betaConv
trans
173
ref
refl
appThm
175
remove
173
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
185
remove
appTerm
thm
nil
5
ref
162
ref
9
ref
6
ref
9
ref
10
ref
9
ref
81
ref
14
ref
"Hardware.or3"
"_33803"
1
ref
var
192
def
"_33804"
1
ref
var
193
def
"_33805"
1
ref
var
194
def
"_33806"
1
ref
var
195
def
85
ref
167
ref
87
ref
101
ref
192
ref
varTerm
196
def
appTerm
193
ref
varTerm
197
def
appTerm
170
ref
appTerm
appTerm
101
ref
170
ref
appTerm
198
def
194
ref
varTerm
199
def
appTerm
195
ref
varTerm
200
def
appTerm
appTerm
absTerm
appTerm
201
def
absTerm
202
def
absTerm
203
def
absTerm
204
def
absTerm
205
def
defineConst
206
def
pop
180
ref
constTerm
207
def
182
ref
appTerm
31
ref
appTerm
32
ref
appTerm
113
ref
appTerm
appTerm
85
ref
167
ref
87
ref
101
ref
182
ref
appTerm
208
def
31
ref
appTerm
170
ref
appTerm
appTerm
198
remove
32
ref
appTerm
113
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
209
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
192
remove
nil
47
ref
9
ref
193
ref
9
ref
194
ref
9
ref
195
ref
14
ref
207
ref
196
ref
appTerm
197
ref
appTerm
199
ref
appTerm
200
ref
appTerm
appTerm
201
remove
appTerm
210
def
absTerm
211
def
appTerm
212
def
absTerm
213
def
appTerm
214
def
absTerm
215
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
215
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
193
remove
nil
47
ref
214
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
213
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
194
remove
nil
47
ref
212
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
211
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
195
remove
nil
47
ref
210
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
206
remove
196
ref
refl
appThm
205
remove
196
remove
appTerm
betaConv
trans
197
ref
refl
appThm
204
remove
197
remove
appTerm
betaConv
trans
199
ref
refl
appThm
203
remove
199
remove
appTerm
betaConv
trans
200
ref
refl
appThm
202
remove
200
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
209
remove
appTerm
thm
nil
5
ref
162
ref
9
ref
6
ref
9
ref
10
ref
9
ref
81
ref
14
ref
"Hardware.xor3"
"_33835"
1
ref
var
216
def
"_33836"
1
ref
var
217
def
"_33837"
1
ref
var
218
def
"_33838"
1
ref
var
219
def
85
ref
167
ref
87
ref
"Hardware.xor2"
"_33685"
1
ref
var
220
def
"_33686"
1
ref
var
221
def
"_33687"
1
ref
var
222
def
19
ref
20
ref
14
ref
21
ref
222
ref
varTerm
223
def
appTerm
23
ref
appTerm
appTerm
56
ref
14
ref
21
ref
220
ref
varTerm
224
def
appTerm
23
ref
appTerm
appTerm
21
ref
221
ref
varTerm
225
def
appTerm
23
ref
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
226
def
absTerm
227
def
absTerm
228
def
absTerm
229
def
defineConst
230
def
pop
100
ref
constTerm
231
def
216
ref
varTerm
232
def
appTerm
217
ref
varTerm
233
def
appTerm
170
ref
appTerm
appTerm
231
ref
170
ref
appTerm
234
def
218
ref
varTerm
235
def
appTerm
219
ref
varTerm
236
def
appTerm
appTerm
absTerm
appTerm
237
def
absTerm
238
def
absTerm
239
def
absTerm
240
def
absTerm
241
def
defineConst
242
def
pop
180
ref
constTerm
243
def
182
ref
appTerm
31
ref
appTerm
32
ref
appTerm
113
ref
appTerm
appTerm
85
ref
167
ref
87
ref
231
ref
182
ref
appTerm
31
ref
appTerm
170
ref
appTerm
appTerm
234
remove
32
ref
appTerm
113
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
244
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
216
remove
nil
47
ref
9
ref
217
ref
9
ref
218
ref
9
ref
219
ref
14
ref
243
remove
232
ref
appTerm
233
ref
appTerm
235
ref
appTerm
236
ref
appTerm
appTerm
237
remove
appTerm
245
def
absTerm
246
def
appTerm
247
def
absTerm
248
def
appTerm
249
def
absTerm
250
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
250
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
217
remove
nil
47
ref
249
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
248
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
218
remove
nil
47
ref
247
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
246
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
219
remove
nil
47
ref
245
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
242
remove
232
ref
refl
appThm
241
remove
232
remove
appTerm
betaConv
trans
233
ref
refl
appThm
240
remove
233
remove
appTerm
betaConv
trans
235
ref
refl
appThm
239
remove
235
remove
appTerm
betaConv
trans
236
ref
refl
appThm
238
remove
236
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
244
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
81
ref
14
ref
231
ref
31
ref
appTerm
32
ref
appTerm
113
ref
appTerm
appTerm
19
ref
20
ref
134
ref
56
remove
14
ref
36
ref
appTerm
34
ref
appTerm
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
251
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
220
remove
nil
47
ref
9
ref
221
ref
9
ref
222
ref
14
ref
231
remove
224
ref
appTerm
225
ref
appTerm
223
ref
appTerm
appTerm
226
remove
appTerm
252
def
absTerm
253
def
appTerm
254
def
absTerm
255
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
255
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
221
remove
nil
47
ref
254
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
253
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
222
remove
nil
47
ref
252
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
230
remove
224
ref
refl
appThm
229
remove
224
remove
appTerm
betaConv
trans
225
ref
refl
appThm
228
remove
225
remove
appTerm
betaConv
trans
223
ref
refl
appThm
227
remove
223
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
251
remove
appTerm
thm
nil
5
ref
"s"
1
ref
var
256
def
9
ref
6
ref
9
ref
10
ref
9
ref
81
ref
14
ref
"Hardware.case1"
"_33706"
1
ref
var
257
def
"_33707"
1
ref
var
258
def
"_33708"
1
ref
var
259
def
"_33709"
1
ref
var
260
def
19
ref
20
ref
14
ref
21
ref
260
ref
varTerm
261
def
appTerm
23
ref
appTerm
appTerm
"Data.Bool.cond"
const
0
remove
2
remove
13
remove
nil
cons
cons
opType
constTerm
262
def
21
ref
257
ref
varTerm
263
def
appTerm
23
ref
appTerm
appTerm
21
ref
258
ref
varTerm
264
def
appTerm
23
ref
appTerm
appTerm
21
ref
259
ref
varTerm
265
def
appTerm
23
ref
appTerm
appTerm
appTerm
absTerm
appTerm
266
def
absTerm
267
def
absTerm
268
def
absTerm
269
def
absTerm
270
def
defineConst
271
def
pop
180
ref
constTerm
272
def
256
remove
varTerm
273
def
appTerm
31
ref
appTerm
32
ref
appTerm
113
ref
appTerm
appTerm
19
remove
20
remove
134
remove
262
remove
21
remove
273
remove
appTerm
23
remove
appTerm
appTerm
36
remove
appTerm
34
remove
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
274
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
257
remove
nil
47
ref
9
ref
258
ref
9
ref
259
ref
9
ref
260
ref
14
ref
272
ref
263
ref
appTerm
264
ref
appTerm
265
ref
appTerm
261
ref
appTerm
appTerm
266
remove
appTerm
275
def
absTerm
276
def
appTerm
277
def
absTerm
278
def
appTerm
279
def
absTerm
280
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
280
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
258
remove
nil
47
ref
279
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
278
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
259
remove
nil
47
ref
277
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
276
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
260
remove
nil
47
ref
275
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
271
remove
263
ref
refl
appThm
270
remove
263
remove
appTerm
betaConv
trans
264
ref
refl
appThm
269
remove
264
remove
appTerm
betaConv
trans
265
ref
refl
appThm
268
remove
265
remove
appTerm
betaConv
trans
261
ref
refl
appThm
267
remove
261
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
274
remove
appTerm
thm
nil
5
ref
"ld"
1
ref
var
281
def
9
ref
162
ref
9
ref
6
ref
14
ref
"Hardware.sticky"
"_33899"
1
ref
var
282
def
"_33900"
1
ref
var
283
def
"_33901"
1
ref
var
284
def
85
ref
"p"
1
ref
var
285
def
85
ref
"q"
1
ref
var
286
def
85
ref
"r"
1
ref
var
287
def
87
ref
272
ref
282
ref
varTerm
288
def
appTerm
"Hardware.ground"
const
1
ref
constTerm
289
def
appTerm
285
ref
varTerm
290
def
appTerm
286
ref
varTerm
291
def
appTerm
appTerm
87
ref
101
remove
283
ref
varTerm
292
def
appTerm
291
ref
appTerm
287
ref
varTerm
293
def
appTerm
appTerm
87
ref
76
remove
293
ref
appTerm
290
ref
appTerm
appTerm
294
def
30
remove
293
ref
appTerm
295
def
284
ref
varTerm
296
def
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
297
def
absTerm
298
def
absTerm
299
def
absTerm
300
def
defineConst
301
def
pop
100
remove
constTerm
302
def
281
remove
varTerm
303
def
appTerm
182
ref
appTerm
31
ref
appTerm
appTerm
85
ref
285
remove
85
ref
286
remove
85
ref
287
remove
87
ref
272
remove
303
remove
appTerm
289
remove
appTerm
290
remove
appTerm
291
ref
appTerm
appTerm
87
ref
208
remove
291
remove
appTerm
293
remove
appTerm
appTerm
294
remove
295
remove
31
ref
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
304
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
282
remove
nil
47
ref
9
ref
283
ref
9
ref
284
ref
14
ref
302
remove
288
ref
appTerm
292
ref
appTerm
296
ref
appTerm
appTerm
297
remove
appTerm
305
def
absTerm
306
def
appTerm
307
def
absTerm
308
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
308
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
283
remove
nil
47
ref
307
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
306
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
284
remove
nil
47
ref
305
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
301
remove
288
ref
refl
appThm
300
remove
288
remove
appTerm
betaConv
trans
292
ref
refl
appThm
299
remove
292
remove
appTerm
betaConv
trans
296
ref
refl
appThm
298
remove
296
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
304
remove
appTerm
thm
nil
5
ref
162
remove
9
ref
6
remove
9
ref
10
remove
9
ref
81
remove
14
ref
"Hardware.majority3"
"_33867"
1
ref
var
309
def
"_33868"
1
ref
var
310
def
"_33869"
1
ref
var
311
def
"_33870"
1
ref
var
312
def
85
ref
167
ref
85
ref
"wy"
1
ref
var
313
def
85
ref
"xy"
1
remove
var
314
def
87
ref
131
ref
309
ref
varTerm
315
def
appTerm
316
def
310
ref
varTerm
317
def
appTerm
170
ref
appTerm
appTerm
87
ref
316
remove
311
ref
varTerm
318
def
appTerm
313
ref
varTerm
319
def
appTerm
appTerm
87
ref
131
remove
317
ref
appTerm
318
ref
appTerm
314
ref
varTerm
320
def
appTerm
appTerm
207
remove
170
remove
appTerm
319
ref
appTerm
320
ref
appTerm
321
def
312
ref
varTerm
322
def
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
323
def
absTerm
324
def
absTerm
325
def
absTerm
326
def
absTerm
327
def
defineConst
328
def
pop
180
remove
constTerm
329
def
182
remove
appTerm
31
remove
appTerm
32
ref
appTerm
113
ref
appTerm
appTerm
85
ref
167
remove
85
ref
313
remove
85
remove
314
remove
184
remove
87
ref
183
remove
32
remove
appTerm
319
remove
appTerm
appTerm
87
remove
133
remove
320
remove
appTerm
appTerm
321
remove
113
remove
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
330
def
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
309
remove
nil
47
ref
9
ref
310
ref
9
ref
311
ref
9
ref
312
ref
14
remove
329
remove
315
ref
appTerm
317
ref
appTerm
318
ref
appTerm
322
ref
appTerm
appTerm
323
remove
appTerm
331
def
absTerm
332
def
appTerm
333
def
absTerm
334
def
appTerm
335
def
absTerm
336
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
336
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
310
remove
nil
47
ref
335
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
ref
334
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
ref
subst
311
remove
nil
47
ref
333
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
subst
nil
5
remove
332
remove
nil
cons
cons
nil
cons
nil
cons
cons
46
remove
subst
312
remove
nil
47
remove
331
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
remove
subst
328
remove
315
ref
refl
appThm
327
remove
315
remove
appTerm
betaConv
trans
317
ref
refl
appThm
326
remove
317
remove
appTerm
betaConv
trans
318
ref
refl
appThm
325
remove
318
remove
appTerm
betaConv
trans
322
ref
refl
appThm
324
remove
322
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
remove
330
remove
appTerm
thm