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