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