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