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#