6
version
"Data.Bool.!"
const
0
def
"->"
typeOp
1
def
1
ref
"bool"
typeOp
nil
opType
2
def
2
ref
nil
cons
3
def
cons
opType
4
def
3
ref
cons
opType
5
def
constTerm
6
def
refl
7
def
"q"
2
ref
var
8
def
"="
const
9
def
1
ref
2
ref
4
ref
nil
cons
cons
opType
10
def
constTerm
11
def
refl
12
def
nil
"l"
"Data.List.list"
typeOp
13
def
3
ref
opType
14
def
var
15
def
"Data.List.[]"
const
16
def
14
ref
constTerm
17
def
nil
cons
cons
nil
cons
nil
cons
cons
15
ref
11
ref
"Data.Word.Bits.compare"
"word_bits_lte"
1
ref
2
ref
1
ref
14
ref
1
ref
14
ref
3
ref
cons
opType
18
def
nil
cons
19
def
cons
opType
20
def
nil
cons
cons
opType
21
def
var
22
def
nil
cons
cons
nil
cons
22
ref
"Data.Bool./\\"
const
10
ref
constTerm
23
def
6
ref
8
ref
0
ref
1
ref
18
ref
3
ref
cons
opType
24
def
constTerm
25
def
15
ref
11
ref
22
ref
varTerm
26
def
8
ref
varTerm
27
def
appTerm
28
def
17
ref
appTerm
15
ref
varTerm
29
def
appTerm
appTerm
27
ref
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
6
ref
8
ref
6
ref
"h"
2
ref
var
30
def
25
ref
"t"
14
ref
var
31
def
25
ref
15
ref
11
ref
28
remove
"Data.List.::"
const
32
def
1
ref
2
ref
1
ref
14
ref
14
ref
nil
cons
33
def
cons
opType
34
def
nil
cons
35
def
cons
opType
constTerm
36
def
30
ref
varTerm
37
def
appTerm
31
ref
varTerm
38
def
appTerm
39
def
appTerm
29
ref
appTerm
appTerm
26
ref
"Data.Bool.\\/"
const
10
ref
constTerm
40
def
23
ref
"Data.Bool.~"
const
4
ref
constTerm
41
def
37
ref
appTerm
appTerm
"Data.List.head"
const
42
def
18
ref
constTerm
29
ref
appTerm
43
def
appTerm
appTerm
23
ref
41
ref
23
ref
37
ref
appTerm
41
ref
43
remove
appTerm
appTerm
appTerm
appTerm
27
ref
appTerm
appTerm
44
def
appTerm
38
ref
appTerm
"Data.List.tail"
const
45
def
34
remove
constTerm
29
ref
appTerm
46
def
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
47
def
refl
48
def
9
ref
1
ref
21
ref
1
ref
21
ref
3
ref
cons
opType
49
def
nil
cons
cons
opType
constTerm
50
def
26
ref
appTerm
51
def
"select"
const
52
def
1
ref
49
ref
21
ref
nil
cons
53
def
cons
opType
constTerm
54
def
47
ref
appTerm
appTerm
assume
sym
appThm
47
ref
26
ref
appTerm
betaConv
55
def
trans
"A"
53
remove
cons
nil
cons
56
def
nil
nil
cons
57
def
cons
nil
9
ref
1
ref
1
ref
1
ref
"A"
varType
58
def
3
ref
cons
opType
59
def
3
ref
cons
opType
60
def
1
ref
60
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
61
def
"Data.Bool.?"
const
62
def
60
ref
constTerm
63
def
appTerm
64
def
"p"
59
ref
var
65
def
65
ref
varTerm
66
def
52
remove
1
ref
59
ref
58
ref
nil
cons
67
def
cons
opType
constTerm
66
ref
appTerm
appTerm
absTerm
appTerm
axiom
subst
48
remove
appThm
"p"
49
ref
var
68
def
68
remove
varTerm
69
def
54
remove
69
remove
appTerm
appTerm
absTerm
47
ref
appTerm
betaConv
trans
62
ref
1
ref
1
ref
1
ref
14
ref
1
ref
2
ref
19
remove
cons
opType
70
def
nil
cons
71
def
cons
opType
72
def
3
ref
cons
opType
73
def
3
ref
cons
opType
74
def
constTerm
75
def
refl
"fn"
72
ref
var
76
def
23
ref
9
ref
1
ref
70
ref
1
ref
70
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
77
def
76
remove
varTerm
78
def
17
ref
appTerm
appTerm
8
ref
15
ref
27
ref
absTerm
79
def
absTerm
80
def
appTerm
appTerm
refl
7
ref
30
ref
25
ref
refl
81
def
31
ref
77
ref
78
ref
39
ref
appTerm
appTerm
refl
30
ref
31
ref
"_30995"
70
ref
var
82
def
8
ref
15
ref
82
remove
varTerm
44
ref
appTerm
46
ref
appTerm
absTerm
absTerm
absTerm
83
def
absTerm
84
def
absTerm
85
def
37
ref
appTerm
betaConv
38
ref
refl
86
def
appThm
84
remove
38
ref
appTerm
betaConv
trans
78
remove
38
ref
appTerm
87
def
refl
appThm
83
remove
87
remove
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
1
ref
2
ref
1
ref
14
ref
1
ref
70
ref
71
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
var
85
remove
nil
cons
cons
"b"
70
remove
var
80
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
"A"
3
ref
cons
88
def
"B"
71
remove
cons
nil
cons
cons
57
ref
cons
"f"
1
ref
58
ref
1
ref
13
remove
67
ref
opType
89
def
1
ref
"B"
varType
90
def
90
ref
nil
cons
91
def
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
92
def
var
93
def
62
ref
1
ref
1
ref
1
ref
89
ref
91
ref
cons
opType
94
def
3
ref
cons
opType
3
ref
cons
opType
constTerm
"fn"
94
remove
var
95
def
23
ref
9
ref
1
ref
90
ref
1
ref
90
ref
3
ref
cons
opType
96
def
nil
cons
cons
opType
constTerm
97
def
95
remove
varTerm
98
def
16
remove
89
ref
constTerm
appTerm
appTerm
"b"
90
ref
var
99
def
varTerm
100
def
appTerm
appTerm
0
ref
60
ref
constTerm
101
def
"h"
58
ref
var
102
def
0
ref
1
ref
1
ref
89
ref
3
ref
cons
opType
103
def
3
ref
cons
opType
constTerm
104
def
"t"
89
ref
var
105
def
97
remove
98
ref
32
remove
1
ref
58
ref
1
ref
89
ref
89
ref
nil
cons
106
def
cons
opType
107
def
nil
cons
cons
opType
constTerm
102
ref
varTerm
108
def
appTerm
105
ref
varTerm
109
def
appTerm
110
def
appTerm
appTerm
93
remove
varTerm
111
def
108
ref
appTerm
109
ref
appTerm
98
remove
109
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
112
def
111
ref
appTerm
113
def
betaConv
99
remove
0
ref
1
ref
1
ref
92
ref
3
ref
cons
opType
114
def
3
ref
cons
opType
constTerm
112
ref
appTerm
115
def
absTerm
116
def
100
ref
appTerm
117
def
betaConv
nil
0
ref
1
ref
96
ref
3
ref
cons
opType
constTerm
116
ref
appTerm
118
def
axiom
nil
"p"
2
ref
var
119
def
118
remove
nil
cons
cons
8
ref
117
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
11
ref
"Data.Bool.==>"
const
10
ref
constTerm
120
def
119
ref
varTerm
121
def
appTerm
27
ref
appTerm
122
def
appTerm
refl
119
ref
8
ref
11
ref
23
ref
121
ref
appTerm
123
def
27
ref
appTerm
124
def
appTerm
125
def
121
ref
appTerm
absTerm
126
def
absTerm
127
def
121
ref
appTerm
betaConv
27
ref
refl
128
def
appThm
126
remove
27
ref
appTerm
betaConv
trans
appThm
nil
9
ref
1
ref
10
ref
1
ref
10
ref
3
ref
cons
opType
129
def
nil
cons
cons
opType
constTerm
130
def
120
ref
appTerm
127
remove
appTerm
axiom
121
ref
refl
131
def
appThm
128
ref
appThm
eqMp
132
def
sym
133
def
125
remove
refl
8
ref
9
ref
1
ref
129
ref
1
ref
129
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
134
def
"f"
10
remove
var
135
def
135
ref
varTerm
136
def
121
ref
appTerm
27
ref
appTerm
absTerm
137
def
appTerm
135
ref
136
ref
"Data.Bool.T"
const
2
ref
constTerm
138
def
appTerm
138
ref
appTerm
absTerm
139
def
appTerm
absTerm
140
def
27
ref
appTerm
betaConv
appThm
9
ref
1
ref
4
ref
5
remove
nil
cons
cons
opType
constTerm
141
def
123
remove
appTerm
refl
119
ref
140
remove
absTerm
142
def
121
ref
appTerm
betaConv
appThm
nil
130
remove
23
ref
appTerm
142
ref
appTerm
axiom
143
def
131
remove
appThm
eqMp
128
ref
appThm
eqMp
144
def
sym
135
ref
136
ref
refl
nil
"t"
2
ref
var
145
def
121
ref
nil
cons
146
def
cons
nil
cons
nil
cons
cons
11
ref
145
ref
varTerm
147
def
appTerm
138
ref
appTerm
assume
sym
nil
138
ref
axiom
148
def
eqMp
147
ref
assume
148
ref
deductAntisym
deductAntisym
149
def
subst
121
ref
assume
150
def
eqMp
appThm
nil
145
ref
27
ref
nil
cons
151
def
cons
nil
cons
nil
cons
cons
149
ref
subst
27
ref
assume
eqMp
appThm
absThm
eqMp
152
def
nil
"P"
2
ref
var
153
def
146
remove
cons
"Q"
2
ref
var
154
def
151
ref
cons
nil
cons
cons
nil
cons
cons
12
ref
135
ref
136
remove
153
ref
varTerm
155
def
appTerm
156
def
154
ref
varTerm
157
def
appTerm
absTerm
158
def
119
ref
8
ref
121
ref
absTerm
absTerm
159
def
appTerm
betaConv
159
ref
155
ref
appTerm
betaConv
157
ref
refl
160
def
appThm
8
ref
155
ref
absTerm
157
ref
appTerm
betaConv
trans
trans
appThm
139
ref
159
ref
appTerm
betaConv
159
ref
138
ref
appTerm
betaConv
138
ref
refl
161
def
appThm
8
ref
138
ref
absTerm
138
ref
appTerm
betaConv
trans
trans
appThm
11
ref
23
ref
155
ref
appTerm
162
def
157
ref
appTerm
163
def
appTerm
refl
8
ref
134
remove
135
remove
156
remove
27
ref
appTerm
absTerm
appTerm
139
ref
appTerm
absTerm
157
ref
appTerm
betaConv
appThm
141
remove
162
remove
appTerm
refl
142
remove
155
ref
appTerm
betaConv
appThm
143
remove
155
ref
refl
appThm
eqMp
160
ref
appThm
eqMp
163
remove
assume
eqMp
164
def
159
remove
refl
appThm
eqMp
sym
148
ref
eqMp
165
def
subst
166
def
deductAntisym
eqMp
132
remove
122
ref
assume
eqMp
sym
150
ref
eqMp
12
ref
137
remove
119
ref
8
ref
27
ref
absTerm
167
def
absTerm
168
def
appTerm
betaConv
168
ref
121
ref
appTerm
betaConv
128
ref
appThm
167
ref
27
ref
appTerm
betaConv
trans
trans
appThm
139
remove
168
ref
appTerm
betaConv
168
ref
138
ref
appTerm
betaConv
161
remove
appThm
167
ref
138
ref
appTerm
betaConv
trans
trans
169
def
appThm
144
remove
124
remove
assume
eqMp
168
ref
refl
170
def
appThm
eqMp
sym
148
ref
eqMp
171
def
proveHyp
deductAntisym
172
def
subst
proveHyp
"A"
91
remove
cons
nil
cons
"P"
96
remove
var
116
remove
nil
cons
cons
"x"
90
remove
var
100
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
119
ref
101
ref
"P"
59
ref
var
173
def
varTerm
174
def
appTerm
175
def
nil
cons
176
def
cons
8
ref
174
ref
"x"
58
ref
var
177
def
varTerm
178
def
appTerm
179
def
nil
cons
180
def
cons
nil
cons
cons
nil
cons
cons
181
def
133
ref
subst
181
remove
171
remove
152
remove
deductAntisym
182
def
subst
11
ref
179
ref
appTerm
refl
177
ref
138
ref
absTerm
183
def
178
ref
appTerm
betaConv
appThm
65
ref
9
ref
1
ref
59
ref
60
remove
nil
cons
cons
opType
constTerm
66
ref
appTerm
183
remove
appTerm
absTerm
184
def
174
ref
appTerm
betaConv
185
def
nil
61
remove
101
ref
appTerm
184
remove
appTerm
axiom
174
ref
refl
186
def
appThm
187
def
175
ref
assume
eqMp
eqMp
178
ref
refl
188
def
appThm
eqMp
sym
148
ref
eqMp
eqMp
nil
153
ref
176
remove
cons
154
ref
180
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
189
def
subst
eqMp
eqMp
nil
119
ref
115
remove
nil
cons
cons
8
ref
113
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
"A"
92
ref
nil
cons
cons
nil
cons
"P"
114
remove
var
112
remove
nil
cons
cons
"x"
92
remove
var
111
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
subst
subst
eqMp
nil
119
ref
75
ref
"_30994"
72
ref
var
190
def
23
ref
77
ref
190
ref
varTerm
191
def
17
ref
appTerm
192
def
appTerm
80
ref
appTerm
193
def
appTerm
6
ref
30
ref
25
ref
31
ref
77
remove
191
ref
39
ref
appTerm
194
def
appTerm
8
ref
15
ref
191
ref
38
ref
appTerm
44
ref
appTerm
195
def
46
ref
appTerm
196
def
absTerm
197
def
absTerm
198
def
appTerm
absTerm
199
def
appTerm
200
def
absTerm
201
def
appTerm
202
def
appTerm
203
def
absTerm
204
def
appTerm
205
def
nil
cons
cons
8
ref
75
remove
190
ref
23
ref
6
ref
8
ref
25
ref
15
ref
11
ref
192
remove
27
ref
appTerm
206
def
29
ref
appTerm
appTerm
207
def
27
ref
appTerm
208
def
absTerm
209
def
appTerm
210
def
absTerm
211
def
appTerm
212
def
appTerm
6
ref
8
ref
6
ref
30
ref
25
ref
31
ref
25
ref
15
ref
11
ref
194
remove
27
ref
appTerm
213
def
29
ref
appTerm
appTerm
214
def
196
remove
appTerm
215
def
absTerm
216
def
appTerm
217
def
absTerm
218
def
appTerm
219
def
absTerm
220
def
appTerm
221
def
absTerm
222
def
appTerm
223
def
appTerm
224
def
absTerm
225
def
appTerm
226
def
nil
cons
227
def
cons
nil
cons
228
def
cons
nil
cons
cons
172
ref
subst
nil
"P"
73
remove
var
229
def
190
ref
120
ref
204
ref
191
ref
appTerm
230
def
appTerm
226
ref
appTerm
231
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
72
ref
nil
cons
cons
nil
cons
232
def
57
ref
cons
11
ref
175
remove
appTerm
refl
185
remove
appThm
187
remove
eqMp
sym
233
def
subst
234
def
subst
190
ref
nil
145
ref
231
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
119
ref
230
ref
nil
cons
235
def
cons
228
ref
cons
nil
cons
cons
236
def
133
ref
subst
236
remove
182
ref
subst
230
ref
betaConv
230
remove
assume
eqMp
nil
119
ref
203
remove
nil
cons
237
def
cons
228
remove
cons
nil
cons
cons
238
def
172
ref
subst
proveHyp
238
ref
133
ref
subst
238
remove
182
ref
subst
225
ref
191
ref
appTerm
239
def
betaConv
240
def
sym
nil
153
ref
193
ref
nil
cons
cons
154
ref
202
remove
nil
cons
241
def
cons
nil
cons
cons
nil
cons
cons
242
def
165
ref
subst
nil
"P"
4
ref
var
243
def
211
remove
nil
cons
cons
nil
cons
nil
cons
cons
88
remove
nil
cons
244
def
57
ref
cons
245
def
233
ref
subst
246
def
subst
8
ref
nil
145
ref
210
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
"P"
18
ref
var
247
def
209
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
33
ref
cons
nil
cons
248
def
57
ref
cons
249
def
233
ref
subst
250
def
subst
15
ref
nil
145
ref
208
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
207
remove
refl
79
remove
29
ref
appTerm
betaConv
appThm
9
ref
1
ref
18
ref
24
remove
nil
cons
cons
opType
constTerm
251
def
206
ref
appTerm
refl
80
remove
27
ref
appTerm
betaConv
appThm
193
remove
assume
128
ref
appThm
eqMp
29
ref
refl
252
def
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
119
ref
212
remove
nil
cons
cons
8
ref
223
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
182
ref
subst
proveHyp
242
remove
12
ref
158
remove
168
ref
appTerm
betaConv
168
remove
155
remove
appTerm
betaConv
160
remove
appThm
167
remove
157
ref
appTerm
betaConv
trans
trans
appThm
169
remove
appThm
164
remove
170
remove
appThm
eqMp
sym
148
ref
eqMp
253
def
subst
nil
243
ref
222
remove
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
8
ref
nil
145
ref
221
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
243
ref
220
remove
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
30
ref
nil
145
ref
219
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
247
ref
218
remove
nil
cons
cons
nil
cons
nil
cons
cons
250
ref
subst
31
ref
nil
145
ref
217
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
247
ref
216
remove
nil
cons
cons
nil
cons
nil
cons
cons
250
ref
subst
15
ref
nil
145
ref
215
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
214
remove
refl
197
remove
29
ref
appTerm
betaConv
appThm
251
remove
213
ref
appTerm
refl
198
remove
27
ref
appTerm
betaConv
appThm
199
ref
38
ref
appTerm
254
def
betaConv
201
ref
37
ref
appTerm
255
def
betaConv
nil
119
ref
241
remove
cons
8
ref
255
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
244
ref
243
ref
201
remove
nil
cons
cons
"x"
2
ref
var
256
def
37
ref
nil
cons
cons
nil
cons
257
def
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
nil
119
ref
200
remove
nil
cons
cons
8
ref
254
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
248
ref
247
ref
199
remove
nil
cons
cons
"x"
14
ref
var
258
def
38
ref
nil
cons
cons
nil
cons
259
def
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
128
ref
appThm
eqMp
252
ref
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
232
ref
229
ref
225
ref
nil
cons
cons
260
def
"x"
72
remove
var
261
def
191
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
11
ref
63
remove
174
ref
appTerm
262
def
appTerm
263
def
refl
65
remove
6
ref
8
ref
120
ref
101
ref
177
ref
120
ref
66
remove
178
ref
appTerm
appTerm
27
ref
appTerm
absTerm
appTerm
appTerm
27
ref
appTerm
absTerm
appTerm
absTerm
264
def
174
remove
appTerm
betaConv
appThm
nil
64
remove
264
remove
appTerm
axiom
186
remove
appThm
eqMp
265
def
sym
nil
243
ref
154
ref
120
ref
101
ref
177
ref
120
ref
179
remove
appTerm
266
def
157
ref
appTerm
absTerm
267
def
appTerm
268
def
appTerm
157
ref
appTerm
269
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
246
remove
subst
154
ref
nil
145
ref
269
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
119
ref
268
remove
nil
cons
270
def
cons
271
def
8
ref
157
ref
nil
cons
272
def
cons
nil
cons
273
def
cons
nil
cons
cons
274
def
133
ref
subst
274
ref
182
ref
subst
nil
119
ref
180
remove
cons
273
ref
cons
nil
cons
cons
172
ref
subst
267
ref
178
ref
appTerm
275
def
betaConv
nil
271
ref
8
ref
275
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
"A"
67
ref
cons
nil
cons
276
def
173
ref
267
remove
nil
cons
cons
177
ref
178
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
153
ref
270
remove
cons
277
def
154
ref
272
ref
cons
nil
cons
278
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
279
def
subst
proveHyp
eqMp
nil
153
ref
237
remove
cons
154
ref
227
ref
cons
nil
cons
280
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
153
ref
235
remove
cons
280
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
119
ref
0
ref
74
remove
constTerm
281
def
261
ref
120
ref
204
ref
261
ref
varTerm
282
def
appTerm
appTerm
226
ref
appTerm
absTerm
appTerm
nil
cons
cons
8
ref
120
ref
205
remove
appTerm
226
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
232
ref
229
ref
204
remove
nil
cons
cons
280
remove
cons
nil
cons
cons
nil
271
remove
8
ref
120
ref
262
ref
appTerm
283
def
157
ref
appTerm
nil
cons
284
def
cons
nil
cons
cons
nil
cons
cons
285
def
133
ref
subst
285
remove
182
ref
subst
nil
119
ref
262
remove
nil
cons
286
def
cons
287
def
273
remove
cons
nil
cons
cons
288
def
133
ref
subst
288
remove
182
ref
subst
274
remove
172
ref
subst
8
ref
120
ref
101
ref
177
ref
266
remove
27
ref
appTerm
absTerm
appTerm
appTerm
27
ref
appTerm
absTerm
289
def
157
remove
appTerm
290
def
betaConv
nil
287
remove
8
ref
6
ref
289
ref
appTerm
291
def
nil
cons
292
def
cons
nil
cons
cons
nil
cons
cons
293
def
172
ref
subst
265
remove
nil
119
ref
263
remove
291
ref
appTerm
nil
cons
cons
8
ref
283
remove
291
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
293
remove
nil
119
ref
11
ref
121
remove
appTerm
27
ref
appTerm
294
def
nil
cons
295
def
cons
8
ref
122
remove
nil
cons
296
def
cons
nil
cons
cons
nil
cons
cons
297
def
133
ref
subst
297
remove
182
ref
subst
133
ref
182
ref
294
remove
assume
150
remove
eqMp
eqMp
166
remove
deductAntisym
eqMp
eqMp
nil
153
ref
295
remove
cons
154
ref
296
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
119
ref
292
remove
cons
8
ref
290
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
244
ref
243
ref
289
remove
nil
cons
cons
256
ref
272
remove
cons
nil
cons
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
153
ref
286
remove
cons
278
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
277
remove
154
ref
284
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
298
def
subst
eqMp
eqMp
proveHyp
nil
119
ref
227
remove
cons
8
ref
62
remove
1
ref
49
ref
3
ref
cons
opType
constTerm
47
ref
appTerm
299
def
nil
cons
300
def
cons
nil
cons
301
def
cons
nil
cons
cons
172
ref
subst
nil
229
remove
190
ref
120
ref
239
ref
appTerm
299
ref
appTerm
302
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
234
remove
subst
190
remove
nil
145
ref
302
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
119
ref
239
ref
nil
cons
303
def
cons
301
ref
cons
nil
cons
cons
304
def
133
ref
subst
304
remove
182
ref
subst
240
remove
239
remove
assume
eqMp
nil
119
ref
224
ref
nil
cons
305
def
cons
301
ref
cons
nil
cons
cons
306
def
172
ref
subst
proveHyp
306
ref
133
ref
subst
306
remove
182
ref
subst
"_30991"
2
ref
var
307
def
"_30992"
14
ref
var
308
def
"_30993"
14
ref
var
309
def
191
remove
308
ref
varTerm
appTerm
310
def
307
remove
varTerm
appTerm
309
ref
varTerm
311
def
appTerm
absTerm
absTerm
absTerm
312
def
refl
nil
119
ref
50
remove
312
ref
appTerm
312
ref
appTerm
nil
cons
cons
301
ref
cons
nil
cons
cons
172
ref
subst
proveHyp
nil
22
remove
312
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
119
ref
51
remove
312
ref
appTerm
313
def
nil
cons
314
def
cons
301
remove
cons
nil
cons
cons
315
def
133
remove
subst
315
remove
182
remove
subst
55
remove
sym
23
ref
refl
316
def
7
ref
8
ref
81
ref
15
ref
12
ref
313
remove
assume
317
def
128
ref
appThm
312
ref
27
ref
appTerm
betaConv
trans
318
def
17
ref
refl
appThm
308
ref
309
ref
310
ref
27
ref
appTerm
311
ref
appTerm
absTerm
absTerm
319
def
17
ref
appTerm
betaConv
trans
252
ref
appThm
309
ref
206
remove
311
ref
appTerm
absTerm
29
ref
appTerm
betaConv
trans
appThm
128
ref
appThm
absThm
appThm
absThm
appThm
appThm
7
ref
8
ref
7
ref
30
ref
81
ref
31
ref
81
ref
15
ref
12
ref
318
remove
39
ref
refl
appThm
319
remove
39
ref
appTerm
betaConv
trans
252
remove
appThm
309
ref
213
remove
311
ref
appTerm
absTerm
29
ref
appTerm
betaConv
trans
appThm
317
remove
44
ref
refl
appThm
312
remove
44
ref
appTerm
betaConv
trans
86
remove
appThm
308
remove
309
ref
310
remove
44
ref
appTerm
311
ref
appTerm
absTerm
absTerm
38
ref
appTerm
betaConv
trans
46
ref
refl
appThm
309
remove
195
remove
311
remove
appTerm
absTerm
46
ref
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
appThm
sym
224
remove
assume
eqMp
eqMp
56
remove
"P"
49
remove
var
47
remove
nil
cons
cons
"x"
21
ref
var
26
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
279
remove
subst
proveHyp
eqMp
nil
153
ref
314
remove
cons
154
ref
300
remove
cons
nil
cons
320
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
153
ref
305
remove
cons
320
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
153
ref
303
remove
cons
320
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
119
ref
281
remove
261
remove
120
ref
225
remove
282
remove
appTerm
appTerm
299
ref
appTerm
absTerm
appTerm
nil
cons
cons
8
ref
120
remove
226
remove
appTerm
299
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
232
remove
260
remove
320
remove
cons
nil
cons
cons
298
remove
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
321
def
pop
hdTl
pop
21
remove
constTerm
322
def
27
ref
appTerm
323
def
17
ref
appTerm
324
def
29
ref
appTerm
appTerm
27
ref
appTerm
absTerm
325
def
29
ref
appTerm
326
def
betaConv
8
ref
25
ref
325
ref
appTerm
327
def
absTerm
328
def
27
ref
appTerm
329
def
betaConv
321
ref
nil
153
remove
6
ref
328
ref
appTerm
nil
cons
330
def
cons
154
remove
6
ref
8
ref
6
ref
30
ref
25
ref
31
ref
25
ref
15
ref
11
ref
323
ref
39
remove
appTerm
29
ref
appTerm
appTerm
322
ref
44
remove
appTerm
38
ref
appTerm
46
remove
appTerm
appTerm
absTerm
331
def
appTerm
332
def
absTerm
333
def
appTerm
334
def
absTerm
335
def
appTerm
336
def
absTerm
337
def
appTerm
nil
cons
338
def
cons
nil
cons
cons
nil
cons
cons
339
def
165
remove
subst
proveHyp
nil
119
ref
330
remove
cons
8
ref
329
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
244
ref
243
ref
328
remove
nil
cons
cons
256
ref
151
remove
cons
nil
cons
340
def
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
nil
119
ref
327
remove
nil
cons
cons
8
ref
326
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
248
ref
247
ref
325
remove
nil
cons
cons
258
remove
29
ref
nil
cons
cons
nil
cons
341
def
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
subst
appThm
128
ref
appThm
nil
340
ref
nil
cons
cons
245
ref
nil
145
ref
9
ref
1
ref
58
remove
59
remove
nil
cons
cons
opType
constTerm
342
def
178
ref
appTerm
178
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
188
remove
eqMp
subst
343
def
subst
trans
absThm
appThm
nil
145
ref
138
remove
nil
cons
cons
nil
cons
nil
cons
cons
344
def
245
ref
145
ref
11
ref
101
ref
177
ref
147
ref
absTerm
appTerm
appTerm
147
ref
appTerm
absTerm
345
def
147
ref
appTerm
346
def
betaConv
nil
6
ref
345
ref
appTerm
347
def
axiom
nil
119
ref
347
remove
nil
cons
cons
8
ref
346
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
244
ref
243
ref
345
remove
nil
cons
cons
256
ref
147
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
348
def
subst
subst
349
def
trans
sym
148
ref
eqMp
nil
6
ref
8
ref
11
ref
324
remove
17
remove
appTerm
appTerm
27
ref
appTerm
absTerm
appTerm
thm
nil
247
ref
15
ref
9
ref
1
ref
"Data.Word.word"
typeOp
nil
opType
350
def
1
ref
350
ref
3
ref
cons
opType
351
def
nil
cons
cons
opType
constTerm
352
def
"Data.Word.Bits.toWord"
"_30952"
14
ref
var
353
def
"Data.Word.fromNatural"
const
1
ref
"Number.Natural.natural"
typeOp
nil
opType
354
def
350
ref
nil
cons
355
def
cons
opType
356
def
constTerm
357
def
"Number.Natural.Bits.fromList"
const
1
ref
14
ref
354
ref
nil
cons
358
def
cons
opType
359
def
constTerm
360
def
353
ref
varTerm
361
def
appTerm
appTerm
362
def
absTerm
363
def
defineConst
364
def
pop
1
ref
14
ref
355
ref
cons
opType
constTerm
365
def
29
ref
appTerm
appTerm
357
ref
360
remove
29
ref
appTerm
appTerm
appTerm
absTerm
366
def
nil
cons
cons
nil
cons
nil
cons
cons
250
ref
subst
353
remove
nil
145
ref
352
ref
365
ref
361
ref
appTerm
appTerm
362
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
364
remove
361
ref
refl
appThm
363
remove
361
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
25
ref
366
remove
appTerm
thm
nil
"P"
351
ref
var
367
def
"w"
350
ref
var
368
def
9
ref
20
remove
constTerm
369
def
"Data.Word.Bits.fromWord"
"_30947"
350
ref
var
370
def
"Number.Natural.Bits.toVector"
const
1
ref
354
ref
1
ref
354
ref
33
ref
cons
opType
nil
cons
cons
opType
constTerm
371
def
"Data.Word.toNatural"
const
1
ref
350
ref
358
ref
cons
opType
constTerm
372
def
370
ref
varTerm
373
def
appTerm
appTerm
"Data.Word.width"
const
354
ref
constTerm
374
def
appTerm
375
def
absTerm
376
def
defineConst
377
def
pop
1
ref
350
ref
33
remove
cons
opType
constTerm
378
def
368
ref
varTerm
379
def
appTerm
380
def
appTerm
371
remove
372
ref
379
ref
appTerm
381
def
appTerm
374
ref
appTerm
appTerm
absTerm
382
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
355
ref
cons
nil
cons
57
ref
cons
233
ref
subst
383
def
subst
370
remove
nil
145
ref
369
remove
378
ref
373
ref
appTerm
appTerm
375
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
377
remove
373
ref
refl
appThm
376
remove
373
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
0
ref
1
ref
351
remove
3
ref
cons
opType
constTerm
384
def
382
remove
appTerm
thm
nil
247
ref
15
ref
11
ref
"Data.Word.Bits.normal"
"_30957"
14
ref
var
385
def
9
ref
1
ref
354
ref
1
ref
354
ref
3
ref
cons
opType
386
def
nil
cons
387
def
cons
opType
388
def
constTerm
389
def
"Data.List.length"
const
359
remove
constTerm
390
def
385
ref
varTerm
391
def
appTerm
appTerm
374
ref
appTerm
392
def
absTerm
393
def
defineConst
394
def
pop
18
remove
constTerm
395
def
29
ref
appTerm
appTerm
389
remove
390
remove
29
ref
appTerm
appTerm
374
remove
appTerm
appTerm
absTerm
396
def
nil
cons
cons
nil
cons
nil
cons
cons
250
remove
subst
385
remove
nil
145
ref
11
ref
395
remove
391
ref
appTerm
appTerm
392
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
394
remove
391
ref
refl
appThm
393
remove
391
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
25
ref
396
remove
appTerm
thm
nil
367
ref
368
ref
352
ref
"Data.Word.not"
"_30986"
350
ref
var
397
def
365
ref
"Data.List.map"
const
1
ref
4
remove
35
remove
cons
opType
constTerm
41
ref
appTerm
398
def
378
remove
397
ref
varTerm
399
def
appTerm
appTerm
appTerm
400
def
absTerm
401
def
defineConst
402
def
pop
1
ref
350
ref
355
remove
cons
opType
403
def
constTerm
404
def
379
ref
appTerm
appTerm
365
remove
398
remove
380
remove
appTerm
appTerm
appTerm
absTerm
405
def
nil
cons
cons
nil
cons
nil
cons
cons
383
ref
subst
397
remove
nil
145
ref
352
ref
404
remove
399
ref
appTerm
appTerm
400
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
402
remove
399
ref
refl
appThm
401
remove
399
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
384
ref
405
remove
appTerm
thm
nil
367
ref
368
ref
0
remove
1
ref
386
ref
3
remove
cons
opType
constTerm
406
def
"n"
354
ref
var
407
def
11
ref
"Data.Word.bit"
"_30935"
350
ref
var
408
def
"_30936"
354
ref
var
409
def
"Number.Natural.Bits.bit"
const
388
remove
constTerm
410
def
372
ref
408
ref
varTerm
411
def
appTerm
appTerm
409
ref
varTerm
412
def
appTerm
413
def
absTerm
414
def
absTerm
415
def
defineConst
416
def
pop
1
ref
350
ref
387
remove
cons
opType
constTerm
417
def
379
ref
appTerm
407
ref
varTerm
418
def
appTerm
appTerm
410
remove
381
ref
appTerm
418
ref
appTerm
appTerm
absTerm
appTerm
absTerm
419
def
nil
cons
cons
nil
cons
nil
cons
cons
383
ref
subst
408
remove
nil
145
ref
406
ref
409
ref
11
ref
417
remove
411
ref
appTerm
412
ref
appTerm
appTerm
413
remove
appTerm
420
def
absTerm
421
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
"P"
386
remove
var
422
def
421
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
358
ref
cons
nil
cons
57
remove
cons
233
remove
subst
423
def
subst
409
remove
nil
145
ref
420
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
416
remove
411
ref
refl
appThm
415
remove
411
remove
appTerm
betaConv
trans
412
ref
refl
appThm
414
remove
412
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
384
ref
419
remove
appTerm
thm
nil
367
ref
368
ref
406
ref
407
ref
352
ref
"Data.Word.shiftLeft"
"_30911"
350
ref
var
424
def
"_30912"
354
ref
var
425
def
357
ref
"Number.Natural.Bits.shiftLeft"
const
1
ref
354
ref
1
ref
354
ref
358
remove
cons
opType
nil
cons
cons
opType
426
def
constTerm
427
def
372
ref
424
ref
varTerm
428
def
appTerm
appTerm
425
ref
varTerm
429
def
appTerm
appTerm
430
def
absTerm
431
def
absTerm
432
def
defineConst
433
def
pop
1
ref
350
ref
356
remove
nil
cons
cons
opType
434
def
constTerm
435
def
379
ref
appTerm
418
ref
appTerm
appTerm
357
ref
427
remove
381
ref
appTerm
418
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
436
def
nil
cons
cons
nil
cons
nil
cons
cons
383
ref
subst
424
remove
nil
145
ref
406
ref
425
ref
352
ref
435
remove
428
ref
appTerm
429
ref
appTerm
appTerm
430
remove
appTerm
437
def
absTerm
438
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
422
ref
438
remove
nil
cons
cons
nil
cons
nil
cons
cons
423
ref
subst
425
remove
nil
145
ref
437
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
433
remove
428
ref
refl
appThm
432
remove
428
remove
appTerm
betaConv
trans
429
ref
refl
appThm
431
remove
429
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
384
ref
436
remove
appTerm
thm
nil
367
ref
368
remove
406
ref
407
remove
352
ref
"Data.Word.shiftRight"
"_30923"
350
ref
var
439
def
"_30924"
354
remove
var
440
def
357
ref
"Number.Natural.Bits.shiftRight"
const
426
ref
constTerm
441
def
372
ref
439
ref
varTerm
442
def
appTerm
appTerm
440
ref
varTerm
443
def
appTerm
appTerm
444
def
absTerm
445
def
absTerm
446
def
defineConst
447
def
pop
434
remove
constTerm
448
def
379
remove
appTerm
418
ref
appTerm
appTerm
357
ref
441
remove
381
remove
appTerm
418
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
449
def
nil
cons
cons
nil
cons
nil
cons
cons
383
ref
subst
439
remove
nil
145
ref
406
remove
440
ref
352
ref
448
remove
442
ref
appTerm
443
ref
appTerm
appTerm
444
remove
appTerm
450
def
absTerm
451
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
422
remove
451
remove
nil
cons
cons
nil
cons
nil
cons
cons
423
remove
subst
440
remove
nil
145
ref
450
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
447
remove
442
ref
refl
appThm
446
remove
442
remove
appTerm
betaConv
trans
443
ref
refl
appThm
445
remove
443
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
384
ref
449
remove
appTerm
thm
nil
367
ref
"w1"
350
ref
var
452
def
384
ref
"w2"
350
ref
var
453
def
352
ref
"Data.Word.and"
"_30962"
350
ref
var
454
def
"_30963"
350
ref
var
455
def
357
ref
"Number.Natural.Bits.and"
const
426
ref
constTerm
456
def
372
ref
454
ref
varTerm
457
def
appTerm
appTerm
372
ref
455
ref
varTerm
458
def
appTerm
appTerm
appTerm
459
def
absTerm
460
def
absTerm
461
def
defineConst
462
def
pop
1
ref
350
ref
403
remove
nil
cons
cons
opType
463
def
constTerm
464
def
452
ref
varTerm
465
def
appTerm
453
ref
varTerm
466
def
appTerm
appTerm
357
ref
456
remove
372
ref
465
ref
appTerm
467
def
appTerm
372
ref
466
ref
appTerm
468
def
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
469
def
nil
cons
cons
nil
cons
nil
cons
cons
383
ref
subst
454
remove
nil
145
ref
384
ref
455
ref
352
ref
464
remove
457
ref
appTerm
458
ref
appTerm
appTerm
459
remove
appTerm
470
def
absTerm
471
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
367
ref
471
remove
nil
cons
cons
nil
cons
nil
cons
cons
383
ref
subst
455
remove
nil
145
ref
470
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
462
remove
457
ref
refl
appThm
461
remove
457
remove
appTerm
betaConv
trans
458
ref
refl
appThm
460
remove
458
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
384
ref
469
remove
appTerm
thm
nil
367
ref
452
remove
384
ref
453
remove
352
ref
"Data.Word.or"
"_30974"
350
ref
var
472
def
"_30975"
350
remove
var
473
def
357
ref
"Number.Natural.Bits.or"
const
426
remove
constTerm
474
def
372
ref
472
ref
varTerm
475
def
appTerm
appTerm
372
remove
473
ref
varTerm
476
def
appTerm
appTerm
appTerm
477
def
absTerm
478
def
absTerm
479
def
defineConst
480
def
pop
463
remove
constTerm
481
def
465
remove
appTerm
466
remove
appTerm
appTerm
357
remove
474
remove
467
remove
appTerm
468
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
482
def
nil
cons
cons
nil
cons
nil
cons
cons
383
ref
subst
472
remove
nil
145
ref
384
ref
473
ref
352
remove
481
remove
475
ref
appTerm
476
ref
appTerm
appTerm
477
remove
appTerm
483
def
absTerm
484
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
149
ref
subst
nil
367
remove
484
remove
nil
cons
cons
nil
cons
nil
cons
cons
383
remove
subst
473
remove
nil
145
remove
483
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
remove
subst
480
remove
475
ref
refl
appThm
479
remove
475
remove
appTerm
betaConv
trans
476
ref
refl
appThm
478
remove
476
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
384
remove
482
remove
appTerm
thm
7
ref
8
ref
7
ref
"h1"
2
ref
var
485
def
7
remove
"h2"
2
remove
var
486
def
81
ref
"t1"
14
ref
var
487
def
81
remove
"t2"
14
remove
var
488
def
12
remove
nil
15
remove
36
ref
486
ref
varTerm
489
def
appTerm
488
ref
varTerm
490
def
appTerm
491
def
nil
cons
cons
31
ref
487
ref
varTerm
492
def
nil
cons
cons
30
ref
485
ref
varTerm
493
def
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
331
ref
29
remove
appTerm
494
def
betaConv
333
ref
38
remove
appTerm
495
def
betaConv
335
ref
37
remove
appTerm
496
def
betaConv
337
ref
27
ref
appTerm
497
def
betaConv
321
remove
339
remove
253
remove
subst
proveHyp
nil
119
ref
338
remove
cons
8
ref
497
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
244
ref
243
ref
337
remove
nil
cons
cons
340
remove
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
nil
119
ref
336
remove
nil
cons
cons
8
ref
496
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
244
remove
243
remove
335
remove
nil
cons
cons
257
remove
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
nil
119
ref
334
remove
nil
cons
cons
8
ref
495
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
248
ref
247
ref
333
remove
nil
cons
cons
259
remove
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
nil
119
ref
332
remove
nil
cons
cons
8
ref
494
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
248
remove
247
remove
331
remove
nil
cons
cons
341
remove
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
subst
322
ref
refl
40
ref
refl
23
ref
41
ref
493
ref
appTerm
appTerm
498
def
refl
nil
31
remove
490
ref
nil
cons
cons
30
remove
489
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
499
def
245
ref
105
ref
342
remove
42
remove
1
ref
89
ref
67
remove
cons
opType
constTerm
110
ref
appTerm
appTerm
108
ref
appTerm
absTerm
500
def
109
ref
appTerm
501
def
betaConv
102
ref
104
ref
500
ref
appTerm
502
def
absTerm
503
def
108
ref
appTerm
504
def
betaConv
nil
101
ref
503
ref
appTerm
505
def
axiom
nil
119
ref
505
remove
nil
cons
cons
8
ref
504
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
276
ref
173
ref
503
remove
nil
cons
cons
177
remove
108
ref
nil
cons
cons
nil
cons
506
def
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
nil
119
ref
502
remove
nil
cons
cons
8
ref
501
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
"A"
106
remove
cons
nil
cons
507
def
"P"
103
ref
var
508
def
500
remove
nil
cons
cons
"x"
89
ref
var
109
ref
nil
cons
cons
nil
cons
509
def
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
subst
subst
510
def
appThm
appThm
316
remove
41
ref
refl
511
def
23
ref
493
ref
appTerm
512
def
refl
511
remove
510
remove
appThm
appThm
appThm
appThm
128
remove
appThm
appThm
appThm
492
ref
refl
appThm
499
remove
245
remove
105
remove
9
remove
1
remove
89
remove
103
remove
nil
cons
cons
opType
constTerm
45
remove
107
remove
constTerm
110
remove
appTerm
appTerm
109
ref
appTerm
absTerm
513
def
109
remove
appTerm
514
def
betaConv
102
remove
104
remove
513
ref
appTerm
515
def
absTerm
516
def
108
remove
appTerm
517
def
betaConv
nil
101
remove
516
ref
appTerm
518
def
axiom
nil
119
ref
518
remove
nil
cons
cons
8
ref
517
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
proveHyp
276
remove
173
remove
516
remove
nil
cons
cons
506
remove
cons
nil
cons
cons
189
ref
subst
eqMp
eqMp
nil
119
remove
515
remove
nil
cons
cons
8
ref
514
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
remove
subst
proveHyp
507
remove
508
remove
513
remove
nil
cons
cons
509
remove
cons
nil
cons
cons
189
remove
subst
eqMp
eqMp
subst
subst
appThm
trans
appThm
322
remove
40
remove
498
remove
489
ref
appTerm
appTerm
23
remove
41
ref
512
remove
41
remove
489
remove
appTerm
appTerm
appTerm
appTerm
27
remove
appTerm
appTerm
appTerm
492
ref
appTerm
490
remove
appTerm
519
def
refl
appThm
nil
256
remove
519
ref
nil
cons
cons
nil
cons
nil
cons
cons
343
remove
subst
trans
absThm
appThm
344
remove
249
remove
348
remove
subst
subst
520
def
trans
absThm
appThm
520
remove
trans
absThm
appThm
349
ref
trans
absThm
appThm
349
ref
trans
absThm
appThm
349
remove
trans
sym
148
remove
eqMp
nil
6
ref
8
remove
6
ref
485
remove
6
remove
486
remove
25
ref
487
remove
25
remove
488
remove
11
remove
323
remove
36
remove
493
remove
appTerm
492
remove
appTerm
appTerm
491
remove
appTerm
appTerm
519
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm