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