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