6
version
"Data.List.nubReverse"
"setify"
"->"
typeOp
0
def
"Data.List.list"
typeOp
"A"
varType
1
def
nil
cons
2
def
opType
3
def
3
ref
nil
cons
4
def
cons
opType
5
def
var
6
def
nil
cons
cons
nil
cons
6
ref
"Data.Bool./\\"
const
0
ref
"bool"
typeOp
nil
opType
7
def
0
ref
7
ref
7
ref
nil
cons
8
def
cons
opType
9
def
nil
cons
cons
opType
10
def
constTerm
11
def
"="
const
12
def
0
ref
3
ref
0
ref
3
ref
8
ref
cons
opType
13
def
nil
cons
14
def
cons
opType
constTerm
15
def
6
remove
varTerm
16
def
"Data.List.[]"
const
3
ref
constTerm
17
def
appTerm
appTerm
17
ref
appTerm
appTerm
"Data.Bool.!"
const
18
def
0
ref
0
ref
1
ref
8
ref
cons
opType
19
def
8
ref
cons
opType
20
def
constTerm
21
def
"h"
1
ref
var
22
def
18
ref
0
ref
13
ref
8
ref
cons
opType
constTerm
23
def
"t"
3
ref
var
24
def
15
ref
16
ref
"Data.List.::"
const
0
ref
1
ref
5
ref
nil
cons
25
def
cons
opType
constTerm
22
ref
varTerm
26
def
appTerm
27
def
24
ref
varTerm
28
def
appTerm
29
def
appTerm
appTerm
"Data.Bool.cond"
const
0
ref
7
ref
0
ref
3
ref
25
ref
cons
opType
nil
cons
30
def
cons
opType
constTerm
"Data.List.member"
const
0
ref
1
ref
14
remove
cons
opType
constTerm
26
ref
appTerm
28
ref
appTerm
appTerm
31
def
16
ref
28
ref
appTerm
32
def
appTerm
27
ref
32
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
33
def
refl
34
def
12
ref
0
ref
5
ref
0
ref
5
ref
8
ref
cons
opType
35
def
nil
cons
cons
opType
constTerm
16
ref
appTerm
"select"
const
36
def
0
ref
35
ref
25
ref
cons
opType
constTerm
37
def
33
ref
appTerm
appTerm
assume
sym
appThm
33
ref
16
remove
appTerm
betaConv
trans
"A"
25
remove
cons
nil
cons
nil
nil
cons
38
def
cons
nil
12
ref
0
ref
20
ref
0
ref
20
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
39
def
"Data.Bool.?"
const
40
def
20
ref
constTerm
appTerm
"p"
19
ref
var
41
def
41
ref
varTerm
42
def
36
remove
0
ref
19
ref
2
ref
cons
opType
constTerm
42
ref
appTerm
appTerm
absTerm
appTerm
axiom
subst
34
remove
appThm
"p"
35
ref
var
43
def
43
remove
varTerm
44
def
37
remove
44
remove
appTerm
appTerm
absTerm
33
remove
appTerm
betaConv
trans
40
ref
0
ref
35
remove
8
ref
cons
opType
constTerm
refl
"fn"
5
ref
var
45
def
11
ref
15
ref
45
remove
varTerm
46
def
17
ref
appTerm
appTerm
17
ref
appTerm
appTerm
refl
21
ref
refl
22
ref
23
ref
refl
24
ref
15
ref
46
ref
29
ref
appTerm
appTerm
refl
22
ref
24
ref
"_16294"
3
ref
var
47
def
31
ref
47
remove
varTerm
48
def
appTerm
27
ref
48
remove
appTerm
appTerm
absTerm
49
def
absTerm
50
def
absTerm
51
def
26
ref
appTerm
betaConv
28
ref
refl
appThm
50
remove
28
ref
appTerm
betaConv
trans
46
remove
28
ref
appTerm
52
def
refl
appThm
49
remove
52
remove
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
0
ref
1
ref
30
remove
cons
opType
var
51
remove
nil
cons
cons
"b"
3
ref
var
17
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
"A"
2
remove
cons
"B"
4
ref
cons
nil
cons
cons
38
ref
cons
"f"
0
ref
1
ref
0
ref
3
ref
0
ref
"B"
varType
53
def
53
ref
nil
cons
54
def
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
55
def
var
56
def
40
remove
0
ref
0
ref
0
ref
3
ref
54
ref
cons
opType
57
def
8
ref
cons
opType
8
ref
cons
opType
constTerm
"fn"
57
remove
var
58
def
11
ref
12
ref
0
ref
53
ref
0
ref
53
ref
8
ref
cons
opType
59
def
nil
cons
cons
opType
constTerm
60
def
58
remove
varTerm
61
def
17
ref
appTerm
appTerm
"b"
53
ref
var
62
def
varTerm
63
def
appTerm
appTerm
21
ref
22
ref
23
ref
24
ref
60
remove
61
ref
29
ref
appTerm
appTerm
56
remove
varTerm
64
def
26
remove
appTerm
28
ref
appTerm
61
remove
28
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
65
def
64
ref
appTerm
66
def
betaConv
62
remove
18
ref
0
ref
0
ref
55
ref
8
ref
cons
opType
67
def
8
ref
cons
opType
constTerm
65
ref
appTerm
68
def
absTerm
69
def
63
ref
appTerm
70
def
betaConv
nil
18
remove
0
ref
59
ref
8
ref
cons
opType
constTerm
69
ref
appTerm
71
def
axiom
nil
"p"
7
ref
var
72
def
71
remove
nil
cons
cons
"q"
7
ref
var
73
def
70
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
12
ref
10
ref
constTerm
74
def
"Data.Bool.==>"
const
10
ref
constTerm
75
def
72
ref
varTerm
76
def
appTerm
73
ref
varTerm
77
def
appTerm
78
def
appTerm
refl
72
ref
73
ref
74
ref
11
ref
76
ref
appTerm
79
def
77
ref
appTerm
80
def
appTerm
81
def
76
ref
appTerm
absTerm
82
def
absTerm
83
def
76
ref
appTerm
betaConv
77
ref
refl
84
def
appThm
82
remove
77
ref
appTerm
betaConv
trans
appThm
nil
12
ref
0
ref
10
ref
0
ref
10
ref
8
ref
cons
opType
85
def
nil
cons
cons
opType
constTerm
86
def
75
remove
appTerm
83
remove
appTerm
axiom
76
ref
refl
87
def
appThm
84
ref
appThm
eqMp
88
def
sym
89
def
81
remove
refl
73
ref
12
ref
0
ref
85
ref
0
ref
85
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
90
def
"f"
10
remove
var
91
def
91
ref
varTerm
92
def
76
ref
appTerm
77
ref
appTerm
absTerm
93
def
appTerm
91
ref
92
ref
"Data.Bool.T"
const
7
ref
constTerm
94
def
appTerm
94
ref
appTerm
absTerm
95
def
appTerm
absTerm
96
def
77
ref
appTerm
betaConv
appThm
12
ref
0
ref
9
ref
0
ref
9
remove
8
remove
cons
opType
nil
cons
cons
opType
constTerm
97
def
79
remove
appTerm
refl
72
ref
96
remove
absTerm
98
def
76
ref
appTerm
betaConv
appThm
nil
86
remove
11
ref
appTerm
98
ref
appTerm
axiom
99
def
87
remove
appThm
eqMp
84
ref
appThm
eqMp
100
def
sym
91
ref
92
ref
refl
nil
"t"
7
ref
var
101
def
76
ref
nil
cons
102
def
cons
nil
cons
nil
cons
cons
74
ref
101
ref
varTerm
103
def
appTerm
94
ref
appTerm
assume
sym
nil
94
ref
axiom
104
def
eqMp
103
remove
assume
104
ref
deductAntisym
deductAntisym
105
def
subst
76
ref
assume
106
def
eqMp
appThm
nil
101
ref
77
ref
nil
cons
107
def
cons
nil
cons
nil
cons
cons
105
ref
subst
77
ref
assume
eqMp
appThm
absThm
eqMp
108
def
nil
"P"
7
ref
var
109
def
102
remove
cons
"Q"
7
remove
var
110
def
107
remove
cons
nil
cons
cons
nil
cons
cons
74
ref
refl
111
def
91
ref
92
remove
109
ref
varTerm
112
def
appTerm
113
def
110
ref
varTerm
114
def
appTerm
absTerm
115
def
72
ref
73
ref
76
ref
absTerm
absTerm
116
def
appTerm
betaConv
116
ref
112
ref
appTerm
betaConv
114
ref
refl
117
def
appThm
73
ref
112
ref
absTerm
114
ref
appTerm
betaConv
trans
trans
appThm
95
ref
116
ref
appTerm
betaConv
116
ref
94
ref
appTerm
betaConv
94
ref
refl
118
def
appThm
73
ref
94
ref
absTerm
94
ref
appTerm
betaConv
trans
trans
appThm
74
ref
11
remove
112
ref
appTerm
119
def
114
ref
appTerm
120
def
appTerm
refl
73
ref
90
remove
91
remove
113
remove
77
ref
appTerm
absTerm
appTerm
95
ref
appTerm
absTerm
114
ref
appTerm
betaConv
appThm
97
remove
119
remove
appTerm
refl
98
remove
112
ref
appTerm
betaConv
appThm
99
remove
112
ref
refl
appThm
eqMp
117
ref
appThm
eqMp
120
remove
assume
eqMp
121
def
116
remove
refl
appThm
eqMp
sym
104
ref
eqMp
122
def
subst
deductAntisym
eqMp
88
remove
78
remove
assume
eqMp
sym
106
remove
eqMp
111
ref
93
remove
72
ref
73
ref
77
ref
absTerm
123
def
absTerm
124
def
appTerm
betaConv
124
ref
76
remove
appTerm
betaConv
84
remove
appThm
123
ref
77
remove
appTerm
betaConv
trans
trans
appThm
95
remove
124
ref
appTerm
betaConv
124
ref
94
ref
appTerm
betaConv
118
remove
appThm
123
ref
94
ref
appTerm
betaConv
trans
trans
125
def
appThm
100
remove
80
remove
assume
eqMp
124
ref
refl
126
def
appThm
eqMp
sym
104
ref
eqMp
127
def
proveHyp
deductAntisym
128
def
subst
proveHyp
"A"
54
remove
cons
nil
cons
"P"
59
remove
var
69
remove
nil
cons
cons
"x"
53
remove
var
63
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
72
ref
21
ref
"P"
19
ref
var
varTerm
129
def
appTerm
130
def
nil
cons
131
def
cons
73
ref
129
ref
"x"
1
remove
var
132
def
varTerm
133
def
appTerm
134
def
nil
cons
135
def
cons
nil
cons
cons
nil
cons
cons
136
def
89
remove
subst
136
remove
127
remove
108
remove
deductAntisym
subst
74
ref
134
remove
appTerm
refl
132
remove
94
remove
absTerm
137
def
133
ref
appTerm
betaConv
appThm
41
remove
12
remove
0
remove
19
remove
20
remove
nil
cons
cons
opType
constTerm
42
remove
appTerm
137
remove
appTerm
absTerm
138
def
129
ref
appTerm
betaConv
139
def
nil
39
remove
21
ref
appTerm
138
remove
appTerm
axiom
129
remove
refl
appThm
140
def
130
ref
assume
eqMp
eqMp
133
remove
refl
appThm
eqMp
sym
104
ref
eqMp
eqMp
nil
109
ref
131
remove
cons
110
ref
135
remove
cons
nil
cons
cons
nil
cons
cons
122
ref
subst
deductAntisym
eqMp
141
def
subst
eqMp
eqMp
nil
72
remove
68
remove
nil
cons
cons
73
remove
66
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
128
remove
subst
proveHyp
"A"
55
ref
nil
cons
cons
nil
cons
"P"
67
remove
var
65
remove
nil
cons
cons
"x"
55
remove
var
64
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
141
remove
subst
eqMp
eqMp
subst
subst
eqMp
eqMp
eqMp
defineConstList
142
def
pop
143
def
pop
142
ref
nil
109
remove
15
ref
143
remove
hdTl
pop
5
ref
constTerm
144
def
17
ref
appTerm
appTerm
17
remove
appTerm
145
def
nil
cons
cons
110
remove
21
remove
22
remove
23
ref
24
remove
15
ref
144
ref
29
remove
appTerm
appTerm
31
remove
144
ref
28
remove
appTerm
146
def
appTerm
27
remove
146
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
147
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
def
111
remove
115
remove
124
ref
appTerm
betaConv
124
remove
112
remove
appTerm
betaConv
117
remove
appThm
123
remove
114
remove
appTerm
betaConv
trans
trans
appThm
125
remove
appThm
121
remove
126
remove
appThm
eqMp
sym
104
remove
eqMp
subst
proveHyp
nil
147
remove
thm
142
remove
148
remove
122
remove
subst
proveHyp
nil
145
remove
thm
nil
"P"
13
remove
var
"l"
3
ref
var
149
def
15
ref
"Data.List.nub"
"_16297"
3
remove
var
150
def
"Data.List.reverse"
const
5
ref
constTerm
151
def
144
ref
151
ref
150
ref
varTerm
152
def
appTerm
appTerm
appTerm
153
def
absTerm
154
def
defineConst
155
def
pop
5
remove
constTerm
156
def
149
remove
varTerm
157
def
appTerm
appTerm
151
ref
144
remove
151
remove
157
remove
appTerm
appTerm
appTerm
appTerm
absTerm
158
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
4
remove
cons
nil
cons
38
remove
cons
74
remove
130
remove
appTerm
refl
139
remove
appThm
140
remove
eqMp
sym
subst
subst
150
remove
nil
101
remove
15
remove
156
remove
152
ref
appTerm
appTerm
153
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
105
remove
subst
155
remove
152
ref
refl
appThm
154
remove
152
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
23
remove
158
remove
appTerm
thm