6
version
"Data.Bool.!"
const
0
def
"->"
typeOp
1
def
1
ref
"Algebra.Monoid.monoid"
typeOp
nil
opType
2
def
"bool"
typeOp
nil
opType
3
def
nil
cons
4
def
cons
opType
5
def
4
ref
cons
opType
constTerm
6
def
refl
7
def
"x"
2
ref
var
8
def
0
ref
1
ref
1
ref
"Number.Natural.natural"
typeOp
nil
opType
9
def
4
ref
cons
opType
10
def
4
ref
cons
opType
constTerm
11
def
refl
"n"
9
ref
var
12
def
"="
const
13
def
1
ref
2
ref
5
ref
nil
cons
cons
opType
constTerm
14
def
refl
15
def
nil
"l"
"Data.List.list"
typeOp
16
def
4
ref
opType
17
def
var
18
def
"Number.Natural.Bits.toList"
const
1
ref
9
ref
17
ref
nil
cons
19
def
cons
opType
constTerm
12
ref
varTerm
20
def
appTerm
21
def
nil
cons
cons
"z"
2
ref
var
22
def
"Algebra.Monoid.0"
const
2
ref
constTerm
23
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
8
ref
14
ref
"Algebra.Monoid.multAdd"
const
1
ref
2
ref
1
ref
2
ref
1
ref
17
ref
2
ref
nil
cons
24
def
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
25
def
22
ref
varTerm
26
def
appTerm
8
ref
varTerm
27
def
appTerm
28
def
18
ref
varTerm
29
def
appTerm
appTerm
"Algebra.Monoid.+"
const
1
ref
2
ref
1
ref
2
ref
24
ref
cons
opType
nil
cons
cons
opType
30
def
constTerm
31
def
26
ref
appTerm
32
def
"Algebra.Monoid.*"
const
1
ref
2
ref
1
ref
9
ref
24
ref
cons
opType
nil
cons
cons
opType
constTerm
33
def
27
ref
appTerm
34
def
"Number.Natural.Bits.fromList"
const
1
ref
17
ref
9
ref
nil
cons
35
def
cons
opType
constTerm
36
def
29
ref
appTerm
appTerm
appTerm
appTerm
37
def
absTerm
38
def
27
ref
appTerm
39
def
betaConv
22
ref
6
ref
38
ref
appTerm
40
def
absTerm
41
def
26
ref
appTerm
42
def
betaConv
18
ref
6
ref
41
ref
appTerm
43
def
absTerm
44
def
29
ref
appTerm
45
def
betaConv
46
def
nil
"P"
5
remove
var
47
def
22
ref
6
ref
8
ref
14
ref
28
ref
"Data.List.[]"
const
48
def
17
ref
constTerm
49
def
appTerm
appTerm
50
def
32
ref
34
ref
36
ref
49
ref
appTerm
51
def
appTerm
appTerm
appTerm
absTerm
52
def
appTerm
53
def
absTerm
54
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
24
remove
cons
nil
cons
55
def
nil
nil
cons
56
def
cons
57
def
13
ref
1
ref
3
ref
1
ref
3
ref
4
ref
cons
opType
58
def
nil
cons
cons
opType
59
def
constTerm
60
def
0
ref
1
ref
1
ref
"A"
varType
61
def
4
ref
cons
opType
62
def
4
ref
cons
opType
63
def
constTerm
64
def
"P"
62
ref
var
65
def
varTerm
66
def
appTerm
67
def
appTerm
refl
"p"
62
ref
var
68
def
13
ref
1
ref
62
ref
63
ref
nil
cons
cons
opType
constTerm
68
remove
varTerm
appTerm
"x"
61
ref
var
69
def
"Data.Bool.T"
const
3
ref
constTerm
70
def
absTerm
71
def
appTerm
absTerm
72
def
66
ref
appTerm
betaConv
73
def
appThm
nil
13
ref
1
ref
63
ref
1
ref
63
remove
4
ref
cons
opType
nil
cons
cons
opType
constTerm
64
ref
appTerm
72
remove
appTerm
axiom
66
ref
refl
appThm
74
def
eqMp
sym
75
def
subst
76
def
subst
22
ref
nil
"t"
3
ref
var
77
def
53
remove
nil
cons
cons
nil
cons
nil
cons
cons
60
ref
77
ref
varTerm
78
def
appTerm
79
def
70
ref
appTerm
80
def
assume
sym
nil
70
ref
axiom
81
def
eqMp
78
ref
assume
81
ref
deductAntisym
deductAntisym
82
def
subst
nil
47
ref
52
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
8
ref
15
ref
8
ref
50
remove
26
ref
appTerm
absTerm
83
def
27
ref
appTerm
84
def
betaConv
22
ref
6
ref
83
ref
appTerm
85
def
absTerm
86
def
26
ref
appTerm
87
def
betaConv
nil
6
ref
86
ref
appTerm
88
def
axiom
nil
"p"
3
ref
var
89
def
88
remove
nil
cons
cons
"q"
3
ref
var
90
def
87
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
60
ref
"Data.Bool.==>"
const
59
ref
constTerm
91
def
89
ref
varTerm
92
def
appTerm
93
def
90
ref
varTerm
94
def
appTerm
95
def
appTerm
refl
89
ref
90
ref
60
ref
"Data.Bool./\\"
const
59
ref
constTerm
96
def
92
ref
appTerm
97
def
94
ref
appTerm
98
def
appTerm
99
def
92
ref
appTerm
absTerm
100
def
absTerm
101
def
92
ref
appTerm
betaConv
94
ref
refl
102
def
appThm
100
remove
94
ref
appTerm
betaConv
trans
appThm
nil
13
ref
1
ref
59
ref
1
ref
59
ref
4
ref
cons
opType
103
def
nil
cons
cons
opType
constTerm
104
def
91
ref
appTerm
101
remove
appTerm
axiom
92
ref
refl
105
def
appThm
102
ref
appThm
eqMp
106
def
sym
107
def
99
remove
refl
90
ref
13
ref
1
ref
103
ref
1
ref
103
remove
4
ref
cons
opType
nil
cons
cons
opType
constTerm
108
def
"f"
59
ref
var
109
def
109
ref
varTerm
110
def
92
ref
appTerm
94
ref
appTerm
absTerm
111
def
appTerm
109
ref
110
ref
70
ref
appTerm
70
ref
appTerm
absTerm
112
def
appTerm
absTerm
113
def
94
ref
appTerm
betaConv
appThm
13
ref
1
ref
58
ref
1
ref
58
ref
4
ref
cons
opType
114
def
nil
cons
cons
opType
constTerm
115
def
97
remove
appTerm
refl
89
ref
113
remove
absTerm
116
def
92
ref
appTerm
betaConv
appThm
nil
104
ref
96
ref
appTerm
116
ref
appTerm
axiom
117
def
105
remove
appThm
eqMp
102
ref
appThm
eqMp
118
def
sym
109
ref
110
ref
refl
nil
77
ref
92
ref
nil
cons
119
def
cons
nil
cons
nil
cons
cons
82
ref
subst
92
ref
assume
120
def
eqMp
appThm
nil
77
ref
94
ref
nil
cons
121
def
cons
nil
cons
nil
cons
cons
82
ref
subst
94
ref
assume
eqMp
appThm
absThm
eqMp
122
def
nil
"P"
3
ref
var
123
def
119
remove
cons
"Q"
3
ref
var
124
def
121
remove
cons
nil
cons
cons
nil
cons
cons
60
ref
refl
125
def
109
ref
110
remove
123
ref
varTerm
126
def
appTerm
127
def
124
ref
varTerm
128
def
appTerm
absTerm
89
ref
90
ref
92
ref
absTerm
absTerm
129
def
appTerm
betaConv
129
ref
126
ref
appTerm
betaConv
128
ref
refl
130
def
appThm
90
ref
126
ref
absTerm
128
ref
appTerm
betaConv
trans
trans
appThm
112
ref
129
ref
appTerm
betaConv
129
ref
70
ref
appTerm
betaConv
70
ref
refl
131
def
appThm
90
ref
70
ref
absTerm
70
ref
appTerm
betaConv
trans
trans
appThm
60
ref
96
ref
126
ref
appTerm
132
def
128
ref
appTerm
133
def
appTerm
refl
90
ref
108
remove
109
remove
127
remove
94
ref
appTerm
absTerm
appTerm
112
ref
appTerm
absTerm
128
ref
appTerm
betaConv
appThm
115
ref
132
remove
appTerm
refl
116
remove
126
ref
appTerm
betaConv
appThm
117
remove
126
ref
refl
134
def
appThm
eqMp
130
ref
appThm
eqMp
133
remove
assume
eqMp
129
remove
refl
appThm
eqMp
sym
81
ref
eqMp
135
def
subst
deductAntisym
eqMp
106
remove
95
remove
assume
eqMp
sym
120
remove
eqMp
125
ref
111
remove
89
ref
90
ref
94
ref
absTerm
136
def
absTerm
137
def
appTerm
betaConv
137
ref
92
remove
appTerm
betaConv
102
remove
appThm
136
ref
94
ref
appTerm
betaConv
trans
trans
appThm
112
remove
137
ref
appTerm
betaConv
137
ref
70
ref
appTerm
betaConv
131
remove
appThm
136
remove
70
ref
appTerm
betaConv
trans
trans
appThm
118
remove
98
remove
assume
eqMp
137
remove
refl
appThm
eqMp
sym
81
ref
eqMp
138
def
proveHyp
deductAntisym
139
def
subst
proveHyp
55
ref
47
ref
86
remove
nil
cons
cons
8
ref
26
ref
nil
cons
140
def
cons
nil
cons
141
def
cons
nil
cons
cons
nil
89
ref
67
ref
nil
cons
142
def
cons
90
ref
66
remove
69
ref
varTerm
143
def
appTerm
144
def
nil
cons
145
def
cons
nil
cons
cons
nil
cons
cons
146
def
107
ref
subst
146
remove
138
remove
122
remove
deductAntisym
147
def
subst
60
ref
144
remove
appTerm
refl
71
remove
143
ref
appTerm
betaConv
appThm
73
remove
74
remove
67
remove
assume
eqMp
eqMp
143
ref
refl
148
def
appThm
eqMp
sym
81
ref
eqMp
eqMp
nil
123
ref
142
remove
cons
124
ref
145
remove
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
deductAntisym
eqMp
149
def
subst
eqMp
eqMp
nil
89
ref
85
remove
nil
cons
cons
90
ref
84
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
83
remove
nil
cons
cons
8
ref
27
ref
nil
cons
cons
nil
cons
150
def
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
appThm
32
ref
refl
151
def
34
ref
refl
152
def
nil
13
ref
1
ref
9
ref
10
ref
nil
cons
cons
opType
constTerm
153
def
51
remove
appTerm
"Number.Natural.zero"
const
9
ref
constTerm
154
def
appTerm
axiom
appThm
8
ref
14
ref
34
ref
154
ref
appTerm
appTerm
23
ref
appTerm
absTerm
155
def
27
ref
appTerm
156
def
betaConv
nil
6
ref
155
ref
appTerm
157
def
axiom
nil
89
ref
157
remove
nil
cons
cons
90
ref
156
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
155
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
158
def
trans
appThm
nil
141
ref
nil
cons
cons
159
def
8
ref
14
ref
31
ref
27
ref
appTerm
160
def
23
ref
appTerm
appTerm
27
ref
appTerm
absTerm
161
def
27
ref
appTerm
162
def
betaConv
nil
6
ref
161
ref
appTerm
163
def
axiom
nil
89
ref
163
remove
nil
cons
cons
90
ref
162
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
161
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
164
def
trans
appThm
159
remove
57
ref
nil
77
ref
13
remove
1
ref
61
ref
62
remove
nil
cons
cons
opType
constTerm
165
def
143
ref
appTerm
143
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
148
remove
eqMp
subst
166
def
subst
167
def
trans
absThm
eqMp
eqMp
absThm
eqMp
nil
89
ref
6
ref
54
remove
appTerm
168
def
nil
cons
cons
90
ref
0
ref
114
remove
constTerm
169
def
"h"
3
ref
var
170
def
0
ref
1
ref
1
ref
17
ref
4
ref
cons
opType
171
def
4
ref
cons
opType
constTerm
172
def
"t"
17
ref
var
173
def
91
ref
6
ref
22
ref
6
ref
8
ref
14
ref
28
ref
173
ref
varTerm
174
def
appTerm
appTerm
32
ref
34
ref
36
ref
174
ref
appTerm
175
def
appTerm
appTerm
appTerm
absTerm
176
def
appTerm
177
def
absTerm
178
def
appTerm
179
def
appTerm
6
ref
22
ref
6
ref
8
ref
14
ref
28
remove
"Data.List.::"
const
180
def
1
ref
3
ref
1
ref
17
ref
19
ref
cons
opType
nil
cons
cons
opType
constTerm
170
ref
varTerm
181
def
appTerm
174
ref
appTerm
182
def
appTerm
appTerm
183
def
32
ref
34
ref
36
ref
182
ref
appTerm
184
def
appTerm
appTerm
appTerm
185
def
absTerm
186
def
appTerm
187
def
absTerm
188
def
appTerm
189
def
appTerm
190
def
absTerm
191
def
appTerm
192
def
absTerm
193
def
appTerm
194
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
147
ref
subst
proveHyp
nil
"P"
58
remove
var
195
def
193
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
4
ref
cons
nil
cons
196
def
56
ref
cons
197
def
75
ref
subst
subst
170
ref
nil
77
ref
192
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
"P"
171
ref
var
198
def
191
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
19
remove
cons
nil
cons
199
def
56
ref
cons
75
remove
subst
200
def
subst
173
ref
nil
77
ref
190
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
89
ref
179
remove
nil
cons
201
def
cons
202
def
90
ref
189
remove
nil
cons
203
def
cons
nil
cons
cons
nil
cons
cons
204
def
107
ref
subst
204
remove
147
ref
subst
nil
47
ref
188
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
22
ref
nil
77
ref
187
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
47
ref
186
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
8
ref
nil
77
ref
185
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
15
ref
173
ref
183
remove
25
ref
"Data.Bool.cond"
const
205
def
1
ref
3
ref
30
remove
nil
cons
cons
opType
constTerm
206
def
181
ref
appTerm
32
ref
27
ref
appTerm
207
def
appTerm
26
ref
appTerm
208
def
appTerm
160
ref
27
ref
appTerm
209
def
appTerm
174
ref
appTerm
appTerm
absTerm
210
def
174
ref
appTerm
211
def
betaConv
170
ref
172
ref
210
ref
appTerm
212
def
absTerm
213
def
181
ref
appTerm
214
def
betaConv
8
ref
169
ref
213
ref
appTerm
215
def
absTerm
216
def
27
ref
appTerm
217
def
betaConv
22
ref
6
ref
216
ref
appTerm
218
def
absTerm
219
def
26
ref
appTerm
220
def
betaConv
nil
6
ref
219
ref
appTerm
221
def
axiom
nil
89
ref
221
remove
nil
cons
cons
90
ref
220
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
219
remove
nil
cons
cons
141
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
218
remove
nil
cons
cons
90
ref
217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
216
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
215
remove
nil
cons
cons
90
ref
214
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
196
ref
195
ref
213
remove
nil
cons
cons
"x"
3
ref
var
222
def
181
ref
nil
cons
cons
nil
cons
223
def
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
212
remove
nil
cons
cons
90
ref
211
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
199
ref
198
ref
210
remove
nil
cons
cons
"x"
17
remove
var
224
def
174
ref
nil
cons
cons
nil
cons
225
def
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
appThm
151
ref
152
ref
173
ref
153
ref
184
remove
appTerm
"Number.Natural.Bits.cons"
const
1
ref
3
ref
1
ref
9
ref
35
ref
cons
opType
226
def
nil
cons
227
def
cons
opType
constTerm
181
ref
appTerm
228
def
175
ref
appTerm
229
def
appTerm
absTerm
230
def
174
ref
appTerm
231
def
betaConv
170
ref
172
ref
230
ref
appTerm
232
def
absTerm
233
def
181
ref
appTerm
234
def
betaConv
nil
169
ref
233
ref
appTerm
235
def
axiom
nil
89
ref
235
remove
nil
cons
cons
90
ref
234
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
196
ref
195
ref
233
remove
nil
cons
cons
223
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
232
remove
nil
cons
cons
90
ref
231
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
199
ref
198
ref
230
remove
nil
cons
cons
225
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
appThm
appThm
appThm
sym
15
ref
nil
8
ref
209
ref
nil
cons
cons
22
ref
208
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
27
ref
appTerm
236
def
betaConv
178
ref
26
ref
appTerm
237
def
betaConv
nil
202
remove
90
ref
237
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
55
ref
47
ref
178
remove
nil
cons
cons
141
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
177
remove
nil
cons
cons
90
ref
236
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
176
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
appThm
32
ref
34
ref
229
remove
appTerm
appTerm
refl
appThm
sym
14
ref
31
ref
208
ref
appTerm
33
ref
209
ref
appTerm
175
ref
appTerm
238
def
appTerm
appTerm
refl
151
ref
152
ref
nil
"t"
9
ref
var
239
def
175
ref
nil
cons
240
def
cons
nil
cons
nil
cons
cons
239
ref
153
ref
228
remove
239
remove
varTerm
241
def
appTerm
appTerm
"Number.Natural.+"
const
1
ref
9
ref
227
remove
cons
opType
242
def
constTerm
243
def
"Number.Natural.fromBool"
const
1
ref
3
ref
35
ref
cons
opType
constTerm
244
def
181
ref
appTerm
245
def
appTerm
"Number.Natural.*"
const
242
ref
constTerm
246
def
"Number.Natural.bit0"
const
226
ref
constTerm
"Number.Natural.bit1"
const
226
remove
constTerm
154
ref
appTerm
247
def
appTerm
248
def
appTerm
249
def
241
ref
appTerm
appTerm
appTerm
absTerm
250
def
241
ref
appTerm
251
def
betaConv
170
ref
11
ref
250
ref
appTerm
252
def
absTerm
253
def
181
ref
appTerm
254
def
betaConv
nil
169
ref
253
ref
appTerm
255
def
axiom
nil
89
ref
255
remove
nil
cons
cons
90
ref
254
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
196
ref
195
ref
253
remove
nil
cons
cons
223
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
252
remove
nil
cons
cons
90
ref
251
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
"A"
35
remove
cons
nil
cons
256
def
"P"
10
remove
var
257
def
250
remove
nil
cons
cons
"x"
9
ref
var
258
def
241
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
appThm
nil
12
ref
249
remove
175
ref
appTerm
nil
cons
cons
"m"
9
ref
var
259
def
245
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
12
ref
14
ref
34
ref
243
remove
259
ref
varTerm
260
def
appTerm
20
ref
appTerm
appTerm
appTerm
31
ref
34
ref
260
ref
appTerm
261
def
appTerm
34
ref
20
ref
appTerm
262
def
appTerm
appTerm
absTerm
263
def
20
ref
appTerm
264
def
betaConv
259
ref
11
ref
263
ref
appTerm
265
def
absTerm
266
def
260
ref
appTerm
267
def
betaConv
8
ref
11
ref
266
ref
appTerm
268
def
absTerm
269
def
27
ref
appTerm
270
def
betaConv
nil
6
ref
269
ref
appTerm
271
def
axiom
nil
89
ref
271
remove
nil
cons
cons
90
ref
270
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
269
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
268
remove
nil
cons
cons
90
ref
267
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
256
ref
257
ref
266
remove
nil
cons
cons
258
ref
260
ref
nil
cons
cons
nil
cons
272
def
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
265
remove
nil
cons
cons
90
ref
264
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
256
ref
257
ref
263
remove
nil
cons
cons
258
remove
20
ref
nil
cons
cons
nil
cons
273
def
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
31
ref
34
ref
245
remove
appTerm
274
def
appTerm
refl
nil
12
ref
240
remove
cons
259
ref
248
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
12
ref
14
ref
34
ref
246
remove
260
ref
appTerm
20
ref
appTerm
appTerm
appTerm
33
ref
261
remove
appTerm
20
ref
appTerm
appTerm
absTerm
275
def
20
ref
appTerm
276
def
betaConv
259
remove
11
ref
275
ref
appTerm
277
def
absTerm
278
def
260
remove
appTerm
279
def
betaConv
8
ref
11
ref
278
ref
appTerm
280
def
absTerm
281
def
27
ref
appTerm
282
def
betaConv
nil
6
ref
281
ref
appTerm
283
def
axiom
nil
89
ref
283
remove
nil
cons
cons
90
ref
282
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
281
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
280
remove
nil
cons
cons
90
ref
279
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
256
ref
257
ref
278
remove
nil
cons
cons
272
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
277
remove
nil
cons
cons
90
ref
276
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
256
ref
257
ref
275
remove
nil
cons
cons
273
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
33
remove
refl
8
ref
14
ref
34
ref
248
remove
appTerm
appTerm
209
remove
appTerm
absTerm
284
def
27
ref
appTerm
285
def
betaConv
nil
6
ref
284
ref
appTerm
286
def
axiom
nil
89
ref
286
remove
nil
cons
cons
90
ref
285
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
284
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
appThm
175
remove
refl
appThm
trans
appThm
trans
trans
appThm
nil
22
ref
238
ref
nil
cons
cons
"y"
2
ref
var
287
def
274
ref
nil
cons
cons
141
ref
cons
cons
nil
cons
cons
22
ref
14
ref
160
ref
31
ref
287
ref
varTerm
288
def
appTerm
26
ref
appTerm
appTerm
289
def
appTerm
31
ref
160
remove
288
ref
appTerm
appTerm
26
ref
appTerm
290
def
appTerm
291
def
absTerm
292
def
26
ref
appTerm
293
def
betaConv
287
ref
6
ref
292
ref
appTerm
294
def
absTerm
295
def
288
ref
appTerm
296
def
betaConv
8
ref
6
ref
295
ref
appTerm
297
def
absTerm
298
def
27
ref
appTerm
299
def
betaConv
7
ref
8
ref
7
ref
287
ref
7
remove
22
ref
291
remove
assume
sym
14
ref
290
remove
appTerm
289
remove
appTerm
300
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
nil
6
ref
8
ref
6
ref
287
remove
6
ref
22
ref
300
remove
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
89
ref
6
ref
298
ref
appTerm
nil
cons
cons
90
ref
299
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
298
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
297
remove
nil
cons
cons
90
ref
296
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
295
remove
nil
cons
cons
8
ref
288
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
294
remove
nil
cons
cons
90
ref
293
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
292
remove
nil
cons
cons
141
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
trans
appThm
sym
31
ref
refl
nil
89
ref
60
ref
181
ref
appTerm
301
def
"Data.Bool.F"
const
3
ref
constTerm
302
def
appTerm
303
def
nil
cons
304
def
cons
90
ref
14
ref
208
remove
appTerm
32
ref
274
remove
appTerm
appTerm
nil
cons
305
def
cons
nil
cons
306
def
cons
nil
cons
cons
307
def
107
ref
subst
307
remove
147
ref
subst
60
ref
"_30284"
3
ref
var
308
def
14
ref
206
ref
308
remove
varTerm
309
def
appTerm
207
ref
appTerm
26
ref
appTerm
appTerm
32
ref
34
ref
244
ref
309
remove
appTerm
appTerm
appTerm
appTerm
absTerm
310
def
181
ref
appTerm
311
def
appTerm
refl
312
def
310
ref
302
ref
appTerm
betaConv
appThm
125
remove
311
remove
betaConv
appThm
313
def
14
ref
206
ref
302
ref
appTerm
207
ref
appTerm
26
ref
appTerm
appTerm
32
ref
34
ref
244
ref
302
ref
appTerm
appTerm
appTerm
appTerm
refl
appThm
trans
310
remove
refl
314
def
303
remove
assume
appThm
eqMp
sym
15
ref
nil
"t2"
2
ref
var
140
remove
cons
"t1"
2
remove
var
207
ref
nil
cons
315
def
cons
nil
cons
cons
nil
cons
cons
316
def
57
ref
"t2"
61
ref
var
317
def
165
ref
205
ref
1
ref
3
ref
1
ref
61
ref
1
ref
61
ref
61
ref
nil
cons
318
def
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
319
def
302
ref
appTerm
"t1"
61
ref
var
320
def
varTerm
321
def
appTerm
317
ref
varTerm
322
def
appTerm
appTerm
322
ref
appTerm
absTerm
323
def
322
ref
appTerm
324
def
betaConv
320
ref
64
ref
323
ref
appTerm
325
def
absTerm
326
def
321
ref
appTerm
327
def
betaConv
nil
64
ref
326
ref
appTerm
328
def
axiom
nil
89
ref
328
remove
nil
cons
cons
90
ref
327
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
"A"
318
ref
cons
nil
cons
329
def
65
ref
326
remove
nil
cons
cons
69
ref
321
ref
nil
cons
cons
nil
cons
330
def
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
325
remove
nil
cons
cons
90
ref
324
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
329
ref
65
ref
323
remove
nil
cons
cons
69
ref
322
ref
nil
cons
cons
nil
cons
331
def
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
332
def
subst
subst
appThm
151
ref
152
ref
nil
"b"
3
ref
var
333
def
302
ref
nil
cons
cons
nil
cons
nil
cons
cons
333
ref
153
ref
244
ref
333
ref
varTerm
334
def
appTerm
appTerm
205
remove
1
ref
3
ref
242
remove
nil
cons
cons
opType
constTerm
334
ref
appTerm
247
ref
appTerm
154
ref
appTerm
appTerm
absTerm
335
def
334
ref
appTerm
336
def
betaConv
nil
169
ref
335
ref
appTerm
337
def
axiom
nil
89
ref
337
remove
nil
cons
cons
90
ref
336
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
196
ref
195
ref
335
remove
nil
cons
cons
222
ref
334
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
338
def
subst
nil
"t2"
9
ref
var
154
remove
nil
cons
cons
"t1"
9
remove
var
247
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
339
def
256
ref
56
remove
cons
340
def
332
remove
subst
subst
trans
appThm
158
remove
trans
appThm
164
remove
trans
appThm
167
remove
trans
sym
81
ref
eqMp
eqMp
eqMp
nil
123
ref
304
ref
cons
124
ref
305
ref
cons
nil
cons
341
def
cons
nil
cons
cons
135
ref
subst
deductAntisym
eqMp
nil
89
ref
301
remove
70
ref
appTerm
342
def
nil
cons
343
def
cons
306
remove
cons
nil
cons
cons
344
def
107
remove
subst
344
remove
147
remove
subst
312
remove
"_30282"
3
ref
var
345
def
14
ref
206
ref
345
remove
varTerm
346
def
appTerm
207
ref
appTerm
26
ref
appTerm
appTerm
32
ref
34
ref
244
ref
346
remove
appTerm
appTerm
appTerm
appTerm
absTerm
70
ref
appTerm
betaConv
appThm
313
remove
14
ref
206
remove
70
ref
appTerm
207
remove
appTerm
26
remove
appTerm
appTerm
32
remove
34
ref
244
remove
70
ref
appTerm
appTerm
appTerm
appTerm
refl
appThm
trans
314
remove
342
remove
assume
appThm
eqMp
sym
15
remove
316
remove
57
ref
317
remove
165
remove
319
remove
70
ref
appTerm
321
ref
appTerm
322
ref
appTerm
appTerm
321
ref
appTerm
absTerm
347
def
322
remove
appTerm
348
def
betaConv
320
remove
64
ref
347
ref
appTerm
349
def
absTerm
350
def
321
remove
appTerm
351
def
betaConv
nil
64
ref
350
ref
appTerm
352
def
axiom
nil
89
ref
352
remove
nil
cons
cons
90
ref
351
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
329
ref
65
ref
350
remove
nil
cons
cons
330
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
349
remove
nil
cons
cons
90
ref
348
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
329
remove
65
remove
347
remove
nil
cons
cons
331
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
353
def
subst
subst
appThm
151
remove
152
ref
nil
333
remove
70
remove
nil
cons
354
def
cons
nil
cons
nil
cons
cons
338
remove
subst
339
remove
340
ref
353
remove
subst
subst
trans
appThm
8
ref
14
ref
34
ref
247
remove
appTerm
appTerm
27
ref
appTerm
absTerm
355
def
27
ref
appTerm
356
def
betaConv
nil
6
ref
355
ref
appTerm
357
def
axiom
nil
89
ref
357
remove
nil
cons
cons
90
ref
356
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
355
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
trans
appThm
appThm
nil
8
ref
315
remove
cons
nil
cons
nil
cons
cons
166
ref
subst
trans
sym
81
ref
eqMp
eqMp
eqMp
nil
123
ref
343
remove
cons
358
def
341
remove
cons
nil
cons
cons
135
ref
subst
deductAntisym
eqMp
77
ref
"Data.Bool.\\/"
const
59
remove
constTerm
359
def
80
remove
appTerm
79
remove
302
remove
appTerm
appTerm
absTerm
360
def
181
remove
appTerm
361
def
betaConv
nil
169
ref
360
ref
appTerm
362
def
axiom
nil
89
ref
362
remove
nil
cons
cons
90
ref
361
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
196
ref
195
ref
360
remove
nil
cons
cons
223
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
358
remove
124
ref
304
remove
cons
"R"
3
ref
var
363
def
305
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
89
ref
91
ref
128
ref
appTerm
364
def
363
remove
varTerm
365
def
appTerm
366
def
nil
cons
cons
90
ref
365
ref
nil
cons
367
def
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
nil
89
ref
91
ref
126
ref
appTerm
368
def
365
ref
appTerm
nil
cons
cons
90
ref
91
ref
366
remove
appTerm
365
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
"r"
3
remove
var
369
def
91
ref
368
remove
369
ref
varTerm
370
def
appTerm
appTerm
371
def
91
ref
364
remove
370
ref
appTerm
appTerm
370
ref
appTerm
appTerm
absTerm
372
def
365
remove
appTerm
373
def
betaConv
60
ref
359
ref
126
ref
appTerm
374
def
128
ref
appTerm
375
def
appTerm
refl
90
ref
169
ref
369
ref
371
remove
91
ref
91
ref
94
remove
appTerm
370
ref
appTerm
appTerm
370
ref
appTerm
376
def
appTerm
absTerm
appTerm
absTerm
128
remove
appTerm
betaConv
appThm
115
remove
374
remove
appTerm
refl
89
ref
90
ref
169
ref
369
remove
91
ref
93
remove
370
remove
appTerm
appTerm
376
remove
appTerm
absTerm
appTerm
absTerm
absTerm
377
def
126
remove
appTerm
betaConv
appThm
nil
104
remove
359
remove
appTerm
377
remove
appTerm
axiom
134
remove
appThm
eqMp
130
remove
appThm
eqMp
375
remove
assume
eqMp
nil
89
ref
169
ref
372
ref
appTerm
nil
cons
cons
90
ref
373
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
196
ref
195
ref
372
remove
nil
cons
cons
222
ref
367
remove
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
proveHyp
proveHyp
proveHyp
appThm
238
remove
refl
appThm
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
123
remove
201
remove
cons
124
remove
203
remove
cons
nil
cons
cons
nil
cons
cons
135
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
89
ref
96
ref
168
remove
appTerm
194
remove
appTerm
nil
cons
cons
90
ref
172
ref
44
ref
appTerm
nil
cons
378
def
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
91
ref
refl
379
def
96
ref
refl
44
ref
49
remove
appTerm
betaConv
appThm
169
ref
refl
170
remove
172
ref
refl
380
def
173
remove
379
remove
44
ref
174
remove
appTerm
betaConv
appThm
44
ref
182
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
380
remove
18
ref
46
remove
absThm
appThm
appThm
nil
"p"
171
remove
var
44
remove
nil
cons
381
def
cons
nil
cons
nil
cons
cons
197
remove
"p"
1
ref
16
remove
318
remove
opType
382
def
4
ref
cons
opType
383
def
var
384
def
91
ref
96
remove
384
remove
varTerm
385
def
48
remove
382
ref
constTerm
appTerm
appTerm
64
ref
"h"
61
ref
var
386
def
0
ref
1
ref
383
ref
4
ref
cons
opType
387
def
constTerm
388
def
"t"
382
ref
var
389
def
91
remove
385
ref
389
remove
varTerm
390
def
appTerm
appTerm
385
ref
180
remove
1
ref
61
remove
1
ref
382
ref
382
ref
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
386
remove
varTerm
appTerm
390
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
388
remove
"l"
382
remove
var
391
def
385
ref
391
remove
varTerm
appTerm
absTerm
appTerm
appTerm
absTerm
392
def
385
ref
appTerm
393
def
betaConv
nil
0
remove
1
remove
387
ref
4
remove
cons
opType
constTerm
392
ref
appTerm
394
def
axiom
nil
89
ref
394
remove
nil
cons
cons
90
ref
393
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
"A"
383
ref
nil
cons
cons
nil
cons
"P"
387
remove
var
392
remove
nil
cons
cons
"x"
383
remove
var
385
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
subst
eqMp
eqMp
nil
89
ref
378
remove
cons
90
ref
45
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
199
remove
198
ref
381
remove
cons
224
remove
29
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
43
remove
nil
cons
cons
90
ref
42
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
41
remove
nil
cons
cons
141
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
nil
89
ref
40
remove
nil
cons
cons
90
ref
39
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
ref
47
ref
38
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
395
def
subst
nil
8
ref
34
remove
36
remove
21
ref
appTerm
396
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
8
ref
14
ref
31
remove
23
ref
appTerm
27
ref
appTerm
appTerm
27
ref
appTerm
absTerm
397
def
27
ref
appTerm
398
def
betaConv
nil
6
ref
397
ref
appTerm
399
def
axiom
nil
89
ref
399
remove
nil
cons
cons
90
ref
398
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
55
remove
47
ref
397
remove
nil
cons
cons
150
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
subst
trans
152
remove
12
ref
153
remove
396
remove
appTerm
20
ref
appTerm
absTerm
400
def
20
remove
appTerm
401
def
betaConv
nil
11
ref
400
ref
appTerm
402
def
axiom
nil
89
ref
402
remove
nil
cons
cons
90
ref
401
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
proveHyp
256
remove
257
remove
400
remove
nil
cons
cons
273
remove
cons
nil
cons
cons
149
ref
subst
eqMp
eqMp
appThm
trans
appThm
262
ref
refl
appThm
nil
8
ref
262
ref
nil
cons
cons
nil
cons
nil
cons
cons
166
remove
subst
trans
absThm
appThm
nil
77
ref
354
remove
cons
nil
cons
nil
cons
cons
403
def
340
remove
77
ref
60
remove
64
remove
69
remove
78
ref
absTerm
appTerm
appTerm
78
ref
appTerm
absTerm
404
def
78
ref
appTerm
405
def
betaConv
nil
169
remove
404
ref
appTerm
406
def
axiom
nil
89
remove
406
remove
nil
cons
cons
90
remove
405
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
remove
subst
proveHyp
196
remove
195
remove
404
remove
nil
cons
cons
222
remove
78
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
149
remove
subst
eqMp
eqMp
407
def
subst
subst
trans
absThm
appThm
403
remove
57
remove
407
remove
subst
subst
trans
sym
81
remove
eqMp
nil
6
ref
8
ref
11
remove
12
remove
14
remove
25
remove
23
remove
appTerm
27
remove
appTerm
21
remove
appTerm
appTerm
262
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
47
ref
22
ref
6
ref
8
ref
172
remove
18
ref
37
ref
absTerm
408
def
appTerm
409
def
absTerm
410
def
appTerm
411
def
absTerm
412
def
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
22
remove
nil
77
ref
411
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
47
remove
410
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
remove
subst
8
remove
nil
77
ref
409
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
198
remove
408
remove
nil
cons
cons
nil
cons
nil
cons
cons
200
remove
subst
18
remove
nil
77
remove
37
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
remove
subst
395
remove
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
6
remove
412
remove
appTerm
thm