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