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