6
version
nil
"P"
"->"
typeOp
0
def
"Hardware.wire"
"Hardware.wire"
"Hardware.signals"
nil
"A"
"Data.Stream.stream"
typeOp
"bool"
typeOp
nil
opType
1
def
nil
cons
2
def
opType
3
def
nil
cons
4
def
cons
nil
cons
nil
nil
cons
5
def
cons
6
def
nil
"="
const
7
def
0
ref
0
ref
0
ref
"A"
varType
8
def
2
ref
cons
opType
9
def
2
ref
cons
opType
10
def
0
ref
10
ref
2
ref
cons
opType
nil
cons
cons
opType
constTerm
11
def
"Data.Bool.?"
const
10
ref
constTerm
12
def
appTerm
"p"
9
ref
var
13
def
13
ref
varTerm
14
def
"select"
const
15
def
0
ref
9
ref
8
ref
nil
cons
cons
opType
constTerm
14
ref
appTerm
appTerm
absTerm
appTerm
axiom
16
def
subst
"x"
3
ref
var
"Data.Bool.T"
const
1
ref
constTerm
17
def
absTerm
18
def
refl
appThm
"p"
0
ref
3
ref
2
ref
cons
opType
19
def
var
20
def
20
remove
varTerm
21
def
15
ref
0
ref
19
ref
4
ref
cons
opType
constTerm
21
remove
appTerm
appTerm
absTerm
18
ref
appTerm
betaConv
trans
6
ref
"t"
1
ref
var
22
def
7
ref
0
ref
1
ref
0
ref
1
ref
2
ref
cons
opType
23
def
nil
cons
cons
opType
24
def
constTerm
25
def
12
remove
"x"
8
remove
var
26
def
22
ref
varTerm
27
def
absTerm
appTerm
appTerm
27
ref
appTerm
absTerm
28
def
17
ref
appTerm
29
def
betaConv
nil
"Data.Bool.!"
const
30
def
0
ref
23
ref
2
ref
cons
opType
31
def
constTerm
32
def
28
ref
appTerm
33
def
axiom
nil
"p"
1
ref
var
34
def
33
remove
nil
cons
cons
"q"
1
ref
var
35
def
29
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
25
ref
"Data.Bool.==>"
const
24
ref
constTerm
36
def
34
ref
varTerm
37
def
appTerm
35
ref
varTerm
38
def
appTerm
39
def
appTerm
refl
34
ref
35
ref
25
ref
"Data.Bool./\\"
const
24
ref
constTerm
40
def
37
ref
appTerm
41
def
38
ref
appTerm
42
def
appTerm
43
def
37
ref
appTerm
absTerm
44
def
absTerm
45
def
37
ref
appTerm
betaConv
38
ref
refl
46
def
appThm
44
remove
38
ref
appTerm
betaConv
trans
appThm
nil
7
ref
0
ref
24
ref
0
ref
24
ref
2
ref
cons
opType
47
def
nil
cons
cons
opType
constTerm
48
def
36
remove
appTerm
45
remove
appTerm
axiom
37
ref
refl
49
def
appThm
46
ref
appThm
eqMp
50
def
sym
51
def
43
remove
refl
35
ref
7
ref
0
ref
47
ref
0
ref
47
remove
2
ref
cons
opType
nil
cons
cons
opType
constTerm
52
def
"f"
24
remove
var
53
def
53
ref
varTerm
54
def
37
ref
appTerm
38
ref
appTerm
absTerm
55
def
appTerm
53
ref
54
ref
17
ref
appTerm
17
ref
appTerm
absTerm
56
def
appTerm
absTerm
57
def
38
ref
appTerm
betaConv
appThm
7
ref
0
ref
23
ref
31
remove
nil
cons
cons
opType
constTerm
58
def
41
remove
appTerm
refl
34
ref
57
remove
absTerm
59
def
37
ref
appTerm
betaConv
appThm
nil
48
remove
40
ref
appTerm
59
ref
appTerm
axiom
60
def
49
remove
appThm
eqMp
46
ref
appThm
eqMp
61
def
sym
53
ref
54
ref
refl
nil
22
ref
37
ref
nil
cons
62
def
cons
nil
cons
nil
cons
cons
25
ref
27
ref
appTerm
17
ref
appTerm
assume
sym
nil
17
ref
axiom
63
def
eqMp
27
ref
assume
63
ref
deductAntisym
deductAntisym
64
def
subst
37
ref
assume
65
def
eqMp
appThm
nil
22
ref
38
ref
nil
cons
66
def
cons
nil
cons
nil
cons
cons
64
ref
subst
38
ref
assume
eqMp
appThm
absThm
eqMp
67
def
nil
"P"
1
ref
var
68
def
62
remove
cons
"Q"
1
ref
var
69
def
66
remove
cons
nil
cons
cons
nil
cons
cons
25
ref
refl
70
def
53
ref
54
remove
68
ref
varTerm
71
def
appTerm
72
def
69
ref
varTerm
73
def
appTerm
absTerm
74
def
34
ref
35
ref
37
ref
absTerm
absTerm
75
def
appTerm
betaConv
75
ref
71
ref
appTerm
betaConv
73
ref
refl
76
def
appThm
35
ref
71
ref
absTerm
73
ref
appTerm
betaConv
trans
trans
appThm
56
ref
75
ref
appTerm
betaConv
75
ref
17
ref
appTerm
betaConv
17
ref
refl
77
def
appThm
35
ref
17
ref
absTerm
17
ref
appTerm
betaConv
trans
trans
appThm
25
ref
40
ref
71
ref
appTerm
78
def
73
ref
appTerm
79
def
appTerm
refl
35
ref
52
remove
53
remove
72
remove
38
ref
appTerm
absTerm
appTerm
56
ref
appTerm
absTerm
73
ref
appTerm
betaConv
appThm
58
remove
78
remove
appTerm
refl
59
remove
71
ref
appTerm
betaConv
appThm
60
remove
71
ref
refl
appThm
eqMp
76
ref
appThm
eqMp
79
remove
assume
eqMp
80
def
75
remove
refl
appThm
eqMp
sym
63
ref
eqMp
81
def
subst
deductAntisym
eqMp
50
remove
39
remove
assume
eqMp
sym
65
remove
eqMp
70
ref
55
remove
34
ref
35
ref
38
ref
absTerm
82
def
absTerm
83
def
appTerm
betaConv
83
ref
37
remove
appTerm
betaConv
46
remove
appThm
82
ref
38
remove
appTerm
betaConv
trans
trans
appThm
56
remove
83
ref
appTerm
betaConv
83
ref
17
ref
appTerm
betaConv
77
remove
appThm
82
ref
17
ref
appTerm
betaConv
trans
trans
84
def
appThm
61
remove
42
remove
assume
eqMp
83
ref
refl
85
def
appThm
eqMp
sym
63
ref
eqMp
86
def
proveHyp
deductAntisym
87
def
subst
proveHyp
"A"
2
ref
cons
nil
cons
88
def
"P"
23
remove
var
89
def
28
remove
nil
cons
cons
"x"
1
ref
var
90
def
17
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
34
ref
30
ref
10
ref
constTerm
91
def
"P"
9
ref
var
varTerm
92
def
appTerm
93
def
nil
cons
94
def
cons
35
ref
92
ref
26
ref
varTerm
95
def
appTerm
96
def
nil
cons
97
def
cons
nil
cons
cons
nil
cons
cons
98
def
51
remove
subst
98
remove
86
remove
67
remove
deductAntisym
99
def
subst
25
ref
96
remove
appTerm
refl
26
remove
17
ref
absTerm
100
def
95
ref
appTerm
betaConv
appThm
13
remove
7
ref
0
ref
9
remove
10
remove
nil
cons
cons
opType
constTerm
14
remove
appTerm
100
remove
appTerm
absTerm
101
def
92
ref
appTerm
betaConv
102
def
nil
11
remove
91
remove
appTerm
101
remove
appTerm
axiom
92
remove
refl
appThm
103
def
93
ref
assume
eqMp
eqMp
95
remove
refl
appThm
eqMp
sym
63
ref
eqMp
eqMp
nil
68
ref
94
remove
cons
69
ref
97
remove
cons
nil
cons
cons
nil
cons
cons
81
remove
subst
deductAntisym
eqMp
104
def
subst
eqMp
eqMp
sym
63
ref
eqMp
105
def
subst
eqMp
defineTypeOp
106
def
pop
107
def
pop
108
def
pop
109
def
pop
nil
opType
110
def
2
ref
cons
opType
111
def
var
112
def
"a"
110
ref
var
113
def
7
ref
0
ref
110
ref
111
ref
nil
cons
cons
opType
constTerm
114
def
109
remove
0
ref
3
ref
110
ref
nil
cons
115
def
cons
opType
constTerm
116
def
108
remove
0
ref
110
ref
4
ref
cons
opType
constTerm
117
def
113
ref
varTerm
118
def
appTerm
appTerm
119
def
appTerm
118
ref
appTerm
120
def
absTerm
121
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
115
ref
cons
nil
cons
5
ref
cons
25
ref
93
remove
appTerm
refl
102
remove
appThm
103
remove
eqMp
sym
122
def
subst
123
def
subst
113
ref
nil
22
ref
120
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
114
ref
refl
113
ref
119
remove
absTerm
118
ref
appTerm
betaConv
appThm
113
remove
118
ref
absTerm
118
ref
appTerm
betaConv
appThm
107
remove
118
remove
refl
appThm
eqMp
eqMp
absThm
eqMp
124
def
nil
30
ref
0
ref
111
ref
2
ref
cons
opType
constTerm
125
def
"w"
110
ref
var
126
def
114
ref
116
ref
117
ref
126
ref
varTerm
127
def
appTerm
128
def
appTerm
appTerm
127
ref
appTerm
absTerm
appTerm
129
def
thm
40
ref
125
ref
121
remove
appTerm
130
def
appTerm
refl
30
ref
0
ref
19
ref
2
ref
cons
opType
constTerm
131
def
refl
"r"
3
ref
var
132
def
nil
22
ref
7
ref
0
ref
3
ref
19
ref
nil
cons
cons
opType
constTerm
133
def
117
ref
116
ref
132
ref
varTerm
134
def
appTerm
appTerm
appTerm
134
ref
appTerm
135
def
nil
cons
cons
nil
cons
nil
cons
cons
22
ref
25
ref
25
ref
17
ref
appTerm
136
def
27
ref
appTerm
appTerm
27
ref
appTerm
absTerm
137
def
27
ref
appTerm
138
def
betaConv
nil
32
remove
137
ref
appTerm
139
def
axiom
nil
34
ref
139
remove
nil
cons
cons
35
ref
138
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
87
remove
subst
proveHyp
88
remove
89
remove
137
remove
nil
cons
cons
90
remove
27
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
104
remove
subst
eqMp
eqMp
140
def
subst
absThm
appThm
appThm
124
remove
nil
34
ref
130
remove
nil
cons
cons
35
ref
131
ref
132
ref
136
ref
135
ref
appTerm
141
def
absTerm
142
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
99
ref
subst
proveHyp
nil
"P"
19
remove
var
142
remove
nil
cons
cons
nil
cons
nil
cons
cons
6
remove
122
ref
subst
subst
132
ref
nil
22
ref
141
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
70
ref
18
remove
134
ref
appTerm
143
def
betaConv
appThm
135
ref
refl
appThm
70
ref
132
ref
135
remove
absTerm
134
ref
appTerm
betaConv
appThm
132
remove
143
remove
absTerm
134
ref
appTerm
betaConv
appThm
106
remove
134
remove
refl
appThm
eqMp
sym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
68
ref
129
remove
nil
cons
cons
69
ref
131
remove
"s"
3
ref
var
144
def
133
remove
117
ref
116
ref
144
remove
varTerm
145
def
appTerm
appTerm
appTerm
145
remove
appTerm
absTerm
appTerm
146
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
70
ref
74
remove
83
ref
appTerm
betaConv
83
remove
71
remove
appTerm
betaConv
76
remove
appThm
82
remove
73
remove
appTerm
betaConv
trans
trans
appThm
84
remove
appThm
80
remove
85
remove
appThm
eqMp
sym
63
remove
eqMp
147
def
subst
proveHyp
nil
146
remove
thm
nil
112
ref
126
ref
7
ref
0
ref
0
ref
"Number.Natural.natural"
typeOp
nil
opType
148
def
2
ref
cons
opType
149
def
0
ref
149
ref
2
ref
cons
opType
150
def
nil
cons
cons
opType
constTerm
151
def
"Hardware.signal"
"_33507"
110
ref
var
152
def
"Data.Stream.nth"
const
0
ref
3
remove
149
ref
nil
cons
153
def
cons
opType
constTerm
154
def
117
remove
152
ref
varTerm
155
def
appTerm
appTerm
156
def
absTerm
157
def
defineConst
158
def
pop
0
ref
110
ref
153
ref
cons
opType
constTerm
159
def
127
ref
appTerm
160
def
appTerm
154
remove
128
remove
appTerm
appTerm
absTerm
161
def
nil
cons
cons
nil
cons
nil
cons
cons
123
ref
subst
152
remove
nil
22
ref
151
remove
159
remove
155
ref
appTerm
appTerm
156
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
158
remove
155
ref
refl
appThm
157
remove
155
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
125
ref
161
remove
appTerm
thm
"Hardware.ground"
116
ref
"Data.Stream.replicate"
const
0
ref
1
ref
4
remove
cons
opType
constTerm
162
def
"Data.Bool.F"
const
1
remove
constTerm
appTerm
appTerm
163
def
defineConst
164
def
pop
165
def
pop
164
remove
nil
114
ref
165
remove
110
ref
constTerm
166
def
appTerm
163
remove
appTerm
thm
"Hardware.power"
116
remove
162
remove
17
ref
appTerm
appTerm
167
def
defineConst
168
def
pop
169
def
pop
168
remove
nil
114
remove
169
remove
110
ref
constTerm
170
def
appTerm
167
remove
appTerm
thm
nil
"P"
0
ref
"Hardware.bus"
"Hardware.bus"
"Hardware.Bus.wires"
nil
"A"
"Data.List.list"
typeOp
171
def
115
remove
opType
172
def
nil
cons
173
def
cons
nil
cons
5
ref
cons
174
def
16
remove
subst
"x"
172
ref
var
17
remove
absTerm
175
def
refl
appThm
"p"
0
ref
172
ref
2
ref
cons
opType
176
def
var
177
def
177
remove
varTerm
178
def
15
remove
0
ref
176
ref
173
ref
cons
opType
constTerm
178
remove
appTerm
appTerm
absTerm
175
ref
appTerm
betaConv
trans
174
ref
105
remove
subst
eqMp
defineTypeOp
179
def
pop
180
def
pop
181
def
pop
182
def
pop
nil
opType
183
def
2
ref
cons
opType
184
def
var
185
def
"a"
183
ref
var
186
def
7
ref
0
ref
183
ref
184
ref
nil
cons
187
def
cons
opType
constTerm
188
def
182
remove
0
ref
172
ref
183
ref
nil
cons
189
def
cons
opType
constTerm
190
def
181
remove
0
ref
183
ref
173
ref
cons
opType
constTerm
191
def
186
ref
varTerm
192
def
appTerm
appTerm
193
def
appTerm
192
ref
appTerm
194
def
absTerm
195
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
189
ref
cons
nil
cons
5
ref
cons
122
ref
subst
196
def
subst
186
ref
nil
22
ref
194
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
188
ref
refl
186
ref
193
remove
absTerm
192
ref
appTerm
betaConv
appThm
186
remove
192
ref
absTerm
192
ref
appTerm
betaConv
appThm
180
remove
192
remove
refl
appThm
eqMp
eqMp
absThm
eqMp
197
def
nil
30
ref
0
ref
184
remove
2
ref
cons
opType
constTerm
198
def
"x"
183
ref
var
199
def
188
ref
190
ref
191
ref
199
ref
varTerm
200
def
appTerm
201
def
appTerm
appTerm
200
ref
appTerm
absTerm
appTerm
202
def
thm
40
ref
198
ref
195
remove
appTerm
203
def
appTerm
refl
30
ref
0
ref
176
ref
2
ref
cons
opType
constTerm
204
def
refl
"r"
172
ref
var
205
def
nil
22
ref
7
ref
0
ref
172
ref
176
ref
nil
cons
cons
opType
constTerm
206
def
191
ref
190
ref
205
ref
varTerm
207
def
appTerm
appTerm
appTerm
207
ref
appTerm
208
def
nil
cons
cons
nil
cons
nil
cons
cons
140
remove
subst
absThm
appThm
appThm
197
remove
nil
34
remove
203
remove
nil
cons
cons
35
remove
204
ref
205
ref
136
remove
208
ref
appTerm
209
def
absTerm
210
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
99
remove
subst
proveHyp
nil
"P"
176
remove
var
210
remove
nil
cons
cons
nil
cons
nil
cons
cons
174
remove
122
ref
subst
subst
205
ref
nil
22
ref
209
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
70
ref
175
remove
207
ref
appTerm
211
def
betaConv
appThm
208
ref
refl
appThm
70
remove
205
ref
208
remove
absTerm
207
ref
appTerm
betaConv
appThm
205
remove
211
remove
absTerm
207
ref
appTerm
betaConv
appThm
179
remove
207
remove
refl
appThm
eqMp
sym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
68
remove
202
remove
nil
cons
cons
69
remove
204
remove
"l"
172
ref
var
212
def
206
remove
191
ref
190
ref
212
remove
varTerm
213
def
appTerm
appTerm
appTerm
213
remove
appTerm
absTerm
appTerm
214
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
147
remove
subst
proveHyp
nil
214
remove
thm
"Hardware.Bus.nil"
190
ref
"Data.List.[]"
const
172
ref
constTerm
215
def
appTerm
216
def
defineConst
217
def
pop
218
def
pop
217
remove
nil
188
ref
218
remove
183
ref
constTerm
appTerm
216
remove
appTerm
thm
nil
112
remove
126
ref
188
ref
"Hardware.Bus.single"
"_33512"
110
ref
var
219
def
190
ref
"Data.List.::"
const
0
ref
110
ref
0
ref
172
ref
173
ref
cons
opType
nil
cons
220
def
cons
opType
constTerm
221
def
219
ref
varTerm
222
def
appTerm
215
ref
appTerm
appTerm
223
def
absTerm
224
def
defineConst
225
def
pop
0
ref
110
ref
189
ref
cons
opType
constTerm
226
def
127
ref
appTerm
appTerm
190
ref
221
remove
127
remove
appTerm
215
remove
appTerm
appTerm
appTerm
absTerm
227
def
nil
cons
cons
nil
cons
nil
cons
cons
123
remove
subst
219
remove
nil
22
ref
188
ref
226
remove
222
ref
appTerm
appTerm
223
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
225
remove
222
ref
refl
appThm
224
remove
222
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
125
remove
227
remove
appTerm
thm
nil
185
ref
199
ref
198
ref
"y"
183
ref
var
228
def
188
ref
"Hardware.Bus.append"
"_33517"
183
ref
var
229
def
"_33518"
183
ref
var
230
def
190
ref
"Data.List.@"
const
0
ref
172
ref
220
ref
cons
opType
constTerm
231
def
191
ref
229
ref
varTerm
232
def
appTerm
appTerm
191
ref
230
ref
varTerm
233
def
appTerm
appTerm
appTerm
234
def
absTerm
235
def
absTerm
236
def
defineConst
237
def
pop
0
ref
183
ref
0
ref
183
ref
189
ref
cons
opType
nil
cons
cons
opType
constTerm
238
def
200
ref
appTerm
228
ref
varTerm
239
def
appTerm
appTerm
190
ref
231
remove
201
ref
appTerm
191
ref
239
ref
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
240
def
nil
cons
cons
nil
cons
nil
cons
cons
196
ref
subst
229
remove
nil
22
ref
198
ref
230
ref
188
ref
238
remove
232
ref
appTerm
233
ref
appTerm
appTerm
234
remove
appTerm
241
def
absTerm
242
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
185
ref
242
remove
nil
cons
cons
nil
cons
nil
cons
cons
196
ref
subst
230
remove
nil
22
ref
241
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
237
remove
232
ref
refl
appThm
236
remove
232
remove
appTerm
betaConv
trans
233
ref
refl
appThm
235
remove
233
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
198
ref
240
remove
appTerm
thm
nil
185
ref
199
ref
7
ref
0
ref
148
ref
153
remove
cons
opType
243
def
constTerm
244
def
"Hardware.Bus.width"
"_33529"
183
ref
var
245
def
"Data.List.length"
const
0
ref
172
ref
148
ref
nil
cons
246
def
cons
opType
constTerm
247
def
191
ref
245
ref
varTerm
248
def
appTerm
appTerm
249
def
absTerm
250
def
defineConst
251
def
pop
0
ref
183
ref
246
ref
cons
opType
constTerm
252
def
200
ref
appTerm
253
def
appTerm
247
remove
201
ref
appTerm
appTerm
absTerm
254
def
nil
cons
cons
nil
cons
nil
cons
cons
196
ref
subst
245
remove
nil
22
ref
244
remove
252
ref
248
ref
appTerm
appTerm
249
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
251
remove
248
ref
refl
appThm
250
remove
248
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
198
ref
254
remove
appTerm
thm
nil
185
ref
199
ref
30
remove
150
remove
constTerm
255
def
"t"
148
ref
var
256
def
7
remove
0
ref
171
remove
2
ref
opType
257
def
0
ref
257
ref
2
remove
cons
opType
nil
cons
cons
opType
constTerm
258
def
"Hardware.Bus.signal"
"_33534"
183
ref
var
259
def
"_33535"
148
ref
var
260
def
"Data.List.map"
const
0
ref
111
remove
0
ref
172
remove
257
remove
nil
cons
261
def
cons
opType
nil
cons
cons
opType
constTerm
262
def
126
ref
160
ref
260
ref
varTerm
263
def
appTerm
absTerm
appTerm
191
ref
259
ref
varTerm
264
def
appTerm
appTerm
265
def
absTerm
266
def
absTerm
267
def
defineConst
268
def
pop
0
ref
183
ref
0
ref
148
ref
261
remove
cons
opType
nil
cons
cons
opType
constTerm
269
def
200
ref
appTerm
256
remove
varTerm
270
def
appTerm
appTerm
262
remove
126
remove
160
remove
270
remove
appTerm
absTerm
appTerm
201
ref
appTerm
appTerm
absTerm
appTerm
absTerm
271
def
nil
cons
cons
nil
cons
nil
cons
cons
196
ref
subst
259
remove
nil
22
ref
255
ref
260
ref
258
remove
269
remove
264
ref
appTerm
263
ref
appTerm
appTerm
265
remove
appTerm
272
def
absTerm
273
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
"P"
149
remove
var
274
def
273
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
246
ref
cons
nil
cons
5
remove
cons
122
remove
subst
275
def
subst
260
remove
nil
22
ref
272
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
268
remove
264
ref
refl
appThm
267
remove
264
remove
appTerm
betaConv
trans
263
ref
refl
appThm
266
remove
263
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
198
ref
271
remove
appTerm
thm
nil
185
ref
199
remove
255
ref
"k"
148
ref
var
276
def
255
ref
"n"
148
ref
var
277
def
198
ref
228
remove
25
ref
"Hardware.Bus.sub"
"_33546"
183
ref
var
278
def
"_33547"
148
ref
var
279
def
"_33548"
148
ref
var
280
def
"_33549"
183
ref
var
281
def
40
ref
"Number.Natural.<="
const
243
remove
constTerm
282
def
"Number.Natural.+"
const
0
ref
148
ref
0
ref
148
ref
246
remove
cons
opType
nil
cons
cons
opType
constTerm
283
def
279
ref
varTerm
284
def
appTerm
280
ref
varTerm
285
def
appTerm
appTerm
252
remove
278
ref
varTerm
286
def
appTerm
appTerm
appTerm
188
ref
281
ref
varTerm
287
def
appTerm
190
ref
"Data.List.take"
const
0
ref
148
ref
220
remove
cons
opType
288
def
constTerm
289
def
285
ref
appTerm
"Data.List.drop"
const
288
remove
constTerm
290
def
284
ref
appTerm
191
remove
286
ref
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
291
def
absTerm
292
def
absTerm
293
def
absTerm
294
def
absTerm
295
def
defineConst
296
def
pop
0
ref
183
remove
0
ref
148
ref
0
ref
148
ref
187
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
297
def
200
remove
appTerm
276
remove
varTerm
298
def
appTerm
277
ref
varTerm
299
def
appTerm
239
ref
appTerm
appTerm
40
remove
282
remove
283
remove
298
ref
appTerm
299
ref
appTerm
appTerm
253
remove
appTerm
appTerm
188
ref
239
remove
appTerm
190
ref
289
remove
299
ref
appTerm
290
remove
298
remove
appTerm
201
remove
appTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
300
def
nil
cons
cons
nil
cons
nil
cons
cons
196
ref
subst
278
remove
nil
22
ref
255
ref
279
ref
255
ref
280
ref
198
ref
281
ref
25
remove
297
remove
286
ref
appTerm
284
ref
appTerm
285
ref
appTerm
287
ref
appTerm
appTerm
291
remove
appTerm
301
def
absTerm
302
def
appTerm
303
def
absTerm
304
def
appTerm
305
def
absTerm
306
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
274
ref
306
remove
nil
cons
cons
nil
cons
nil
cons
cons
275
ref
subst
279
remove
nil
22
ref
305
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
274
ref
304
remove
nil
cons
cons
nil
cons
nil
cons
cons
275
ref
subst
280
remove
nil
22
ref
303
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
nil
185
remove
302
remove
nil
cons
cons
nil
cons
nil
cons
cons
196
remove
subst
281
remove
nil
22
ref
301
remove
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
296
remove
286
ref
refl
appThm
295
remove
286
remove
appTerm
betaConv
trans
284
ref
refl
appThm
294
remove
284
remove
appTerm
betaConv
trans
285
ref
refl
appThm
293
remove
285
remove
appTerm
betaConv
trans
287
ref
refl
appThm
292
remove
287
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
198
remove
300
remove
appTerm
thm
nil
274
ref
277
ref
188
ref
"Hardware.Bus.ground"
"_33578"
148
ref
var
307
def
190
ref
"Data.List.replicate"
const
0
ref
110
remove
0
ref
148
ref
173
remove
cons
opType
nil
cons
cons
opType
constTerm
308
def
166
remove
appTerm
309
def
307
ref
varTerm
310
def
appTerm
appTerm
311
def
absTerm
312
def
defineConst
313
def
pop
0
remove
148
ref
189
remove
cons
opType
314
def
constTerm
315
def
299
ref
appTerm
appTerm
190
ref
309
remove
299
ref
appTerm
appTerm
appTerm
absTerm
316
def
nil
cons
cons
nil
cons
nil
cons
cons
275
ref
subst
307
remove
nil
22
ref
188
ref
315
remove
310
ref
appTerm
appTerm
311
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
ref
subst
313
remove
310
ref
refl
appThm
312
remove
310
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
255
ref
316
remove
appTerm
thm
nil
274
remove
277
remove
188
ref
"Hardware.Bus.power"
"_33583"
148
remove
var
317
def
190
ref
308
remove
170
remove
appTerm
318
def
317
ref
varTerm
319
def
appTerm
appTerm
320
def
absTerm
321
def
defineConst
322
def
pop
314
remove
constTerm
323
def
299
ref
appTerm
appTerm
190
remove
318
remove
299
remove
appTerm
appTerm
appTerm
absTerm
324
def
nil
cons
cons
nil
cons
nil
cons
cons
275
remove
subst
317
remove
nil
22
remove
188
remove
323
remove
319
ref
appTerm
appTerm
320
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
64
remove
subst
322
remove
319
ref
refl
appThm
321
remove
319
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
255
remove
324
remove
appTerm
thm