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