The Scheduling Zoo, shop problems
Lax434175.ZooShops · concepts/Lax434175/ZooShops.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The 327 shop problems of The Scheduling Zoo, each as a specification, and the 237 relations of the zoo among them that are derived here.
A relation of the zoo states that one problem generalizes another. The 221 relations of the first list hold field by field, so that the more special problem is a special case of the more general one. The 16 relations of the second list need a threshold step, so that the decision version of the more special problem reduces to that of the more general one. Each pair lists the more general problem first.
Theorem. Every pair of the first list is a special case, and every pair of the second list is a reduction of decision versions.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.OperationsFamily |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The Scheduling Zoo, shop problems |
| 6 | type: theorem |
| 7 | --- |
| 8 | The 327 shop problems of The Scheduling Zoo, each as a |
| 9 | specification, and the 237 relations of the zoo among them that are |
| 10 | derived here. |
| 11 | |
| 12 | A relation of the zoo states that one problem generalizes another. The |
| 13 | 221 relations of the first list hold field by field, so that the more |
| 14 | special problem is a special case of the more general one. The |
| 15 | 16 relations of the second list need a threshold step, so that the |
| 16 | decision version of the more special problem reduces to that of the more |
| 17 | general one. |
| 18 | Each pair lists the more general problem first. |
| 19 | |
| 20 | **Theorem.** Every pair of the first list is a special case, and every pair |
| 21 | of the second list is a reduction of decision versions. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax434175.ZooShops |
| 25 | open Lax434175 Lax434175.Problems Lax434175.Assembly |
| 26 | |
| 27 | /-- The family of the problems listed here. -/ |
| 28 | abbrev F := OperationsFamily.family |
| 29 | |
| 30 | /-- `F2|no-idle;no-wait|Cmax` -/ |
| 31 | def p0 : Spec F := |
| 32 | OperationsFamily.spec (shopType := .flow) (waiting := .noWait) (idling := .noIdle) |
| 33 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 34 | |
| 35 | /-- `F|no-idle;no-wait|Cmax` -/ |
| 36 | def p1 : Spec F := |
| 37 | OperationsFamily.spec (shopType := .flow) (waiting := .noWait) (idling := .noIdle) |
| 38 | (machineSets := .shop .byPosition) (objective := .makespan) |
| 39 | |
| 40 | /-- `F2|tj|Cmax` -/ |
| 41 | def p2 : Spec F := |
| 42 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 43 | (transportation := { shape := .job, robot := false }) (machineCount := .atMost 2) |
| 44 | (objective := .makespan) |
| 45 | |
| 46 | /-- `F2|pij=1;tj|Cmax` -/ |
| 47 | def p3 : Spec F := |
| 48 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 49 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := false }) |
| 50 | (machineCount := .atMost 2) (objective := .makespan) |
| 51 | |
| 52 | /-- `F||Cmax` -/ |
| 53 | def p4 : Spec F := |
| 54 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 55 | (objective := .makespan) |
| 56 | |
| 57 | /-- `O2||ΣCj` -/ |
| 58 | def p5 : Spec F := |
| 59 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 60 | (machineCount := .atMost 2) (objective := .sumC) |
| 61 | |
| 62 | /-- `O2|fixj|ΣCj` -/ |
| 63 | def p6 : Spec F := |
| 64 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .fix) |
| 65 | (machineCount := .atMost 2) (objective := .sumC) |
| 66 | |
| 67 | /-- `O2|Mj|ΣCj` -/ |
| 68 | def p7 : Spec F := |
| 69 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .sets) |
| 70 | (machineCount := .atMost 2) (objective := .sumC) |
| 71 | |
| 72 | /-- `F|intree;pij=1|ΣCj` -/ |
| 73 | def p8 : Spec F := |
| 74 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 75 | (machineSets := .shop .byPosition) (precedence := ⟨.intree, .zero⟩) (objective := .sumC) |
| 76 | |
| 77 | /-- `O|pij=1;rj|ΣwjUj` -/ |
| 78 | def p9 : Spec F := |
| 79 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 80 | (machineSets := .shop .byPosition) (objective := .sumWU) |
| 81 | |
| 82 | /-- `J|fixj;n=2|ΣwjUj` -/ |
| 83 | def p10 : Spec F := |
| 84 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 2) (machineSets := .shop .fix) |
| 85 | (objective := .sumWU) |
| 86 | |
| 87 | /-- `J|fixj;n=2|ΣwjTj` -/ |
| 88 | def p11 : Spec F := |
| 89 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 2) (machineSets := .shop .fix) |
| 90 | (objective := .sumWT) |
| 91 | |
| 92 | /-- `F|Mj;prec;rj;n=k|ΣwjUj` -/ |
| 93 | def p12 : Spec F := |
| 94 | OperationsFamily.spec (shopType := .flow) (jobCount := .constant) (release := .releaseDates) |
| 95 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .sumWU) |
| 96 | |
| 97 | /-- `F|Mj;prec;rj;n=k|ΣwjTj` -/ |
| 98 | def p13 : Spec F := |
| 99 | OperationsFamily.spec (shopType := .flow) (jobCount := .constant) (release := .releaseDates) |
| 100 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .sumWT) |
| 101 | |
| 102 | /-- `O|Mj;prec;rj;n=k|ΣwjUj` -/ |
| 103 | def p14 : Spec F := |
| 104 | OperationsFamily.spec (shopType := .open) (jobCount := .constant) (release := .releaseDates) |
| 105 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .sumWU) |
| 106 | |
| 107 | /-- `O|Mj;prec;rj;n=k|ΣwjTj` -/ |
| 108 | def p15 : Spec F := |
| 109 | OperationsFamily.spec (shopType := .open) (jobCount := .constant) (release := .releaseDates) |
| 110 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .sumWT) |
| 111 | |
| 112 | /-- `O|pij=1;intree|Lmax` -/ |
| 113 | def p16 : Spec F := |
| 114 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 115 | (machineSets := .shop .byPosition) (precedence := ⟨.intree, .zero⟩) (objective := .lmax) |
| 116 | |
| 117 | /-- `O2|pij=1;prec;rj|Lmax` -/ |
| 118 | def p17 : Spec F := |
| 119 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 120 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 121 | (objective := .lmax) |
| 122 | |
| 123 | /-- `J|prec;rj;n=k;no-wait|ΣwjUj` -/ |
| 124 | def p18 : Spec F := |
| 125 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (waiting := .noWait) |
| 126 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 127 | (objective := .sumWU) |
| 128 | |
| 129 | /-- `J|prec;rj;n=k;no-wait|ΣwjTj` -/ |
| 130 | def p19 : Spec F := |
| 131 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (waiting := .noWait) |
| 132 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 133 | (objective := .sumWT) |
| 134 | |
| 135 | /-- `O|pij=1;chains;rj|Lmax` -/ |
| 136 | def p20 : Spec F := |
| 137 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 138 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) (objective := .lmax) |
| 139 | |
| 140 | /-- `O|pij=1;intree;no-wait|ΣCj` -/ |
| 141 | def p21 : Spec F := |
| 142 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 143 | (machineSets := .shop .byPosition) (precedence := ⟨.intree, .zero⟩) (objective := .sumC) |
| 144 | |
| 145 | /-- `O|pij=1;rj;no-wait|ΣwjUj` -/ |
| 146 | def p22 : Spec F := |
| 147 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 148 | (release := .releaseDates) (machineSets := .shop .byPosition) (objective := .sumWU) |
| 149 | |
| 150 | /-- `F3;R1|pij=1;tk;rj|Cmax` -/ |
| 151 | def p23 : Spec F := |
| 152 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 153 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := true }) |
| 154 | (machineCount := .atMost 3) (objective := .makespan) |
| 155 | |
| 156 | /-- `F3;R1|pij=1;tk|Lmax` -/ |
| 157 | def p24 : Spec F := |
| 158 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 159 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := true }) |
| 160 | (machineCount := .atMost 3) (objective := .lmax) |
| 161 | |
| 162 | /-- `F|pij=1;tj|ΣCj` -/ |
| 163 | def p25 : Spec F := |
| 164 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 165 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := false }) |
| 166 | (objective := .sumC) |
| 167 | |
| 168 | /-- `F2|pij=1;tj;rj|ΣCj` -/ |
| 169 | def p26 : Spec F := |
| 170 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 171 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := false }) |
| 172 | (machineCount := .atMost 2) (objective := .sumC) |
| 173 | |
| 174 | /-- `F2|pij=1;tj|ΣwjCj` -/ |
| 175 | def p27 : Spec F := |
| 176 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 177 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := false }) |
| 178 | (machineCount := .atMost 2) (objective := .sumWC) |
| 179 | |
| 180 | /-- `O2|pij=1;tjkl=T;rj|Cmax` -/ |
| 181 | def p28 : Spec F := |
| 182 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 183 | (machineSets := .shop .byPosition) (transportation := { shape := .uniform, robot := false }) |
| 184 | (machineCount := .atMost 2) (objective := .makespan) |
| 185 | |
| 186 | /-- `O2|pij=1;tkl|Cmax` -/ |
| 187 | def p29 : Spec F := |
| 188 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 189 | (machineSets := .shop .byPosition) (transportation := { shape := .pair, robot := false }) |
| 190 | (machineCount := .atMost 2) (objective := .makespan) |
| 191 | |
| 192 | /-- `O2|pij=1;tkl|ΣwjCj` -/ |
| 193 | def p30 : Spec F := |
| 194 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 195 | (machineSets := .shop .byPosition) (transportation := { shape := .pair, robot := false }) |
| 196 | (machineCount := .atMost 2) (objective := .sumWC) |
| 197 | |
| 198 | /-- `O2|pij=1;tjkl=T|ΣUj` -/ |
| 199 | def p31 : Spec F := |
| 200 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 201 | (machineSets := .shop .byPosition) (transportation := { shape := .uniform, robot := false }) |
| 202 | (machineCount := .atMost 2) (objective := .sumU) |
| 203 | |
| 204 | /-- `O2|pij=1;tj;rj|ΣCj` -/ |
| 205 | def p32 : Spec F := |
| 206 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 207 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := false }) |
| 208 | (machineCount := .atMost 2) (objective := .sumC) |
| 209 | |
| 210 | /-- `O2|pij=1;tj|ΣwjCj` -/ |
| 211 | def p33 : Spec F := |
| 212 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 213 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := false }) |
| 214 | (machineCount := .atMost 2) (objective := .sumWC) |
| 215 | |
| 216 | /-- `O|pij=1;intree;no-wait|Lmax` -/ |
| 217 | def p34 : Spec F := |
| 218 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 219 | (machineSets := .shop .byPosition) (precedence := ⟨.intree, .zero⟩) (objective := .lmax) |
| 220 | |
| 221 | /-- `O|pij=1;outtree;no-wait|Lmax` -/ |
| 222 | def p35 : Spec F := |
| 223 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 224 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .lmax) |
| 225 | |
| 226 | /-- `F|Mj;intree;rj;pij=1|Cmax` -/ |
| 227 | def p36 : Spec F := |
| 228 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 229 | (machineSets := .shop .sets) (precedence := ⟨.intree, .zero⟩) (objective := .makespan) |
| 230 | |
| 231 | /-- `F|Mj;outtree;pij=1|Lmax` -/ |
| 232 | def p37 : Spec F := |
| 233 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 234 | (machineSets := .shop .sets) (precedence := ⟨.outtree, .zero⟩) (objective := .lmax) |
| 235 | |
| 236 | /-- `O|pij=1;rj|Lmax` -/ |
| 237 | def p38 : Spec F := |
| 238 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 239 | (machineSets := .shop .byPosition) (objective := .lmax) |
| 240 | |
| 241 | /-- `O|pij=1|ΣwjCj` -/ |
| 242 | def p39 : Spec F := |
| 243 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 244 | (machineSets := .shop .byPosition) (objective := .sumWC) |
| 245 | |
| 246 | /-- `O2|pij=1;prec|ΣUj` -/ |
| 247 | def p40 : Spec F := |
| 248 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 249 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 250 | (objective := .sumU) |
| 251 | |
| 252 | /-- `O|pij=1;tree;no-wait|Cmax` -/ |
| 253 | def p41 : Spec F := |
| 254 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 255 | (machineSets := .shop .byPosition) (precedence := ⟨.tree, .zero⟩) (objective := .makespan) |
| 256 | |
| 257 | /-- `O2|pij=1;prec;no-wait|Cmax` -/ |
| 258 | def p42 : Spec F := |
| 259 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 260 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 261 | (objective := .makespan) |
| 262 | |
| 263 | /-- `O|pij=1;rj;no-wait|Lmax` -/ |
| 264 | def p43 : Spec F := |
| 265 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 266 | (release := .releaseDates) (machineSets := .shop .byPosition) (objective := .lmax) |
| 267 | |
| 268 | /-- `O|pij=1;outtree;no-wait|ΣCj` -/ |
| 269 | def p44 : Spec F := |
| 270 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 271 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .sumC) |
| 272 | |
| 273 | /-- `O|pij=1;no-wait|ΣwjTj` -/ |
| 274 | def p45 : Spec F := |
| 275 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 276 | (machineSets := .shop .byPosition) (objective := .sumWT) |
| 277 | |
| 278 | /-- `F|Mj;n=3|Cmax` -/ |
| 279 | def p46 : Spec F := |
| 280 | OperationsFamily.spec (shopType := .flow) (jobCount := .atMost 3) (machineSets := .shop .sets) |
| 281 | (objective := .makespan) |
| 282 | |
| 283 | /-- `F|Mj;rj;pij=1|Cmax` -/ |
| 284 | def p47 : Spec F := |
| 285 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 286 | (machineSets := .shop .sets) (objective := .makespan) |
| 287 | |
| 288 | /-- `F|Mj;rj;pij=1|ΣCj` -/ |
| 289 | def p48 : Spec F := |
| 290 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 291 | (machineSets := .shop .sets) (objective := .sumC) |
| 292 | |
| 293 | /-- `F|Mj;pij=1|ΣwjCj` -/ |
| 294 | def p49 : Spec F := |
| 295 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 296 | (machineSets := .shop .sets) (objective := .sumWC) |
| 297 | |
| 298 | /-- `F|Mj;pij=1|ΣwjUj` -/ |
| 299 | def p50 : Spec F := |
| 300 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 301 | (machineSets := .shop .sets) (objective := .sumWU) |
| 302 | |
| 303 | /-- `F|Mj;pij=1|ΣTj` -/ |
| 304 | def p51 : Spec F := |
| 305 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 306 | (machineSets := .shop .sets) (objective := .sumT) |
| 307 | |
| 308 | /-- `J|Mj;prec;rj;pij=1;n=k|ΣwjUj` -/ |
| 309 | def p52 : Spec F := |
| 310 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (processingTimes := .unit) |
| 311 | (release := .releaseDates) (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) |
| 312 | (objective := .sumWU) |
| 313 | |
| 314 | /-- `J|Mj;prec;rj;pij=1;n=k|ΣwjTj` -/ |
| 315 | def p53 : Spec F := |
| 316 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (processingTimes := .unit) |
| 317 | (release := .releaseDates) (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) |
| 318 | (objective := .sumWT) |
| 319 | |
| 320 | /-- `O|Mj;rj;pij=1|Cmax` -/ |
| 321 | def p54 : Spec F := |
| 322 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 323 | (machineSets := .shop .sets) (objective := .makespan) |
| 324 | |
| 325 | /-- `O|Mj;rj;pij=1|ΣCj` -/ |
| 326 | def p55 : Spec F := |
| 327 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 328 | (machineSets := .shop .sets) (objective := .sumC) |
| 329 | |
| 330 | /-- `O|Mj;pij=1|ΣwjCj` -/ |
| 331 | def p56 : Spec F := |
| 332 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 333 | (machineSets := .shop .sets) (objective := .sumWC) |
| 334 | |
| 335 | /-- `O|Mj;pij=1|ΣwjUj` -/ |
| 336 | def p57 : Spec F := |
| 337 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 338 | (machineSets := .shop .sets) (objective := .sumWU) |
| 339 | |
| 340 | /-- `O|Mj;pij=1|ΣTj` -/ |
| 341 | def p58 : Spec F := |
| 342 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 343 | (machineSets := .shop .sets) (objective := .sumT) |
| 344 | |
| 345 | /-- `F|pij=1;outtree;rj|Cmax` -/ |
| 346 | def p59 : Spec F := |
| 347 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 348 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .makespan) |
| 349 | |
| 350 | /-- `F|pij=1;tree|Cmax` -/ |
| 351 | def p60 : Spec F := |
| 352 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 353 | (machineSets := .shop .byPosition) (precedence := ⟨.tree, .zero⟩) (objective := .makespan) |
| 354 | |
| 355 | /-- `F|pij=1;intree|Lmax` -/ |
| 356 | def p61 : Spec F := |
| 357 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 358 | (machineSets := .shop .byPosition) (precedence := ⟨.intree, .zero⟩) (objective := .lmax) |
| 359 | |
| 360 | /-- `F2|pij=1;prec;rj|Lmax` -/ |
| 361 | def p62 : Spec F := |
| 362 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 363 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 364 | (objective := .lmax) |
| 365 | |
| 366 | /-- `O2|fixj|Cmax` -/ |
| 367 | def p63 : Spec F := |
| 368 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .fix) |
| 369 | (machineCount := .atMost 2) (objective := .makespan) |
| 370 | |
| 371 | /-- `J2|fixj;n=k|Cmax` -/ |
| 372 | def p64 : Spec F := |
| 373 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (machineSets := .shop .fix) |
| 374 | (machineCount := .atMost 2) (objective := .makespan) |
| 375 | |
| 376 | /-- `F2|fixj|Cmax` -/ |
| 377 | def p65 : Spec F := |
| 378 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .fix) |
| 379 | (machineCount := .atMost 2) (objective := .makespan) |
| 380 | |
| 381 | /-- `J2|fixj;pij=1|Cmax` -/ |
| 382 | def p66 : Spec F := |
| 383 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .fix) |
| 384 | (machineCount := .atMost 2) (objective := .makespan) |
| 385 | |
| 386 | /-- `J|prec;pij=1;rj;n=k|ΣwjUj` -/ |
| 387 | def p67 : Spec F := |
| 388 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (processingTimes := .unit) |
| 389 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 390 | (objective := .sumWU) |
| 391 | |
| 392 | /-- `J|prec;pij=1;rj;n=k|ΣwjTj` -/ |
| 393 | def p68 : Spec F := |
| 394 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (processingTimes := .unit) |
| 395 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 396 | (objective := .sumWT) |
| 397 | |
| 398 | /-- `F|fixj;rj;pij=1|Cmax` -/ |
| 399 | def p69 : Spec F := |
| 400 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 401 | (machineSets := .shop .fix) (objective := .makespan) |
| 402 | |
| 403 | /-- `F|fixj;rj;pij=1|ΣCj` -/ |
| 404 | def p70 : Spec F := |
| 405 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 406 | (machineSets := .shop .fix) (objective := .sumC) |
| 407 | |
| 408 | /-- `F|fixj;pij=1|ΣwjCj` -/ |
| 409 | def p71 : Spec F := |
| 410 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 411 | (objective := .sumWC) |
| 412 | |
| 413 | /-- `F|fixj;pij=1|ΣwjUj` -/ |
| 414 | def p72 : Spec F := |
| 415 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 416 | (objective := .sumWU) |
| 417 | |
| 418 | /-- `F|fixj;pij=1|ΣwjTj` -/ |
| 419 | def p73 : Spec F := |
| 420 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 421 | (objective := .sumWT) |
| 422 | |
| 423 | /-- `J|fixj;prec;rj;pij=1;n=k|ΣwjUj` -/ |
| 424 | def p74 : Spec F := |
| 425 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (processingTimes := .unit) |
| 426 | (release := .releaseDates) (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) |
| 427 | (objective := .sumWU) |
| 428 | |
| 429 | /-- `J|fixj;prec;rj;pij=1;n=k|ΣwjTj` -/ |
| 430 | def p75 : Spec F := |
| 431 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (processingTimes := .unit) |
| 432 | (release := .releaseDates) (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) |
| 433 | (objective := .sumWT) |
| 434 | |
| 435 | /-- `O|fixj;rj;pij=1|Cmax` -/ |
| 436 | def p76 : Spec F := |
| 437 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 438 | (machineSets := .shop .fix) (objective := .makespan) |
| 439 | |
| 440 | /-- `O|fixj;rj;pij=1|ΣCj` -/ |
| 441 | def p77 : Spec F := |
| 442 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 443 | (machineSets := .shop .fix) (objective := .sumC) |
| 444 | |
| 445 | /-- `O|fixj;pij=1|ΣwjCj` -/ |
| 446 | def p78 : Spec F := |
| 447 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 448 | (objective := .sumWC) |
| 449 | |
| 450 | /-- `O|fixj;pij=1|ΣwjUj` -/ |
| 451 | def p79 : Spec F := |
| 452 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 453 | (objective := .sumWU) |
| 454 | |
| 455 | /-- `O|fixj;pij=1|ΣTj` -/ |
| 456 | def p80 : Spec F := |
| 457 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 458 | (objective := .sumT) |
| 459 | |
| 460 | /-- `F|pij=1;outtree;rj|ΣCj` -/ |
| 461 | def p81 : Spec F := |
| 462 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 463 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .sumC) |
| 464 | |
| 465 | /-- `F2|pij=1;prec|ΣCj` -/ |
| 466 | def p82 : Spec F := |
| 467 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 468 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 469 | (objective := .sumC) |
| 470 | |
| 471 | /-- `F|pij=1;intree;rj|Cmax` -/ |
| 472 | def p83 : Spec F := |
| 473 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 474 | (machineSets := .shop .byPosition) (precedence := ⟨.intree, .zero⟩) (objective := .makespan) |
| 475 | |
| 476 | /-- `F|pij=1;outtree|Lmax` -/ |
| 477 | def p84 : Spec F := |
| 478 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 479 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .lmax) |
| 480 | |
| 481 | /-- `F2|pij=1;chains|ΣUj` -/ |
| 482 | def p85 : Spec F := |
| 483 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 484 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 485 | (machineCount := .atMost 2) (objective := .sumU) |
| 486 | |
| 487 | /-- `F3|pij=1;chains|ΣUj` -/ |
| 488 | def p86 : Spec F := |
| 489 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 490 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 491 | (machineCount := .atMost 3) (objective := .sumU) |
| 492 | |
| 493 | /-- `F2|pij=1;chains|ΣTj` -/ |
| 494 | def p87 : Spec F := |
| 495 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 496 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 497 | (machineCount := .atMost 2) (objective := .sumT) |
| 498 | |
| 499 | /-- `F3|pij=1;chains|ΣTj` -/ |
| 500 | def p88 : Spec F := |
| 501 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 502 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 503 | (machineCount := .atMost 3) (objective := .sumT) |
| 504 | |
| 505 | /-- `F|fixj;tree;rj;pij=1|Cmax` -/ |
| 506 | def p89 : Spec F := |
| 507 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 508 | (machineSets := .shop .fix) (precedence := ⟨.tree, .zero⟩) (objective := .makespan) |
| 509 | |
| 510 | /-- `F|fixj;tree;pij=1|Lmax` -/ |
| 511 | def p90 : Spec F := |
| 512 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 513 | (precedence := ⟨.tree, .zero⟩) (objective := .lmax) |
| 514 | |
| 515 | /-- `O|pij=1;rj|ΣCj` -/ |
| 516 | def p91 : Spec F := |
| 517 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 518 | (machineSets := .shop .byPosition) (objective := .sumC) |
| 519 | |
| 520 | /-- `J2|n=k|ΣwjUj` -/ |
| 521 | def p92 : Spec F := |
| 522 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) |
| 523 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWU) |
| 524 | |
| 525 | /-- `J2|n=k|ΣwjTj` -/ |
| 526 | def p93 : Spec F := |
| 527 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) |
| 528 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWT) |
| 529 | |
| 530 | /-- `F2;S1|pij=p;sij=s;rj|Cmax` -/ |
| 531 | def p94 : Spec F := |
| 532 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 533 | (machineSets := .shop .byPosition) (server := .equal) (machineCount := .atMost 2) |
| 534 | (objective := .makespan) |
| 535 | |
| 536 | /-- `F;S1|pij=1;sij=s;rj|Cmax` -/ |
| 537 | def p95 : Spec F := |
| 538 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 539 | (machineSets := .shop .byPosition) (server := .equal) (objective := .makespan) |
| 540 | |
| 541 | /-- `F;S1|pij=p;sij=s|Cmax` -/ |
| 542 | def p96 : Spec F := |
| 543 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 544 | (machineSets := .shop .byPosition) (server := .equal) (objective := .makespan) |
| 545 | |
| 546 | /-- `F2;S1|pij=p;sij=s;rj|ΣCj` -/ |
| 547 | def p97 : Spec F := |
| 548 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 549 | (machineSets := .shop .byPosition) (server := .equal) (machineCount := .atMost 2) |
| 550 | (objective := .sumC) |
| 551 | |
| 552 | /-- `F;S1|pij=1;sij=s;rj|ΣCj` -/ |
| 553 | def p98 : Spec F := |
| 554 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 555 | (machineSets := .shop .byPosition) (server := .equal) (objective := .sumC) |
| 556 | |
| 557 | /-- `F2;S1|pij=p|Cmax` -/ |
| 558 | def p99 : Spec F := |
| 559 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 560 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 2) |
| 561 | (objective := .makespan) |
| 562 | |
| 563 | /-- `F2;S1|sij=s|Cmax` -/ |
| 564 | def p100 : Spec F := |
| 565 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) (server := .equal) |
| 566 | (machineCount := .atMost 2) (objective := .makespan) |
| 567 | |
| 568 | /-- `F2;S1|pij=1;rj|Lmax` -/ |
| 569 | def p101 : Spec F := |
| 570 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 571 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 2) |
| 572 | (objective := .lmax) |
| 573 | |
| 574 | /-- `F3;S1|pij=1;rj|Lmax` -/ |
| 575 | def p102 : Spec F := |
| 576 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 577 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 3) |
| 578 | (objective := .lmax) |
| 579 | |
| 580 | /-- `F2;S1|pij=1;rj|ΣCj` -/ |
| 581 | def p103 : Spec F := |
| 582 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 583 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 2) |
| 584 | (objective := .sumC) |
| 585 | |
| 586 | /-- `F3;S1|pij=1;rj|ΣCj` -/ |
| 587 | def p104 : Spec F := |
| 588 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 589 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 3) |
| 590 | (objective := .sumC) |
| 591 | |
| 592 | /-- `F2;S1|pij=1|ΣwjUj` -/ |
| 593 | def p105 : Spec F := |
| 594 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 595 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 2) |
| 596 | (objective := .sumWU) |
| 597 | |
| 598 | /-- `F3;S1|pij=1|ΣwjUj` -/ |
| 599 | def p106 : Spec F := |
| 600 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 601 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 3) |
| 602 | (objective := .sumWU) |
| 603 | |
| 604 | /-- `F2;S1|pij=1|ΣTj` -/ |
| 605 | def p107 : Spec F := |
| 606 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 607 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 2) |
| 608 | (objective := .sumT) |
| 609 | |
| 610 | /-- `F3;S1|pij=1|ΣTj` -/ |
| 611 | def p108 : Spec F := |
| 612 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 613 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 3) |
| 614 | (objective := .sumT) |
| 615 | |
| 616 | /-- `F2;S1|pij=1|ΣwjTj` -/ |
| 617 | def p109 : Spec F := |
| 618 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 619 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 2) |
| 620 | (objective := .sumWT) |
| 621 | |
| 622 | /-- `F3;S1|pij=1|ΣwjTj` -/ |
| 623 | def p110 : Spec F := |
| 624 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 625 | (machineSets := .shop .byPosition) (server := .arbitrary) (machineCount := .atMost 3) |
| 626 | (objective := .sumWT) |
| 627 | |
| 628 | /-- `F3;S1|sij=1|Cmax` -/ |
| 629 | def p111 : Spec F := |
| 630 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) (server := .unit) |
| 631 | (machineCount := .atMost 3) (objective := .makespan) |
| 632 | |
| 633 | /-- `F2;S1|sij=1|ΣCj` -/ |
| 634 | def p112 : Spec F := |
| 635 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) (server := .unit) |
| 636 | (machineCount := .atMost 2) (objective := .sumC) |
| 637 | |
| 638 | /-- `F2;S1|pij=p;sij=s|ΣwjUj` -/ |
| 639 | def p113 : Spec F := |
| 640 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 641 | (machineSets := .shop .byPosition) (server := .equal) (machineCount := .atMost 2) |
| 642 | (objective := .sumWU) |
| 643 | |
| 644 | /-- `F;S1|pij=1;sij=s|ΣwjUj` -/ |
| 645 | def p114 : Spec F := |
| 646 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 647 | (machineSets := .shop .byPosition) (server := .equal) (objective := .sumWU) |
| 648 | |
| 649 | /-- `F2;S1|pij=p;sij=s|ΣwjTj` -/ |
| 650 | def p115 : Spec F := |
| 651 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 652 | (machineSets := .shop .byPosition) (server := .equal) (machineCount := .atMost 2) |
| 653 | (objective := .sumWT) |
| 654 | |
| 655 | /-- `F;S1|pij=1;sij=s|ΣwjTj` -/ |
| 656 | def p116 : Spec F := |
| 657 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 658 | (machineSets := .shop .byPosition) (server := .equal) (objective := .sumWT) |
| 659 | |
| 660 | /-- `F2;S1|pij=p;sij=1;rj|ΣwjCj` -/ |
| 661 | def p117 : Spec F := |
| 662 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 663 | (machineSets := .shop .byPosition) (server := .unit) (machineCount := .atMost 2) |
| 664 | (objective := .sumWC) |
| 665 | |
| 666 | /-- `F2;S1|pij=p;sij=1;rj|ΣwjUj` -/ |
| 667 | def p118 : Spec F := |
| 668 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 669 | (machineSets := .shop .byPosition) (server := .unit) (machineCount := .atMost 2) |
| 670 | (objective := .sumWU) |
| 671 | |
| 672 | /-- `F2;S1|pij=p;sij=1;rj|ΣTj` -/ |
| 673 | def p119 : Spec F := |
| 674 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 675 | (machineSets := .shop .byPosition) (server := .unit) (machineCount := .atMost 2) |
| 676 | (objective := .sumT) |
| 677 | |
| 678 | /-- `O|pij=1;tree|Cmax` -/ |
| 679 | def p120 : Spec F := |
| 680 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 681 | (machineSets := .shop .byPosition) (precedence := ⟨.tree, .zero⟩) (objective := .makespan) |
| 682 | |
| 683 | /-- `O|pij=1;outtree|ΣCj` -/ |
| 684 | def p121 : Spec F := |
| 685 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 686 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .sumC) |
| 687 | |
| 688 | /-- `O2|pij=1;tree|ΣCj` -/ |
| 689 | def p122 : Spec F := |
| 690 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 691 | (machineSets := .shop .byPosition) (precedence := ⟨.tree, .zero⟩) (machineCount := .atMost 2) |
| 692 | (objective := .sumC) |
| 693 | |
| 694 | /-- `F2|pij=1;prec;rj|ΣCj` -/ |
| 695 | def p123 : Spec F := |
| 696 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 697 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 698 | (objective := .sumC) |
| 699 | |
| 700 | /-- `O2|pij=1;prec|ΣCj` -/ |
| 701 | def p124 : Spec F := |
| 702 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 703 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 704 | (objective := .sumC) |
| 705 | |
| 706 | /-- `F2|no-wait|Cmax` -/ |
| 707 | def p125 : Spec F := |
| 708 | OperationsFamily.spec (shopType := .flow) (waiting := .noWait) |
| 709 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 710 | |
| 711 | /-- `F3||Cmax` -/ |
| 712 | def p126 : Spec F := |
| 713 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 714 | (machineCount := .atMost 3) (objective := .makespan) |
| 715 | |
| 716 | /-- `F2||ΣCj` -/ |
| 717 | def p127 : Spec F := |
| 718 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 719 | (machineCount := .atMost 2) (objective := .sumC) |
| 720 | |
| 721 | /-- `J2||ΣCj` -/ |
| 722 | def p128 : Spec F := |
| 723 | OperationsFamily.spec (shopType := .job) (machineSets := .shop .dedicated) |
| 724 | (machineCount := .atMost 2) (objective := .sumC) |
| 725 | |
| 726 | /-- `F2|fixj|ΣCj` -/ |
| 727 | def p129 : Spec F := |
| 728 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .fix) |
| 729 | (machineCount := .atMost 2) (objective := .sumC) |
| 730 | |
| 731 | /-- `F3|Mj|Cmax` -/ |
| 732 | def p130 : Spec F := |
| 733 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .sets) |
| 734 | (machineCount := .atMost 3) (objective := .makespan) |
| 735 | |
| 736 | /-- `F2|Mj|ΣCj` -/ |
| 737 | def p131 : Spec F := |
| 738 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .sets) |
| 739 | (machineCount := .atMost 2) (objective := .sumC) |
| 740 | |
| 741 | /-- `O2||Cmax` -/ |
| 742 | def p132 : Spec F := |
| 743 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 744 | (machineCount := .atMost 2) (objective := .makespan) |
| 745 | |
| 746 | /-- `O3||Cmax` -/ |
| 747 | def p133 : Spec F := |
| 748 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 749 | (machineCount := .atMost 3) (objective := .makespan) |
| 750 | |
| 751 | /-- `O|fixj;n=3|Cmax` -/ |
| 752 | def p134 : Spec F := |
| 753 | OperationsFamily.spec (shopType := .open) (jobCount := .atMost 3) (machineSets := .shop .fix) |
| 754 | (objective := .makespan) |
| 755 | |
| 756 | /-- `O3|fixj|Cmax` -/ |
| 757 | def p135 : Spec F := |
| 758 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .fix) |
| 759 | (machineCount := .atMost 3) (objective := .makespan) |
| 760 | |
| 761 | /-- `O|Mj;n=3|Cmax` -/ |
| 762 | def p136 : Spec F := |
| 763 | OperationsFamily.spec (shopType := .open) (jobCount := .atMost 3) (machineSets := .shop .sets) |
| 764 | (objective := .makespan) |
| 765 | |
| 766 | /-- `O3|Mj|Cmax` -/ |
| 767 | def p137 : Spec F := |
| 768 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .sets) |
| 769 | (machineCount := .atMost 3) (objective := .makespan) |
| 770 | |
| 771 | /-- `F2;R1|pij=1;tjk|Cmax` -/ |
| 772 | def p138 : Spec F := |
| 773 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 774 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 775 | (machineCount := .atMost 2) (objective := .makespan) |
| 776 | |
| 777 | /-- `F2;R1|pij=p;tj∈T1,T2|Cmax` -/ |
| 778 | def p139 : Spec F := |
| 779 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 780 | (machineSets := .shop .byPosition) (transportation := { shape := .twoValues, robot := true }) |
| 781 | (machineCount := .atMost 2) (objective := .makespan) |
| 782 | |
| 783 | /-- `F;R1|n≥m-1;pij=p;tk|Cmax` -/ |
| 784 | def p140 : Spec F := |
| 785 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 786 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := true }) |
| 787 | (machineCount := .atMostJobsPlusOne) (objective := .makespan) |
| 788 | |
| 789 | /-- `F2;R1|pij=p;tj|Cmax` -/ |
| 790 | def p141 : Spec F := |
| 791 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 792 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := true }) |
| 793 | (machineCount := .atMost 2) (objective := .makespan) |
| 794 | |
| 795 | /-- `F2;R1|tjk=T|Cmax` -/ |
| 796 | def p142 : Spec F := |
| 797 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 798 | (transportation := { shape := .uniform, robot := true }) (machineCount := .atMost 2) |
| 799 | (objective := .makespan) |
| 800 | |
| 801 | /-- `F2||Cmax` -/ |
| 802 | def p143 : Spec F := |
| 803 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 804 | (machineCount := .atMost 2) (objective := .makespan) |
| 805 | |
| 806 | /-- `F2|tk|Cmax` -/ |
| 807 | def p144 : Spec F := |
| 808 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 809 | (transportation := { shape := .source, robot := false }) (machineCount := .atMost 2) |
| 810 | (objective := .makespan) |
| 811 | |
| 812 | /-- `F2|tjk=T|Cmax` -/ |
| 813 | def p145 : Spec F := |
| 814 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 815 | (transportation := { shape := .uniform, robot := false }) (machineCount := .atMost 2) |
| 816 | (objective := .makespan) |
| 817 | |
| 818 | /-- `J|Mj;prec;rj;n=2|Lmax` -/ |
| 819 | def p146 : Spec F := |
| 820 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 2) (release := .releaseDates) |
| 821 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .lmax) |
| 822 | |
| 823 | /-- `J2|Mj;n=3|Cmax` -/ |
| 824 | def p147 : Spec F := |
| 825 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 3) (machineSets := .shop .sets) |
| 826 | (machineCount := .atMost 2) (objective := .makespan) |
| 827 | |
| 828 | /-- `O|Mj;pij=1|Cmax` -/ |
| 829 | def p148 : Spec F := |
| 830 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 831 | (machineSets := .shop .sets) (objective := .makespan) |
| 832 | |
| 833 | /-- `J2|pij=1;no-wait|Cmax` -/ |
| 834 | def p149 : Spec F := |
| 835 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 836 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .makespan) |
| 837 | |
| 838 | /-- `F|fixj;prec;rj;n=k|ΣwjUj` -/ |
| 839 | def p150 : Spec F := |
| 840 | OperationsFamily.spec (shopType := .flow) (jobCount := .constant) (release := .releaseDates) |
| 841 | (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) (objective := .sumWU) |
| 842 | |
| 843 | /-- `F|fixj;prec;rj;n=k|ΣwjTj` -/ |
| 844 | def p151 : Spec F := |
| 845 | OperationsFamily.spec (shopType := .flow) (jobCount := .constant) (release := .releaseDates) |
| 846 | (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) (objective := .sumWT) |
| 847 | |
| 848 | /-- `O|fixj;prec;rj;pij=1;n=2|ΣwjUj` -/ |
| 849 | def p152 : Spec F := |
| 850 | OperationsFamily.spec (shopType := .open) (jobCount := .atMost 2) (processingTimes := .unit) |
| 851 | (release := .releaseDates) (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) |
| 852 | (objective := .sumWU) |
| 853 | |
| 854 | /-- `O|fixj;prec;rj;n=k|ΣwjUj` -/ |
| 855 | def p153 : Spec F := |
| 856 | OperationsFamily.spec (shopType := .open) (jobCount := .constant) (release := .releaseDates) |
| 857 | (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) (objective := .sumWU) |
| 858 | |
| 859 | /-- `O|fixj;prec;rj;pij=1;n=2|ΣwjTj` -/ |
| 860 | def p154 : Spec F := |
| 861 | OperationsFamily.spec (shopType := .open) (jobCount := .atMost 2) (processingTimes := .unit) |
| 862 | (release := .releaseDates) (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) |
| 863 | (objective := .sumWT) |
| 864 | |
| 865 | /-- `O|fixj;prec;rj;n=k|ΣwjTj` -/ |
| 866 | def p155 : Spec F := |
| 867 | OperationsFamily.spec (shopType := .open) (jobCount := .constant) (release := .releaseDates) |
| 868 | (machineSets := .shop .fix) (precedence := ⟨.prec, .zero⟩) (objective := .sumWT) |
| 869 | |
| 870 | /-- `F|fixj;n=3|Cmax` -/ |
| 871 | def p156 : Spec F := |
| 872 | OperationsFamily.spec (shopType := .flow) (jobCount := .atMost 3) (machineSets := .shop .fix) |
| 873 | (objective := .makespan) |
| 874 | |
| 875 | /-- `F2;R1|pij=p;tk;rj|ΣwjCj` -/ |
| 876 | def p157 : Spec F := |
| 877 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 878 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := true }) |
| 879 | (machineCount := .atMost 2) (objective := .sumWC) |
| 880 | |
| 881 | /-- `F2;R1|pij=p;tk;rj|ΣwjUj` -/ |
| 882 | def p158 : Spec F := |
| 883 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 884 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := true }) |
| 885 | (machineCount := .atMost 2) (objective := .sumWU) |
| 886 | |
| 887 | /-- `F2;R1|pij=p;tk;rj|ΣTj` -/ |
| 888 | def p159 : Spec F := |
| 889 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 890 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := true }) |
| 891 | (machineCount := .atMost 2) (objective := .sumT) |
| 892 | |
| 893 | /-- `F2;R1|pij=p;tk|ΣwjTj` -/ |
| 894 | def p160 : Spec F := |
| 895 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 896 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := true }) |
| 897 | (machineCount := .atMost 2) (objective := .sumWT) |
| 898 | |
| 899 | /-- `F3;R1|pij=p;tjk;rj|Cmax` -/ |
| 900 | def p161 : Spec F := |
| 901 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) (release := .releaseDates) |
| 902 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 903 | (machineCount := .atMost 3) (objective := .makespan) |
| 904 | |
| 905 | /-- `F2;R1|pij=1;tj;rj|Lmax` -/ |
| 906 | def p162 : Spec F := |
| 907 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 908 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := true }) |
| 909 | (machineCount := .atMost 2) (objective := .lmax) |
| 910 | |
| 911 | /-- `F3;R1|pij=1;tjk;rj|Lmax` -/ |
| 912 | def p163 : Spec F := |
| 913 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 914 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 915 | (machineCount := .atMost 3) (objective := .lmax) |
| 916 | |
| 917 | /-- `F3;R1|pij=p;tjk|Lmax` -/ |
| 918 | def p164 : Spec F := |
| 919 | OperationsFamily.spec (shopType := .flow) (processingTimes := .equal) |
| 920 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 921 | (machineCount := .atMost 3) (objective := .lmax) |
| 922 | |
| 923 | /-- `F2;R1|pij=1;tj;rj|ΣCj` -/ |
| 924 | def p165 : Spec F := |
| 925 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 926 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := true }) |
| 927 | (machineCount := .atMost 2) (objective := .sumC) |
| 928 | |
| 929 | /-- `F3;R1|pij=1;tjk;rj|ΣCj` -/ |
| 930 | def p166 : Spec F := |
| 931 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 932 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 933 | (machineCount := .atMost 3) (objective := .sumC) |
| 934 | |
| 935 | /-- `F2;R1|pij=1;tj|ΣwjUj` -/ |
| 936 | def p167 : Spec F := |
| 937 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 938 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := true }) |
| 939 | (machineCount := .atMost 2) (objective := .sumWU) |
| 940 | |
| 941 | /-- `F3;R1|pij=1;tjk|ΣwjUj` -/ |
| 942 | def p168 : Spec F := |
| 943 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 944 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 945 | (machineCount := .atMost 3) (objective := .sumWU) |
| 946 | |
| 947 | /-- `F2;R1|pij=1;tj|ΣTj` -/ |
| 948 | def p169 : Spec F := |
| 949 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 950 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := true }) |
| 951 | (machineCount := .atMost 2) (objective := .sumT) |
| 952 | |
| 953 | /-- `F3;R1|pij=1;tjk|ΣTj` -/ |
| 954 | def p170 : Spec F := |
| 955 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 956 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 957 | (machineCount := .atMost 3) (objective := .sumT) |
| 958 | |
| 959 | /-- `F2;R1|pij=1;tj|ΣwjTj` -/ |
| 960 | def p171 : Spec F := |
| 961 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 962 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := true }) |
| 963 | (machineCount := .atMost 2) (objective := .sumWT) |
| 964 | |
| 965 | /-- `F3;R1|pij=1;tjk|ΣwjTj` -/ |
| 966 | def p172 : Spec F := |
| 967 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 968 | (machineSets := .shop .byPosition) (transportation := { shape := .jobSource, robot := true }) |
| 969 | (machineCount := .atMost 3) (objective := .sumWT) |
| 970 | |
| 971 | /-- `J2|pij=1|ΣUj` -/ |
| 972 | def p173 : Spec F := |
| 973 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 974 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumU) |
| 975 | |
| 976 | /-- `J2|pij=1|ΣwjUj` -/ |
| 977 | def p174 : Spec F := |
| 978 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 979 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWU) |
| 980 | |
| 981 | /-- `J2|Mj;pij=1|ΣwjUj` -/ |
| 982 | def p175 : Spec F := |
| 983 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .sets) |
| 984 | (machineCount := .atMost 2) (objective := .sumWU) |
| 985 | |
| 986 | /-- `O|pij=1;no-wait|ΣwjUj` -/ |
| 987 | def p176 : Spec F := |
| 988 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 989 | (machineSets := .shop .byPosition) (objective := .sumWU) |
| 990 | |
| 991 | /-- `O2|no-wait|ΣCj` -/ |
| 992 | def p177 : Spec F := |
| 993 | OperationsFamily.spec (shopType := .open) (waiting := .noWait) |
| 994 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .sumC) |
| 995 | |
| 996 | /-- `J2|pij=1|ΣCj` -/ |
| 997 | def p178 : Spec F := |
| 998 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 999 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumC) |
| 1000 | |
| 1001 | /-- `J2|pij=1;no-wait|ΣCj` -/ |
| 1002 | def p179 : Spec F := |
| 1003 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1004 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumC) |
| 1005 | |
| 1006 | /-- `O|pij=1;rj|ΣUj` -/ |
| 1007 | def p180 : Spec F := |
| 1008 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 1009 | (machineSets := .shop .byPosition) (objective := .sumU) |
| 1010 | |
| 1011 | /-- `O|fixj;rj;pij=1|ΣUj` -/ |
| 1012 | def p181 : Spec F := |
| 1013 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 1014 | (machineSets := .shop .fix) (objective := .sumU) |
| 1015 | |
| 1016 | /-- `O|Mj;rj;pij=1|ΣUj` -/ |
| 1017 | def p182 : Spec F := |
| 1018 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 1019 | (machineSets := .shop .sets) (objective := .sumU) |
| 1020 | |
| 1021 | /-- `O||Cmax` -/ |
| 1022 | def p183 : Spec F := |
| 1023 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 1024 | (objective := .makespan) |
| 1025 | |
| 1026 | /-- `O2|pij=1;intree|ΣwjCj` -/ |
| 1027 | def p184 : Spec F := |
| 1028 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1029 | (machineSets := .shop .byPosition) (precedence := ⟨.intree, .zero⟩) |
| 1030 | (machineCount := .atMost 2) (objective := .sumWC) |
| 1031 | |
| 1032 | /-- `O2|pij=1;outtree|ΣwjCj` -/ |
| 1033 | def p185 : Spec F := |
| 1034 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1035 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) |
| 1036 | (machineCount := .atMost 2) (objective := .sumWC) |
| 1037 | |
| 1038 | /-- `J3|pij=1|ΣCj` -/ |
| 1039 | def p186 : Spec F := |
| 1040 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 1041 | (machineSets := .shop .dedicated) (machineCount := .atMost 3) (objective := .sumC) |
| 1042 | |
| 1043 | /-- `J3|fixj;pij=1|ΣCj` -/ |
| 1044 | def p187 : Spec F := |
| 1045 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1046 | (machineCount := .atMost 3) (objective := .sumC) |
| 1047 | |
| 1048 | /-- `O|fixj|Cmax` -/ |
| 1049 | def p188 : Spec F := |
| 1050 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .fix) (objective := .makespan) |
| 1051 | |
| 1052 | /-- `J3|Mj;pij=1|ΣCj` -/ |
| 1053 | def p189 : Spec F := |
| 1054 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .sets) |
| 1055 | (machineCount := .atMost 3) (objective := .sumC) |
| 1056 | |
| 1057 | /-- `O|Mj|Cmax` -/ |
| 1058 | def p190 : Spec F := |
| 1059 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .sets) (objective := .makespan) |
| 1060 | |
| 1061 | /-- `O|pij=1|ΣUj` -/ |
| 1062 | def p191 : Spec F := |
| 1063 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1064 | (machineSets := .shop .byPosition) (objective := .sumU) |
| 1065 | |
| 1066 | /-- `O|pij=1|ΣTj` -/ |
| 1067 | def p192 : Spec F := |
| 1068 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1069 | (machineSets := .shop .byPosition) (objective := .sumT) |
| 1070 | |
| 1071 | /-- `O2|rj|Cmax` -/ |
| 1072 | def p193 : Spec F := |
| 1073 | OperationsFamily.spec (shopType := .open) (release := .releaseDates) |
| 1074 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 1075 | |
| 1076 | /-- `O2||Lmax` -/ |
| 1077 | def p194 : Spec F := |
| 1078 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 1079 | (machineCount := .atMost 2) (objective := .lmax) |
| 1080 | |
| 1081 | /-- `O2|fixj;rj|Cmax` -/ |
| 1082 | def p195 : Spec F := |
| 1083 | OperationsFamily.spec (shopType := .open) (release := .releaseDates) (machineSets := .shop .fix) |
| 1084 | (machineCount := .atMost 2) (objective := .makespan) |
| 1085 | |
| 1086 | /-- `O2|fixj|Lmax` -/ |
| 1087 | def p196 : Spec F := |
| 1088 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .fix) |
| 1089 | (machineCount := .atMost 2) (objective := .lmax) |
| 1090 | |
| 1091 | /-- `O2|Mj;rj|Cmax` -/ |
| 1092 | def p197 : Spec F := |
| 1093 | OperationsFamily.spec (shopType := .open) (release := .releaseDates) |
| 1094 | (machineSets := .shop .sets) (machineCount := .atMost 2) (objective := .makespan) |
| 1095 | |
| 1096 | /-- `O2|Mj|Lmax` -/ |
| 1097 | def p198 : Spec F := |
| 1098 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .sets) |
| 1099 | (machineCount := .atMost 2) (objective := .lmax) |
| 1100 | |
| 1101 | /-- `O|pij=1;prec;no-wait|ΣCj` -/ |
| 1102 | def p199 : Spec F := |
| 1103 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1104 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (objective := .sumC) |
| 1105 | |
| 1106 | /-- `F|Mj;prec;pij=1|ΣCj` -/ |
| 1107 | def p200 : Spec F := |
| 1108 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1109 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .sumC) |
| 1110 | |
| 1111 | /-- `O|Mj;prec;pij=1|ΣCj` -/ |
| 1112 | def p201 : Spec F := |
| 1113 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1114 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .sumC) |
| 1115 | |
| 1116 | /-- `J2||Cmax` -/ |
| 1117 | def p202 : Spec F := |
| 1118 | OperationsFamily.spec (shopType := .job) (machineSets := .shop .dedicated) |
| 1119 | (machineCount := .atMost 2) (objective := .makespan) |
| 1120 | |
| 1121 | /-- `J3|pij=1;rcrc|Cmax` -/ |
| 1122 | def p203 : Spec F := |
| 1123 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 1124 | (machineSets := .shop .recirculation) (machineCount := .atMost 3) (objective := .makespan) |
| 1125 | |
| 1126 | /-- `J3|Mj;pij=1|Cmax` -/ |
| 1127 | def p204 : Spec F := |
| 1128 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .sets) |
| 1129 | (machineCount := .atMost 3) (objective := .makespan) |
| 1130 | |
| 1131 | /-- `F2|chains|Cmax` -/ |
| 1132 | def p205 : Spec F := |
| 1133 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1134 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 1135 | |
| 1136 | /-- `F2|rj|Cmax` -/ |
| 1137 | def p206 : Spec F := |
| 1138 | OperationsFamily.spec (shopType := .flow) (release := .releaseDates) |
| 1139 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 1140 | |
| 1141 | /-- `F2||Lmax` -/ |
| 1142 | def p207 : Spec F := |
| 1143 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1144 | (machineCount := .atMost 2) (objective := .lmax) |
| 1145 | |
| 1146 | /-- `F2|Mj|Cmax` -/ |
| 1147 | def p208 : Spec F := |
| 1148 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .sets) |
| 1149 | (machineCount := .atMost 2) (objective := .makespan) |
| 1150 | |
| 1151 | /-- `F2|Mj;chains|Cmax` -/ |
| 1152 | def p209 : Spec F := |
| 1153 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .sets) |
| 1154 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 1155 | |
| 1156 | /-- `F2|Mj;rj|Cmax` -/ |
| 1157 | def p210 : Spec F := |
| 1158 | OperationsFamily.spec (shopType := .flow) (release := .releaseDates) |
| 1159 | (machineSets := .shop .sets) (machineCount := .atMost 2) (objective := .makespan) |
| 1160 | |
| 1161 | /-- `F2|Mj|Lmax` -/ |
| 1162 | def p211 : Spec F := |
| 1163 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .sets) |
| 1164 | (machineCount := .atMost 2) (objective := .lmax) |
| 1165 | |
| 1166 | /-- `F|pij=1;prec|Cmax` -/ |
| 1167 | def p212 : Spec F := |
| 1168 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1169 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1170 | |
| 1171 | /-- `O2|outtree;pij=1;rj|ΣCj` -/ |
| 1172 | def p213 : Spec F := |
| 1173 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 1174 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) |
| 1175 | (machineCount := .atMost 2) (objective := .sumC) |
| 1176 | |
| 1177 | /-- `J|prec;rj;n=k|ΣwjUj` -/ |
| 1178 | def p214 : Spec F := |
| 1179 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (release := .releaseDates) |
| 1180 | (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) (objective := .sumWU) |
| 1181 | |
| 1182 | /-- `J|prec;rj;n=k|ΣwjTj` -/ |
| 1183 | def p215 : Spec F := |
| 1184 | OperationsFamily.spec (shopType := .job) (jobCount := .constant) (release := .releaseDates) |
| 1185 | (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) (objective := .sumWT) |
| 1186 | |
| 1187 | /-- `F2|rj;no-wait|Cmax` -/ |
| 1188 | def p216 : Spec F := |
| 1189 | OperationsFamily.spec (shopType := .flow) (waiting := .noWait) (release := .releaseDates) |
| 1190 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 1191 | |
| 1192 | /-- `F2|no-wait|Lmax` -/ |
| 1193 | def p217 : Spec F := |
| 1194 | OperationsFamily.spec (shopType := .flow) (waiting := .noWait) |
| 1195 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .lmax) |
| 1196 | |
| 1197 | /-- `F2|no-wait|ΣCj` -/ |
| 1198 | def p218 : Spec F := |
| 1199 | OperationsFamily.spec (shopType := .flow) (waiting := .noWait) |
| 1200 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .sumC) |
| 1201 | |
| 1202 | /-- `J2|no-wait|ΣCj` -/ |
| 1203 | def p219 : Spec F := |
| 1204 | OperationsFamily.spec (shopType := .job) (waiting := .noWait) (machineSets := .shop .dedicated) |
| 1205 | (machineCount := .atMost 2) (objective := .sumC) |
| 1206 | |
| 1207 | /-- `F3|no-wait|Cmax` -/ |
| 1208 | def p220 : Spec F := |
| 1209 | OperationsFamily.spec (shopType := .flow) (waiting := .noWait) |
| 1210 | (machineSets := .shop .byPosition) (machineCount := .atMost 3) (objective := .makespan) |
| 1211 | |
| 1212 | /-- `O|pij=1;tjkl=T|Cmax` -/ |
| 1213 | def p221 : Spec F := |
| 1214 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1215 | (machineSets := .shop .byPosition) (transportation := { shape := .uniform, robot := false }) |
| 1216 | (objective := .makespan) |
| 1217 | |
| 1218 | /-- `O|pij=1;tkl=tlk|Cmax` -/ |
| 1219 | def p222 : Spec F := |
| 1220 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1221 | (machineSets := .shop .byPosition) |
| 1222 | (transportation := { shape := .pairSymmetric, robot := false }) (objective := .makespan) |
| 1223 | |
| 1224 | /-- `J|prec;rj;n=2|ΣwjUj` -/ |
| 1225 | def p223 : Spec F := |
| 1226 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 2) (release := .releaseDates) |
| 1227 | (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) (objective := .sumWU) |
| 1228 | |
| 1229 | /-- `J|prec;rj;n=2|ΣwjTj` -/ |
| 1230 | def p224 : Spec F := |
| 1231 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 2) (release := .releaseDates) |
| 1232 | (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) (objective := .sumWT) |
| 1233 | |
| 1234 | /-- `O2|no-wait|Cmax` -/ |
| 1235 | def p225 : Spec F := |
| 1236 | OperationsFamily.spec (shopType := .open) (waiting := .noWait) |
| 1237 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 1238 | |
| 1239 | /-- `J2|no-wait|Cmax` -/ |
| 1240 | def p226 : Spec F := |
| 1241 | OperationsFamily.spec (shopType := .job) (waiting := .noWait) (machineSets := .shop .dedicated) |
| 1242 | (machineCount := .atMost 2) (objective := .makespan) |
| 1243 | |
| 1244 | /-- `J3|pij=1;no-wait|Cmax` -/ |
| 1245 | def p227 : Spec F := |
| 1246 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1247 | (machineSets := .shop .dedicated) (machineCount := .atMost 3) (objective := .makespan) |
| 1248 | |
| 1249 | /-- `J3|pij=1;no-wait|ΣCj` -/ |
| 1250 | def p228 : Spec F := |
| 1251 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1252 | (machineSets := .shop .dedicated) (machineCount := .atMost 3) (objective := .sumC) |
| 1253 | |
| 1254 | /-- `J3|n=3|Cmax` -/ |
| 1255 | def p229 : Spec F := |
| 1256 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 3) |
| 1257 | (machineSets := .shop .dedicated) (machineCount := .atMost 3) (objective := .makespan) |
| 1258 | |
| 1259 | /-- `J3|n=3|ΣCj` -/ |
| 1260 | def p230 : Spec F := |
| 1261 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 3) |
| 1262 | (machineSets := .shop .dedicated) (machineCount := .atMost 3) (objective := .sumC) |
| 1263 | |
| 1264 | /-- `J3|fixj;n=3|Cmax` -/ |
| 1265 | def p231 : Spec F := |
| 1266 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 3) (machineSets := .shop .fix) |
| 1267 | (machineCount := .atMost 3) (objective := .makespan) |
| 1268 | |
| 1269 | /-- `J3|fixj;n=3|ΣCj` -/ |
| 1270 | def p232 : Spec F := |
| 1271 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 3) (machineSets := .shop .fix) |
| 1272 | (machineCount := .atMost 3) (objective := .sumC) |
| 1273 | |
| 1274 | /-- `J3|Mj;n=3|ΣCj` -/ |
| 1275 | def p233 : Spec F := |
| 1276 | OperationsFamily.spec (shopType := .job) (jobCount := .atMost 3) (machineSets := .shop .sets) |
| 1277 | (machineCount := .atMost 3) (objective := .sumC) |
| 1278 | |
| 1279 | /-- `J2|chains;pij=1|Cmax` -/ |
| 1280 | def p234 : Spec F := |
| 1281 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 1282 | (machineSets := .shop .dedicated) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1283 | (objective := .makespan) |
| 1284 | |
| 1285 | /-- `J2|Mj;chains;pij=1|Cmax` -/ |
| 1286 | def p235 : Spec F := |
| 1287 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .sets) |
| 1288 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 1289 | |
| 1290 | /-- `J2|pij=1;rj|Cmax` -/ |
| 1291 | def p236 : Spec F := |
| 1292 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1293 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .makespan) |
| 1294 | |
| 1295 | /-- `J2|pij=1;rj|ΣUj` -/ |
| 1296 | def p237 : Spec F := |
| 1297 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1298 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumU) |
| 1299 | |
| 1300 | /-- `J2|pij=1;rj|ΣCj` -/ |
| 1301 | def p238 : Spec F := |
| 1302 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1303 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumC) |
| 1304 | |
| 1305 | /-- `J2|chains;pij=1|ΣCj` -/ |
| 1306 | def p239 : Spec F := |
| 1307 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 1308 | (machineSets := .shop .dedicated) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1309 | (objective := .sumC) |
| 1310 | |
| 1311 | /-- `J2|pij=1|ΣwjCj` -/ |
| 1312 | def p240 : Spec F := |
| 1313 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 1314 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWC) |
| 1315 | |
| 1316 | /-- `J2|pij=1;rj|ΣwjCj` -/ |
| 1317 | def p241 : Spec F := |
| 1318 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1319 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWC) |
| 1320 | |
| 1321 | /-- `J2|pij=1|ΣwjTj` -/ |
| 1322 | def p242 : Spec F := |
| 1323 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) |
| 1324 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWT) |
| 1325 | |
| 1326 | /-- `J2|chains;pij=1;no-wait|Cmax` -/ |
| 1327 | def p243 : Spec F := |
| 1328 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1329 | (machineSets := .shop .dedicated) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1330 | (objective := .makespan) |
| 1331 | |
| 1332 | /-- `J2|pij=1;rj;no-wait|Lmax` -/ |
| 1333 | def p244 : Spec F := |
| 1334 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1335 | (release := .releaseDates) (machineSets := .shop .dedicated) (machineCount := .atMost 2) |
| 1336 | (objective := .lmax) |
| 1337 | |
| 1338 | /-- `J2|chains;pij=1;no-wait|ΣCj` -/ |
| 1339 | def p245 : Spec F := |
| 1340 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1341 | (machineSets := .shop .dedicated) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1342 | (objective := .sumC) |
| 1343 | |
| 1344 | /-- `J2|pij=1;rj;no-wait|ΣCj` -/ |
| 1345 | def p246 : Spec F := |
| 1346 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1347 | (release := .releaseDates) (machineSets := .shop .dedicated) (machineCount := .atMost 2) |
| 1348 | (objective := .sumC) |
| 1349 | |
| 1350 | /-- `J2|pij=1;no-wait|ΣwjCj` -/ |
| 1351 | def p247 : Spec F := |
| 1352 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1353 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWC) |
| 1354 | |
| 1355 | /-- `J2|pij=1;no-wait|ΣwjTj` -/ |
| 1356 | def p248 : Spec F := |
| 1357 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (waiting := .noWait) |
| 1358 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumWT) |
| 1359 | |
| 1360 | /-- `J2|fixj;rj;pij=1|ΣCj` -/ |
| 1361 | def p249 : Spec F := |
| 1362 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1363 | (machineSets := .shop .fix) (machineCount := .atMost 2) (objective := .sumC) |
| 1364 | |
| 1365 | /-- `J2|fixj;chains;pij=1|ΣCj` -/ |
| 1366 | def p250 : Spec F := |
| 1367 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1368 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumC) |
| 1369 | |
| 1370 | /-- `J2|fixj;pij=1|ΣwjCj` -/ |
| 1371 | def p251 : Spec F := |
| 1372 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1373 | (machineCount := .atMost 2) (objective := .sumWC) |
| 1374 | |
| 1375 | /-- `J2|fixj;rj;pij=1|ΣwjCj` -/ |
| 1376 | def p252 : Spec F := |
| 1377 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1378 | (machineSets := .shop .fix) (machineCount := .atMost 2) (objective := .sumWC) |
| 1379 | |
| 1380 | /-- `J2|Mj;rj;pij=1|ΣCj` -/ |
| 1381 | def p253 : Spec F := |
| 1382 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1383 | (machineSets := .shop .sets) (machineCount := .atMost 2) (objective := .sumC) |
| 1384 | |
| 1385 | /-- `J2|Mj;chains;pij=1|ΣCj` -/ |
| 1386 | def p254 : Spec F := |
| 1387 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .sets) |
| 1388 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumC) |
| 1389 | |
| 1390 | /-- `J2|Mj;pij=1|ΣwjCj` -/ |
| 1391 | def p255 : Spec F := |
| 1392 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .sets) |
| 1393 | (machineCount := .atMost 2) (objective := .sumWC) |
| 1394 | |
| 1395 | /-- `J2|Mj;rj;pij=1|ΣwjCj` -/ |
| 1396 | def p256 : Spec F := |
| 1397 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1398 | (machineSets := .shop .sets) (machineCount := .atMost 2) (objective := .sumWC) |
| 1399 | |
| 1400 | /-- `J2|Mj;rj;pij=1|ΣUj` -/ |
| 1401 | def p257 : Spec F := |
| 1402 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (release := .releaseDates) |
| 1403 | (machineSets := .shop .sets) (machineCount := .atMost 2) (objective := .sumU) |
| 1404 | |
| 1405 | /-- `J2|Mj;pij=1|ΣwjTj` -/ |
| 1406 | def p258 : Spec F := |
| 1407 | OperationsFamily.spec (shopType := .job) (processingTimes := .unit) (machineSets := .shop .sets) |
| 1408 | (machineCount := .atMost 2) (objective := .sumWT) |
| 1409 | |
| 1410 | /-- `O|pij=1;outtree;rj|Cmax` -/ |
| 1411 | def p259 : Spec F := |
| 1412 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 1413 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .makespan) |
| 1414 | |
| 1415 | /-- `O|pij=1;prec|Cmax` -/ |
| 1416 | def p260 : Spec F := |
| 1417 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1418 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1419 | |
| 1420 | /-- `O|pij=1;outtree|Lmax` -/ |
| 1421 | def p261 : Spec F := |
| 1422 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1423 | (machineSets := .shop .byPosition) (precedence := ⟨.outtree, .zero⟩) (objective := .lmax) |
| 1424 | |
| 1425 | /-- `O2|pij=1;chains|ΣwjCj` -/ |
| 1426 | def p262 : Spec F := |
| 1427 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1428 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1429 | (machineCount := .atMost 2) (objective := .sumWC) |
| 1430 | |
| 1431 | /-- `O3|pij=1;chains|ΣwjCj` -/ |
| 1432 | def p263 : Spec F := |
| 1433 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1434 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1435 | (machineCount := .atMost 3) (objective := .sumWC) |
| 1436 | |
| 1437 | /-- `O2|pij=1;chains|ΣUj` -/ |
| 1438 | def p264 : Spec F := |
| 1439 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1440 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1441 | (machineCount := .atMost 2) (objective := .sumU) |
| 1442 | |
| 1443 | /-- `O3|pij=1;chains|ΣUj` -/ |
| 1444 | def p265 : Spec F := |
| 1445 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1446 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1447 | (machineCount := .atMost 3) (objective := .sumU) |
| 1448 | |
| 1449 | /-- `O2|pij=1;chains|ΣTj` -/ |
| 1450 | def p266 : Spec F := |
| 1451 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1452 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1453 | (machineCount := .atMost 2) (objective := .sumT) |
| 1454 | |
| 1455 | /-- `O3|pij=1;chains|ΣTj` -/ |
| 1456 | def p267 : Spec F := |
| 1457 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1458 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1459 | (machineCount := .atMost 3) (objective := .sumT) |
| 1460 | |
| 1461 | /-- `O|pij=1;rj;no-wait|ΣCj` -/ |
| 1462 | def p268 : Spec F := |
| 1463 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1464 | (release := .releaseDates) (machineSets := .shop .byPosition) (objective := .sumC) |
| 1465 | |
| 1466 | /-- `O2|pij=1;chains;rj;no-wait|Cmax` -/ |
| 1467 | def p269 : Spec F := |
| 1468 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1469 | (release := .releaseDates) (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1470 | (machineCount := .atMost 2) (objective := .makespan) |
| 1471 | |
| 1472 | /-- `O2|pij=1;chains;rj;no-wait|ΣCj` -/ |
| 1473 | def p270 : Spec F := |
| 1474 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1475 | (release := .releaseDates) (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1476 | (machineCount := .atMost 2) (objective := .sumC) |
| 1477 | |
| 1478 | /-- `O2|pij=1;prec;no-wait|ΣCj` -/ |
| 1479 | def p271 : Spec F := |
| 1480 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1481 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) |
| 1482 | (objective := .sumC) |
| 1483 | |
| 1484 | /-- `O|pij=1;rj;no-wait|ΣwjCj` -/ |
| 1485 | def p272 : Spec F := |
| 1486 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1487 | (release := .releaseDates) (machineSets := .shop .byPosition) (objective := .sumWC) |
| 1488 | |
| 1489 | /-- `O|pij=1;rj;no-wait|ΣTj` -/ |
| 1490 | def p273 : Spec F := |
| 1491 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1492 | (release := .releaseDates) (machineSets := .shop .byPosition) (objective := .sumT) |
| 1493 | |
| 1494 | /-- `O2|pij=1;chains;no-wait|ΣwjCj` -/ |
| 1495 | def p274 : Spec F := |
| 1496 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1497 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1498 | (machineCount := .atMost 2) (objective := .sumWC) |
| 1499 | |
| 1500 | /-- `O3|pij=1;chains;no-wait|ΣwjCj` -/ |
| 1501 | def p275 : Spec F := |
| 1502 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1503 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1504 | (machineCount := .atMost 3) (objective := .sumWC) |
| 1505 | |
| 1506 | /-- `O2|pij=1;chains;no-wait|ΣUj` -/ |
| 1507 | def p276 : Spec F := |
| 1508 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1509 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1510 | (machineCount := .atMost 2) (objective := .sumU) |
| 1511 | |
| 1512 | /-- `O3|pij=1;chains;no-wait|ΣUj` -/ |
| 1513 | def p277 : Spec F := |
| 1514 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1515 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1516 | (machineCount := .atMost 3) (objective := .sumU) |
| 1517 | |
| 1518 | /-- `O2|pij=1;chains;no-wait|ΣTj` -/ |
| 1519 | def p278 : Spec F := |
| 1520 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1521 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1522 | (machineCount := .atMost 2) (objective := .sumT) |
| 1523 | |
| 1524 | /-- `O3|pij=1;chains;no-wait|ΣTj` -/ |
| 1525 | def p279 : Spec F := |
| 1526 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1527 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1528 | (machineCount := .atMost 3) (objective := .sumT) |
| 1529 | |
| 1530 | /-- `F|fixj;prec;pij=1|Cmax` -/ |
| 1531 | def p280 : Spec F := |
| 1532 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1533 | (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1534 | |
| 1535 | /-- `O|fixj;prec;pij=1|Cmax` -/ |
| 1536 | def p281 : Spec F := |
| 1537 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1538 | (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1539 | |
| 1540 | /-- `O|fixj;tree;rj;pij=1|Cmax` -/ |
| 1541 | def p282 : Spec F := |
| 1542 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 1543 | (machineSets := .shop .fix) (precedence := ⟨.tree, .zero⟩) (objective := .makespan) |
| 1544 | |
| 1545 | /-- `O|fixj;tree;pij=1|Lmax` -/ |
| 1546 | def p283 : Spec F := |
| 1547 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1548 | (precedence := ⟨.tree, .zero⟩) (objective := .lmax) |
| 1549 | |
| 1550 | /-- `O2|fixj;chains;pij=1|ΣwjCj` -/ |
| 1551 | def p284 : Spec F := |
| 1552 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1553 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumWC) |
| 1554 | |
| 1555 | /-- `O2|fixj;chains;pij=1|ΣUj` -/ |
| 1556 | def p285 : Spec F := |
| 1557 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1558 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumU) |
| 1559 | |
| 1560 | /-- `O2|fixj;chains;pij=1|ΣTj` -/ |
| 1561 | def p286 : Spec F := |
| 1562 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1563 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumT) |
| 1564 | |
| 1565 | /-- `O|Mj;outtree;rj;pij=1|Cmax` -/ |
| 1566 | def p287 : Spec F := |
| 1567 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (release := .releaseDates) |
| 1568 | (machineSets := .shop .sets) (precedence := ⟨.outtree, .zero⟩) (objective := .makespan) |
| 1569 | |
| 1570 | /-- `O|Mj;prec;pij=1|Cmax` -/ |
| 1571 | def p288 : Spec F := |
| 1572 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1573 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1574 | |
| 1575 | /-- `O|Mj;outtree;pij=1|Lmax` -/ |
| 1576 | def p289 : Spec F := |
| 1577 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1578 | (machineSets := .shop .sets) (precedence := ⟨.outtree, .zero⟩) (objective := .lmax) |
| 1579 | |
| 1580 | /-- `O2|Mj;chains;pij=1|ΣwjCj` -/ |
| 1581 | def p290 : Spec F := |
| 1582 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1583 | (machineSets := .shop .sets) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1584 | (objective := .sumWC) |
| 1585 | |
| 1586 | /-- `O2|Mj;chains;pij=1|ΣUj` -/ |
| 1587 | def p291 : Spec F := |
| 1588 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1589 | (machineSets := .shop .sets) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1590 | (objective := .sumU) |
| 1591 | |
| 1592 | /-- `O2|Mj;chains;pij=1|ΣTj` -/ |
| 1593 | def p292 : Spec F := |
| 1594 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1595 | (machineSets := .shop .sets) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1596 | (objective := .sumT) |
| 1597 | |
| 1598 | /-- `O2|chains|Cmax` -/ |
| 1599 | def p293 : Spec F := |
| 1600 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 1601 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 1602 | |
| 1603 | /-- `F2|pij=1;chains|ΣwjCj` -/ |
| 1604 | def p294 : Spec F := |
| 1605 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1606 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1607 | (machineCount := .atMost 2) (objective := .sumWC) |
| 1608 | |
| 1609 | /-- `F3|pij=1;chains|ΣwjCj` -/ |
| 1610 | def p295 : Spec F := |
| 1611 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1612 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 1613 | (machineCount := .atMost 3) (objective := .sumWC) |
| 1614 | |
| 1615 | /-- `F2|fixj;chains;pij=1|ΣwjCj` -/ |
| 1616 | def p296 : Spec F := |
| 1617 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1618 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumWC) |
| 1619 | |
| 1620 | /-- `O2|fixj;chains|Cmax` -/ |
| 1621 | def p297 : Spec F := |
| 1622 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .fix) |
| 1623 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 1624 | |
| 1625 | /-- `F2|Mj;chains;pij=1|ΣwjCj` -/ |
| 1626 | def p298 : Spec F := |
| 1627 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1628 | (machineSets := .shop .sets) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1629 | (objective := .sumWC) |
| 1630 | |
| 1631 | /-- `O2|Mj;chains|Cmax` -/ |
| 1632 | def p299 : Spec F := |
| 1633 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .sets) |
| 1634 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 1635 | |
| 1636 | /-- `O|pij=1;prec;no-wait|Cmax` -/ |
| 1637 | def p300 : Spec F := |
| 1638 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (waiting := .noWait) |
| 1639 | (machineSets := .shop .byPosition) (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1640 | |
| 1641 | /-- `F|Mj;prec;pij=1|Cmax` -/ |
| 1642 | def p301 : Spec F := |
| 1643 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1644 | (machineSets := .shop .sets) (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1645 | |
| 1646 | /-- `O2|pij=1;tj|Cmax` -/ |
| 1647 | def p302 : Spec F := |
| 1648 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) |
| 1649 | (machineSets := .shop .byPosition) (transportation := { shape := .job, robot := false }) |
| 1650 | (machineCount := .atMost 2) (objective := .makespan) |
| 1651 | |
| 1652 | /-- `F2|pij=1;tj∈T1,T2|Cmax` -/ |
| 1653 | def p303 : Spec F := |
| 1654 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1655 | (machineSets := .shop .byPosition) (transportation := { shape := .twoValues, robot := false }) |
| 1656 | (machineCount := .atMost 2) (objective := .makespan) |
| 1657 | |
| 1658 | /-- `F2|tj∈T1,T2|Cmax` -/ |
| 1659 | def p304 : Spec F := |
| 1660 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1661 | (transportation := { shape := .twoValues, robot := false }) (machineCount := .atMost 2) |
| 1662 | (objective := .makespan) |
| 1663 | |
| 1664 | /-- `O2|tjkl=T|Cmax` -/ |
| 1665 | def p305 : Spec F := |
| 1666 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 1667 | (transportation := { shape := .uniform, robot := false }) (machineCount := .atMost 2) |
| 1668 | (objective := .makespan) |
| 1669 | |
| 1670 | /-- `O2|tj∈T1,T2|Cmax` -/ |
| 1671 | def p306 : Spec F := |
| 1672 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 1673 | (transportation := { shape := .twoValues, robot := false }) (machineCount := .atMost 2) |
| 1674 | (objective := .makespan) |
| 1675 | |
| 1676 | /-- `F|pij=1;rj|ΣwjUj` -/ |
| 1677 | def p307 : Spec F := |
| 1678 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 1679 | (machineSets := .shop .byPosition) (objective := .sumWU) |
| 1680 | |
| 1681 | /-- `F|pij=1;rj|ΣwjTj` -/ |
| 1682 | def p308 : Spec F := |
| 1683 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 1684 | (machineSets := .shop .byPosition) (objective := .sumWT) |
| 1685 | |
| 1686 | /-- `F2|fixj;chains;pij=1|ΣUj` -/ |
| 1687 | def p309 : Spec F := |
| 1688 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1689 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumU) |
| 1690 | |
| 1691 | /-- `F2|fixj;chains;pij=1|ΣTj` -/ |
| 1692 | def p310 : Spec F := |
| 1693 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (machineSets := .shop .fix) |
| 1694 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumT) |
| 1695 | |
| 1696 | /-- `F2|Mj;chains;pij=1|ΣUj` -/ |
| 1697 | def p311 : Spec F := |
| 1698 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1699 | (machineSets := .shop .sets) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1700 | (objective := .sumU) |
| 1701 | |
| 1702 | /-- `F2|Mj;chains;pij=1|ΣTj` -/ |
| 1703 | def p312 : Spec F := |
| 1704 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) |
| 1705 | (machineSets := .shop .sets) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 1706 | (objective := .sumT) |
| 1707 | |
| 1708 | /-- `F|pij=1;tk;rj|ΣwjUj` -/ |
| 1709 | def p313 : Spec F := |
| 1710 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 1711 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := false }) |
| 1712 | (objective := .sumWU) |
| 1713 | |
| 1714 | /-- `F|pij=1;tk;rj|ΣwjTj` -/ |
| 1715 | def p314 : Spec F := |
| 1716 | OperationsFamily.spec (shopType := .flow) (processingTimes := .unit) (release := .releaseDates) |
| 1717 | (machineSets := .shop .byPosition) (transportation := { shape := .source, robot := false }) |
| 1718 | (objective := .sumWT) |
| 1719 | |
| 1720 | /-- `FF(1,m)||ΣZj` -/ |
| 1721 | def p315 : Spec F := |
| 1722 | OperationsFamily.spec (shopType := .flexibleFlow) (machineSets := .shop .stages) |
| 1723 | (objective := .sumZ) |
| 1724 | |
| 1725 | /-- `FF(1,m)||ΣwjZj` -/ |
| 1726 | def p316 : Spec F := |
| 1727 | OperationsFamily.spec (shopType := .flexibleFlow) (machineSets := .shop .stages) |
| 1728 | (objective := .sumWZ) |
| 1729 | |
| 1730 | /-- `FF(1,m)|pj=p|ΣZj` -/ |
| 1731 | def p317 : Spec F := |
| 1732 | OperationsFamily.spec (shopType := .flexibleFlow) (processingTimes := .equal) |
| 1733 | (machineSets := .shop .stages) (objective := .sumZ) |
| 1734 | |
| 1735 | /-- `F3||ΣZj` -/ |
| 1736 | def p318 : Spec F := |
| 1737 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1738 | (machineCount := .atMost 3) (objective := .sumZ) |
| 1739 | |
| 1740 | /-- `F3||ΣwjZj` -/ |
| 1741 | def p319 : Spec F := |
| 1742 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1743 | (machineCount := .atMost 3) (objective := .sumWZ) |
| 1744 | |
| 1745 | /-- `F2||ΣwjZj` -/ |
| 1746 | def p320 : Spec F := |
| 1747 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1748 | (machineCount := .atMost 2) (objective := .sumWZ) |
| 1749 | |
| 1750 | /-- `F2||ΣZj` -/ |
| 1751 | def p321 : Spec F := |
| 1752 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1753 | (machineCount := .atMost 2) (objective := .sumZ) |
| 1754 | |
| 1755 | /-- `F||ΣCj` -/ |
| 1756 | def p322 : Spec F := |
| 1757 | OperationsFamily.spec (shopType := .flow) (machineSets := .shop .byPosition) |
| 1758 | (objective := .sumC) |
| 1759 | |
| 1760 | /-- `O||ΣCj` -/ |
| 1761 | def p323 : Spec F := |
| 1762 | OperationsFamily.spec (shopType := .open) (machineSets := .shop .byPosition) |
| 1763 | (objective := .sumC) |
| 1764 | |
| 1765 | /-- `J3||Cmax` -/ |
| 1766 | def p324 : Spec F := |
| 1767 | OperationsFamily.spec (shopType := .job) (machineSets := .shop .dedicated) |
| 1768 | (machineCount := .atMost 3) (objective := .makespan) |
| 1769 | |
| 1770 | /-- `J||Cmax` -/ |
| 1771 | def p325 : Spec F := |
| 1772 | OperationsFamily.spec (shopType := .job) (machineSets := .shop .dedicated) |
| 1773 | (objective := .makespan) |
| 1774 | |
| 1775 | /-- `O|pij=1;STsd,b|Cmax` -/ |
| 1776 | def p326 : Spec F := |
| 1777 | OperationsFamily.spec (shopType := .open) (processingTimes := .unit) (setups := .batchSetups) |
| 1778 | (machineSets := .shop .byPosition) (objective := .makespan) |
| 1779 | |
| 1780 | /-- The problems with their names in three-field notation. -/ |
| 1781 | def problems : List (String × Spec F) := [ |
| 1782 | ("F2|no-idle;no-wait|Cmax", p0), |
| 1783 | ("F|no-idle;no-wait|Cmax", p1), |
| 1784 | ("F2|tj|Cmax", p2), |
| 1785 | ("F2|pij=1;tj|Cmax", p3), |
| 1786 | ("F||Cmax", p4), |
| 1787 | ("O2||ΣCj", p5), |
| 1788 | ("O2|fixj|ΣCj", p6), |
| 1789 | ("O2|Mj|ΣCj", p7), |
| 1790 | ("F|intree;pij=1|ΣCj", p8), |
| 1791 | ("O|pij=1;rj|ΣwjUj", p9), |
| 1792 | ("J|fixj;n=2|ΣwjUj", p10), |
| 1793 | ("J|fixj;n=2|ΣwjTj", p11), |
| 1794 | ("F|Mj;prec;rj;n=k|ΣwjUj", p12), |
| 1795 | ("F|Mj;prec;rj;n=k|ΣwjTj", p13), |
| 1796 | ("O|Mj;prec;rj;n=k|ΣwjUj", p14), |
| 1797 | ("O|Mj;prec;rj;n=k|ΣwjTj", p15), |
| 1798 | ("O|pij=1;intree|Lmax", p16), |
| 1799 | ("O2|pij=1;prec;rj|Lmax", p17), |
| 1800 | ("J|prec;rj;n=k;no-wait|ΣwjUj", p18), |
| 1801 | ("J|prec;rj;n=k;no-wait|ΣwjTj", p19), |
| 1802 | ("O|pij=1;chains;rj|Lmax", p20), |
| 1803 | ("O|pij=1;intree;no-wait|ΣCj", p21), |
| 1804 | ("O|pij=1;rj;no-wait|ΣwjUj", p22), |
| 1805 | ("F3;R1|pij=1;tk;rj|Cmax", p23), |
| 1806 | ("F3;R1|pij=1;tk|Lmax", p24), |
| 1807 | ("F|pij=1;tj|ΣCj", p25), |
| 1808 | ("F2|pij=1;tj;rj|ΣCj", p26), |
| 1809 | ("F2|pij=1;tj|ΣwjCj", p27), |
| 1810 | ("O2|pij=1;tjkl=T;rj|Cmax", p28), |
| 1811 | ("O2|pij=1;tkl|Cmax", p29), |
| 1812 | ("O2|pij=1;tkl|ΣwjCj", p30), |
| 1813 | ("O2|pij=1;tjkl=T|ΣUj", p31), |
| 1814 | ("O2|pij=1;tj;rj|ΣCj", p32), |
| 1815 | ("O2|pij=1;tj|ΣwjCj", p33), |
| 1816 | ("O|pij=1;intree;no-wait|Lmax", p34), |
| 1817 | ("O|pij=1;outtree;no-wait|Lmax", p35), |
| 1818 | ("F|Mj;intree;rj;pij=1|Cmax", p36), |
| 1819 | ("F|Mj;outtree;pij=1|Lmax", p37), |
| 1820 | ("O|pij=1;rj|Lmax", p38), |
| 1821 | ("O|pij=1|ΣwjCj", p39), |
| 1822 | ("O2|pij=1;prec|ΣUj", p40), |
| 1823 | ("O|pij=1;tree;no-wait|Cmax", p41), |
| 1824 | ("O2|pij=1;prec;no-wait|Cmax", p42), |
| 1825 | ("O|pij=1;rj;no-wait|Lmax", p43), |
| 1826 | ("O|pij=1;outtree;no-wait|ΣCj", p44), |
| 1827 | ("O|pij=1;no-wait|ΣwjTj", p45), |
| 1828 | ("F|Mj;n=3|Cmax", p46), |
| 1829 | ("F|Mj;rj;pij=1|Cmax", p47), |
| 1830 | ("F|Mj;rj;pij=1|ΣCj", p48), |
| 1831 | ("F|Mj;pij=1|ΣwjCj", p49), |
| 1832 | ("F|Mj;pij=1|ΣwjUj", p50), |
| 1833 | ("F|Mj;pij=1|ΣTj", p51), |
| 1834 | ("J|Mj;prec;rj;pij=1;n=k|ΣwjUj", p52), |
| 1835 | ("J|Mj;prec;rj;pij=1;n=k|ΣwjTj", p53), |
| 1836 | ("O|Mj;rj;pij=1|Cmax", p54), |
| 1837 | ("O|Mj;rj;pij=1|ΣCj", p55), |
| 1838 | ("O|Mj;pij=1|ΣwjCj", p56), |
| 1839 | ("O|Mj;pij=1|ΣwjUj", p57), |
| 1840 | ("O|Mj;pij=1|ΣTj", p58), |
| 1841 | ("F|pij=1;outtree;rj|Cmax", p59), |
| 1842 | ("F|pij=1;tree|Cmax", p60), |
| 1843 | ("F|pij=1;intree|Lmax", p61), |
| 1844 | ("F2|pij=1;prec;rj|Lmax", p62), |
| 1845 | ("O2|fixj|Cmax", p63), |
| 1846 | ("J2|fixj;n=k|Cmax", p64), |
| 1847 | ("F2|fixj|Cmax", p65), |
| 1848 | ("J2|fixj;pij=1|Cmax", p66), |
| 1849 | ("J|prec;pij=1;rj;n=k|ΣwjUj", p67), |
| 1850 | ("J|prec;pij=1;rj;n=k|ΣwjTj", p68), |
| 1851 | ("F|fixj;rj;pij=1|Cmax", p69), |
| 1852 | ("F|fixj;rj;pij=1|ΣCj", p70), |
| 1853 | ("F|fixj;pij=1|ΣwjCj", p71), |
| 1854 | ("F|fixj;pij=1|ΣwjUj", p72), |
| 1855 | ("F|fixj;pij=1|ΣwjTj", p73), |
| 1856 | ("J|fixj;prec;rj;pij=1;n=k|ΣwjUj", p74), |
| 1857 | ("J|fixj;prec;rj;pij=1;n=k|ΣwjTj", p75), |
| 1858 | ("O|fixj;rj;pij=1|Cmax", p76), |
| 1859 | ("O|fixj;rj;pij=1|ΣCj", p77), |
| 1860 | ("O|fixj;pij=1|ΣwjCj", p78), |
| 1861 | ("O|fixj;pij=1|ΣwjUj", p79), |
| 1862 | ("O|fixj;pij=1|ΣTj", p80), |
| 1863 | ("F|pij=1;outtree;rj|ΣCj", p81), |
| 1864 | ("F2|pij=1;prec|ΣCj", p82), |
| 1865 | ("F|pij=1;intree;rj|Cmax", p83), |
| 1866 | ("F|pij=1;outtree|Lmax", p84), |
| 1867 | ("F2|pij=1;chains|ΣUj", p85), |
| 1868 | ("F3|pij=1;chains|ΣUj", p86), |
| 1869 | ("F2|pij=1;chains|ΣTj", p87), |
| 1870 | ("F3|pij=1;chains|ΣTj", p88), |
| 1871 | ("F|fixj;tree;rj;pij=1|Cmax", p89), |
| 1872 | ("F|fixj;tree;pij=1|Lmax", p90), |
| 1873 | ("O|pij=1;rj|ΣCj", p91), |
| 1874 | ("J2|n=k|ΣwjUj", p92), |
| 1875 | ("J2|n=k|ΣwjTj", p93), |
| 1876 | ("F2;S1|pij=p;sij=s;rj|Cmax", p94), |
| 1877 | ("F;S1|pij=1;sij=s;rj|Cmax", p95), |
| 1878 | ("F;S1|pij=p;sij=s|Cmax", p96), |
| 1879 | ("F2;S1|pij=p;sij=s;rj|ΣCj", p97), |
| 1880 | ("F;S1|pij=1;sij=s;rj|ΣCj", p98), |
| 1881 | ("F2;S1|pij=p|Cmax", p99), |
| 1882 | ("F2;S1|sij=s|Cmax", p100), |
| 1883 | ("F2;S1|pij=1;rj|Lmax", p101), |
| 1884 | ("F3;S1|pij=1;rj|Lmax", p102), |
| 1885 | ("F2;S1|pij=1;rj|ΣCj", p103), |
| 1886 | ("F3;S1|pij=1;rj|ΣCj", p104), |
| 1887 | ("F2;S1|pij=1|ΣwjUj", p105), |
| 1888 | ("F3;S1|pij=1|ΣwjUj", p106), |
| 1889 | ("F2;S1|pij=1|ΣTj", p107), |
| 1890 | ("F3;S1|pij=1|ΣTj", p108), |
| 1891 | ("F2;S1|pij=1|ΣwjTj", p109), |
| 1892 | ("F3;S1|pij=1|ΣwjTj", p110), |
| 1893 | ("F3;S1|sij=1|Cmax", p111), |
| 1894 | ("F2;S1|sij=1|ΣCj", p112), |
| 1895 | ("F2;S1|pij=p;sij=s|ΣwjUj", p113), |
| 1896 | ("F;S1|pij=1;sij=s|ΣwjUj", p114), |
| 1897 | ("F2;S1|pij=p;sij=s|ΣwjTj", p115), |
| 1898 | ("F;S1|pij=1;sij=s|ΣwjTj", p116), |
| 1899 | ("F2;S1|pij=p;sij=1;rj|ΣwjCj", p117), |
| 1900 | ("F2;S1|pij=p;sij=1;rj|ΣwjUj", p118), |
| 1901 | ("F2;S1|pij=p;sij=1;rj|ΣTj", p119), |
| 1902 | ("O|pij=1;tree|Cmax", p120), |
| 1903 | ("O|pij=1;outtree|ΣCj", p121), |
| 1904 | ("O2|pij=1;tree|ΣCj", p122), |
| 1905 | ("F2|pij=1;prec;rj|ΣCj", p123), |
| 1906 | ("O2|pij=1;prec|ΣCj", p124), |
| 1907 | ("F2|no-wait|Cmax", p125), |
| 1908 | ("F3||Cmax", p126), |
| 1909 | ("F2||ΣCj", p127), |
| 1910 | ("J2||ΣCj", p128), |
| 1911 | ("F2|fixj|ΣCj", p129), |
| 1912 | ("F3|Mj|Cmax", p130), |
| 1913 | ("F2|Mj|ΣCj", p131), |
| 1914 | ("O2||Cmax", p132), |
| 1915 | ("O3||Cmax", p133), |
| 1916 | ("O|fixj;n=3|Cmax", p134), |
| 1917 | ("O3|fixj|Cmax", p135), |
| 1918 | ("O|Mj;n=3|Cmax", p136), |
| 1919 | ("O3|Mj|Cmax", p137), |
| 1920 | ("F2;R1|pij=1;tjk|Cmax", p138), |
| 1921 | ("F2;R1|pij=p;tj∈T1,T2|Cmax", p139), |
| 1922 | ("F;R1|n≥m-1;pij=p;tk|Cmax", p140), |
| 1923 | ("F2;R1|pij=p;tj|Cmax", p141), |
| 1924 | ("F2;R1|tjk=T|Cmax", p142), |
| 1925 | ("F2||Cmax", p143), |
| 1926 | ("F2|tk|Cmax", p144), |
| 1927 | ("F2|tjk=T|Cmax", p145), |
| 1928 | ("J|Mj;prec;rj;n=2|Lmax", p146), |
| 1929 | ("J2|Mj;n=3|Cmax", p147), |
| 1930 | ("O|Mj;pij=1|Cmax", p148), |
| 1931 | ("J2|pij=1;no-wait|Cmax", p149), |
| 1932 | ("F|fixj;prec;rj;n=k|ΣwjUj", p150), |
| 1933 | ("F|fixj;prec;rj;n=k|ΣwjTj", p151), |
| 1934 | ("O|fixj;prec;rj;pij=1;n=2|ΣwjUj", p152), |
| 1935 | ("O|fixj;prec;rj;n=k|ΣwjUj", p153), |
| 1936 | ("O|fixj;prec;rj;pij=1;n=2|ΣwjTj", p154), |
| 1937 | ("O|fixj;prec;rj;n=k|ΣwjTj", p155), |
| 1938 | ("F|fixj;n=3|Cmax", p156), |
| 1939 | ("F2;R1|pij=p;tk;rj|ΣwjCj", p157), |
| 1940 | ("F2;R1|pij=p;tk;rj|ΣwjUj", p158), |
| 1941 | ("F2;R1|pij=p;tk;rj|ΣTj", p159), |
| 1942 | ("F2;R1|pij=p;tk|ΣwjTj", p160), |
| 1943 | ("F3;R1|pij=p;tjk;rj|Cmax", p161), |
| 1944 | ("F2;R1|pij=1;tj;rj|Lmax", p162), |
| 1945 | ("F3;R1|pij=1;tjk;rj|Lmax", p163), |
| 1946 | ("F3;R1|pij=p;tjk|Lmax", p164), |
| 1947 | ("F2;R1|pij=1;tj;rj|ΣCj", p165), |
| 1948 | ("F3;R1|pij=1;tjk;rj|ΣCj", p166), |
| 1949 | ("F2;R1|pij=1;tj|ΣwjUj", p167), |
| 1950 | ("F3;R1|pij=1;tjk|ΣwjUj", p168), |
| 1951 | ("F2;R1|pij=1;tj|ΣTj", p169), |
| 1952 | ("F3;R1|pij=1;tjk|ΣTj", p170), |
| 1953 | ("F2;R1|pij=1;tj|ΣwjTj", p171), |
| 1954 | ("F3;R1|pij=1;tjk|ΣwjTj", p172), |
| 1955 | ("J2|pij=1|ΣUj", p173), |
| 1956 | ("J2|pij=1|ΣwjUj", p174), |
| 1957 | ("J2|Mj;pij=1|ΣwjUj", p175), |
| 1958 | ("O|pij=1;no-wait|ΣwjUj", p176), |
| 1959 | ("O2|no-wait|ΣCj", p177), |
| 1960 | ("J2|pij=1|ΣCj", p178), |
| 1961 | ("J2|pij=1;no-wait|ΣCj", p179), |
| 1962 | ("O|pij=1;rj|ΣUj", p180), |
| 1963 | ("O|fixj;rj;pij=1|ΣUj", p181), |
| 1964 | ("O|Mj;rj;pij=1|ΣUj", p182), |
| 1965 | ("O||Cmax", p183), |
| 1966 | ("O2|pij=1;intree|ΣwjCj", p184), |
| 1967 | ("O2|pij=1;outtree|ΣwjCj", p185), |
| 1968 | ("J3|pij=1|ΣCj", p186), |
| 1969 | ("J3|fixj;pij=1|ΣCj", p187), |
| 1970 | ("O|fixj|Cmax", p188), |
| 1971 | ("J3|Mj;pij=1|ΣCj", p189), |
| 1972 | ("O|Mj|Cmax", p190), |
| 1973 | ("O|pij=1|ΣUj", p191), |
| 1974 | ("O|pij=1|ΣTj", p192), |
| 1975 | ("O2|rj|Cmax", p193), |
| 1976 | ("O2||Lmax", p194), |
| 1977 | ("O2|fixj;rj|Cmax", p195), |
| 1978 | ("O2|fixj|Lmax", p196), |
| 1979 | ("O2|Mj;rj|Cmax", p197), |
| 1980 | ("O2|Mj|Lmax", p198), |
| 1981 | ("O|pij=1;prec;no-wait|ΣCj", p199), |
| 1982 | ("F|Mj;prec;pij=1|ΣCj", p200), |
| 1983 | ("O|Mj;prec;pij=1|ΣCj", p201), |
| 1984 | ("J2||Cmax", p202), |
| 1985 | ("J3|pij=1;rcrc|Cmax", p203), |
| 1986 | ("J3|Mj;pij=1|Cmax", p204), |
| 1987 | ("F2|chains|Cmax", p205), |
| 1988 | ("F2|rj|Cmax", p206), |
| 1989 | ("F2||Lmax", p207), |
| 1990 | ("F2|Mj|Cmax", p208), |
| 1991 | ("F2|Mj;chains|Cmax", p209), |
| 1992 | ("F2|Mj;rj|Cmax", p210), |
| 1993 | ("F2|Mj|Lmax", p211), |
| 1994 | ("F|pij=1;prec|Cmax", p212), |
| 1995 | ("O2|outtree;pij=1;rj|ΣCj", p213), |
| 1996 | ("J|prec;rj;n=k|ΣwjUj", p214), |
| 1997 | ("J|prec;rj;n=k|ΣwjTj", p215), |
| 1998 | ("F2|rj;no-wait|Cmax", p216), |
| 1999 | ("F2|no-wait|Lmax", p217), |
| 2000 | ("F2|no-wait|ΣCj", p218), |
| 2001 | ("J2|no-wait|ΣCj", p219), |
| 2002 | ("F3|no-wait|Cmax", p220), |
| 2003 | ("O|pij=1;tjkl=T|Cmax", p221), |
| 2004 | ("O|pij=1;tkl=tlk|Cmax", p222), |
| 2005 | ("J|prec;rj;n=2|ΣwjUj", p223), |
| 2006 | ("J|prec;rj;n=2|ΣwjTj", p224), |
| 2007 | ("O2|no-wait|Cmax", p225), |
| 2008 | ("J2|no-wait|Cmax", p226), |
| 2009 | ("J3|pij=1;no-wait|Cmax", p227), |
| 2010 | ("J3|pij=1;no-wait|ΣCj", p228), |
| 2011 | ("J3|n=3|Cmax", p229), |
| 2012 | ("J3|n=3|ΣCj", p230), |
| 2013 | ("J3|fixj;n=3|Cmax", p231), |
| 2014 | ("J3|fixj;n=3|ΣCj", p232), |
| 2015 | ("J3|Mj;n=3|ΣCj", p233), |
| 2016 | ("J2|chains;pij=1|Cmax", p234), |
| 2017 | ("J2|Mj;chains;pij=1|Cmax", p235), |
| 2018 | ("J2|pij=1;rj|Cmax", p236), |
| 2019 | ("J2|pij=1;rj|ΣUj", p237), |
| 2020 | ("J2|pij=1;rj|ΣCj", p238), |
| 2021 | ("J2|chains;pij=1|ΣCj", p239), |
| 2022 | ("J2|pij=1|ΣwjCj", p240), |
| 2023 | ("J2|pij=1;rj|ΣwjCj", p241), |
| 2024 | ("J2|pij=1|ΣwjTj", p242), |
| 2025 | ("J2|chains;pij=1;no-wait|Cmax", p243), |
| 2026 | ("J2|pij=1;rj;no-wait|Lmax", p244), |
| 2027 | ("J2|chains;pij=1;no-wait|ΣCj", p245), |
| 2028 | ("J2|pij=1;rj;no-wait|ΣCj", p246), |
| 2029 | ("J2|pij=1;no-wait|ΣwjCj", p247), |
| 2030 | ("J2|pij=1;no-wait|ΣwjTj", p248), |
| 2031 | ("J2|fixj;rj;pij=1|ΣCj", p249), |
| 2032 | ("J2|fixj;chains;pij=1|ΣCj", p250), |
| 2033 | ("J2|fixj;pij=1|ΣwjCj", p251), |
| 2034 | ("J2|fixj;rj;pij=1|ΣwjCj", p252), |
| 2035 | ("J2|Mj;rj;pij=1|ΣCj", p253), |
| 2036 | ("J2|Mj;chains;pij=1|ΣCj", p254), |
| 2037 | ("J2|Mj;pij=1|ΣwjCj", p255), |
| 2038 | ("J2|Mj;rj;pij=1|ΣwjCj", p256), |
| 2039 | ("J2|Mj;rj;pij=1|ΣUj", p257), |
| 2040 | ("J2|Mj;pij=1|ΣwjTj", p258), |
| 2041 | ("O|pij=1;outtree;rj|Cmax", p259), |
| 2042 | ("O|pij=1;prec|Cmax", p260), |
| 2043 | ("O|pij=1;outtree|Lmax", p261), |
| 2044 | ("O2|pij=1;chains|ΣwjCj", p262), |
| 2045 | ("O3|pij=1;chains|ΣwjCj", p263), |
| 2046 | ("O2|pij=1;chains|ΣUj", p264), |
| 2047 | ("O3|pij=1;chains|ΣUj", p265), |
| 2048 | ("O2|pij=1;chains|ΣTj", p266), |
| 2049 | ("O3|pij=1;chains|ΣTj", p267), |
| 2050 | ("O|pij=1;rj;no-wait|ΣCj", p268), |
| 2051 | ("O2|pij=1;chains;rj;no-wait|Cmax", p269), |
| 2052 | ("O2|pij=1;chains;rj;no-wait|ΣCj", p270), |
| 2053 | ("O2|pij=1;prec;no-wait|ΣCj", p271), |
| 2054 | ("O|pij=1;rj;no-wait|ΣwjCj", p272), |
| 2055 | ("O|pij=1;rj;no-wait|ΣTj", p273), |
| 2056 | ("O2|pij=1;chains;no-wait|ΣwjCj", p274), |
| 2057 | ("O3|pij=1;chains;no-wait|ΣwjCj", p275), |
| 2058 | ("O2|pij=1;chains;no-wait|ΣUj", p276), |
| 2059 | ("O3|pij=1;chains;no-wait|ΣUj", p277), |
| 2060 | ("O2|pij=1;chains;no-wait|ΣTj", p278), |
| 2061 | ("O3|pij=1;chains;no-wait|ΣTj", p279), |
| 2062 | ("F|fixj;prec;pij=1|Cmax", p280), |
| 2063 | ("O|fixj;prec;pij=1|Cmax", p281), |
| 2064 | ("O|fixj;tree;rj;pij=1|Cmax", p282), |
| 2065 | ("O|fixj;tree;pij=1|Lmax", p283), |
| 2066 | ("O2|fixj;chains;pij=1|ΣwjCj", p284), |
| 2067 | ("O2|fixj;chains;pij=1|ΣUj", p285), |
| 2068 | ("O2|fixj;chains;pij=1|ΣTj", p286), |
| 2069 | ("O|Mj;outtree;rj;pij=1|Cmax", p287), |
| 2070 | ("O|Mj;prec;pij=1|Cmax", p288), |
| 2071 | ("O|Mj;outtree;pij=1|Lmax", p289), |
| 2072 | ("O2|Mj;chains;pij=1|ΣwjCj", p290), |
| 2073 | ("O2|Mj;chains;pij=1|ΣUj", p291), |
| 2074 | ("O2|Mj;chains;pij=1|ΣTj", p292), |
| 2075 | ("O2|chains|Cmax", p293), |
| 2076 | ("F2|pij=1;chains|ΣwjCj", p294), |
| 2077 | ("F3|pij=1;chains|ΣwjCj", p295), |
| 2078 | ("F2|fixj;chains;pij=1|ΣwjCj", p296), |
| 2079 | ("O2|fixj;chains|Cmax", p297), |
| 2080 | ("F2|Mj;chains;pij=1|ΣwjCj", p298), |
| 2081 | ("O2|Mj;chains|Cmax", p299), |
| 2082 | ("O|pij=1;prec;no-wait|Cmax", p300), |
| 2083 | ("F|Mj;prec;pij=1|Cmax", p301), |
| 2084 | ("O2|pij=1;tj|Cmax", p302), |
| 2085 | ("F2|pij=1;tj∈T1,T2|Cmax", p303), |
| 2086 | ("F2|tj∈T1,T2|Cmax", p304), |
| 2087 | ("O2|tjkl=T|Cmax", p305), |
| 2088 | ("O2|tj∈T1,T2|Cmax", p306), |
| 2089 | ("F|pij=1;rj|ΣwjUj", p307), |
| 2090 | ("F|pij=1;rj|ΣwjTj", p308), |
| 2091 | ("F2|fixj;chains;pij=1|ΣUj", p309), |
| 2092 | ("F2|fixj;chains;pij=1|ΣTj", p310), |
| 2093 | ("F2|Mj;chains;pij=1|ΣUj", p311), |
| 2094 | ("F2|Mj;chains;pij=1|ΣTj", p312), |
| 2095 | ("F|pij=1;tk;rj|ΣwjUj", p313), |
| 2096 | ("F|pij=1;tk;rj|ΣwjTj", p314), |
| 2097 | ("FF(1,m)||ΣZj", p315), |
| 2098 | ("FF(1,m)||ΣwjZj", p316), |
| 2099 | ("FF(1,m)|pj=p|ΣZj", p317), |
| 2100 | ("F3||ΣZj", p318), |
| 2101 | ("F3||ΣwjZj", p319), |
| 2102 | ("F2||ΣwjZj", p320), |
| 2103 | ("F2||ΣZj", p321), |
| 2104 | ("F||ΣCj", p322), |
| 2105 | ("O||ΣCj", p323), |
| 2106 | ("J3||Cmax", p324), |
| 2107 | ("J||Cmax", p325), |
| 2108 | ("O|pij=1;STsd,b|Cmax", p326)] |
| 2109 | |
| 2110 | /-- The relations that hold field by field: general problem, special problem. -/ |
| 2111 | def specialCases : List (Spec F × Spec F) := [ |
| 2112 | (p1, p0), (p2, p3), (p325, p4), (p6, p5), (p7, p5), (p323, p5), (p200, p8), (p283, p16), |
| 2113 | (p199, p21), (p161, p23), (p163, p23), (p163, p24), (p164, p24), (p20, p38), (p56, p39), (p78, p39), |
| 2114 | (p300, p41), (p300, p42), (p199, p44), (p36, p47), (p287, p54), (p89, p59), (p89, p60), (p90, p60), |
| 2115 | (p212, p60), (p90, p61), (p135, p63), (p195, p63), (p196, p63), (p297, p63), (p52, p67), (p74, p67), |
| 2116 | (p214, p67), (p53, p68), (p75, p68), (p215, p68), (p89, p69), (p73, p71), (p282, p76), (p123, p82), |
| 2117 | (p36, p83), (p89, p83), (p37, p84), (p90, p84), (p86, p85), (p309, p85), (p311, p85), (p88, p87), |
| 2118 | (p310, p87), (p312, p87), (p55, p91), (p77, p91), (p102, p101), (p104, p103), (p106, p105), (p108, p107), |
| 2119 | (p109, p107), (p110, p108), (p110, p109), (p260, p120), (p282, p120), (p283, p120), (p201, p121), (p124, p122), |
| 2120 | (p216, p125), (p217, p125), (p220, p125), (p226, p125), (p4, p126), (p130, p126), (p324, p126), (p128, p127), |
| 2121 | (p129, p127), (p131, p127), (p322, p127), (p63, p132), (p133, p132), (p193, p132), (p194, p132), (p293, p132), |
| 2122 | (p305, p132), (p135, p133), (p137, p133), (p183, p133), (p188, p134), (p188, p135), (p190, p136), (p190, p137), |
| 2123 | (p141, p139), (p65, p143), (p126, p143), (p145, p143), (p202, p143), (p205, p143), (p206, p143), (p207, p143), |
| 2124 | (p208, p143), (p144, p145), (p304, p145), (p54, p148), (p190, p148), (p288, p148), (p289, p148), (p226, p149), |
| 2125 | (p227, p149), (p243, p149), (p244, p149), (p153, p152), (p155, p154), (p171, p169), (p172, p170), (p174, p173), |
| 2126 | (p237, p173), (p175, p174), (p22, p176), (p128, p178), (p186, p178), (p238, p178), (p239, p178), (p240, p178), |
| 2127 | (p219, p179), (p228, p179), (p245, p179), (p246, p179), (p247, p179), (p9, p180), (p181, p180), (p182, p180), |
| 2128 | (p188, p183), (p190, p183), (p187, p186), (p189, p186), (p57, p191), (p79, p191), (p180, p191), (p58, p192), |
| 2129 | (p80, p192), (p195, p193), (p197, p193), (p196, p194), (p198, p194), (p324, p202), (p209, p205), (p210, p206), |
| 2130 | (p211, p207), (p130, p208), (p209, p208), (p210, p208), (p211, p208), (p280, p212), (p301, p212), (p219, p218), |
| 2131 | (p222, p221), (p214, p223), (p215, p224), (p231, p229), (p324, p229), (p232, p230), (p233, p230), (p235, p234), |
| 2132 | (p257, p237), (p241, p238), (p249, p238), (p253, p238), (p250, p239), (p254, p239), (p241, p240), (p242, p240), |
| 2133 | (p251, p240), (p255, p240), (p252, p241), (p256, p241), (p258, p242), (p248, p247), (p252, p249), (p252, p251), |
| 2134 | (p256, p253), (p256, p255), (p258, p255), (p282, p259), (p287, p259), (p281, p260), (p288, p260), (p283, p261), |
| 2135 | (p289, p261), (p184, p262), (p185, p262), (p263, p262), (p284, p262), (p290, p262), (p40, p264), (p265, p264), |
| 2136 | (p285, p264), (p291, p264), (p267, p266), (p286, p266), (p292, p266), (p272, p268), (p273, p268), (p199, p271), |
| 2137 | (p275, p274), (p277, p276), (p279, p278), (p297, p293), (p299, p293), (p295, p294), (p296, p294), (p298, p294), |
| 2138 | (p3, p303), (p304, p303), (p2, p304), (p306, p305), (p313, p307), (p314, p308), (p316, p315), (p315, p317), |
| 2139 | (p319, p318), (p319, p320), (p318, p321), (p320, p321), (p325, p324)] |
| 2140 | |
| 2141 | /-- The relations that need a threshold step: general problem, special problem. -/ |
| 2142 | def thresholdReductions : List (Spec F × Spec F) := [ |
| 2143 | (p170, p24), (p273, p43), (p12, p46), (p13, p46), (p182, p54), (p181, p76), (p153, p134), (p155, p134), |
| 2144 | (p14, p136), (p15, p136), (p57, p148), (p58, p148), (p248, p149), (p150, p156), (p151, p156), (p237, p236)] |
| 2145 | |
| 2146 | axiom specialCases_hold : ∀ e ∈ specialCases, |
| 2147 | SpecialCase (problem F e.2) (problem F e.1) |
| 2148 | |
| 2149 | axiom thresholdReductions_hold : ∀ e ∈ thresholdReductions, |
| 2150 | Reducible (problem F e.2) (problem F e.1) |
| 2151 | |
| 2152 | end Lax434175.ZooShops |
| 2153 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments