reference documentation

Article hardware-adder-def.art

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

26744 bytes
6
version
nil
"P"
"->"
typeOp
0
def
"Hardware.bus"
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
9
ref
"s"
1
ref
var
11
def
9
ref
"c"
1
ref
var
12
def
"="
const
13
def
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
nil
cons
cons
opType
14
def
constTerm
15
def
"Hardware.Bus.adder2"
"_34835"
1
ref
var
16
def
"_34836"
1
ref
var
17
def
"_34837"
1
ref
var
18
def
"_34838"
1
ref
var
19
def
"Data.Bool./\\"
const
14
remove
constTerm
20
def
"Hardware.Bus.xor2"
const
0
ref
1
ref
0
ref
1
ref
4
remove
nil
cons
21
def
cons
opType
22
def
nil
cons
cons
opType
23
def
constTerm
24
def
16
ref
varTerm
25
def
appTerm
17
ref
varTerm
26
def
appTerm
18
ref
varTerm
27
def
appTerm
appTerm
"Hardware.Bus.and2"
const
23
ref
constTerm
28
def
25
ref
appTerm
26
ref
appTerm
19
ref
varTerm
29
def
appTerm
appTerm
30
def
absTerm
31
def
absTerm
32
def
absTerm
33
def
absTerm
34
def
defineConst
35
def
pop
0
ref
1
ref
23
remove
nil
cons
36
def
cons
opType
37
def
constTerm
38
def
6
ref
varTerm
39
def
appTerm
10
ref
varTerm
40
def
appTerm
11
ref
varTerm
41
def
appTerm
12
ref
varTerm
42
def
appTerm
appTerm
20
ref
24
remove
39
ref
appTerm
40
ref
appTerm
41
ref
appTerm
appTerm
28
remove
39
ref
appTerm
40
ref
appTerm
42
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
43
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
1
ref
nil
cons
cons
nil
cons
nil
nil
cons
44
def
cons
15
ref
7
ref
0
ref
0
ref
"A"
varType
45
def
3
ref
cons
opType
46
def
3
ref
cons
opType
47
def
constTerm
48
def
"P"
46
ref
var
varTerm
49
def
appTerm
appTerm
refl
"p"
46
ref
var
50
def
13
ref
0
ref
46
remove
47
ref
nil
cons
cons
opType
constTerm
50
remove
varTerm
appTerm
"x"
45
remove
var
"Data.Bool.T"
const
2
ref
constTerm
51
def
absTerm
appTerm
absTerm
52
def
49
ref
appTerm
betaConv
appThm
nil
13
ref
0
ref
47
ref
0
ref
47
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
48
remove
appTerm
52
remove
appTerm
axiom
49
remove
refl
appThm
eqMp
sym
53
def
subst
54
def
subst
16
remove
nil
"t"
2
remove
var
55
def
9
ref
17
ref
9
ref
18
ref
9
ref
19
ref
15
ref
38
ref
25
ref
appTerm
26
ref
appTerm
27
ref
appTerm
29
ref
appTerm
appTerm
30
remove
appTerm
56
def
absTerm
57
def
appTerm
58
def
absTerm
59
def
appTerm
60
def
absTerm
61
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
15
ref
55
ref
varTerm
62
def
appTerm
51
ref
appTerm
assume
sym
nil
51
remove
axiom
63
def
eqMp
62
remove
assume
63
remove
deductAntisym
deductAntisym
64
def
subst
nil
5
ref
61
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
17
remove
nil
55
ref
60
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
59
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
18
remove
nil
55
ref
58
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
57
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
19
remove
nil
55
ref
56
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
35
remove
25
ref
refl
appThm
34
remove
25
remove
appTerm
betaConv
trans
26
ref
refl
appThm
33
remove
26
remove
appTerm
betaConv
trans
27
ref
refl
appThm
32
remove
27
remove
appTerm
betaConv
trans
29
ref
refl
appThm
31
remove
29
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
43
remove
appTerm
thm
nil
"P"
0
ref
"Hardware.wire"
typeOp
nil
opType
65
def
3
ref
cons
opType
66
def
var
67
def
"x"
65
ref
var
68
def
7
remove
0
ref
66
ref
3
ref
cons
opType
69
def
constTerm
70
def
"y"
65
ref
var
71
def
70
ref
"s"
65
ref
var
72
def
70
ref
"c"
65
ref
var
73
def
15
ref
"Hardware.adder2"
"_34758"
65
ref
var
74
def
"_34759"
65
ref
var
75
def
"_34760"
65
ref
var
76
def
"_34761"
65
ref
var
77
def
20
ref
"Hardware.xor2"
const
0
ref
65
ref
0
ref
65
ref
66
remove
nil
cons
78
def
cons
opType
79
def
nil
cons
cons
opType
80
def
constTerm
81
def
74
ref
varTerm
82
def
appTerm
75
ref
varTerm
83
def
appTerm
76
ref
varTerm
84
def
appTerm
appTerm
"Hardware.and2"
const
80
ref
constTerm
85
def
82
ref
appTerm
83
ref
appTerm
77
ref
varTerm
86
def
appTerm
appTerm
87
def
absTerm
88
def
absTerm
89
def
absTerm
90
def
absTerm
91
def
defineConst
92
def
pop
0
ref
65
ref
80
remove
nil
cons
cons
opType
93
def
constTerm
94
def
68
ref
varTerm
95
def
appTerm
71
ref
varTerm
96
def
appTerm
72
ref
varTerm
97
def
appTerm
73
ref
varTerm
98
def
appTerm
appTerm
20
ref
81
remove
95
ref
appTerm
96
ref
appTerm
97
ref
appTerm
appTerm
85
remove
95
ref
appTerm
96
ref
appTerm
98
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
99
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
65
ref
nil
cons
cons
nil
cons
44
remove
cons
53
remove
subst
100
def
subst
74
remove
nil
55
ref
70
ref
75
ref
70
ref
76
ref
70
ref
77
ref
15
ref
94
ref
82
ref
appTerm
83
ref
appTerm
84
ref
appTerm
86
ref
appTerm
appTerm
87
remove
appTerm
101
def
absTerm
102
def
appTerm
103
def
absTerm
104
def
appTerm
105
def
absTerm
106
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
ref
106
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
75
remove
nil
55
ref
105
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
ref
104
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
76
remove
nil
55
ref
103
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
ref
102
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
77
remove
nil
55
ref
101
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
92
remove
82
ref
refl
appThm
91
remove
82
remove
appTerm
betaConv
trans
83
ref
refl
appThm
90
remove
83
remove
appTerm
betaConv
trans
84
ref
refl
appThm
89
remove
84
remove
appTerm
betaConv
trans
86
ref
refl
appThm
88
remove
86
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
70
ref
99
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
"z"
1
ref
var
107
def
9
ref
11
ref
9
ref
12
ref
15
ref
"Hardware.Bus.adder3"
"_34867"
1
ref
var
108
def
"_34868"
1
ref
var
109
def
"_34869"
1
ref
var
110
def
"_34870"
1
ref
var
111
def
"_34871"
1
ref
var
112
def
20
ref
"Hardware.Bus.xor3"
const
37
ref
constTerm
113
def
108
ref
varTerm
114
def
appTerm
109
ref
varTerm
115
def
appTerm
110
ref
varTerm
116
def
appTerm
111
ref
varTerm
117
def
appTerm
appTerm
"Hardware.Bus.majority3"
const
37
ref
constTerm
118
def
114
ref
appTerm
115
ref
appTerm
116
ref
appTerm
112
ref
varTerm
119
def
appTerm
appTerm
120
def
absTerm
121
def
absTerm
122
def
absTerm
123
def
absTerm
124
def
absTerm
125
def
defineConst
126
def
pop
0
ref
1
ref
37
remove
nil
cons
cons
opType
127
def
constTerm
128
def
39
ref
appTerm
40
ref
appTerm
107
ref
varTerm
129
def
appTerm
41
ref
appTerm
42
ref
appTerm
appTerm
20
ref
113
remove
39
ref
appTerm
40
ref
appTerm
129
ref
appTerm
41
ref
appTerm
appTerm
118
remove
39
ref
appTerm
40
ref
appTerm
129
ref
appTerm
42
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
130
def
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
108
remove
nil
55
ref
9
ref
109
ref
9
ref
110
ref
9
ref
111
ref
9
ref
112
ref
15
ref
128
ref
114
ref
appTerm
115
ref
appTerm
116
ref
appTerm
117
ref
appTerm
119
ref
appTerm
appTerm
120
remove
appTerm
131
def
absTerm
132
def
appTerm
133
def
absTerm
134
def
appTerm
135
def
absTerm
136
def
appTerm
137
def
absTerm
138
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
138
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
109
remove
nil
55
ref
137
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
136
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
110
remove
nil
55
ref
135
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
134
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
111
remove
nil
55
ref
133
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
132
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
112
remove
nil
55
ref
131
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
126
remove
114
ref
refl
appThm
125
remove
114
remove
appTerm
betaConv
trans
115
ref
refl
appThm
124
remove
115
remove
appTerm
betaConv
trans
116
ref
refl
appThm
123
remove
116
remove
appTerm
betaConv
trans
117
ref
refl
appThm
122
remove
117
remove
appTerm
betaConv
trans
119
ref
refl
appThm
121
remove
119
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
130
remove
appTerm
thm
nil
67
ref
68
remove
70
ref
71
remove
70
ref
"z"
65
ref
var
139
def
70
ref
72
remove
70
ref
73
remove
15
ref
"Hardware.adder3"
"_34790"
65
ref
var
140
def
"_34791"
65
ref
var
141
def
"_34792"
65
ref
var
142
def
"_34793"
65
ref
var
143
def
"_34794"
65
ref
var
144
def
20
ref
"Hardware.xor3"
const
93
ref
constTerm
145
def
140
ref
varTerm
146
def
appTerm
141
ref
varTerm
147
def
appTerm
142
ref
varTerm
148
def
appTerm
143
ref
varTerm
149
def
appTerm
appTerm
"Hardware.majority3"
const
93
ref
constTerm
150
def
146
ref
appTerm
147
ref
appTerm
148
ref
appTerm
144
ref
varTerm
151
def
appTerm
appTerm
152
def
absTerm
153
def
absTerm
154
def
absTerm
155
def
absTerm
156
def
absTerm
157
def
defineConst
158
def
pop
0
ref
65
ref
93
ref
nil
cons
cons
opType
constTerm
159
def
95
ref
appTerm
96
ref
appTerm
139
remove
varTerm
160
def
appTerm
97
ref
appTerm
98
ref
appTerm
appTerm
20
ref
145
remove
95
ref
appTerm
96
ref
appTerm
160
ref
appTerm
97
remove
appTerm
appTerm
150
remove
95
remove
appTerm
96
remove
appTerm
160
remove
appTerm
98
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
161
def
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
140
remove
nil
55
ref
70
ref
141
ref
70
ref
142
ref
70
ref
143
ref
70
ref
144
ref
15
ref
159
remove
146
ref
appTerm
147
ref
appTerm
148
ref
appTerm
149
ref
appTerm
151
ref
appTerm
appTerm
152
remove
appTerm
162
def
absTerm
163
def
appTerm
164
def
absTerm
165
def
appTerm
166
def
absTerm
167
def
appTerm
168
def
absTerm
169
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
ref
169
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
141
remove
nil
55
ref
168
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
ref
167
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
142
remove
nil
55
ref
166
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
ref
165
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
143
remove
nil
55
ref
164
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
ref
163
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
144
remove
nil
55
ref
162
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
158
remove
146
ref
refl
appThm
157
remove
146
remove
appTerm
betaConv
trans
147
ref
refl
appThm
156
remove
147
remove
appTerm
betaConv
trans
148
ref
refl
appThm
155
remove
148
remove
appTerm
betaConv
trans
149
ref
refl
appThm
154
remove
149
remove
appTerm
betaConv
trans
151
ref
refl
appThm
153
remove
151
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
70
ref
161
remove
appTerm
thm
nil
67
ref
"ld"
65
ref
var
170
def
9
ref
"xs"
1
ref
var
171
def
9
ref
"xc"
1
ref
var
172
def
70
ref
"xb"
65
ref
var
173
def
15
ref
"Hardware.SumCarry.shiftRight"
"_34972"
65
ref
var
174
def
"_34973"
1
ref
var
175
def
"_34974"
1
ref
var
176
def
"_34975"
65
ref
var
177
def
"Data.Bool.?"
const
178
def
0
ref
0
ref
"Number.Natural.natural"
typeOp
nil
opType
179
def
3
ref
cons
opType
180
def
3
remove
cons
opType
constTerm
181
def
"r"
179
ref
var
182
def
178
ref
8
remove
constTerm
183
def
"sp"
1
ref
var
184
def
183
ref
"sq"
1
ref
var
185
def
183
ref
"sr"
1
ref
var
186
def
183
ref
"cp"
1
ref
var
187
def
183
ref
"cq"
1
ref
var
188
def
183
ref
"cr"
1
ref
var
189
def
178
remove
69
remove
constTerm
190
def
"xs0"
65
ref
var
191
def
183
ref
"xs1"
1
ref
var
192
def
190
ref
"sq0"
65
ref
var
193
def
183
ref
"sq1"
1
ref
var
194
def
183
ref
"sq2"
1
ref
var
195
def
190
ref
"sq3"
65
ref
var
196
def
183
ref
"cp0"
1
ref
var
197
def
190
ref
"cp1"
65
ref
var
198
def
183
ref
"cq0"
1
ref
var
199
def
190
ref
"cq1"
65
ref
var
200
def
20
ref
13
remove
0
ref
179
ref
180
remove
nil
cons
cons
opType
constTerm
201
def
"Hardware.Bus.width"
const
0
ref
1
ref
179
ref
nil
cons
202
def
cons
opType
constTerm
203
def
175
ref
varTerm
204
def
appTerm
appTerm
"Number.Natural.+"
const
0
ref
179
ref
0
ref
179
ref
202
remove
cons
opType
205
def
nil
cons
cons
opType
constTerm
206
def
182
ref
varTerm
207
def
appTerm
"Number.Natural.bit1"
const
205
ref
constTerm
"Number.Natural.zero"
const
179
ref
constTerm
208
def
appTerm
209
def
appTerm
210
def
appTerm
appTerm
20
ref
201
ref
203
ref
176
ref
varTerm
211
def
appTerm
appTerm
210
ref
appTerm
appTerm
20
ref
201
ref
203
ref
184
ref
varTerm
212
def
appTerm
appTerm
207
ref
appTerm
appTerm
213
def
20
ref
201
ref
203
ref
185
ref
varTerm
214
def
appTerm
appTerm
210
ref
appTerm
appTerm
215
def
20
ref
201
ref
203
ref
186
ref
varTerm
216
def
appTerm
appTerm
207
ref
appTerm
appTerm
217
def
20
ref
201
ref
203
ref
187
ref
varTerm
218
def
appTerm
appTerm
210
ref
appTerm
appTerm
219
def
20
ref
201
ref
203
ref
188
ref
varTerm
220
def
appTerm
appTerm
210
ref
appTerm
appTerm
221
def
20
ref
201
ref
203
ref
189
ref
varTerm
222
def
appTerm
appTerm
210
ref
appTerm
appTerm
223
def
20
ref
"Hardware.Bus.wire"
const
0
ref
1
ref
0
ref
179
ref
78
ref
cons
opType
nil
cons
cons
opType
constTerm
224
def
204
ref
appTerm
208
ref
appTerm
191
ref
varTerm
225
def
appTerm
appTerm
20
ref
"Hardware.Bus.sub"
const
0
ref
1
ref
0
ref
179
ref
0
ref
179
ref
21
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
226
def
204
ref
appTerm
209
ref
appTerm
207
ref
appTerm
192
ref
varTerm
227
def
appTerm
appTerm
20
ref
224
ref
214
ref
appTerm
228
def
208
ref
appTerm
193
ref
varTerm
229
def
appTerm
appTerm
230
def
20
ref
226
ref
214
remove
appTerm
231
def
208
ref
appTerm
207
ref
appTerm
194
ref
varTerm
232
def
appTerm
appTerm
233
def
20
ref
231
remove
209
ref
appTerm
207
ref
appTerm
195
ref
varTerm
234
def
appTerm
appTerm
235
def
20
ref
228
remove
207
ref
appTerm
196
ref
varTerm
236
def
appTerm
appTerm
237
def
20
ref
226
ref
218
ref
appTerm
208
ref
appTerm
207
ref
appTerm
197
ref
varTerm
238
def
appTerm
appTerm
239
def
20
ref
224
ref
218
ref
appTerm
207
ref
appTerm
198
ref
varTerm
240
def
appTerm
appTerm
241
def
20
ref
226
ref
220
ref
appTerm
208
ref
appTerm
207
ref
appTerm
199
ref
varTerm
242
def
appTerm
appTerm
243
def
20
ref
224
ref
220
ref
appTerm
207
ref
appTerm
200
ref
varTerm
244
def
appTerm
appTerm
245
def
20
ref
38
remove
212
ref
appTerm
238
remove
appTerm
232
remove
appTerm
242
remove
appTerm
appTerm
246
def
20
ref
"Hardware.connect"
const
79
remove
constTerm
247
def
240
remove
appTerm
236
remove
appTerm
appTerm
248
def
20
ref
247
ref
"Hardware.ground"
const
65
ref
constTerm
appTerm
244
remove
appTerm
appTerm
249
def
20
ref
"Hardware.case1"
const
93
remove
constTerm
250
def
174
ref
varTerm
251
def
appTerm
225
ref
appTerm
229
ref
appTerm
177
ref
varTerm
252
def
appTerm
appTerm
20
ref
"Hardware.Bus.case1"
const
0
ref
65
ref
36
remove
cons
opType
constTerm
253
def
251
ref
appTerm
254
def
227
ref
appTerm
234
ref
appTerm
216
ref
appTerm
appTerm
20
ref
254
remove
211
ref
appTerm
220
ref
appTerm
222
ref
appTerm
appTerm
20
ref
"Hardware.Bus.delay"
const
22
remove
constTerm
255
def
216
ref
appTerm
212
remove
appTerm
appTerm
255
remove
222
ref
appTerm
218
remove
appTerm
appTerm
256
def
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
257
def
absTerm
258
def
absTerm
259
def
absTerm
260
def
absTerm
261
def
defineConst
262
def
pop
0
ref
65
ref
0
ref
1
ref
0
ref
1
ref
78
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
263
def
170
remove
varTerm
264
def
appTerm
171
remove
varTerm
265
def
appTerm
172
remove
varTerm
266
def
appTerm
173
remove
varTerm
267
def
appTerm
appTerm
181
ref
182
remove
183
ref
184
remove
183
ref
185
remove
183
ref
186
remove
183
ref
187
remove
183
ref
188
remove
183
ref
189
remove
190
ref
191
remove
183
ref
192
remove
190
ref
193
remove
183
ref
194
remove
183
ref
195
remove
190
ref
196
remove
183
ref
197
remove
190
ref
198
remove
183
ref
199
remove
190
ref
200
remove
20
ref
201
ref
203
ref
265
ref
appTerm
appTerm
210
ref
appTerm
appTerm
20
ref
201
ref
203
ref
266
ref
appTerm
appTerm
210
remove
appTerm
appTerm
213
remove
215
remove
217
remove
219
remove
221
remove
223
remove
20
ref
224
ref
265
ref
appTerm
208
ref
appTerm
225
ref
appTerm
appTerm
20
ref
226
ref
265
remove
appTerm
209
ref
appTerm
207
remove
appTerm
227
ref
appTerm
appTerm
230
remove
233
remove
235
remove
237
remove
239
remove
241
remove
243
remove
245
remove
246
remove
248
remove
249
remove
20
ref
250
remove
264
ref
appTerm
225
remove
appTerm
229
remove
appTerm
267
remove
appTerm
appTerm
20
ref
253
remove
264
remove
appTerm
268
def
227
remove
appTerm
234
remove
appTerm
216
remove
appTerm
appTerm
20
ref
268
remove
266
remove
appTerm
220
remove
appTerm
222
remove
appTerm
appTerm
256
remove
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
269
def
nil
cons
cons
nil
cons
nil
cons
cons
100
ref
subst
174
remove
nil
55
ref
9
ref
175
ref
9
ref
176
ref
70
ref
177
ref
15
ref
263
remove
251
ref
appTerm
204
ref
appTerm
211
ref
appTerm
252
ref
appTerm
appTerm
257
remove
appTerm
270
def
absTerm
271
def
appTerm
272
def
absTerm
273
def
appTerm
274
def
absTerm
275
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
275
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
175
remove
nil
55
ref
274
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
273
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
176
remove
nil
55
ref
272
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
67
remove
271
remove
nil
cons
cons
nil
cons
nil
cons
cons
100
remove
subst
177
remove
nil
55
ref
270
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
262
remove
251
ref
refl
appThm
261
remove
251
remove
appTerm
betaConv
trans
204
ref
refl
appThm
260
remove
204
remove
appTerm
betaConv
trans
211
ref
refl
appThm
259
remove
211
remove
appTerm
betaConv
trans
252
ref
refl
appThm
258
remove
252
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
70
remove
269
remove
appTerm
thm
nil
5
ref
"w"
1
ref
var
276
def
9
ref
6
remove
9
ref
10
remove
9
ref
107
remove
9
ref
11
remove
9
ref
12
remove
15
ref
"Hardware.Bus.adder4"
"_34912"
1
ref
var
277
def
"_34913"
1
ref
var
278
def
"_34914"
1
ref
var
279
def
"_34915"
1
ref
var
280
def
"_34916"
1
ref
var
281
def
"_34917"
1
ref
var
282
def
181
ref
"n"
179
remove
var
283
def
183
ref
"p"
1
ref
var
284
def
183
ref
"q"
1
ref
var
285
def
190
ref
"z0"
65
ref
var
286
def
183
ref
"z1"
1
ref
var
287
def
190
ref
"s0"
65
ref
var
288
def
183
ref
"s1"
1
ref
var
289
def
190
ref
"s2"
65
ref
var
290
def
190
ref
"c0"
65
ref
var
291
def
183
ref
"c1"
1
ref
var
292
def
190
ref
"p0"
65
ref
var
293
def
183
ref
"p1"
1
ref
var
294
def
183
ref
"q1"
1
ref
var
295
def
190
ref
"q2"
65
remove
var
296
def
20
ref
201
ref
203
ref
277
ref
varTerm
297
def
appTerm
appTerm
206
remove
283
ref
varTerm
298
def
appTerm
299
def
209
ref
appTerm
300
def
appTerm
appTerm
20
ref
201
ref
203
ref
278
ref
varTerm
301
def
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
279
ref
varTerm
302
def
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
280
ref
varTerm
303
def
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
281
ref
varTerm
304
def
appTerm
appTerm
299
remove
"Number.Natural.bit0"
const
205
remove
constTerm
209
ref
appTerm
appTerm
305
def
appTerm
appTerm
20
ref
201
ref
203
ref
282
ref
varTerm
306
def
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
284
ref
varTerm
307
def
appTerm
appTerm
300
ref
appTerm
appTerm
308
def
20
ref
201
ref
203
ref
285
ref
varTerm
309
def
appTerm
appTerm
300
ref
appTerm
appTerm
310
def
20
ref
224
ref
303
ref
appTerm
208
ref
appTerm
286
ref
varTerm
311
def
appTerm
appTerm
20
ref
226
ref
303
ref
appTerm
209
ref
appTerm
298
ref
appTerm
287
ref
varTerm
312
def
appTerm
appTerm
20
ref
224
ref
304
ref
appTerm
313
def
208
ref
appTerm
288
ref
varTerm
314
def
appTerm
appTerm
20
ref
226
ref
304
ref
appTerm
209
ref
appTerm
298
ref
appTerm
289
ref
varTerm
315
def
appTerm
appTerm
20
ref
313
remove
300
ref
appTerm
290
ref
varTerm
316
def
appTerm
appTerm
20
ref
224
ref
306
ref
appTerm
208
ref
appTerm
291
ref
varTerm
317
def
appTerm
appTerm
20
ref
226
ref
306
ref
appTerm
209
ref
appTerm
298
ref
appTerm
292
ref
varTerm
318
def
appTerm
appTerm
20
ref
224
ref
307
ref
appTerm
208
ref
appTerm
293
ref
varTerm
319
def
appTerm
appTerm
320
def
20
ref
226
ref
307
ref
appTerm
209
ref
appTerm
298
ref
appTerm
294
ref
varTerm
321
def
appTerm
appTerm
322
def
20
ref
226
ref
309
ref
appTerm
208
ref
appTerm
298
ref
appTerm
295
ref
varTerm
323
def
appTerm
appTerm
324
def
20
ref
224
ref
309
ref
appTerm
298
ref
appTerm
296
ref
varTerm
325
def
appTerm
appTerm
326
def
20
ref
128
ref
297
ref
appTerm
301
ref
appTerm
302
ref
appTerm
307
ref
appTerm
309
ref
appTerm
appTerm
20
ref
94
remove
319
remove
appTerm
311
ref
appTerm
314
ref
appTerm
317
ref
appTerm
appTerm
20
ref
128
ref
321
remove
appTerm
323
remove
appTerm
312
ref
appTerm
315
ref
appTerm
318
ref
appTerm
appTerm
247
remove
325
remove
appTerm
316
ref
appTerm
appTerm
appTerm
327
def
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
328
def
absTerm
329
def
absTerm
330
def
absTerm
331
def
absTerm
332
def
absTerm
333
def
absTerm
334
def
defineConst
335
def
pop
0
remove
1
remove
127
remove
nil
cons
cons
opType
constTerm
336
def
276
remove
varTerm
337
def
appTerm
39
ref
appTerm
40
ref
appTerm
129
ref
appTerm
41
ref
appTerm
42
ref
appTerm
appTerm
181
remove
283
remove
183
ref
284
remove
183
ref
285
remove
190
ref
286
remove
183
ref
287
remove
190
ref
288
remove
183
ref
289
remove
190
ref
290
remove
190
ref
291
remove
183
ref
292
remove
190
ref
293
remove
183
ref
294
remove
183
remove
295
remove
190
remove
296
remove
20
ref
201
ref
203
ref
337
ref
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
39
ref
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
40
ref
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
129
ref
appTerm
appTerm
300
ref
appTerm
appTerm
20
ref
201
ref
203
ref
41
ref
appTerm
appTerm
305
remove
appTerm
appTerm
20
ref
201
remove
203
remove
42
ref
appTerm
appTerm
300
ref
appTerm
appTerm
308
remove
310
remove
20
ref
224
ref
129
ref
appTerm
208
ref
appTerm
311
remove
appTerm
appTerm
20
ref
226
ref
129
remove
appTerm
209
ref
appTerm
298
ref
appTerm
312
remove
appTerm
appTerm
20
ref
224
ref
41
ref
appTerm
338
def
208
ref
appTerm
314
remove
appTerm
appTerm
20
ref
226
ref
41
remove
appTerm
209
ref
appTerm
298
ref
appTerm
315
remove
appTerm
appTerm
20
ref
338
remove
300
remove
appTerm
316
remove
appTerm
appTerm
20
ref
224
remove
42
ref
appTerm
208
remove
appTerm
317
remove
appTerm
appTerm
20
ref
226
remove
42
remove
appTerm
209
remove
appTerm
298
remove
appTerm
318
remove
appTerm
appTerm
320
remove
322
remove
324
remove
326
remove
20
remove
128
remove
337
remove
appTerm
39
remove
appTerm
40
remove
appTerm
307
remove
appTerm
309
remove
appTerm
appTerm
327
remove
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
339
def
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
277
remove
nil
55
ref
9
ref
278
ref
9
ref
279
ref
9
ref
280
ref
9
ref
281
ref
9
ref
282
ref
15
remove
336
remove
297
ref
appTerm
301
ref
appTerm
302
ref
appTerm
303
ref
appTerm
304
ref
appTerm
306
ref
appTerm
appTerm
328
remove
appTerm
340
def
absTerm
341
def
appTerm
342
def
absTerm
343
def
appTerm
344
def
absTerm
345
def
appTerm
346
def
absTerm
347
def
appTerm
348
def
absTerm
349
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
349
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
278
remove
nil
55
ref
348
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
347
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
279
remove
nil
55
ref
346
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
345
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
280
remove
nil
55
ref
344
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
ref
343
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
281
remove
nil
55
ref
342
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
5
remove
341
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
remove
subst
282
remove
nil
55
remove
340
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
remove
subst
335
remove
297
ref
refl
appThm
334
remove
297
remove
appTerm
betaConv
trans
301
ref
refl
appThm
333
remove
301
remove
appTerm
betaConv
trans
302
ref
refl
appThm
332
remove
302
remove
appTerm
betaConv
trans
303
ref
refl
appThm
331
remove
303
remove
appTerm
betaConv
trans
304
ref
refl
appThm
330
remove
304
remove
appTerm
betaConv
trans
306
ref
refl
appThm
329
remove
306
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
remove
339
remove
appTerm
thm