6
version
"Function.o"
"f"
"->"
typeOp
0
def
"B"
varType
1
def
"C"
varType
nil
cons
2
def
cons
opType
3
def
var
4
def
"g"
0
ref
"A"
varType
5
def
1
ref
nil
cons
cons
opType
6
def
var
7
def
"x"
5
ref
var
8
def
4
remove
varTerm
7
ref
varTerm
8
ref
varTerm
9
def
appTerm
10
def
appTerm
absTerm
absTerm
absTerm
11
def
defineConst
12
def
pop
13
def
pop
12
remove
nil
"="
const
14
def
0
ref
0
ref
3
ref
0
ref
6
ref
0
ref
5
ref
2
remove
cons
opType
nil
cons
15
def
cons
opType
nil
cons
16
def
cons
opType
17
def
0
ref
17
ref
"bool"
typeOp
nil
opType
18
def
nil
cons
19
def
cons
opType
nil
cons
cons
opType
constTerm
13
remove
17
remove
constTerm
appTerm
11
remove
appTerm
thm
"Function.id"
8
ref
9
ref
absTerm
20
def
defineConst
21
def
pop
22
def
pop
21
remove
nil
14
ref
0
ref
0
ref
5
ref
5
ref
nil
cons
23
def
cons
opType
24
def
0
ref
24
ref
19
ref
cons
opType
nil
cons
cons
opType
constTerm
22
remove
24
remove
constTerm
appTerm
20
remove
appTerm
thm
"Function.const"
8
ref
"y"
1
ref
var
25
def
9
ref
absTerm
absTerm
26
def
defineConst
27
def
pop
28
def
pop
27
remove
nil
14
ref
0
ref
0
ref
5
ref
0
ref
1
ref
23
remove
cons
opType
nil
cons
cons
opType
29
def
0
ref
29
ref
19
ref
cons
opType
nil
cons
cons
opType
constTerm
28
remove
29
remove
constTerm
appTerm
26
remove
appTerm
thm
"Function.Combinator.s"
"f"
0
ref
5
ref
3
remove
nil
cons
cons
opType
30
def
var
31
def
7
remove
8
ref
31
ref
varTerm
32
def
9
ref
appTerm
10
remove
appTerm
absTerm
absTerm
absTerm
33
def
defineConst
34
def
pop
35
def
pop
34
remove
nil
14
ref
0
ref
0
ref
30
ref
16
remove
cons
opType
36
def
0
ref
36
ref
19
ref
cons
opType
nil
cons
cons
opType
constTerm
35
remove
36
remove
constTerm
appTerm
33
remove
appTerm
thm
"Function.flip"
31
remove
"x"
1
ref
var
37
def
"y"
5
ref
var
38
def
32
remove
38
remove
varTerm
appTerm
37
remove
varTerm
appTerm
absTerm
absTerm
absTerm
39
def
defineConst
40
def
pop
41
def
pop
40
remove
nil
14
ref
0
ref
0
ref
30
remove
0
ref
1
ref
15
remove
cons
opType
nil
cons
cons
opType
42
def
0
ref
42
ref
19
ref
cons
opType
nil
cons
cons
opType
constTerm
41
remove
42
remove
constTerm
appTerm
39
remove
appTerm
thm
"Function.Combinator.w"
"f"
0
ref
5
ref
6
ref
nil
cons
43
def
cons
opType
44
def
var
45
def
8
ref
45
remove
varTerm
9
ref
appTerm
9
ref
appTerm
absTerm
absTerm
46
def
defineConst
47
def
pop
48
def
pop
47
remove
nil
14
ref
0
ref
0
ref
44
remove
43
ref
cons
opType
49
def
0
ref
49
ref
19
ref
cons
opType
nil
cons
cons
opType
constTerm
48
remove
49
remove
constTerm
appTerm
46
remove
appTerm
thm
nil
"P"
0
ref
6
ref
19
ref
cons
opType
50
def
var
51
def
"f"
6
ref
var
52
def
14
ref
0
ref
18
ref
0
ref
18
ref
19
ref
cons
opType
nil
cons
cons
opType
53
def
constTerm
54
def
"Function.injective"
"_1861"
6
ref
var
55
def
"Data.Bool.!"
const
56
def
0
ref
0
ref
5
ref
19
ref
cons
opType
57
def
19
ref
cons
opType
58
def
constTerm
59
def
"x1"
5
ref
var
60
def
59
ref
"x2"
5
ref
var
61
def
"Data.Bool.==>"
const
53
remove
constTerm
62
def
14
ref
0
ref
1
ref
0
ref
1
remove
19
ref
cons
opType
63
def
nil
cons
cons
opType
constTerm
64
def
55
ref
varTerm
65
def
60
ref
varTerm
66
def
appTerm
appTerm
65
ref
61
ref
varTerm
67
def
appTerm
appTerm
appTerm
14
ref
0
ref
5
remove
57
ref
nil
cons
cons
opType
constTerm
66
ref
appTerm
67
ref
appTerm
68
def
appTerm
absTerm
appTerm
absTerm
appTerm
69
def
absTerm
70
def
defineConst
71
def
pop
50
ref
constTerm
72
def
52
ref
varTerm
73
def
appTerm
appTerm
59
ref
60
remove
59
ref
61
remove
62
remove
64
ref
73
ref
66
remove
appTerm
appTerm
73
ref
67
remove
appTerm
appTerm
appTerm
68
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
74
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
43
remove
cons
nil
cons
nil
nil
cons
cons
54
ref
59
ref
"P"
57
ref
var
varTerm
75
def
appTerm
appTerm
refl
"p"
57
ref
var
76
def
14
ref
0
ref
57
remove
58
ref
nil
cons
cons
opType
constTerm
76
remove
varTerm
appTerm
8
ref
"Data.Bool.T"
const
18
ref
constTerm
77
def
absTerm
appTerm
absTerm
78
def
75
ref
appTerm
betaConv
appThm
nil
14
remove
0
ref
58
ref
0
ref
58
ref
19
ref
cons
opType
nil
cons
cons
opType
constTerm
59
remove
appTerm
78
remove
appTerm
axiom
75
remove
refl
appThm
eqMp
sym
subst
79
def
subst
55
remove
nil
"t"
18
remove
var
80
def
54
ref
72
remove
65
ref
appTerm
appTerm
69
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
80
ref
varTerm
81
def
appTerm
77
ref
appTerm
assume
sym
nil
77
remove
axiom
82
def
eqMp
81
remove
assume
82
remove
deductAntisym
deductAntisym
83
def
subst
71
remove
65
ref
refl
appThm
70
remove
65
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
56
ref
0
ref
50
ref
19
ref
cons
opType
constTerm
84
def
74
remove
appTerm
thm
nil
51
remove
52
remove
54
ref
"Function.surjective"
"_1866"
6
remove
var
85
def
56
remove
0
remove
63
remove
19
remove
cons
opType
constTerm
86
def
25
ref
"Data.Bool.?"
const
58
remove
constTerm
87
def
8
ref
64
remove
25
ref
varTerm
appTerm
88
def
85
ref
varTerm
89
def
9
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
90
def
absTerm
91
def
defineConst
92
def
pop
50
remove
constTerm
93
def
73
ref
appTerm
appTerm
86
remove
25
remove
87
remove
8
remove
88
remove
73
remove
9
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
94
def
nil
cons
cons
nil
cons
nil
cons
cons
79
remove
subst
85
remove
nil
80
remove
54
remove
93
remove
89
ref
appTerm
appTerm
90
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
83
remove
subst
92
remove
89
ref
refl
appThm
91
remove
89
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
84
remove
94
remove
appTerm
thm