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