-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathprover.9.scm
281 lines (273 loc) · 13.3 KB
/
prover.9.scm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
(load "prover-load-j-bob.scm")
(jbob.prove (dethm.set?/atoms)
'(((defun rotate (x)
(cons (car (car x)) (cons (cdr (car x)) (cdr x))))
nil)))
(jbob.prove (defun.rotate)
'(((dethm rotate/cons (x y z)
(equal (rotate (cons (cons x y) z)) (cons x (cons y z))))
nil
((1) (rotate (cons (cons x y) z)))
((1 1 1) (car/cons (cons x y) z))
((1 1) (car/cons x y))
((1 2 1 1) (car/cons (cons x y) z))
((1 2 1) (cdr/cons x y))
((1 2 2) (cdr/cons (cons x y) z))
(() (equal-same (cons x (cons y z)))))))
(jbob.prove (dethm.rotate/cons)
'(((defun align (x)
(if (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
(size x)
((Q) (natp/size x))
(()
(if-true
(if (atom x)
't
(if (atom (car x))
(< (size (cdr x)) (size x))
(< (size (rotate x)) (size x))))
'nil))
((E A) (size/cdr x))
((E E 1 1 1) (cons/car+cdr x))
((E E 2 1) (cons/car+cdr x))
((E E 1 1 1 1) (cons/car+cdr (car x)))
((E E 2 1 1) (cons/car+cdr (car x)))
((E E 1 1) (rotate/cons (car (car x)) (cdr (car x)) (cdr x))))))
(jbob.prove (dethm.rotate/cons)
'(((defun wt (x)
(if (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
(size x)
((Q) (natp/size x))
(()
(if-true
(if (atom x)
't
(if (< (size (car x)) (size x)) (< (size (cdr x)) (size x)) 'nil))
'nil))
((E Q) (size/car x))
((E A) (size/cdr x))
((E) (if-true 't 'nil))
(() (if-same (atom x) 't)))))
(jbob.prove (defun.wt)
'(((dethm natp/wt (x)
(equal (natp (wt x)) 't))
(star-induction x)
((A 1 1) (wt x))
((A 1 1) (if-nest-A (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
((A 1) (natp '1))
((A) (equal-same 't))
((E A A 1 1) (wt x))
((E A A 1 1)
(if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
((E A A)
(if-true (equal (natp (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
((E A A Q) (equal-if (natp (wt (car x))) 't))
((E A A A)
(if-true (equal (natp (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
((E A A A Q) (natp/+ (wt (car x)) (wt (car x))))
((E A A Q) (equal-if (natp (wt (car x))) 't))
((E A A Q) (equal-if (natp (wt (cdr x))) 't))
((E A A A A 1) (natp/+ (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
((E A A A A) (equal-same 't))
((E A A A) (if-same (natp (+ (wt (car x)) (wt (car x)))) 't))
((E A A) (if-same (natp (wt (cdr x))) 't))
((E A) (if-same (equal (natp (wt (cdr x))) 't) 't))
((E) (if-same (equal (natp (wt (car x))) 't) 't))
(() (if-same (atom x) 't)))
((dethm positive/wt (x)
(equal (< '0 (wt x)) 't))
(star-induction x)
((A 1 2) (wt x))
((A 1 2) (if-nest-A (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
((A 1) (< '0 '1))
((A) (equal-same 't))
((E A A 1 2) (wt x))
((E A A 1 2)
(if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
((E A A)
(if-true (equal (< '0 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
((E A A Q) (equal-if (< '0 (wt (car x))) 't))
((E A A A)
(if-true (equal (< '0 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
((E A A A Q) (positives-+ (wt (car x)) (wt (car x))))
((E A A Q) (equal-if (< '0 (wt (car x))) 't))
((E A A Q) (equal-if (< '0 (wt (cdr x))) 't))
((E A A A A 1) (positives-+ (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
((E A A A A) (equal-same 't))
((E A A A) (if-same (< '0 (+ (wt (car x)) (wt (car x)))) 't))
((E A A) (if-same (< '0 (wt (cdr x))) 't))
((E A) (if-same (equal (< '0 (wt (cdr x))) 't) 't))
((E) (if-same (equal (< '0 (wt (car x))) 't) 't))
(() (if-same (atom x) 't)))
((defun align (x)
(if (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
(wt x)
((Q) (natp/wt x))
(()
(if-true
(if (atom x)
't
(if (atom (car x)) (< (wt (cdr x)) (wt x)) (< (wt (rotate x)) (wt x))))
'nil))
((E A 2) (wt x))
((E A 2) (if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
((E A)
(if-true (< (wt (cdr x)) (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't))
((E A Q) (natp/wt (cdr x)))
((E A A 1) (identity-+ (wt (cdr x))))
((E A A) (common-addends-< '0 (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
((E A Q) (natp/wt (cdr x)))
((E A Q) (positive/wt (car x)))
((E A A) (positives-+ (wt (car x)) (wt (car x))))
((E A) (if-same (< '0 (wt (car x))) 't))
((E E 1 1) (rotate x))
((E E 1) (wt (cons (car (car x)) (cons (cdr (car x)) (cdr x)))))
((E E 1 Q) (atom/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
((E E 1)
(if-false '1
(+ (+ (wt (car (cons (car (car x)) (cons (cdr (car x)) (cdr x)))))
(wt (car (cons (car (car x)) (cons (cdr (car x)) (cdr x))))))
(wt (cdr (cons (car (car x)) (cons (cdr (car x)) (cdr x))))))))
((E E 1 1 1 1) (car/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
((E E 1 1 2 1) (car/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
((E E 1 2 1) (cdr/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
((E E 1 2) (wt (cons (cdr (car x)) (cdr x))))
((E E 1 2 Q) (atom/cons (cdr (car x)) (cdr x)))
((E E 1 2)
(if-false '1
(+ (+ (wt (car (cons (cdr (car x)) (cdr x))))
(wt (car (cons (cdr (car x)) (cdr x)))))
(wt (cdr (cons (cdr (car x)) (cdr x)))))))
((E E 1 2 1 1 1) (car/cons (cdr (car x)) (cdr x)))
((E E 1 2 1 2 1) (car/cons (cdr (car x)) (cdr x)))
((E E 1 2 2 1) (cdr/cons (cdr (car x)) (cdr x)))
((E E 2) (wt x))
((E E 2) (if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
((E E 2 1 1) (wt (car x)))
((E E 2 1 1)
(if-nest-E (atom (car x))
'1
(+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))))
((E E 2 1 2) (wt (car x)))
((E E 2 1 2)
(if-nest-E (atom (car x))
'1
(+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))))
((E E 1)
(associate-+
(+ (wt (car (car x))) (wt (car (car x))))
(+ (wt (cdr (car x))) (wt (cdr (car x))))
(wt (cdr x))))
((E E)
(common-addends-<
(+ (+ (wt (car (car x))) (wt (car (car x))))
(+ (wt (cdr (car x))) (wt (cdr (car x)))))
(+ (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))
(+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x)))))
(wt (cdr x))))
((E E 1)
(associate-+
(+ (wt (car (car x))) (wt (car (car x))))
(wt (cdr (car x)))
(wt (cdr (car x)))))
((E E 1)
(commute-+
(+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))
(wt (cdr (car x)))))
((E E)
(common-addends-<
(wt (cdr (car x)))
(+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))
(+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))))
((E E)
(if-true
(< (wt (cdr (car x)))
(+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x)))))
't))
((E E Q) (natp/wt (cdr (car x))))
((E E A 1) (identity-+ (wt (cdr (car x)))))
((E E A)
(common-addends-<
'0
(+ (wt (car (car x))) (wt (car (car x))))
(wt (cdr (car x)))))
((E E Q) (natp/wt (cdr (car x))))
((E E Q) (positive/wt (car (car x))))
((E E A) (positives-+ (wt (car (car x))) (wt (car (car x)))))
((E E) (if-same (< '0 (wt (car (car x)))) 't))
((E) (if-same (atom (car x)) 't))
(() (if-same (atom x) 't)))))
(jbob.prove (defun.align)
'(((dethm align/align (x)
(equal (align (align x)) (align x)))
(align x)
((A 1 1) (align x))
((A 1 1)
(if-nest-A (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
((A 2) (align x))
((A 2)
(if-nest-A (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
((A 1) (align x))
((A 1)
(if-nest-A (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
((A) (equal-same x))
((E A A 1 1) (align x))
((E A A 1 1)
(if-nest-E (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
((E A A 1 1)
(if-nest-A (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
((E A A 2) (align x))
((E A A 2)
(if-nest-E (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
((E A A 2)
(if-nest-A (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
((E A A 1) (align (cons (car x) (align (cdr x)))))
((E A A 1 Q) (atom/cons (car x) (align (cdr x))))
((E A A 1 E Q 1) (car/cons (car x) (align (cdr x))))
((E A A 1 E A 1) (car/cons (car x) (align (cdr x))))
((E A A 1 E A 2 1) (cdr/cons (car x) (align (cdr x))))
((E A A 1)
(if-false (cons (car x) (align (cdr x)))
(if (atom (car x))
(cons (car x) (align (align (cdr x))))
(align (rotate (cons (car x) (align (cdr x))))))))
((E A A 1)
(if-nest-A (atom (car x))
(cons (car x) (align (align (cdr x))))
(align (rotate (cons (car x) (align (cdr x)))))))
((E A A 1 2) (equal-if (align (align (cdr x))) (align (cdr x))))
((E A A) (equal-same (cons (car x) (align (cdr x)))))
((E A) (if-same (equal (align (align (cdr x))) (align (cdr x))) 't))
((E E A 1 1) (align x))
((E E A 1 1)
(if-nest-E (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
((E E A 1 1)
(if-nest-E (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
((E E A 2) (align x))
((E E A 2)
(if-nest-E (atom x)
x
(if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
((E E A 2)
(if-nest-E (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
((E E A 1) (equal-if (align (align (rotate x))) (align (rotate x))))
((E E A) (equal-same (align (rotate x))))
((E E) (if-same (equal (align (align (rotate x))) (align (rotate x))) 't))
((E) (if-same (atom (car x)) 't))
(() (if-same (atom x) 't)))))