1_  _         __        _
2|__|        |  |       |
3|  | IGHER  |__| RDER  |__ OGIC
4===============================
5(Built on Aug  7)
6
7#lisp`(load 'eval)`;;
8[fasl eval.o]
9() : void
10
11#loadt`conv`;;
12
13type conv defined
14
15INST_TY_TERM = 
16-
17: (((term # term) list # (type # type) list) -> thm -> thm)
18
19GSPEC = - : (thm -> thm)
20
21PART_MATCH = - : ((term -> term) -> thm -> conv)
22
23MATCH_MP = - : (thm -> thm -> thm)
24
25REWRITE_CONV = - : (thm -> conv)
26
27NO_CONV = - : conv
28
29ALL_CONV = - : conv
30
31() : void
32
33() : void
34
35THENC = - : (conv -> conv -> conv)
36
37ORELSEC = - : (conv -> conv -> conv)
38
39FIRST_CONV = - : (conv list -> conv)
40
41EVERY_CONV = - : (conv list -> conv)
42
43REPEATC = - : (conv -> conv)
44
45CHANGED_CONV = - : ((* -> thm) -> * -> thm)
46
47TRY_CONV = - : (conv -> conv)
48
49SUB_CONV = - : (conv -> conv)
50
51DEPTH_CONV = - : (conv -> conv)
52
53REDEPTH_CONV = - : (conv -> conv)
54
55TOP_DEPTH_CONV = - : (conv -> conv)
56
57CONV_RULE = - : (conv -> thm -> thm)
58
59CONV_TAC = - : (conv -> tactic)
60
61
62File conv loaded
63() : void
64
65#loadt`mk_ADDER`;;
66
67() : void
68Runtime: 2.9s
69GC: 0.0s
70
71() : void
72Runtime: 32.1s
73GC: 0.0s
74
75|- PWR o = (o = T)
76Runtime: 150.6s
77GC: 0.0s
78
79|- GND o = (o = F)
80Runtime: 150.1s
81GC: 0.0s
82
83|- PTRAN(g,s,d) = (g = F) ==> (s = d)
84Runtime: 272.5s
85GC: 0.0s
86
87|- NTRAN(g,s,d) = (g = T) ==> (s = d)
88Runtime: 286.8s
89GC: 0.0s
90
91|- ADD1_IMP(a,b,cin,sum,cout) =
92   (?p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11.
93     PTRAN(p1,p0,p2) /\
94     PTRAN(cin,p0,p3) /\
95     PTRAN(b,p2,p3) /\
96     PTRAN(a,p2,p4) /\
97     PTRAN(p1,p3,p4) /\
98     NTRAN(a,p4,p5) /\
99     NTRAN(p1,p4,p6) /\
100     NTRAN(b,p5,p6) /\
101     NTRAN(p1,p5,p11) /\
102     NTRAN(cin,p6,p11) /\
103     PTRAN(a,p0,p7) /\
104     PTRAN(b,p0,p7) /\
105     PTRAN(a,p0,p8) /\
106     PTRAN(cin,p7,p1) /\
107     PTRAN(b,p8,p1) /\
108     NTRAN(cin,p1,p9) /\
109     NTRAN(b,p1,p10) /\
110     NTRAN(a,p9,p11) /\
111     NTRAN(b,p9,p11) /\
112     NTRAN(a,p10,p11) /\
113     PWR p0 /\
114     PTRAN(p4,p0,sum) /\
115     NTRAN(p4,sum,p11) /\
116     GND p11 /\
117     PTRAN(p1,p0,cout) /\
118     NTRAN(p1,cout,p11))
119Runtime: 5304.3s
120GC: 0.0s
121
122() : void
123Runtime: 592.6s
124GC: 0.0s
125
126PTRAN = |- PTRAN(g,s,d) = (g = F) ==> (s = d)
127NTRAN = |- NTRAN(g,s,d) = (g = T) ==> (s = d)
128PWR = |- PWR o = (o = T)
129GND = |- GND o = (o = F)
130ADD1_IMP = 
131|- ADD1_IMP(a,b,cin,sum,cout) =
132   (?p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11.
133     PTRAN(p1,p0,p2) /\
134     PTRAN(cin,p0,p3) /\
135     PTRAN(b,p2,p3) /\
136     PTRAN(a,p2,p4) /\
137     PTRAN(p1,p3,p4) /\
138     NTRAN(a,p4,p5) /\
139     NTRAN(p1,p4,p6) /\
140     NTRAN(b,p5,p6) /\
141     NTRAN(p1,p5,p11) /\
142     NTRAN(cin,p6,p11) /\
143     PTRAN(a,p0,p7) /\
144     PTRAN(b,p0,p7) /\
145     PTRAN(a,p0,p8) /\
146     PTRAN(cin,p7,p1) /\
147     PTRAN(b,p8,p1) /\
148     NTRAN(cin,p1,p9) /\
149     NTRAN(b,p1,p10) /\
150     NTRAN(a,p9,p11) /\
151     NTRAN(b,p9,p11) /\
152     NTRAN(a,p10,p11) /\
153     PWR p0 /\
154     PTRAN(p4,p0,sum) /\
155     NTRAN(p4,sum,p11) /\
156     GND p11 /\
157     PTRAN(p1,p0,cout) /\
158     NTRAN(p1,cout,p11))
159Runtime: 4581.6s
160GC: 0.0s
161
162EQ_FLIP_CONV = - : (term list -> conv)
163Runtime: 4.9s
164GC: 0.0s
165
166extract_vars = - : (thm -> term list)
167Runtime: 5.1s
168GC: 0.0s
169
170CONJ_SIMP_RULE = - : (thm -> thm)
171Runtime: 4.3s
172GC: 0.0s
173
174CMOS_UNWIND = - : (thm -> thm)
175Runtime: 4.2s
176GC: 0.0s
177
178iterate = - : ((* -> *) -> * -> *)
179Runtime: 6.2s
180GC: 0.0s
181
182CMOS_EXPAND = - : (thm -> thm)
183Runtime: 4.1s
184GC: 0.0s
185
186prove_case1 = - : ((term # term # term) -> thm)
187Runtime: 5.4s
188GC: 0.0s
189
190TTT_Thm = |- ADD1_IMP(T,T,T,sum,cout) = (sum = T) /\ (cout = T)
191Runtime: 158770.2s
192GC: 45712.5s
193
194TTF_Thm = |- ADD1_IMP(T,T,F,sum,cout) = (sum = F) /\ (cout = T)
195Runtime: 204599.4s
196GC: 53208.7s
197
198TFT_Thm = |- ADD1_IMP(T,F,T,sum,cout) = (sum = F) /\ (cout = T)
199Runtime: 231374.2s
200GC: 66360.2s
201
202TFF_Thm = |- ADD1_IMP(T,F,F,sum,cout) = (sum = T) /\ (cout = F)
203Runtime: 260606.1s
204GC: 73437.0s
205
206FTT_Thm = |- ADD1_IMP(F,T,T,sum,cout) = (sum = F) /\ (cout = T)
207Runtime: 238501.1s
208GC: 66846.0s
209
210FTF_Thm = |- ADD1_IMP(F,T,F,sum,cout) = (sum = T) /\ (cout = F)
211Runtime: 240344.7s
212GC: 67433.1s
213
214FFT_Thm = |- ADD1_IMP(F,F,T,sum,cout) = (sum = T) /\ (cout = F)
215Runtime: 233080.9s
216GC: 67204.6s
217
218FFF_Thm = |- ADD1_IMP(F,F,F,sum,cout) = (sum = F) /\ (cout = F)
219Runtime: 187595.6s
220GC: 53923.5s
221
222Theory ADD_SLICE loaded
223() : void
224Runtime: 483.9s
225GC: 0.0s
226
227|- ADD2_IMP(a,b,cin,ph1,ph1_bar,sum,cout) =
228   (?p0 p1 p2 p3 p4 p5 p6 p7 p8.
229     PWR p0 /\
230     GND p8 /\
231     PTRAN(ph1,p0,p1) /\
232     PTRAN(a,p1,p2) /\
233     PTRAN(b,p2,sum) /\
234     NTRAN(a,p1,p3) /\
235     NTRAN(cin,p3,sum) /\
236     NTRAN(ph1,sum,p8) /\
237     NTRAN(b,p1,p3) /\
238     NTRAN(b,cout,p4) /\
239     NTRAN(cin,cout,p4) /\
240     NTRAN(a,cout,p4) /\
241     NTRAN(sum,p4,p7) /\
242     PTRAN(ph1_bar,p0,cout) /\
243     NTRAN(a,cout,p5) /\
244     NTRAN(b,p5,p6) /\
245     NTRAN(cin,p6,p7) /\
246     NTRAN(ph1_bar,p7,p8))
247Runtime: 3770.0s
248GC: 0.0s
249
250ADD2_IMP = 
251|- ADD2_IMP(a,b,cin,ph1,ph1_bar,sum,cout) =
252   (?p0 p1 p2 p3 p4 p5 p6 p7 p8.
253     PWR p0 /\
254     GND p8 /\
255     PTRAN(ph1,p0,p1) /\
256     PTRAN(a,p1,p2) /\
257     PTRAN(b,p2,sum) /\
258     NTRAN(a,p1,p3) /\
259     NTRAN(cin,p3,sum) /\
260     NTRAN(ph1,sum,p8) /\
261     NTRAN(b,p1,p3) /\
262     NTRAN(b,cout,p4) /\
263     NTRAN(cin,cout,p4) /\
264     NTRAN(a,cout,p4) /\
265     NTRAN(sum,p4,p7) /\
266     PTRAN(ph1_bar,p0,cout) /\
267     NTRAN(a,cout,p5) /\
268     NTRAN(b,p5,p6) /\
269     NTRAN(cin,p6,p7) /\
270     NTRAN(ph1_bar,p7,p8))
271Runtime: 2560.7s
272GC: 0.0s
273
274prove_case2 = - : ((term # term # term # term) -> thm)
275Runtime: 4.2s
276GC: 0.0s
277
278TTTT_Thm = |- ADD2_IMP(T,T,T,T,F,sum,cout) = (sum = F) /\ (cout = T)
279Runtime: 124608.3s
280GC: 34314.9s
281
282TTFT_Thm = 
283|- ADD2_IMP(T,T,F,T,F,sum,cout) =
284   (?p0 p1 p3 p4 p5 p6 p8.
285     (p5 = T) /\
286     (p6 = T) /\
287     (p4 = T) /\
288     (sum = F) /\
289     (p1 = p3) /\
290     (cout = T) /\
291     (p0 = T) /\
292     (p8 = F))
293Runtime: 114238.4s
294GC: 34478.8s
295
296TFTT_Thm = 
297|- ADD2_IMP(T,F,T,T,F,sum,cout) =
298   (?p0 p1 p2 p3 p4 p5 p6 p7 p8.
299     (p4 = T) /\
300     (p5 = T) /\
301     (p1 = F) /\
302     (p2 = F) /\
303     (p3 = F) /\
304     (sum = F) /\
305     (cout = T) /\
306     (p6 = p7) /\
307     (p0 = T) /\
308     (p8 = F))
309Runtime: 119296.0s
310GC: 34759.2s
311
312TFFT_Thm = 
313|- ADD2_IMP(T,F,F,T,F,sum,cout) =
314   (?p0 p1 p2 p3 p4 p5 p8.
315     (p4 = T) /\
316     (p5 = T) /\
317     (p2 = F) /\
318     (p1 = p3) /\
319     (sum = F) /\
320     (cout = T) /\
321     (p0 = T) /\
322     (p8 = F))
323Runtime: 111625.1s
324GC: 34757.8s
325
326FTTT_Thm = 
327|- ADD2_IMP(F,T,T,T,F,sum,cout) =
328   (?p0 p1 p2 p3 p4 p5 p6 p7 p8.
329     (p2 = F) /\
330     (p4 = T) /\
331     (p1 = F) /\
332     (p3 = F) /\
333     (p5 = p7) /\
334     (sum = F) /\
335     (cout = T) /\
336     (p6 = p7) /\
337     (p0 = T) /\
338     (p8 = F))
339Runtime: 118960.3s
340GC: 28279.4s
341
342FTFT_Thm = 
343|- ADD2_IMP(F,T,F,T,F,sum,cout) =
344   (?p0 p1 p2 p3 p4 p5 p6 p8.
345     (p4 = T) /\
346     (p1 = p2) /\
347     (sum = F) /\
348     (p1 = p3) /\
349     (cout = T) /\
350     (p5 = p6) /\
351     (p0 = T) /\
352     (p8 = F))
353Runtime: 109637.0s
354GC: 28476.3s
355
356FFTT_Thm = 
357|- ADD2_IMP(F,F,T,T,F,sum,cout) =
358   (?p0 p1 p2 p3 p4 p6 p7 p8.
359     (p4 = T) /\
360     (p1 = F) /\
361     (p2 = F) /\
362     (p3 = F) /\
363     (sum = F) /\
364     (cout = T) /\
365     (p6 = p7) /\
366     (p0 = T) /\
367     (p8 = F))
368Runtime: 114741.9s
369GC: 35303.5s
370
371FFFT_Thm = |- ADD2_IMP(F,F,F,T,F,sum,cout) = (sum = F) /\ (cout = T)
372Runtime: 102416.0s
373GC: 28789.9s
374
375TTTF_Thm = |- ADD2_IMP(T,T,T,F,T,sum,cout) = (sum = T) /\ (cout = F)
376Runtime: 141261.1s
377GC: 43240.3s
378
379TTFF_Thm = 
380|- ADD2_IMP(T,T,F,F,T,sum,cout) =
381   (?p0 p1 p3 p4 p5 p6 p7 p8.
382     ((sum = T) ==> (p4 = F)) /\
383     (p3 = T) /\
384     (cout = p6) /\
385     (p1 = T) /\
386     (cout = p4) /\
387     (p5 = p6) /\
388     (p7 = F) /\
389     (p0 = T) /\
390     (p8 = F))
391Runtime: 100645.9s
392GC: 36135.1s
393
394TFTF_Thm = |- ADD2_IMP(T,F,T,F,T,sum,cout) = (cout = F) /\ (sum = T)
395Runtime: 164891.5s
396GC: 51755.0s
397
398TFFF_Thm = 
399|- ADD2_IMP(T,F,F,F,T,sum,cout) =
400   (?p0 p1 p2 p3 p4 p5 p7 p8.
401     ((sum = T) ==> (p4 = F)) /\
402     (p3 = T) /\
403     (p1 = T) /\
404     (p2 = sum) /\
405     (cout = p4) /\
406     (cout = p5) /\
407     (p7 = F) /\
408     (p0 = T) /\
409     (p8 = F))
410Runtime: 103004.9s
411GC: 29258.5s
412
413FTTF_Thm = |- ADD2_IMP(F,T,T,F,T,sum,cout) = (cout = F) /\ (sum = T)
414Runtime: 146238.8s
415GC: 44178.8s
416
417FTFF_Thm = 
418|- ADD2_IMP(F,T,F,F,T,sum,cout) =
419   (?p0 p1 p2 p3 p4 p5 p6 p7 p8.
420     ((sum = T) ==> (p4 = F)) /\
421     (p2 = T) /\
422     (p3 = T) /\
423     (p1 = T) /\
424     (cout = p4) /\
425     (p5 = p6) /\
426     (p7 = F) /\
427     (p0 = T) /\
428     (p8 = F))
429Runtime: 101240.5s
430GC: 29795.6s
431
432FFTF_Thm = |- ADD2_IMP(F,F,T,F,T,sum,cout) = (cout = F) /\ (sum = T)
433Runtime: 139629.1s
434GC: 44773.6s
435
436FFFF_Thm = |- ADD2_IMP(F,F,F,F,T,sum,cout) = (sum = T)
437Runtime: 120563.7s
438GC: 37322.7s
439
440
441File mk_ADDER loaded
442() : void
443Runtime: 3728466.0s
444GC: 1083903.1s
445
446#