6
version
"A"
"->"
typeOp
0
def
"A"
varType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
nil
cons
cons
nil
cons
nil
nil
cons
cons
nil
"="
const
5
def
0
ref
0
ref
4
ref
3
ref
cons
opType
6
def
0
ref
6
ref
3
ref
cons
opType
7
def
nil
cons
cons
opType
constTerm
8
def
"Data.Bool.!"
const
9
def
6
ref
constTerm
10
def
appTerm
"p"
4
ref
var
11
def
5
ref
0
ref
4
ref
6
ref
nil
cons
cons
opType
constTerm
12
def
11
ref
varTerm
13
def
appTerm
14
def
"x"
1
ref
var
15
def
"Data.Bool.T"
const
2
ref
constTerm
16
def
absTerm
appTerm
absTerm
appTerm
axiom
17
def
subst
"p"
6
ref
var
18
def
8
ref
18
remove
varTerm
appTerm
refl
"x"
4
ref
var
nil
5
ref
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
19
def
nil
cons
cons
opType
20
def
constTerm
21
def
16
ref
appTerm
5
ref
0
ref
19
ref
0
ref
19
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
22
def
"p"
2
ref
var
23
def
23
ref
varTerm
24
def
absTerm
25
def
appTerm
25
remove
appTerm
appTerm
axiom
26
def
absThm
appThm
absThm
trans
11
ref
17
remove
11
ref
14
remove
refl
15
ref
26
ref
absThm
appThm
absThm
trans
15
ref
nil
5
ref
0
ref
20
ref
0
ref
20
ref
3
ref
cons
opType
27
def
nil
cons
cons
opType
constTerm
28
def
"Data.Bool.==>"
const
20
ref
constTerm
29
def
appTerm
23
ref
"q"
2
ref
var
30
def
21
ref
"Data.Bool./\\"
const
20
ref
constTerm
31
def
24
ref
appTerm
30
ref
varTerm
32
def
appTerm
appTerm
24
ref
appTerm
absTerm
absTerm
appTerm
axiom
23
ref
30
ref
21
ref
refl
nil
28
remove
31
remove
appTerm
23
ref
30
ref
5
remove
0
ref
27
ref
0
ref
27
remove
3
remove
cons
opType
nil
cons
cons
opType
constTerm
33
def
"f"
20
ref
var
34
def
34
ref
varTerm
35
def
24
ref
appTerm
32
ref
appTerm
absTerm
appTerm
36
def
34
ref
35
ref
16
ref
appTerm
16
remove
appTerm
absTerm
appTerm
absTerm
absTerm
appTerm
axiom
23
remove
30
remove
36
remove
refl
34
remove
35
remove
refl
26
ref
appThm
26
remove
appThm
absThm
appThm
absThm
absThm
trans
24
remove
refl
37
def
appThm
32
remove
refl
appThm
appThm
37
remove
appThm
absThm
absThm
trans
13
ref
15
ref
varTerm
appTerm
38
def
refl
appThm
13
ref
"select"
const
0
remove
4
ref
1
ref
nil
cons
cons
opType
constTerm
39
def
13
remove
appTerm
appTerm
40
def
refl
appThm
absThm
appThm
absThm
appThm
sym
nil
"a"
6
remove
var
41
def
8
remove
41
remove
varTerm
appTerm
"b"
4
ref
var
22
remove
"c"
2
ref
var
42
def
42
remove
varTerm
absTerm
43
def
appTerm
43
remove
appTerm
44
def
absTerm
appTerm
absTerm
"d"
4
ref
var
45
def
"e"
4
remove
var
46
def
12
remove
46
remove
varTerm
appTerm
"f"
1
ref
var
44
ref
absTerm
appTerm
absTerm
"g"
1
remove
var
47
def
"h"
2
ref
var
48
def
"i"
2
ref
var
49
def
21
remove
"j"
2
ref
var
50
def
"k"
2
remove
var
51
def
33
remove
"l"
20
ref
var
52
def
52
remove
varTerm
50
remove
varTerm
appTerm
51
remove
varTerm
appTerm
absTerm
appTerm
"m"
20
remove
var
53
def
53
remove
varTerm
44
ref
appTerm
44
remove
appTerm
absTerm
appTerm
absTerm
absTerm
48
remove
varTerm
54
def
appTerm
49
remove
varTerm
appTerm
appTerm
54
remove
appTerm
absTerm
absTerm
45
remove
varTerm
55
def
47
remove
varTerm
appTerm
appTerm
55
ref
39
remove
55
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
9
remove
7
remove
constTerm
11
remove
10
remove
15
remove
29
remove
38
remove
appTerm
40
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm