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