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