6
version
nil
"P"
"->"
typeOp
0
def
"Set.set"
typeOp
1
def
"Data.Pair.*"
typeOp
"A"
varType
2
def
"B"
varType
3
def
nil
cons
4
def
cons
opType
5
def
nil
cons
6
def
opType
7
def
"bool"
typeOp
nil
opType
8
def
nil
cons
9
def
cons
opType
10
def
var
"s"
7
ref
var
11
def
"Data.Bool.!"
const
12
def
0
ref
0
ref
2
ref
9
ref
cons
opType
13
def
9
ref
cons
opType
14
def
constTerm
15
def
"x"
2
ref
var
16
def
12
ref
0
ref
0
ref
3
ref
9
ref
cons
opType
17
def
9
ref
cons
opType
18
def
constTerm
19
def
"y"
3
ref
var
20
def
"="
const
21
def
0
ref
8
ref
0
ref
8
ref
9
ref
cons
opType
22
def
nil
cons
cons
opType
23
def
constTerm
24
def
"Relation.fromSet"
"_11143"
7
ref
var
25
def
"_11144"
2
ref
var
26
def
"_11145"
3
ref
var
27
def
"Set.member"
const
0
ref
5
ref
10
ref
nil
cons
28
def
cons
opType
constTerm
29
def
"Data.Pair.,"
const
0
ref
2
ref
0
ref
3
remove
6
remove
cons
opType
nil
cons
cons
opType
constTerm
30
def
26
ref
varTerm
31
def
appTerm
27
ref
varTerm
32
def
appTerm
appTerm
25
ref
varTerm
33
def
appTerm
34
def
absTerm
35
def
absTerm
36
def
absTerm
37
def
defineConst
38
def
pop
0
ref
7
ref
0
ref
2
ref
17
ref
nil
cons
cons
opType
39
def
nil
cons
40
def
cons
opType
constTerm
41
def
11
remove
varTerm
42
def
appTerm
16
ref
varTerm
43
def
appTerm
20
ref
varTerm
44
def
appTerm
appTerm
29
remove
30
remove
43
ref
appTerm
44
ref
appTerm
45
def
appTerm
42
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
46
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
7
ref
nil
cons
47
def
cons
nil
cons
nil
nil
cons
48
def
cons
24
ref
15
ref
"P"
13
ref
var
49
def
varTerm
50
def
appTerm
appTerm
refl
"p"
13
ref
var
51
def
21
ref
0
ref
13
ref
14
ref
nil
cons
cons
opType
constTerm
51
remove
varTerm
appTerm
16
ref
"Data.Bool.T"
const
8
ref
constTerm
52
def
absTerm
appTerm
absTerm
53
def
50
ref
appTerm
betaConv
appThm
nil
21
ref
0
ref
14
ref
0
ref
14
ref
9
ref
cons
opType
nil
cons
cons
opType
constTerm
15
ref
appTerm
53
remove
appTerm
axiom
50
remove
refl
appThm
eqMp
sym
54
def
subst
subst
25
remove
nil
"t"
8
remove
var
55
def
15
ref
26
ref
19
remove
27
ref
24
ref
41
ref
33
ref
appTerm
31
ref
appTerm
32
ref
appTerm
appTerm
34
remove
appTerm
56
def
absTerm
57
def
appTerm
58
def
absTerm
59
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
24
ref
55
ref
varTerm
60
def
appTerm
52
ref
appTerm
assume
sym
nil
52
remove
axiom
61
def
eqMp
60
remove
assume
61
remove
deductAntisym
deductAntisym
62
def
subst
nil
49
remove
59
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
26
remove
nil
55
ref
58
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
"P"
17
remove
var
57
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
4
remove
cons
nil
cons
48
ref
cons
54
ref
subst
subst
27
remove
nil
55
ref
56
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
38
remove
33
ref
refl
appThm
37
remove
33
remove
appTerm
betaConv
trans
31
ref
refl
appThm
36
remove
31
remove
appTerm
betaConv
trans
32
ref
refl
appThm
35
remove
32
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
12
ref
0
ref
10
remove
9
ref
cons
opType
constTerm
46
remove
appTerm
thm
nil
"P"
0
ref
39
ref
9
ref
cons
opType
63
def
var
64
def
"r"
39
ref
var
65
def
21
ref
0
ref
7
ref
28
remove
cons
opType
66
def
constTerm
67
def
"Relation.toSet"
"_11164"
39
ref
var
68
def
"Set.fromPredicate"
const
69
def
0
ref
0
ref
5
ref
9
ref
cons
opType
70
def
47
ref
cons
opType
constTerm
71
def
"v"
5
ref
var
72
def
"Data.Bool.?"
const
73
def
14
remove
constTerm
74
def
16
ref
73
ref
18
remove
constTerm
75
def
20
ref
"Data.Bool./\\"
const
23
ref
constTerm
76
def
21
ref
0
ref
5
remove
70
remove
nil
cons
cons
opType
constTerm
72
ref
varTerm
appTerm
45
remove
appTerm
appTerm
77
def
68
ref
varTerm
78
def
43
ref
appTerm
44
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
79
def
absTerm
80
def
defineConst
81
def
pop
0
ref
39
ref
47
ref
cons
opType
82
def
constTerm
83
def
65
ref
varTerm
84
def
appTerm
85
def
appTerm
71
remove
72
remove
74
remove
16
ref
75
remove
20
remove
77
remove
84
ref
43
ref
appTerm
44
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
86
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
40
ref
cons
nil
cons
48
ref
cons
54
ref
subst
87
def
subst
68
remove
nil
55
ref
67
remove
83
ref
78
ref
appTerm
appTerm
79
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
81
remove
78
ref
refl
appThm
80
remove
78
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
12
ref
0
ref
63
ref
9
ref
cons
opType
constTerm
88
def
86
remove
appTerm
thm
"Relation.empty"
41
ref
"Set.{}"
const
7
ref
constTerm
appTerm
89
def
defineConst
90
def
pop
91
def
pop
90
remove
nil
21
ref
0
ref
39
ref
63
remove
nil
cons
cons
opType
92
def
constTerm
93
def
91
remove
39
ref
constTerm
appTerm
89
remove
appTerm
thm
"Relation.universe"
41
ref
"Set.universe"
const
7
ref
constTerm
appTerm
94
def
defineConst
95
def
pop
96
def
pop
95
remove
nil
93
ref
96
remove
39
ref
constTerm
appTerm
94
remove
appTerm
thm
nil
64
ref
65
ref
88
ref
"s"
39
ref
var
97
def
24
ref
"Relation.subrelation"
"_11169"
39
ref
var
98
def
"_11170"
39
ref
var
99
def
"Set.subset"
const
66
remove
constTerm
100
def
83
ref
98
ref
varTerm
101
def
appTerm
appTerm
83
ref
99
ref
varTerm
102
def
appTerm
appTerm
103
def
absTerm
104
def
absTerm
105
def
defineConst
106
def
pop
107
def
92
remove
constTerm
108
def
84
ref
appTerm
97
ref
varTerm
109
def
appTerm
appTerm
100
remove
85
ref
appTerm
83
ref
109
ref
appTerm
110
def
appTerm
appTerm
absTerm
appTerm
absTerm
111
def
nil
cons
cons
nil
cons
nil
cons
cons
87
ref
subst
98
remove
nil
55
ref
88
ref
99
ref
24
ref
108
remove
101
ref
appTerm
102
ref
appTerm
appTerm
103
remove
appTerm
112
def
absTerm
113
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
64
ref
113
remove
nil
cons
cons
nil
cons
nil
cons
cons
87
ref
subst
99
remove
nil
55
ref
112
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
106
remove
101
ref
refl
appThm
105
remove
101
remove
appTerm
betaConv
trans
102
ref
refl
appThm
104
remove
102
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
88
ref
111
remove
appTerm
thm
nil
64
ref
65
ref
88
ref
97
ref
93
ref
"Relation.union"
"_11181"
39
ref
var
114
def
"_11182"
39
ref
var
115
def
41
ref
"Set.union"
const
0
ref
7
ref
0
ref
7
remove
47
ref
cons
opType
nil
cons
cons
opType
116
def
constTerm
117
def
83
ref
114
ref
varTerm
118
def
appTerm
appTerm
83
ref
115
ref
varTerm
119
def
appTerm
appTerm
appTerm
120
def
absTerm
121
def
absTerm
122
def
defineConst
123
def
pop
0
ref
39
ref
0
ref
39
ref
40
ref
cons
opType
nil
cons
cons
opType
124
def
constTerm
125
def
84
ref
appTerm
109
ref
appTerm
appTerm
41
ref
117
remove
85
ref
appTerm
110
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
126
def
nil
cons
cons
nil
cons
nil
cons
cons
87
ref
subst
114
remove
nil
55
ref
88
ref
115
ref
93
ref
125
remove
118
ref
appTerm
119
ref
appTerm
appTerm
120
remove
appTerm
127
def
absTerm
128
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
64
ref
128
remove
nil
cons
cons
nil
cons
nil
cons
cons
87
ref
subst
115
remove
nil
55
ref
127
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
123
remove
118
ref
refl
appThm
122
remove
118
remove
appTerm
betaConv
trans
119
ref
refl
appThm
121
remove
119
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
88
ref
126
remove
appTerm
thm
nil
64
ref
65
remove
88
ref
97
remove
93
ref
"Relation.intersect"
"_11193"
39
ref
var
129
def
"_11194"
39
remove
var
130
def
41
ref
"Set.intersect"
const
116
remove
constTerm
131
def
83
ref
129
ref
varTerm
132
def
appTerm
appTerm
83
ref
130
ref
varTerm
133
def
appTerm
appTerm
appTerm
134
def
absTerm
135
def
absTerm
136
def
defineConst
137
def
pop
124
remove
constTerm
138
def
84
remove
appTerm
109
remove
appTerm
appTerm
41
ref
131
remove
85
remove
appTerm
110
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
139
def
nil
cons
cons
nil
cons
nil
cons
cons
87
ref
subst
129
remove
nil
55
ref
88
ref
130
ref
93
ref
138
remove
132
ref
appTerm
133
ref
appTerm
appTerm
134
remove
appTerm
140
def
absTerm
141
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
64
remove
141
remove
nil
cons
cons
nil
cons
nil
cons
cons
87
remove
subst
130
remove
nil
55
ref
140
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
137
remove
132
ref
refl
appThm
136
remove
132
remove
appTerm
betaConv
trans
133
ref
refl
appThm
135
remove
133
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
88
remove
139
remove
appTerm
thm
nil
"P"
0
ref
1
ref
40
ref
opType
142
def
9
ref
cons
opType
143
def
var
144
def
"s"
142
ref
var
145
def
93
ref
"Relation.bigUnion"
"_11205"
142
ref
var
146
def
41
ref
"Set.bigUnion"
const
0
ref
1
ref
47
ref
opType
147
def
47
remove
cons
opType
148
def
constTerm
149
def
"Set.image"
const
0
ref
82
remove
0
ref
142
ref
147
remove
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
83
remove
appTerm
150
def
146
ref
varTerm
151
def
appTerm
appTerm
appTerm
152
def
absTerm
153
def
defineConst
154
def
pop
0
ref
142
ref
40
remove
cons
opType
155
def
constTerm
156
def
145
ref
varTerm
157
def
appTerm
appTerm
41
ref
149
remove
150
ref
157
ref
appTerm
158
def
appTerm
appTerm
appTerm
absTerm
159
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
142
ref
nil
cons
cons
nil
cons
48
ref
cons
54
ref
subst
160
def
subst
146
remove
nil
55
ref
93
ref
156
remove
151
ref
appTerm
appTerm
152
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
154
remove
151
ref
refl
appThm
153
remove
151
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
12
ref
0
ref
143
remove
9
ref
cons
opType
constTerm
161
def
159
remove
appTerm
thm
nil
144
remove
145
remove
93
ref
"Relation.bigIntersect"
"_11210"
142
remove
var
162
def
41
ref
"Set.bigIntersect"
const
148
remove
constTerm
163
def
150
remove
162
ref
varTerm
164
def
appTerm
appTerm
appTerm
165
def
absTerm
166
def
defineConst
167
def
pop
168
def
155
remove
constTerm
169
def
157
remove
appTerm
appTerm
41
remove
163
remove
158
remove
appTerm
appTerm
appTerm
absTerm
170
def
nil
cons
cons
nil
cons
nil
cons
cons
160
remove
subst
162
remove
nil
55
ref
93
remove
169
remove
164
ref
appTerm
appTerm
165
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
167
remove
164
ref
refl
appThm
166
remove
164
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
161
remove
170
remove
appTerm
thm
nil
"P"
0
ref
0
ref
2
ref
13
remove
nil
cons
cons
opType
171
def
9
ref
cons
opType
172
def
var
173
def
"r"
171
ref
var
174
def
24
ref
"Relation.reflexive"
"_11215"
171
ref
var
175
def
15
ref
16
ref
175
ref
varTerm
176
def
43
ref
appTerm
43
ref
appTerm
absTerm
appTerm
177
def
absTerm
178
def
defineConst
179
def
pop
172
ref
constTerm
180
def
174
ref
varTerm
181
def
appTerm
appTerm
15
ref
16
ref
181
ref
43
ref
appTerm
182
def
43
ref
appTerm
183
def
absTerm
appTerm
appTerm
absTerm
184
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
171
ref
nil
cons
185
def
cons
nil
cons
48
remove
cons
54
remove
subst
186
def
subst
175
remove
nil
55
ref
24
ref
180
remove
176
ref
appTerm
appTerm
177
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
179
remove
176
ref
refl
appThm
178
remove
176
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
12
remove
0
ref
172
ref
9
remove
cons
opType
187
def
constTerm
188
def
184
remove
appTerm
thm
nil
173
ref
174
ref
24
ref
"Relation.irreflexive"
"_11220"
171
ref
var
189
def
15
ref
16
ref
"Data.Bool.~"
const
22
remove
constTerm
190
def
189
ref
varTerm
191
def
43
ref
appTerm
43
ref
appTerm
appTerm
absTerm
appTerm
192
def
absTerm
193
def
defineConst
194
def
pop
172
ref
constTerm
195
def
181
ref
appTerm
appTerm
15
ref
16
ref
190
remove
183
remove
appTerm
absTerm
appTerm
appTerm
absTerm
196
def
nil
cons
cons
nil
cons
nil
cons
cons
186
ref
subst
189
remove
nil
55
ref
24
ref
195
remove
191
ref
appTerm
appTerm
192
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
194
remove
191
ref
refl
appThm
193
remove
191
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
188
ref
196
remove
appTerm
thm
nil
173
ref
174
ref
24
ref
"Relation.transitive"
"_11225"
171
ref
var
197
def
15
ref
16
ref
15
ref
"y"
2
ref
var
198
def
15
ref
"z"
2
remove
var
199
def
"Data.Bool.==>"
const
23
remove
constTerm
200
def
76
ref
197
ref
varTerm
201
def
43
remove
appTerm
202
def
198
ref
varTerm
203
def
appTerm
appTerm
201
ref
203
ref
appTerm
199
ref
varTerm
204
def
appTerm
appTerm
appTerm
202
remove
204
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
205
def
absTerm
206
def
defineConst
207
def
pop
172
ref
constTerm
208
def
181
ref
appTerm
appTerm
15
ref
16
remove
15
ref
198
remove
15
remove
199
remove
200
remove
76
ref
182
ref
203
ref
appTerm
appTerm
181
ref
203
remove
appTerm
204
ref
appTerm
appTerm
appTerm
182
remove
204
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
209
def
nil
cons
cons
nil
cons
nil
cons
cons
186
ref
subst
197
remove
nil
55
ref
24
remove
208
ref
201
ref
appTerm
appTerm
205
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
207
remove
201
ref
refl
appThm
206
remove
201
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
188
ref
209
remove
appTerm
thm
nil
173
remove
174
remove
21
remove
0
ref
171
ref
172
ref
nil
cons
cons
opType
210
def
constTerm
211
def
"Relation.transitiveClosure"
"_11230"
171
ref
var
212
def
168
remove
0
ref
1
remove
185
ref
opType
213
def
185
ref
cons
opType
constTerm
214
def
69
remove
0
ref
172
remove
213
remove
nil
cons
cons
opType
constTerm
215
def
"v"
171
ref
var
216
def
73
remove
187
remove
constTerm
217
def
"s"
171
ref
var
218
def
76
ref
211
ref
216
ref
varTerm
appTerm
218
ref
varTerm
219
def
appTerm
appTerm
220
def
76
ref
107
remove
210
remove
constTerm
221
def
212
ref
varTerm
222
def
appTerm
219
ref
appTerm
appTerm
208
remove
219
ref
appTerm
223
def
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
224
def
absTerm
225
def
defineConst
226
def
pop
0
remove
171
remove
185
remove
cons
opType
constTerm
227
def
181
ref
appTerm
appTerm
214
remove
215
remove
216
remove
217
remove
218
remove
220
remove
76
remove
221
remove
181
remove
appTerm
219
remove
appTerm
appTerm
223
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
228
def
nil
cons
cons
nil
cons
nil
cons
cons
186
remove
subst
212
remove
nil
55
remove
211
remove
227
remove
222
ref
appTerm
appTerm
224
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
remove
subst
226
remove
222
ref
refl
appThm
225
remove
222
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
188
remove
228
remove
appTerm
thm