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