6
version
"F"
"!"
"p"
"->"
typeOp
0
def
"A"
varType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
var
5
def
"="
const
6
def
0
ref
4
ref
0
ref
4
ref
3
ref
cons
opType
7
def
nil
cons
cons
opType
constTerm
5
ref
varTerm
8
def
appTerm
"x"
1
ref
var
9
def
"T"
6
ref
0
ref
0
ref
2
ref
3
ref
cons
opType
10
def
0
ref
10
ref
3
ref
cons
opType
11
def
nil
cons
cons
opType
constTerm
12
def
"p"
2
ref
var
13
def
13
ref
varTerm
14
def
absTerm
15
def
appTerm
15
ref
appTerm
16
def
defineConst
17
def
pop
2
ref
constTerm
18
def
absTerm
appTerm
absTerm
19
def
defineConst
20
def
pop
21
def
11
remove
constTerm
22
def
15
remove
appTerm
23
def
defineConst
24
def
pop
25
def
pop
24
remove
nil
6
ref
0
ref
2
ref
10
ref
nil
cons
cons
opType
26
def
constTerm
27
def
25
remove
2
ref
constTerm
28
def
appTerm
23
remove
appTerm
thm
"~"
13
ref
"==>"
13
ref
"q"
2
ref
var
29
def
27
ref
"/\\"
13
ref
29
ref
6
ref
0
ref
0
ref
26
ref
3
ref
cons
opType
30
def
0
ref
30
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
"f"
26
ref
var
31
def
31
ref
varTerm
32
def
14
ref
appTerm
29
ref
varTerm
33
def
appTerm
absTerm
appTerm
31
remove
32
remove
18
ref
appTerm
18
ref
appTerm
absTerm
appTerm
absTerm
absTerm
34
def
defineConst
35
def
pop
26
ref
constTerm
36
def
14
ref
appTerm
33
ref
appTerm
appTerm
14
ref
appTerm
absTerm
absTerm
37
def
defineConst
38
def
pop
26
ref
constTerm
39
def
14
remove
appTerm
40
def
28
ref
appTerm
absTerm
41
def
defineConst
42
def
pop
43
def
pop
42
remove
nil
12
remove
43
remove
10
remove
constTerm
appTerm
41
remove
appTerm
thm
17
remove
nil
27
ref
18
ref
appTerm
16
remove
appTerm
thm
20
remove
nil
6
ref
0
ref
7
ref
0
ref
7
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
44
def
21
remove
7
ref
constTerm
45
def
appTerm
19
remove
appTerm
thm
38
remove
nil
6
ref
0
ref
26
ref
30
remove
nil
cons
cons
opType
constTerm
46
def
39
ref
appTerm
37
remove
appTerm
thm
35
remove
nil
46
ref
36
ref
appTerm
34
remove
appTerm
thm
"?"
5
ref
22
ref
29
ref
39
ref
45
ref
9
ref
39
ref
8
ref
9
ref
varTerm
47
def
appTerm
48
def
appTerm
33
ref
appTerm
absTerm
appTerm
appTerm
33
ref
appTerm
absTerm
appTerm
absTerm
49
def
defineConst
50
def
pop
51
def
pop
50
remove
nil
44
ref
51
remove
7
ref
constTerm
52
def
appTerm
49
remove
appTerm
thm
"\\/"
13
remove
29
remove
22
remove
"r"
2
ref
var
53
def
39
ref
40
remove
53
remove
varTerm
54
def
appTerm
appTerm
39
ref
39
ref
33
remove
appTerm
54
ref
appTerm
appTerm
54
remove
appTerm
appTerm
absTerm
appTerm
absTerm
absTerm
55
def
defineConst
56
def
pop
57
def
pop
56
remove
nil
46
remove
57
remove
26
remove
constTerm
appTerm
55
remove
appTerm
thm
"?!"
5
remove
36
ref
52
remove
8
ref
appTerm
appTerm
45
ref
9
ref
45
remove
"y"
1
ref
var
58
def
39
ref
36
ref
48
remove
appTerm
8
remove
58
remove
varTerm
59
def
appTerm
appTerm
appTerm
6
ref
0
ref
1
ref
4
ref
nil
cons
cons
opType
constTerm
47
remove
appTerm
60
def
59
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
61
def
defineConst
62
def
pop
63
def
pop
62
remove
nil
44
remove
63
remove
7
remove
constTerm
appTerm
61
remove
appTerm
thm
"cond"
"t"
2
ref
var
64
def
"t1"
1
ref
var
65
def
"t2"
1
ref
var
66
def
"select"
const
0
ref
4
remove
1
ref
nil
cons
67
def
cons
opType
constTerm
9
remove
36
remove
39
ref
27
remove
64
remove
varTerm
appTerm
68
def
18
remove
appTerm
appTerm
60
ref
65
remove
varTerm
appTerm
appTerm
appTerm
39
remove
68
remove
28
remove
appTerm
appTerm
60
remove
66
remove
varTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
absTerm
absTerm
69
def
defineConst
70
def
pop
71
def
pop
70
remove
nil
6
remove
0
ref
0
ref
2
remove
0
ref
1
ref
0
ref
1
remove
67
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
72
def
0
remove
72
ref
3
remove
cons
opType
nil
cons
cons
opType
constTerm
71
remove
72
remove
constTerm
appTerm
69
remove
appTerm
thm