6
version
"Data.List.last"
"LAST"
"->"
typeOp
0
def
"Data.List.list"
typeOp
"A"
varType
1
def
nil
cons
2
def
opType
3
def
2
ref
cons
opType
4
def
var
5
def
nil
cons
cons
nil
cons
5
ref
"Data.Bool.!"
const
6
def
0
ref
0
ref
1
ref
"bool"
typeOp
nil
opType
7
def
nil
cons
8
def
cons
opType
9
def
8
ref
cons
opType
10
def
constTerm
11
def
"h"
1
ref
var
12
def
6
ref
0
ref
0
ref
3
ref
8
ref
cons
opType
13
def
8
ref
cons
opType
constTerm
14
def
"t"
3
ref
var
15
def
"="
const
16
def
0
ref
1
ref
9
ref
nil
cons
cons
opType
constTerm
17
def
5
ref
varTerm
18
def
"Data.List.::"
const
0
ref
1
ref
0
ref
3
ref
3
ref
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
12
ref
varTerm
19
def
appTerm
15
ref
varTerm
20
def
appTerm
21
def
appTerm
appTerm
"Data.Bool.cond"
const
0
ref
7
ref
0
ref
1
ref
0
ref
1
ref
2
ref
cons
opType
nil
cons
22
def
cons
opType
nil
cons
cons
opType
constTerm
"Data.List.null"
const
13
remove
constTerm
20
ref
appTerm
appTerm
19
ref
appTerm
23
def
18
ref
20
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
24
def
absTerm
25
def
refl
26
def
16
ref
0
ref
4
ref
0
ref
4
ref
8
ref
cons
opType
27
def
nil
cons
cons
opType
constTerm
18
ref
appTerm
"select"
const
28
def
0
ref
27
ref
4
ref
nil
cons
29
def
cons
opType
constTerm
30
def
25
ref
appTerm
appTerm
assume
sym
appThm
25
ref
18
ref
appTerm
betaConv
31
def
trans
"A"
29
remove
cons
nil
cons
32
def
nil
nil
cons
33
def
cons
34
def
nil
16
ref
0
ref
10
ref
0
ref
10
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
35
def
"Data.Bool.?"
const
36
def
10
ref
constTerm
37
def
appTerm
38
def
"p"
9
ref
var
39
def
39
ref
varTerm
40
def
28
remove
0
ref
9
ref
2
ref
cons
opType
constTerm
40
ref
appTerm
appTerm
absTerm
appTerm
axiom
subst
26
remove
appThm
"p"
27
ref
var
41
def
41
remove
varTerm
42
def
30
remove
42
remove
appTerm
appTerm
absTerm
25
ref
appTerm
betaConv
trans
36
ref
0
ref
27
ref
8
ref
cons
opType
43
def
constTerm
44
def
refl
"fn"
4
ref
var
45
def
"Data.Bool./\\"
const
0
ref
7
ref
0
ref
7
ref
8
ref
cons
opType
46
def
nil
cons
cons
opType
47
def
constTerm
48
def
17
ref
45
remove
varTerm
49
def
"Data.List.[]"
const
3
ref
constTerm
50
def
appTerm
appTerm
"b"
1
ref
var
varTerm
51
def
appTerm
appTerm
refl
11
ref
refl
12
ref
14
ref
refl
15
ref
17
ref
49
ref
21
ref
appTerm
appTerm
refl
12
ref
15
ref
"_16132"
1
ref
var
52
def
23
ref
52
remove
varTerm
appTerm
absTerm
53
def
absTerm
54
def
absTerm
55
def
19
ref
appTerm
betaConv
20
ref
refl
appThm
54
remove
20
ref
appTerm
betaConv
trans
49
remove
20
ref
appTerm
56
def
refl
appThm
53
remove
56
remove
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
0
ref
1
ref
0
ref
3
ref
22
remove
cons
opType
nil
cons
cons
opType
var
55
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
2
ref
cons
57
def
"B"
2
remove
cons
nil
cons
cons
33
ref
cons
"f"
0
ref
1
ref
0
ref
3
ref
0
ref
"B"
varType
58
def
58
ref
nil
cons
59
def
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
60
def
var
61
def
36
remove
0
ref
0
ref
0
ref
3
remove
59
ref
cons
opType
62
def
8
ref
cons
opType
8
ref
cons
opType
constTerm
"fn"
62
remove
var
63
def
48
ref
16
ref
0
ref
58
ref
0
ref
58
ref
8
ref
cons
opType
64
def
nil
cons
cons
opType
constTerm
65
def
63
remove
varTerm
66
def
50
ref
appTerm
appTerm
"b"
58
ref
var
67
def
varTerm
68
def
appTerm
appTerm
11
ref
12
ref
14
ref
15
ref
65
remove
66
ref
21
ref
appTerm
appTerm
61
remove
varTerm
69
def
19
remove
appTerm
20
ref
appTerm
66
remove
20
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
70
def
69
ref
appTerm
71
def
betaConv
67
remove
6
ref
0
ref
0
ref
60
ref
8
ref
cons
opType
72
def
8
ref
cons
opType
constTerm
70
ref
appTerm
73
def
absTerm
74
def
68
ref
appTerm
75
def
betaConv
nil
6
ref
0
ref
64
ref
8
ref
cons
opType
constTerm
74
ref
appTerm
76
def
axiom
nil
"p"
7
ref
var
77
def
76
remove
nil
cons
cons
"q"
7
ref
var
78
def
75
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
16
ref
47
ref
constTerm
79
def
"Data.Bool.==>"
const
47
ref
constTerm
80
def
77
ref
varTerm
81
def
appTerm
78
ref
varTerm
82
def
appTerm
83
def
appTerm
refl
77
ref
78
ref
79
ref
48
ref
81
ref
appTerm
84
def
82
ref
appTerm
85
def
appTerm
86
def
81
ref
appTerm
absTerm
87
def
absTerm
88
def
81
ref
appTerm
betaConv
82
ref
refl
89
def
appThm
87
remove
82
ref
appTerm
betaConv
trans
appThm
nil
16
ref
0
ref
47
ref
0
ref
47
ref
8
ref
cons
opType
90
def
nil
cons
cons
opType
constTerm
91
def
80
ref
appTerm
88
remove
appTerm
axiom
81
ref
refl
92
def
appThm
89
ref
appThm
eqMp
93
def
sym
94
def
86
remove
refl
78
ref
16
ref
0
ref
90
ref
0
ref
90
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
95
def
"f"
47
remove
var
96
def
96
ref
varTerm
97
def
81
ref
appTerm
82
ref
appTerm
absTerm
98
def
appTerm
96
ref
97
ref
"Data.Bool.T"
const
7
ref
constTerm
99
def
appTerm
99
ref
appTerm
absTerm
100
def
appTerm
absTerm
101
def
82
ref
appTerm
betaConv
appThm
16
ref
0
ref
46
ref
0
ref
46
ref
8
ref
cons
opType
102
def
nil
cons
cons
opType
constTerm
103
def
84
remove
appTerm
refl
77
ref
101
remove
absTerm
104
def
81
ref
appTerm
betaConv
appThm
nil
91
remove
48
ref
appTerm
104
ref
appTerm
axiom
105
def
92
remove
appThm
eqMp
89
ref
appThm
eqMp
106
def
sym
96
ref
97
ref
refl
nil
"t"
7
ref
var
107
def
81
ref
nil
cons
108
def
cons
nil
cons
nil
cons
cons
79
ref
107
ref
varTerm
109
def
appTerm
99
ref
appTerm
assume
sym
nil
99
ref
axiom
110
def
eqMp
109
remove
assume
110
ref
deductAntisym
deductAntisym
111
def
subst
81
ref
assume
112
def
eqMp
appThm
nil
107
ref
82
ref
nil
cons
113
def
cons
nil
cons
nil
cons
cons
111
ref
subst
82
ref
assume
eqMp
appThm
absThm
eqMp
114
def
nil
"P"
7
ref
var
115
def
108
remove
cons
"Q"
7
ref
var
116
def
113
remove
cons
nil
cons
cons
nil
cons
cons
79
ref
refl
117
def
96
ref
97
remove
115
ref
varTerm
118
def
appTerm
119
def
116
ref
varTerm
120
def
appTerm
absTerm
121
def
77
ref
78
ref
81
ref
absTerm
absTerm
122
def
appTerm
betaConv
122
ref
118
ref
appTerm
betaConv
120
ref
refl
123
def
appThm
78
ref
118
ref
absTerm
120
ref
appTerm
betaConv
trans
trans
appThm
100
ref
122
ref
appTerm
betaConv
122
ref
99
ref
appTerm
betaConv
99
ref
refl
124
def
appThm
78
ref
99
ref
absTerm
99
ref
appTerm
betaConv
trans
trans
appThm
79
ref
48
ref
118
ref
appTerm
125
def
120
ref
appTerm
126
def
appTerm
refl
78
ref
95
remove
96
remove
119
remove
82
ref
appTerm
absTerm
appTerm
100
ref
appTerm
absTerm
120
ref
appTerm
betaConv
appThm
103
remove
125
remove
appTerm
refl
104
remove
118
ref
appTerm
betaConv
appThm
105
remove
118
ref
refl
appThm
eqMp
123
ref
appThm
eqMp
126
remove
assume
eqMp
127
def
122
remove
refl
appThm
eqMp
sym
110
ref
eqMp
128
def
subst
129
def
deductAntisym
eqMp
93
remove
83
ref
assume
eqMp
sym
112
ref
eqMp
117
ref
98
remove
77
ref
78
ref
82
ref
absTerm
130
def
absTerm
131
def
appTerm
betaConv
131
ref
81
ref
appTerm
betaConv
89
remove
appThm
130
ref
82
ref
appTerm
betaConv
trans
trans
appThm
100
remove
131
ref
appTerm
betaConv
131
ref
99
ref
appTerm
betaConv
124
remove
appThm
130
ref
99
ref
appTerm
betaConv
trans
trans
132
def
appThm
106
remove
85
remove
assume
eqMp
131
ref
refl
133
def
appThm
eqMp
sym
110
ref
eqMp
134
def
proveHyp
deductAntisym
135
def
subst
proveHyp
"A"
59
remove
cons
nil
cons
"P"
64
remove
var
74
remove
nil
cons
cons
"x"
58
remove
var
68
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
77
ref
11
ref
"P"
9
ref
var
136
def
varTerm
137
def
appTerm
138
def
nil
cons
139
def
cons
78
ref
137
ref
"x"
1
remove
var
140
def
varTerm
141
def
appTerm
142
def
nil
cons
143
def
cons
nil
cons
cons
nil
cons
cons
144
def
94
ref
subst
144
remove
134
remove
114
remove
deductAntisym
145
def
subst
79
ref
142
ref
appTerm
refl
140
ref
99
remove
absTerm
146
def
141
ref
appTerm
betaConv
appThm
39
ref
16
remove
0
remove
9
remove
10
remove
nil
cons
cons
opType
constTerm
40
ref
appTerm
146
remove
appTerm
absTerm
147
def
137
ref
appTerm
betaConv
148
def
nil
35
remove
11
ref
appTerm
147
remove
appTerm
axiom
137
ref
refl
149
def
appThm
150
def
138
ref
assume
eqMp
eqMp
141
ref
refl
appThm
eqMp
sym
110
ref
eqMp
eqMp
nil
115
ref
139
remove
cons
116
ref
143
ref
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
151
def
subst
eqMp
eqMp
nil
77
ref
73
remove
nil
cons
cons
78
ref
71
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
"A"
60
ref
nil
cons
cons
nil
cons
"P"
72
remove
var
70
remove
nil
cons
cons
"x"
60
remove
var
69
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
eqMp
eqMp
subst
subst
eqMp
nil
77
ref
44
ref
5
ref
48
remove
17
ref
18
ref
50
remove
appTerm
appTerm
51
remove
appTerm
152
def
appTerm
24
ref
appTerm
153
def
absTerm
154
def
appTerm
155
def
nil
cons
cons
78
ref
44
remove
25
ref
appTerm
156
def
nil
cons
157
def
cons
nil
cons
158
def
cons
nil
cons
cons
135
ref
subst
nil
"P"
27
remove
var
159
def
5
ref
80
ref
154
ref
18
ref
appTerm
160
def
appTerm
156
ref
appTerm
161
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
34
remove
79
ref
138
remove
appTerm
refl
148
remove
appThm
150
remove
eqMp
sym
162
def
subst
subst
5
remove
nil
107
ref
161
remove
nil
cons
cons
nil
cons
nil
cons
cons
111
ref
subst
nil
77
ref
160
ref
nil
cons
163
def
cons
158
ref
cons
nil
cons
cons
164
def
94
ref
subst
164
remove
145
ref
subst
160
ref
betaConv
160
remove
assume
eqMp
nil
77
ref
153
remove
nil
cons
165
def
cons
158
remove
cons
nil
cons
cons
166
def
135
ref
subst
proveHyp
166
ref
94
ref
subst
166
remove
145
ref
subst
31
remove
sym
nil
115
ref
152
remove
nil
cons
cons
116
ref
24
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
117
remove
121
remove
131
ref
appTerm
betaConv
131
remove
118
remove
appTerm
betaConv
123
remove
appThm
130
remove
120
ref
appTerm
betaConv
trans
trans
appThm
132
remove
appThm
127
remove
133
remove
appThm
eqMp
sym
110
remove
eqMp
subst
eqMp
32
ref
159
ref
25
remove
nil
cons
cons
"x"
4
ref
var
167
def
18
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
79
ref
37
remove
137
ref
appTerm
168
def
appTerm
169
def
refl
39
remove
6
ref
102
remove
constTerm
170
def
78
ref
80
ref
11
ref
140
ref
80
ref
40
remove
141
ref
appTerm
appTerm
82
ref
appTerm
absTerm
appTerm
appTerm
82
ref
appTerm
absTerm
appTerm
absTerm
171
def
137
remove
appTerm
betaConv
appThm
nil
38
remove
171
remove
appTerm
axiom
149
remove
appThm
eqMp
172
def
sym
nil
"P"
46
remove
var
173
def
116
ref
80
ref
11
ref
140
ref
80
ref
142
remove
appTerm
174
def
120
ref
appTerm
absTerm
175
def
appTerm
176
def
appTerm
120
ref
appTerm
177
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
8
remove
cons
nil
cons
178
def
33
remove
cons
162
remove
subst
subst
116
ref
nil
107
remove
177
remove
nil
cons
cons
nil
cons
nil
cons
cons
111
remove
subst
nil
77
ref
176
remove
nil
cons
179
def
cons
180
def
78
ref
120
ref
nil
cons
181
def
cons
nil
cons
182
def
cons
nil
cons
cons
183
def
94
ref
subst
183
ref
145
ref
subst
nil
77
ref
143
remove
cons
182
ref
cons
nil
cons
cons
135
ref
subst
175
ref
141
ref
appTerm
184
def
betaConv
nil
180
ref
78
ref
184
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
57
remove
nil
cons
136
remove
175
remove
nil
cons
cons
140
ref
141
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
115
ref
179
remove
cons
185
def
116
ref
181
ref
cons
nil
cons
186
def
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
eqMp
nil
115
ref
165
remove
cons
116
ref
157
remove
cons
nil
cons
187
def
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
115
ref
163
remove
cons
187
ref
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
77
ref
6
remove
43
remove
constTerm
167
ref
80
ref
154
ref
167
remove
varTerm
appTerm
appTerm
156
ref
appTerm
absTerm
appTerm
nil
cons
cons
78
ref
80
ref
155
remove
appTerm
156
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
32
remove
159
remove
154
remove
nil
cons
cons
187
remove
cons
nil
cons
cons
nil
180
remove
78
ref
80
ref
168
ref
appTerm
188
def
120
ref
appTerm
nil
cons
189
def
cons
nil
cons
cons
nil
cons
cons
190
def
94
ref
subst
190
remove
145
ref
subst
nil
77
ref
168
remove
nil
cons
191
def
cons
192
def
182
remove
cons
nil
cons
cons
193
def
94
ref
subst
193
remove
145
ref
subst
183
remove
135
ref
subst
78
ref
80
remove
11
ref
140
remove
174
remove
82
ref
appTerm
absTerm
appTerm
appTerm
82
ref
appTerm
absTerm
194
def
120
remove
appTerm
195
def
betaConv
nil
192
remove
78
ref
170
remove
194
ref
appTerm
196
def
nil
cons
197
def
cons
nil
cons
cons
nil
cons
cons
198
def
135
ref
subst
172
remove
nil
77
ref
169
remove
196
ref
appTerm
nil
cons
cons
78
ref
188
remove
196
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
198
remove
nil
77
ref
79
remove
81
remove
appTerm
82
remove
appTerm
199
def
nil
cons
200
def
cons
78
ref
83
remove
nil
cons
201
def
cons
nil
cons
cons
nil
cons
cons
202
def
94
ref
subst
202
remove
145
ref
subst
94
remove
145
remove
199
remove
assume
112
remove
eqMp
eqMp
129
remove
deductAntisym
eqMp
eqMp
nil
115
ref
200
remove
cons
116
ref
201
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
77
remove
197
remove
cons
78
remove
195
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
remove
subst
proveHyp
178
remove
173
remove
194
remove
nil
cons
cons
"x"
7
remove
var
181
remove
cons
nil
cons
cons
nil
cons
cons
151
remove
subst
eqMp
eqMp
eqMp
eqMp
nil
115
remove
191
remove
cons
186
remove
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
nil
185
remove
116
remove
189
remove
cons
nil
cons
cons
nil
cons
cons
128
remove
subst
deductAntisym
eqMp
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
203
def
pop
204
def
pop
203
remove
nil
11
remove
12
remove
14
remove
15
remove
17
remove
204
remove
hdTl
pop
4
remove
constTerm
205
def
21
remove
appTerm
appTerm
23
remove
205
remove
20
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm