OKlibrary  0.2.1.6
3k.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 11.1.2011 (Swansea) */
00002 /* Copyright 2011, 2013 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/RamseyTheory/Lisp/VanderWaerden/Numbers.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/RamseyTheory/Lisp/VanderWaerden/Certificates.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/RamseyTheory/Lisp/VanderWaerden/PdNumbers.mac")$
00025 
00026 
00027 /* For k >= 1 a list of lists of certificates for best lower bounds
00028    on vdw_2(3,k). Each certificate c is to be translated into a full
00029    certificate by create_certificate2_vdw(c,n), where n+1 is the current lower
00030    bound w.r.t. k.
00031  */
00032 
00033 certificates_vdw_3k : [
00034 [],[],[[1,2,5,6],[1,3,6,8],[1,4,5,8]],[],[],[],[],[],[],[],
00035 [],[],[],[],[],[],[],[],[],
00036 /* k=20: */
00037 [[20,32,37,45,47,52,66,76,81,83,
00038 98,99,103,104,106,116,135,145,150,152,
00039 158,162,173,190,199,216,227,231,237,239,
00040 244,254,273,283,285,286,290,291,306,308,
00041 313,323,337,342,344,352,357,369]],
00042 /* k=21: */
00043 [[9,27,29,36,38,48,61,62,82,101,
00044 105,107,110,123,124,130,131,133,144,163,
00045 167,169,170,179,192,213,232,236,238,246,
00046 255,268,269,271,289,308,312,314,315,324,
00047 330,337,338,351,358,374,376,381,383,395]],
00048 /* k=22: */
00049 [[3,22,23,33,46,61,77,80,91,96,
00050 104,110,123,133,135,139,148,152,154,164,
00051 177,183,191,196,207,210,226,239,241,254,
00052 264,265,283,284,294,307,309,322,338,341,
00053 352,357,365,371,384,394,396,400,409,415,
00054 425,438,442,452]],
00055 /* k=23: */
00056 [[5,6,9,27,32,34,50,67,72,78,
00057 99,101,104,113,114,116,121,137,140,145,
00058 162,172,183,185,195,206,214,232,239,241,
00059 261,278,300,301,321,328,331,344,346,347,
00060 352,354,375,389,390,402,412,413,420,425,
00061 439,441,445,454,464,485,491,510,514]],
00062 /* k=24: */
00063 [[22,41,58,63,71,78,80,95,99,100,
00064 109,117,121,124,145,146,150,158,174,182,
00065 186,187,208,211,215,223,233,252,254,261,
00066 283,291,302,310,332,339,341,360,370,378,
00067 382,385,406,407,411,419,435,443,447,448,
00068 469,476,484,493,494,498,513,515,522,530,
00069 535,552,571]],
00070 /* k=25: */
00071 [[17,20,40,49,57,77,86,91,93,99,
00072 117,128,150,151,154,156,167,175,188,193,
00073 197,204,212,224,228,242,247,265,267,271,
00074 278,279,286,304,313,321,335,350,353,358,
00075 372,373,382,390,410,419,424,426,434,450,
00076 461,471,483,484,487,489,500,506,521,526,
00077 530,537,545,557,561,575,580,598,600,604,
00078 611,612,637,646]],
00079 /* k=26: */
00080 [[1,6,16,28,47,73,75,80,104,109,
00081 110,112,117,126,141,146,163,176,186,191,
00082 197,201,220,221,234,237,238,250,257,269,
00083 274,295,308,312,326,334,339,343,345,349,
00084 361,363,380,398,406,408,413,437,442,443,
00085 445,450,459,474,496,509,516,519,524,530,
00086 534,553,554,565,567,570,571,583,602,607,
00087 628,641,645,659,676,678,696,701]],
00088 /* k=27: */
00089 [[25,29,35,54,72,74,77,99,103,111,
00090 114,135,136,149,165,176,188,192,202,209,
00091 223,246,250,251,260,266,287,294,296,313,
00092 321,325,331,333,334,336,358,361,362,377,
00093 387,405,407,410,414,432,436,442,444,447,
00094 468,469,482,498,521,525,535,542,556,579,
00095 583,584,593,599,620,629,646,654,658,664,
00096 666,667,669,694,701,710,731,747,764]],
00097 /* k=28: */
00098 [[28,39,62,64,81,95,112,133,138,155,
00099 157,169,170,173,175,179,186,187,206,210,
00100 216,231,244,266,281,295,297,298,303,327,
00101 332,334,360,379,391,395,397,401,406,414,
00102 432,443,445,453,471,483,488,502,503,506,
00103 508,512,520,539,543,549,564,577,594,599,
00104 614,628,630,631,650,660,665,667,693,712,
00105 724,734,739,741,765,776,786,799,816]],
00106 /* k=29: */
00107 [[16,38,57,75,94,116,119,127,153,155,
00108 168,186,193,201,202,205,223,229,230,232,
00109 243,250,264,266,269,287,304,312,317,338,
00110 340,343,349,361,387,398,424,427,428,445,
00111 449,460,465,486,488,491,498,519,534,535,
00112 538,556,562,563,565,576,583,597,599,602,
00113 612,620,630,637,645,650,671,673,676,694,
00114 720,723,731,757,761,778,785,798,824,831,
00115 859]],
00116 /* k=30: */
00117 [[23,40,63,90,98,100,109,111,134,147,
00118 164,172,179,189,201,208,209,225,226,240,
00119 248,257,259,283,290,319,327,331,336,359,
00120 368,370,373,374,386,388,411,423,438,442,
00121 462,467,484,485,497,499,505,534,541,542,
00122 544,555,558,573,581,592,616,623,652,660,
00123 666,669,670,689,692,701,703,707,719,721,
00124 738,764,766,771,795,812,817,818,832,845,
00125 849,877,888]],
00126 /* k=31: */
00127 [[13,33,50,61,71,75,80,95,108,123,
00128 142,143,154,159,173,182,188,190,201,219,
00129 235,252,261,267,276,278,283,292,312,329,
00130 335,354,359,385,400,417,421,431,438,452,
00131 464,467,479,493,500,510,514,531,546,572,
00132 577,596,602,619,639,648,653,655,664,670,
00133 679,696,712,730,741,743,749,758,772,777,
00134 788,789,808,823,836,851,856,860,870,881,
00135 898,918]],
00136 /* k=32: */
00137 [[16,43,49,61,66,81,86,103,132,155,
00138 158,164,172,192,195,197,214,228,234,238,
00139 246,251,265,275,290,319,327,343,354,356,
00140 357,376,377,380,394,401,423,451,454,456,
00141 465,473,488,502,505,530,541,547,549,567,
00142 578,579,584,613,623,635,636,645,652,660,
00143 672,676,687,689,690,719,734,752,756,769,
00144 783,789,806,820,824,835,858,861,874,882,
00145 911,932,935,941,946,969,978]],
00146 /* k=33: */
00147 [[30,37,52,64,86,101,104,123,125,141,
00148 154,180,197,199,211,212,217,228,234,248,
00149 265,286,289,303,326,332,337,339,359,369,
00150 374,384,400,402,421,433,434,439,443,448,
00151 451,480,487,495,525,530,550,561,562,581,
00152 596,598,604,619,636,665,672,693,702,707,
00153 715,730,735,754,766,776,781,784,789,807,
00154 809,813,828,858,877,878,881,892,895,915,
00155 918,929,957,976,989,994,1015,1025,1050]],
00156 /* k=34: */
00157 [[33,41,43,52,82,106,110,111,122,126,
00158 144,147,157,163,180,196,217,218,221,230,
00159 231,233,265,284,291,304,311,329,333,341,
00160 342,369,376,379,381,406,407,415,418,422,
00161 444,469,480,492,513,524,543,550,551,580,
00162 588,592,607,635,637,638,659,661,666,674,
00163 677,698,699,728,736,755,765,776,785,814,
00164 820,822,823,825,829,857,860,866,899,924,
00165 931,957,968,971,995,998,1000,1010,1024,1035,
00166 1047,1068,1081,1098,1106,1110]],
00167 /* k=35: */
00168 [[35,60,69,92,96,97,108,138,146,151,
00169 166,182,190,212,219,225,239,262,264,277,
00170 280,293,301,313,314,319,323,331,350,356,
00171 360,365,368,375,410,430,439,441,447,465,
00172 476,479,498,502,521,523,553,572,576,609,
00173 610,613,619,647,664,689,693,706,708,726,
00174 735,737,758,772,795,804,811,819,841,854,
00175 874,886,909,911,920,922,928,942,957,967,
00176 983,985,996,1004,1020,1034,1039,1053,1078,1091,
00177 1113,1137,1144,1145,1170]],
00178 /* k=36: */
00179 [[11,45,62,75,82,94,120,122,127,133,
00180 136,149,156,186,188,193,211,238,260,262,
00181 275,279,281,284,285,299,305,322,355,358,
00182 378,379,381,386,390,416,427,460,466,469,
00183 484,492,503,521,538,543,564,581,595,601,
00184 614,618,630,632,667,677,688,719,723,729,
00185 756,766,778,785,788,822,825,836,839,860,
00186 867,871,896,913,933,934,936,941,945,963,
00187 971,988,1010,1037,1039,1045,1062,1089,1093,1098,
00188 1099,1113,1118,1121,1130,1132,1155,1172,1193,1222,
00189 1224]],
00190 /* k=37: */
00191 [[6,40,63,66,79,80,99,114,124,137,
00192 153,178,198,216,224,225,233,235,248,251,
00193 262,285,294,327,331,338,358,373,395,396,
00194 399,412,420,447,470,473,475,479,512,516,
00195 531,543,561,580,581,584,586,590,598,621,
00196 654,677,679,708,709,714,746,753,771,775,
00197 790,812,817,825,840,876,882,899,919,923,
00198 928,930,954,965,997,1010,1012,1024,1028,1041,
00199 1047,1062,1065,1076,1104,1135,1136,1139,1141,1150,
00200 1153,1158,1186,1188,1189,1197,1227,1232,1247,1264,
00201 1283,1298,1320,1321,1333]],
00202 /* k=38: */
00203 [[35,50,58,72,95,97,110,134,147,161,
00204 163,164,193,198,201,226,237,245,275,280,
00205 300,309,312,331,332,354,369,383,391,409,
00206 410,415,442,446,448,459,480,497,516,526,
00207 539,541,563,570,608,615,631,645,652,665,
00208 674,707,712,718,738,742,753,775,776,781,
00209 800,829,867,874,886,890,901,909,923,924,
00210 929,964,970,975,1001,1007,1008,1012,1040,1051,
00211 1057,1081,1086,1109,1118,1131,1148,1162,1163,1168,
00212 1189,1200,1234,1242,1244,1259,1265,1293,1301,1303,
00213 1310,1311,1331,1348]],
00214 /* k=39: */
00215 [[3,8,22,57,59,80,102,122,130,133,
00216 170,191,194,195,204,229,242,248,276,295,
00217 307,315,322,353,359,376,381,408,413,414,
00218 443,446,451,454,461,480,507,525,529,537,
00219 554,566,572,575,598,602,609,614,651,676,
00220 685,702,709,723,725,760,787,824,831,834,
00221 840,857,873,877,887,895,907,910,935,951,
00222 979,981,984,988,998,1016,1018,1019,1056,1079,
00223 1080,1092,1117,1146,1153,1183,1184,1190,1191,1195,
00224 1228,1231,1232,1238,1241,1257,1262,1270,1275,1305,
00225 1314,1337,1342,1375,1388]]
00226 ]$
00227 
00228 /* The "full certificates" (as partitions) for vdw_2(3,k): */
00229 full_certificate_vdw_3k(k) := block([lb : vanderwaerden3k(k)],
00230  if listp(lb) then lb : first(lb),
00231  lb : lb-1,
00232  map(lambda([S], create_certificate2_vdw(S,lb)), certificates_vdw_3k[k]))$
00233 
00234 /* The certificates as lists resp. strings: */
00235 full_certificate_list_vdw_3k(k) :=
00236   map(certificatevdw2list, full_certificate_vdw_3k(k))$
00237 full_certificate_string_vdw_3k(k) :=
00238   map(certificatevdw2string, full_certificate_vdw_3k(k))$
00239 
00240 /* Checking whether certificates_vdw_3k[k] are actually vdW-certificates
00241    for the corresponding lower bound (returning true resp. false for
00242    every alleged certificate):
00243 */
00244 check_certificates_vdw_3k(k) := block([C : certificates_vdw_3k[k]],
00245   if emptyp(C) then return([]),
00246   block([n : vanderwaerden3k(k)],
00247     if listp(n) then n : first(n),
00248     n : n-1,
00249     create_list(certificate_vdw_p([3,k],n,create_certificate2_vdw(c,n)),
00250                 c, C)))$
00251 
00252 
00253 /* ****************************
00254    * Palindromic certificates *
00255    ****************************
00256 */
00257 
00258 /*
00259   Each of the following certificates c w.r.t. [3,k] (resp. [k,3] for k < 3)
00260   and n has to be translated via create_certificate2c_pdvdw(c,n) into a full
00261   certificate.
00262 
00263   If the current (or precise) bound pdvanderwaerden3k(k) is [a,b], with a,b
00264   natural numbers (so pdvanderwaerden3k(k)[1] is either a or [a,x],
00265   while pdvanderwaerden3k(k)[2] is either b or [b,y]), then certificates for
00266   a-1 and b-1 have to be provided.
00267 
00268   Now certificates_pdvdw_3k[k] is a pair, where the first component is the
00269   list of the (compressed, half, for the part belonging to the smaller length
00270   (which is 3 for k >= 3, and in these cases the other part belongs to length
00271   k)) certificates w.r.t. a-1, and where the second component is the list of
00272   certificates w.r.t. b-1.
00273 */
00274 
00275 certificates_pdvdw_3k : [
00276 /* k=1: */
00277 [
00278  [[]],
00279  [[]]
00280 ],
00281 /* k=2: */
00282 [
00283  [[]],
00284  [[3]]
00285 ],
00286 /* k=3: */
00287 [
00288  [[3]],
00289  [[2,3],[1,3]]
00290 ],
00291 /* k=4: */
00292 [
00293  [[1,3,7]],
00294  [[3,5,6]]
00295 ],
00296 /* k=5: */
00297 [
00298  [[5,6]],
00299  [[3,5,10]]
00300 ],
00301 /* k=6: */
00302 [
00303  [[3,9,10,14]],
00304  [[6,7,13,14]]
00305 ],
00306 /* k=7: */
00307 [
00308  [[1,6,8,12,13,19]],
00309  [[1,2,7,10,16,21]]
00310 ],
00311 /* k=8: */
00312 [
00313  [[8,11,15,16,18,23]],
00314  [[3,6,11,13,18,22,28]]
00315 ],
00316 /* k=9: */
00317 [
00318  [[5,9,10,16,19,25,30]],
00319  [[9,10,17,21,23,27,28,34]]
00320 ],
00321 /* k=10: */
00322 [
00323  [[10,15,17,18,28,29,31,32,42]],
00324  [[10,19,20,23,24,31,32,37,46]]
00325 ],
00326 /* k=11: */
00327 [
00328  [[4,8,18,20,21,30,31,35,37,46,
00329 51]],
00330  [[3,5,9,11,16,24,25,31,35,42,
00331 44,55]]
00332 ],
00333 /* k=12: */
00334 [
00335  [[12,14,23,25,26,28,39,48,54,59,
00336 61]],
00337  [[10,19,29,32,36,38,46,49,51,55,
00338 67]]
00339 ],
00340 /* k=13: */
00341 [
00342  [[2,5,17,28,30,31,36,47,59,61,
00343 62,69]],
00344  [[11,16,28,33,44,46,47,51,52,54,
00345 65,70,73]]
00346 ],
00347 /* k=14: */
00348 [
00349  [[3,11,18,22,30,37,48,50,61,67,
00350 69,76,79,80]],
00351  [[5,6,9,18,20,28,37,43,52,60,
00352 62,71,74,75,89]]
00353 ],
00354 /* k=15: */
00355 [
00356  [[6,17,25,26,31,34,40,48,57,68,
00357 72,85,91,94,99]],
00358  [[12,19,29,32,44,48,54,57,58,61,
00359 73,75,86,100]]
00360 ],
00361 /* k=16: */
00362 [
00363  [[15,25,32,38,41,42,47,60,64,72,
00364 75,76,89,98,104,115]],
00365  [[16,26,29,30,35,45,47,48,58,73,
00366 83,84,96,102,105,115]]
00367 ],
00368 /* k=17: */
00369 [
00370  [[15,32,34,37,54,56,62,69,73,83,
00371 86,98,100,108,115,119,120]],
00372  [[5,12,18,22,33,40,46,55,56,67,
00373 69,76,84,86,95,108,110,127,137,138]]
00374 ],
00375 /* k=18: */
00376 [
00377  [[3,6,23,30,32,49,50,55,73,76,
00378 82,84,98,101,108,111,117,130,131,142]],
00379  [[7,16,20,38,39,43,44,57,74,82,
00380 92,93,95,96,101,111,119,124,139,150]]
00381 ],
00382 /* k=19: */
00383 [
00384  [[12,15,17,33,34,38,41,58,76,77,
00385 79,88,90,91,109,126,129,133,134,136,
00386 152,155,166]],
00387  [[12,31,37,39,46,54,56,60,63,82,
00388 92,94,97,98,113,117,120,122,135,139,
00389 141,154,168]]
00390 ],
00391 /* k=20: */
00392 [
00393  [[17,18,20,31,50,56,63,64,67,73,
00394 89,100,102,119,123,125,142,145,155,156,
00395 176,178,181]],
00396  [[20,32,37,45,47,52,66,76,81,83,
00397    98,99,103,104,106,116,135,145,150,152,
00398    158,162,173,190]]
00399 ],
00400 /* k=21: */
00401 [
00402  [[7,9,16,17,29,33,38,45,56,76,
00403 84,87,91,102,109,110,115,122,125,138,
00404 155,156,176,178,184,193]],
00405  [[19,21,27,28,32,46,56,57,77,79,
00406 88,90,107,115,117,132,141,143,164,166,
00407 170,181,183,201]]
00408 ],
00409 /* k=22: */
00410 [
00411  [[4,13,21,30,50,59,67,69,82,90,
00412 92,101,118,119,136,142,145,147,168,170,
00413 187,207,211,214,216]],
00414  [[19,37,44,49,57,59,60,66,82,93,
00415 108,109,111,118,119,122,131,146,147,155,
00416 160,171,193,204,216,221,222]]
00417 ],
00418 /* k=23: */
00419 [
00420  [[12,35,56,57,67,72,81,82,89,112,
00421 113,117,118,125,136,148,151,163,174,181,
00422 182,186,187,210,217,227,232,243]],
00423  [[23,24,43,46,66,70,73,82,83,102,
00424 112,125,128,129,139,159,162,164,171,182,
00425 187,198,218,220,221,228,243]]
00426 ],
00427 /* k=24: */
00428 [
00429  [[1,20,29,30,46,55,77,78,87,104,
00430 106,107,114,117,132,143,164,175,190,193,
00431 200,201,203,220,229,230,252,261,262,277,
00432 278,281]],
00433  [[22,41,58,63,71,78,80,95,99,100,
00434 109,117,121,124,145,146,150,158,174,182,
00435 186,187,208,211,215,223,233,252,254,261,
00436 283,291]]
00437 ],
00438 /* k=25: */
00439 [
00440  [[20,30,49,50,72,88,89,91,102,117,
00441 131,137,147,149,150,159,166,175,176,178,
00442 188,194,208,223,234,236,237,253,275,276,
00443 281,291]],
00444  [[25,30,41,59,68,73,97,99,112,118,
00445 131,141,142,146,155,162,184,191,200,204,
00446 205,215,228,234,247,249,273,278,286,287,
00447 291,302]]
00448 ],
00449 /* k=26: */
00450 [
00451  [[4,18,23,36,57,79,86,105,113,120,
00452 128,129,142,157,158,163,166,181,207,210,
00453 215,216,231,244,245,260,265,268,282,287,
00454 297,316]],
00455  [[16,40,47,61,66,81,84,98,110,126,
00456 127,134,147,153,161,176,177,189,190,192,
00457 206,211,229,234,248,255,263,272,277,284,
00458 298,316]]
00459 ],
00460 /* k=27: */
00461 [
00462  [[19,38,61,67,81,82,104,109,119,120,
00463 123,132,135,139,148,149,162,181,191,206,
00464 212,222,241,254,255,268,283,284,294,297,
00465 323,328]],
00466  [[23,30,56,67,93,105,106,116,118,124,
00467 128,136,137,147,162,186,190,191,211,229,
00468 230,234,240,253,265,273,283,284,292,314,
00469 327,341,348]]
00470 ],
00471 /* k=28: */
00472 [
00473  [[27,33,47,56,76,90,101,121,134,150,
00474 158,159,172,174,187,188,193,203,206,222,
00475 245,261,264,274,280,293,295,309,324,333,
00476 346,351,362]],
00477  [[22,45,47,52,78,89,91,115,127,128,
00478 138,146,150,158,159,169,184,212,213,233,
00479 251,252,256,262,275,287,295,305,306,314,
00480 336,349,363,370]]
00481 ],
00482 /* k=29: */
00483 [
00484  [[23,44,73,87,91,98,103,120,143,160,
00485 172,185,186,189,197,203,214,226,230,236,
00486 259,261,265,290,302,306,313,323,335,348,
00487 360,363,388,389,393]],
00488  [[14,16,17,34,50,65,67,72,75,103,
00489 108,109,124,137,154,161,169,180,188,195,
00490 212,225,246,256,261,283,299,307,314,328,
00491 335,336,348,369,391,393,399,406]]
00492 ],
00493 /* k=30: */
00494 [
00495  [[30,56,57,75,85,91,92,115,123,134,
00496 144,149,159,160,178,192,201,230,236,247,
00497 249,260,266,275,295,308,333,347,352,363,
00498 366,382,392,394,395,411]],
00499  [[30,32,35,37,45,50,67,86,101,123,
00500 124,132,136,139,153,168,173,190,194,206,
00501 231,236,247,255,281,292,293,298,317,318,
00502 334,346,352,354,359,363,385,404,414]]
00503 ],
00504 /* k=31: */
00505 [
00506  [[13,17,22,30,42,51,68,79,84,88,
00507 93,113,143,150,177,181,183,208,217,234,
00508 236,237,263,267,276,279,296,299,301,305,
00509 330,338,342,367,370,372,401,422,434,436,
00510 453]],
00511  [[13,33,50,61,71,75,80,95,108,123,
00512 142,143,154,159,173,182,188,190,201,219,
00513 235,252,261,267,276,278,283,292,312,329,
00514 335,354,359,385,400,417,421,431,438,452,
00515 464]]
00516 ],
00517 /* k=32: */
00518 [
00519  [[25,29,37,57,64,69,87,118,119,126,
00520 132,157,158,170,189,194,212,232,243,255,
00521 263,281,282,286,310,323,335,343,344,348,
00522 374,379,385,393,416,424,437,468,471,478
00523 ]],
00524  [[12,13,32,54,60,63,81,101,103,120,
00525 134,138,163,169,172,196,209,233,234,240,
00526 265,267,273,274,276,286,304,320,327,347,
00527 357,382,388,391,397,398,422,450,459,479]]
00528 ],
00529 /* k=33: */
00530 [
00531  [[32,34,55,63,64,77,82,113,121,131,
00532 140,152,156,170,189,202,214,218,220,231,
00533 232,237,245,267,282,311,313,325,329,330,
00534 348,379,386,388,417,450,453,462,468,472,
00535 481,485]],
00536  [[3,10,33,38,71,74,84,85,87,95,
00537 101,125,144,175,177,178,195,209,219,226,
00538 236,256,268,273,291,302,329,330,349,360,
00539 384,397,413,423,436,443,444,453,454,458,
00540 490]]
00541 ],
00542 /* k=34: */
00543 [
00544  [[10,25,47,49,54,82,91,116,149,153,
00545 158,175,189,191,194,228,232,237,241,258,
00546 260,274,278,295,302,336,337,347,352,384,
00547 387,389,406,411,443,447,450,458,459,482,
00548 484,493,524]],
00549  [[24,25,35,58,72,98,99,121,130,146,
00550 158,177,178,183,204,206,209,215,237,246,
00551 251,275,280,289,311,322,343,348,349,352,
00552 380,391,396,399,426,428,454,463,473,491,
00553 496,497,510,532,533,537]]
00554 ],
00555 /* k=35: */
00556 [
00557  [[8,21,43,72,76,93,95,119,124,126,
00558 137,146,161,190,200,213,235,259,260,262,
00559 268,272,294,297,321,327,342,358,362,364,
00560 365,367,373,391,402,426,428,432,435,445,
00561 467,482,513,539,550]],
00562  [[29,38,57,64,74,104,111,121,128,141,
00563 147,149,160,186,215,229,238,248,252,278,
00564 299,303,325,331,342,345,380,382,386,389,
00565 405,423,426,454,474,483,484,491,493,496,
00566 497,517,548,570]]
00567 ],
00568 /* k=36: */
00569 [
00570  [[7,36,47,64,93,129,134,142,166,168,
00571 171,180,183,187,193,209,212,214,234,265,
00572 291,304,308,323,332,344,352,357,376,378,
00573 386,390,393,398,405,427,431,460,485,509,
00574 513,514,516,549,555,567,578]],
00575  [[4,30,44,69,75,80,98,112,123,132,
00576 161,163,164,197,208,222,243,245,250,263,
00577 265,279,300,302,311,316,349,351,380,385,
00578 405,438,445,464,467,474,475,479,504,511,
00579 532,546,561,569,593,598]]
00580 ],
00581 /* k=37: */
00582 [
00583  [[31,38,54,68,92,94,95,111,112,141,
00584 149,178,181,185,199,222,223,236,240,242,
00585 243,280,309,326,327,329,346,370,384,393,
00586 397,407,420,428,458,475,481,483,499,501,
00587 502,536,567,568,575,588,606,612,622,625,
00588 630]],
00589  [[8,33,65,72,76,107,109,113,118,141,
00590 176,178,187,220,229,252,255,263,266,270,
00591 294,301,324,335,337,342,352,372,377,381,
00592 389,405,435,442,446,448,451,462,485,514,
00593 527,536,553,562,564,573,596,620,625,638]]
00594 ],
00595 /* k=38: */
00596 [
00597  [[11,47,60,69,82,90,92,126,141,143,
00598 149,163,166,174,197,232,233,247,255,282,
00599 284,289,327,341,343,348,385,386,388,416,
00600 430,432,440,459,469,470,477,507,526,527,
00601 534,563,565,587,588,608,618,655,662]],
00602  [[12,20,57,90,91,95,96,105,126,128,
00603 140,174,179,196,205,234,242,247,274,285,
00604 308,313,322,327,339,345,350,362,376,401,
00605 419,433,438,461,469,487,496,506,507,512,
00606 540,561,580,603,607,617,618,644,655,683]]
00607 ],
00608 /* k=39: */
00609 [
00610  [[2,19,25,32,35,42,76,81,92,93,
00611 122,129,134,164,183,190,201,203,240,241,
00612 264,298,300,312,315,317,329,352,386,391,
00613 403,425,426,428,442,446,479,499,513,522,
00614 534,559,560,576,613,627,634,661,664,668,
00615 670,671,687,699]],
00616  [[4,39,64,68,101,106,125,126,162,175,
00617 183,200,212,219,229,250,257,267,287,293,
00618 304,306,330,347,348,380,384,397,405,415,
00619 422,451,458,476,478,479,489,508,515,516,
00620 525,528,546,550,583,589,602,637,639,664,
00621 680,694,698]]
00622 ]
00623 ]$
00624 
00625 /* Making the data related to certificates_pdvdw_3k[k] available in an
00626    easy to use form: the parameter tuple, the two lower bounds, and then
00627    the two lists of certificates.
00628 */
00629 extract_data_certificates_pdvdw_3k(k) := block([C1,C2,L,n1,n2],
00630   [C1,C2] : certificates_pdvdw_3k[k],
00631   L : if k<3 then [k,3] else [3,k],
00632   [n1,n2] : pdvanderwaerden3k(k),
00633   if listp(n1) then n1 : first(n1),
00634   if listp(n2) then n2 : first(n2),
00635   [L,n1,n2,C1,C2])$
00636     
00637 
00638 /* The compressed "full certificates" (as partitions with two blocks) for
00639    vdw_2^pd(3,k):
00640 */
00641 cfull_certificate_pdvdw_3k(k) := block([L,n1,n2,C1,C2],
00642   [L,n1,n2,C1,C2] : extract_data_certificates_pdvdw_3k(k),
00643   [n1,n2] : ceiling(([n1,n2]-1)/2),
00644   [map(lambda([c], create_certificate2_vdw(c,n1)), C1),
00645    map(lambda([c], create_certificate2_vdw(c,n2)), C2)
00646   ])$
00647 
00648 /* The certificates as bit-string: */
00649 cfull_certificate_string_pdvdw_3k(k) :=
00650   map(lambda([L], map(certificatevdw2string,L)), cfull_certificate_pdvdw_3k(k))$
00651 
00652 /* Checking whether certificates_pdvdw_3k[k] are actually pd-vdW-certificates
00653    for the corresponding pair of lower bounds (returning true resp. false for
00654    every alleged certificate):
00655 */
00656 check_certificates_pdvdw_3k(k) := block([L,n1,n2,C1,C2],
00657   [L,n1,n2,C1,C2] : extract_data_certificates_pdvdw_3k(k),
00658   [n1,n2] : [n1,n2]-1,
00659   [
00660    create_list(
00661      certificate_pdvdw_p(L,n1,create_certificate2c_pdvdw(c,n1)),
00662      c, C1),
00663    create_list(
00664      certificate_pdvdw_p(L,n2,create_certificate2c_pdvdw(c,n2)),
00665      c, C2)
00666   ])$
00667