# LTS Termination Proof

by AProVE

## Input

Integer Transition System
• Initial Location: f913_0__init__GE, f9340_0_possibleValues_GE, f8234_0_resolve_aux_GE, f9691_0_possibleValues_GE, __init, f9214_0_possibleValues_GE, f8739_0_possibleValues_GE, f10650_0_resolve_aux_GE, f1158_0__init__GE, f7719_0_resolve_aux_LE, f10649_0_resolve_aux_GE, f9214_0_possibleValues_GE', f1907_0_resolve_GE, f2103_0_resolve_GE, f8467_0_resolve_aux_GE, f1_0_main_Load, f8384_0_possibleValues_GE
• Transitions: (pre-variables and post-variables)  f1_0_main_Load 1 f913_0__init__GE: x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ _arg2 = _arg3P ∧ 0 = _arg2P ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ 1 ≤ _arg2 − 1 ∧ _arg1P ≤ _arg1 f913_0__init__GE 2 f1158_0__init__GE: x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x1 = _x6 ∧ x2 = _x7 ∧ x3 = _x8 ∧ x4 = _x9 ∧ x5 = _x10 ∧ x6 = _x11 ∧ _x2 = _x9 ∧ 0 = _x8 ∧ _x1 = _x7 ∧ 0 ≤ _x6 − 1 ∧ 0 ≤ _x − 1 ∧ _x1 ≤ 8 ∧ _x6 ≤ _x f1158_0__init__GE 3 f913_0__init__GE: x1 = _x12 ∧ x2 = _x13 ∧ x3 = _x14 ∧ x4 = _x15 ∧ x5 = _x16 ∧ x6 = _x19 ∧ x1 = _x20 ∧ x2 = _x21 ∧ x3 = _x22 ∧ x4 = _x23 ∧ x5 = _x24 ∧ x6 = _x25 ∧ _x15 = _x22 ∧ _x13 + 1 = _x21 ∧ 0 ≤ _x20 − 1 ∧ 0 ≤ _x12 − 1 ∧ 8 ≤ _x14 − 1 ∧ _x20 ≤ _x12 f1158_0__init__GE 4 f1158_0__init__GE: x1 = _x26 ∧ x2 = _x27 ∧ x3 = _x28 ∧ x4 = _x29 ∧ x5 = _x30 ∧ x6 = _x31 ∧ x1 = _x32 ∧ x2 = _x33 ∧ x3 = _x34 ∧ x4 = _x35 ∧ x5 = _x36 ∧ x6 = _x37 ∧ _x27 ≤ 8 ∧ _x28 ≤ 8 ∧ −1 ≤ _x38 − 1 ∧ _x28 ≤ _x38 − 1 ∧ _x28 ≤ _x39 − 1 ∧ −1 ≤ _x39 − 1 ∧ _x32 ≤ _x26 ∧ 0 ≤ _x26 − 1 ∧ 0 ≤ _x32 − 1 ∧ _x27 = _x33 ∧ _x28 + 1 = _x34 ∧ _x29 = _x35 f913_0__init__GE 5 f1907_0_resolve_GE: x1 = _x40 ∧ x2 = _x41 ∧ x3 = _x42 ∧ x4 = _x43 ∧ x5 = _x46 ∧ x6 = _x47 ∧ x1 = _x48 ∧ x2 = _x49 ∧ x3 = _x50 ∧ x4 = _x51 ∧ x5 = _x53 ∧ x6 = _x54 ∧ _x42 = _x53 ∧ 0 = _x51 ∧ 0 = _x50 ∧ 0 = _x49 ∧ 0 ≤ _x48 − 1 ∧ 0 ≤ _x40 − 1 ∧ 8 ≤ _x41 − 1 ∧ _x48 ≤ _x40 f1907_0_resolve_GE 6 f7719_0_resolve_aux_LE: x1 = _x55 ∧ x2 = _x56 ∧ x3 = _x57 ∧ x4 = _x58 ∧ x5 = _x59 ∧ x6 = _x60 ∧ x1 = _x61 ∧ x2 = _x62 ∧ x3 = _x66 ∧ x4 = _x67 ∧ x5 = _x68 ∧ x6 = _x69 ∧ _x56 = _x61 ∧ _x57 = _x58 ∧ 0 ≤ _x55 − 1 ∧ 1 ≤ _x59 − 1 ∧ 8 ≤ _x57 − 1 f1907_0_resolve_GE 7 f2103_0_resolve_GE: x1 = _x70 ∧ x2 = _x71 ∧ x3 = _x74 ∧ x4 = _x75 ∧ x5 = _x76 ∧ x6 = _x77 ∧ x1 = _x78 ∧ x2 = _x79 ∧ x3 = _x80 ∧ x4 = _x81 ∧ x5 = _x82 ∧ x6 = _x83 ∧ _x76 = _x82 ∧ 0 = _x81 ∧ _x74 = _x80 ∧ _x71 = _x79 ∧ _x74 = _x75 ∧ 0 ≤ _x78 − 1 ∧ 0 ≤ _x70 − 1 ∧ _x74 ≤ 8 ∧ _x78 ≤ _x70 f2103_0_resolve_GE 8 f1907_0_resolve_GE: x1 = _x84 ∧ x2 = _x85 ∧ x3 = _x89 ∧ x4 = _x90 ∧ x5 = _x91 ∧ x6 = _x92 ∧ x1 = _x96 ∧ x2 = _x97 ∧ x3 = _x98 ∧ x4 = _x99 ∧ x5 = _x105 ∧ x6 = _x106 ∧ _x91 = _x105 ∧ _x89 + 1 = _x99 ∧ _x89 + 1 = _x98 ∧ _x85 = _x97 ∧ 0 ≤ _x96 − 1 ∧ 0 ≤ _x84 − 1 ∧ 8 ≤ _x90 − 1 ∧ _x96 ≤ _x84 f2103_0_resolve_GE 9 f2103_0_resolve_GE: x1 = _x107 ∧ x2 = _x108 ∧ x3 = _x114 ∧ x4 = _x115 ∧ x5 = _x116 ∧ x6 = _x117 ∧ x1 = _x118 ∧ x2 = _x119 ∧ x3 = _x122 ∧ x4 = _x123 ∧ x5 = _x124 ∧ x6 = _x125 ∧ _x114 ≤ 8 ∧ _x115 ≤ 8 ∧ −1 ≤ _x126 − 1 ∧ _x127 ≤ −1 ∧ _x115 ≤ _x126 − 1 ∧ _x118 ≤ _x107 ∧ 0 ≤ _x107 − 1 ∧ 0 ≤ _x118 − 1 ∧ _x108 = _x119 ∧ _x114 = _x122 ∧ _x115 + 1 = _x123 ∧ _x116 = _x124 f2103_0_resolve_GE 10 f2103_0_resolve_GE: x1 = _x128 ∧ x2 = _x129 ∧ x3 = _x130 ∧ x4 = _x133 ∧ x5 = _x134 ∧ x6 = _x135 ∧ x1 = _x142 ∧ x2 = _x143 ∧ x3 = _x144 ∧ x4 = _x145 ∧ x5 = _x146 ∧ x6 = _x147 ∧ _x130 ≤ 8 ∧ _x133 ≤ 8 ∧ −1 ≤ _x148 − 1 ∧ 0 ≤ _x149 − 1 ∧ _x133 ≤ _x148 − 1 ∧ _x142 ≤ _x128 ∧ 0 ≤ _x128 − 1 ∧ 0 ≤ _x142 − 1 ∧ _x129 = _x143 ∧ _x130 = _x144 ∧ _x133 + 1 = _x145 ∧ _x134 = _x146 f2103_0_resolve_GE 11 f2103_0_resolve_GE: x1 = _x150 ∧ x2 = _x153 ∧ x3 = _x154 ∧ x4 = _x155 ∧ x5 = _x162 ∧ x6 = _x163 ∧ x1 = _x164 ∧ x2 = _x165 ∧ x3 = _x166 ∧ x4 = _x167 ∧ x5 = _x168 ∧ x6 = _x169 ∧ _x154 ≤ 8 ∧ _x155 ≤ 8 ∧ _x155 ≤ _x170 − 1 ∧ −1 ≤ _x170 − 1 ∧ _x164 ≤ _x150 ∧ 0 ≤ _x150 − 1 ∧ 0 ≤ _x164 − 1 ∧ _x153 + 1 = _x165 ∧ _x154 = _x166 ∧ _x155 + 1 = _x167 ∧ _x162 = _x168 f7719_0_resolve_aux_LE 12 f8234_0_resolve_aux_GE: x1 = _x171 ∧ x2 = _x172 ∧ x3 = _x173 ∧ x4 = _x174 ∧ x5 = _x175 ∧ x6 = _x178 ∧ x1 = _x179 ∧ x2 = _x180 ∧ x3 = _x181 ∧ x4 = _x182 ∧ x5 = _x189 ∧ x6 = _x190 ∧ 0 = _x181 ∧ 0 = _x180 ∧ _x171 = _x179 ∧ 0 ≤ _x171 − 1 f8234_0_resolve_aux_GE 13 f8467_0_resolve_aux_GE: x1 = _x191 ∧ x2 = _x192 ∧ x3 = _x193 ∧ x4 = _x194 ∧ x5 = _x197 ∧ x6 = _x198 ∧ x1 = _x199 ∧ x2 = _x203 ∧ x3 = _x204 ∧ x4 = _x205 ∧ x5 = _x206 ∧ x6 = _x210 ∧ 0 = _x204 ∧ _x193 = _x203 ∧ _x191 = _x199 ∧ _x193 ≤ 8 f8467_0_resolve_aux_GE 14 f8234_0_resolve_aux_GE: x1 = _x211 ∧ x2 = _x212 ∧ x3 = _x213 ∧ x4 = _x217 ∧ x5 = _x218 ∧ x6 = _x219 ∧ x1 = _x220 ∧ x2 = _x226 ∧ x3 = _x227 ∧ x4 = _x228 ∧ x5 = _x229 ∧ x6 = _x235 ∧ _x212 + 1 = _x227 ∧ _x213 = _x226 ∧ _x211 = _x220 ∧ 8 ≤ _x213 − 1 f8467_0_resolve_aux_GE 15 f8467_0_resolve_aux_GE: x1 = _x236 ∧ x2 = _x237 ∧ x3 = _x244 ∧ x4 = _x245 ∧ x5 = _x246 ∧ x6 = _x249 ∧ x1 = _x250 ∧ x2 = _x251 ∧ x3 = _x252 ∧ x4 = _x259 ∧ x5 = _x260 ∧ x6 = _x261 ∧ −1 ≤ _x268 − 1 ∧ _x244 ≤ 8 ∧ _x237 ≤ _x268 − 1 ∧ −1 ≤ _x269 − 1 ∧ _x244 ≤ _x269 − 1 ∧ _x270 ≤ −1 ∧ _x236 = _x250 ∧ _x237 = _x251 ∧ _x244 + 1 = _x252 f8467_0_resolve_aux_GE 16 f8467_0_resolve_aux_GE: x1 = _x271 ∧ x2 = _x272 ∧ x3 = _x273 ∧ x4 = _x280 ∧ x5 = _x281 ∧ x6 = _x282 ∧ x1 = _x283 ∧ x2 = _x284 ∧ x3 = _x285 ∧ x4 = _x286 ∧ x5 = _x287 ∧ x6 = _x288 ∧ −1 ≤ _x289 − 1 ∧ _x273 ≤ 8 ∧ _x272 ≤ _x289 − 1 ∧ −1 ≤ _x290 − 1 ∧ _x273 ≤ _x290 − 1 ∧ 0 ≤ _x291 − 1 ∧ _x271 = _x283 ∧ _x272 = _x284 ∧ _x273 + 1 = _x285 f8234_0_resolve_aux_GE 17 f10649_0_resolve_aux_GE: x1 = _x292 ∧ x2 = _x293 ∧ x3 = _x294 ∧ x4 = _x295 ∧ x5 = _x296 ∧ x6 = _x297 ∧ x1 = _x298 ∧ x2 = _x299 ∧ x3 = _x300 ∧ x4 = _x301 ∧ x5 = _x302 ∧ x6 = _x303 ∧ 0 = _x301 ∧ _x293 = _x300 ∧ _x294 = _x299 ∧ _x292 = _x298 ∧ 8 ≤ _x294 − 1 ∧ 0 ≤ _x292 − 1 f8467_0_resolve_aux_GE 18 f10650_0_resolve_aux_GE: x1 = _x304 ∧ x2 = _x305 ∧ x3 = _x306 ∧ x4 = _x307 ∧ x5 = _x308 ∧ x6 = _x309 ∧ x1 = _x310 ∧ x2 = _x311 ∧ x3 = _x312 ∧ x4 = _x313 ∧ x5 = _x314 ∧ x6 = _x315 ∧ −1 ≤ _x316 − 1 ∧ _x306 ≤ 8 ∧ _x305 ≤ _x316 − 1 ∧ −1 ≤ _x317 − 1 ∧ _x306 ≤ _x317 − 1 ∧ 0 ≤ _x304 − 1 ∧ _x304 = _x310 ∧ _x305 = _x311 ∧ _x306 = _x312 ∧ 0 = _x313 f10649_0_resolve_aux_GE 19 f10649_0_resolve_aux_GE: x1 = _x318 ∧ x2 = _x319 ∧ x3 = _x320 ∧ x4 = _x321 ∧ x5 = _x322 ∧ x6 = _x323 ∧ x1 = _x324 ∧ x2 = _x325 ∧ x3 = _x326 ∧ x4 = _x327 ∧ x5 = _x328 ∧ x6 = _x329 ∧ _x321 + 1 = _x327 ∧ _x320 = _x326 ∧ _x319 = _x325 ∧ _x318 = _x324 ∧ _x321 ≤ 8 f10650_0_resolve_aux_GE 20 f10650_0_resolve_aux_GE: x1 = _x330 ∧ x2 = _x331 ∧ x3 = _x332 ∧ x4 = _x333 ∧ x5 = _x334 ∧ x6 = _x335 ∧ x1 = _x336 ∧ x2 = _x337 ∧ x3 = _x338 ∧ x4 = _x339 ∧ x5 = _x340 ∧ x6 = _x341 ∧ _x333 + 1 = _x339 ∧ _x332 = _x338 ∧ _x331 = _x337 ∧ _x330 = _x336 ∧ _x333 ≤ 8 f10649_0_resolve_aux_GE 21 f7719_0_resolve_aux_LE: x1 = _x342 ∧ x2 = _x343 ∧ x3 = _x344 ∧ x4 = _x345 ∧ x5 = _x346 ∧ x6 = _x347 ∧ x1 = _x348 ∧ x2 = _x349 ∧ x3 = _x350 ∧ x4 = _x351 ∧ x5 = _x352 ∧ x6 = _x353 ∧ _x354 ≤ −1 ∧ _x345 ≤ 8 ∧ −1 ≤ _x355 − 1 ∧ _x343 ≤ _x355 − 1 ∧ −1 ≤ _x345 − 1 ∧ −1 ≤ _x356 − 1 ∧ _x344 ≤ _x356 − 1 ∧ 1 ≤ _x343 − 1 ∧ _x342 − 1 ≤ _x342 − 1 ∧ 0 ≤ _x342 − 1 ∧ _x342 − 1 = _x348 f10649_0_resolve_aux_GE 22 f7719_0_resolve_aux_LE: x1 = _x357 ∧ x2 = _x358 ∧ x3 = _x359 ∧ x4 = _x360 ∧ x5 = _x361 ∧ x6 = _x362 ∧ x1 = _x363 ∧ x2 = _x364 ∧ x3 = _x365 ∧ x4 = _x366 ∧ x5 = _x367 ∧ x6 = _x368 ∧ 0 ≤ _x369 − 1 ∧ _x360 ≤ 8 ∧ −1 ≤ _x370 − 1 ∧ _x358 ≤ _x370 − 1 ∧ −1 ≤ _x360 − 1 ∧ −1 ≤ _x371 − 1 ∧ _x359 ≤ _x371 − 1 ∧ 1 ≤ _x358 − 1 ∧ _x357 − 1 ≤ _x357 − 1 ∧ 0 ≤ _x357 − 1 ∧ _x357 − 1 = _x363 f10650_0_resolve_aux_GE 23 f7719_0_resolve_aux_LE: x1 = _x372 ∧ x2 = _x373 ∧ x3 = _x374 ∧ x4 = _x375 ∧ x5 = _x376 ∧ x6 = _x377 ∧ x1 = _x378 ∧ x2 = _x379 ∧ x3 = _x380 ∧ x4 = _x381 ∧ x5 = _x382 ∧ x6 = _x383 ∧ _x384 ≤ −1 ∧ _x375 ≤ 8 ∧ −1 ≤ _x385 − 1 ∧ _x373 ≤ _x385 − 1 ∧ −1 ≤ _x375 − 1 ∧ −1 ≤ _x386 − 1 ∧ _x374 ≤ _x386 − 1 ∧ _x372 − 1 ≤ _x372 − 1 ∧ 0 ≤ _x372 − 1 ∧ _x372 − 1 = _x378 f10650_0_resolve_aux_GE 24 f7719_0_resolve_aux_LE: x1 = _x387 ∧ x2 = _x388 ∧ x3 = _x389 ∧ x4 = _x390 ∧ x5 = _x391 ∧ x6 = _x392 ∧ x1 = _x393 ∧ x2 = _x394 ∧ x3 = _x395 ∧ x4 = _x396 ∧ x5 = _x397 ∧ x6 = _x398 ∧ 0 ≤ _x399 − 1 ∧ _x390 ≤ 8 ∧ −1 ≤ _x400 − 1 ∧ _x388 ≤ _x400 − 1 ∧ −1 ≤ _x390 − 1 ∧ −1 ≤ _x401 − 1 ∧ _x389 ≤ _x401 − 1 ∧ _x387 − 1 ≤ _x387 − 1 ∧ 0 ≤ _x387 − 1 ∧ _x387 − 1 = _x393 f10649_0_resolve_aux_GE 25 f10649_0_resolve_aux_GE: x1 = _x402 ∧ x2 = _x403 ∧ x3 = _x404 ∧ x4 = _x405 ∧ x5 = _x406 ∧ x6 = _x407 ∧ x1 = _x408 ∧ x2 = _x409 ∧ x3 = _x410 ∧ x4 = _x411 ∧ x5 = _x412 ∧ x6 = _x413 ∧ _x414 ≤ −1 ∧ _x405 ≤ 8 ∧ −1 ≤ _x415 − 1 ∧ _x403 ≤ _x415 − 1 ∧ −1 ≤ _x405 − 1 ∧ −1 ≤ _x416 − 1 ∧ _x404 ≤ _x416 − 1 ∧ 1 ≤ _x403 − 1 ∧ 0 ≤ _x402 − 1 ∧ _x402 − 1 ≤ _x402 − 1 ∧ −1 ≤ _x417 − 1 ∧ _x403 ≤ _x417 − 1 ∧ −1 ≤ _x418 − 1 ∧ _x404 ≤ _x418 − 1 ∧ _x402 = _x408 ∧ _x403 = _x409 ∧ _x404 = _x410 ∧ _x405 + 1 = _x411 f10649_0_resolve_aux_GE 26 f10649_0_resolve_aux_GE: x1 = _x419 ∧ x2 = _x420 ∧ x3 = _x421 ∧ x4 = _x422 ∧ x5 = _x423 ∧ x6 = _x424 ∧ x1 = _x425 ∧ x2 = _x426 ∧ x3 = _x427 ∧ x4 = _x428 ∧ x5 = _x429 ∧ x6 = _x430 ∧ 0 ≤ _x431 − 1 ∧ _x422 ≤ 8 ∧ −1 ≤ _x432 − 1 ∧ _x420 ≤ _x432 − 1 ∧ −1 ≤ _x422 − 1 ∧ −1 ≤ _x433 − 1 ∧ _x421 ≤ _x433 − 1 ∧ 1 ≤ _x420 − 1 ∧ 0 ≤ _x419 − 1 ∧ _x419 − 1 ≤ _x419 − 1 ∧ −1 ≤ _x434 − 1 ∧ _x420 ≤ _x434 − 1 ∧ −1 ≤ _x435 − 1 ∧ _x421 ≤ _x435 − 1 ∧ _x419 = _x425 ∧ _x420 = _x426 ∧ _x421 = _x427 ∧ _x422 + 1 = _x428 f10650_0_resolve_aux_GE 27 f10650_0_resolve_aux_GE: x1 = _x436 ∧ x2 = _x437 ∧ x3 = _x438 ∧ x4 = _x439 ∧ x5 = _x440 ∧ x6 = _x441 ∧ x1 = _x442 ∧ x2 = _x443 ∧ x3 = _x444 ∧ x4 = _x445 ∧ x5 = _x446 ∧ x6 = _x447 ∧ _x448 ≤ −1 ∧ _x439 ≤ 8 ∧ −1 ≤ _x449 − 1 ∧ _x437 ≤ _x449 − 1 ∧ −1 ≤ _x439 − 1 ∧ −1 ≤ _x450 − 1 ∧ _x438 ≤ _x450 − 1 ∧ 0 ≤ _x436 − 1 ∧ _x436 − 1 ≤ _x436 − 1 ∧ −1 ≤ _x451 − 1 ∧ _x437 ≤ _x451 − 1 ∧ −1 ≤ _x452 − 1 ∧ _x438 ≤ _x452 − 1 ∧ _x436 = _x442 ∧ _x437 = _x443 ∧ _x438 = _x444 ∧ _x439 + 1 = _x445 f10650_0_resolve_aux_GE 28 f10650_0_resolve_aux_GE: x1 = _x453 ∧ x2 = _x454 ∧ x3 = _x455 ∧ x4 = _x456 ∧ x5 = _x457 ∧ x6 = _x458 ∧ x1 = _x459 ∧ x2 = _x460 ∧ x3 = _x461 ∧ x4 = _x462 ∧ x5 = _x463 ∧ x6 = _x464 ∧ 0 ≤ _x465 − 1 ∧ _x456 ≤ 8 ∧ −1 ≤ _x466 − 1 ∧ _x454 ≤ _x466 − 1 ∧ −1 ≤ _x456 − 1 ∧ −1 ≤ _x467 − 1 ∧ _x455 ≤ _x467 − 1 ∧ 0 ≤ _x453 − 1 ∧ _x453 − 1 ≤ _x453 − 1 ∧ −1 ≤ _x468 − 1 ∧ _x454 ≤ _x468 − 1 ∧ −1 ≤ _x469 − 1 ∧ _x455 ≤ _x469 − 1 ∧ _x453 = _x459 ∧ _x454 = _x460 ∧ _x455 = _x461 ∧ _x456 + 1 = _x462 f8234_0_resolve_aux_GE 29 f8384_0_possibleValues_GE: x1 = _x470 ∧ x2 = _x471 ∧ x3 = _x472 ∧ x4 = _x473 ∧ x5 = _x474 ∧ x6 = _x475 ∧ x1 = _x476 ∧ x2 = _x477 ∧ x3 = _x478 ∧ x4 = _x479 ∧ x5 = _x480 ∧ x6 = _x481 ∧ 0 = _x478 ∧ _x471 = _x477 ∧ _x472 = _x476 ∧ 8 ≤ _x472 − 1 ∧ 0 ≤ _x470 − 1 f8467_0_resolve_aux_GE 30 f8384_0_possibleValues_GE: x1 = _x482 ∧ x2 = _x483 ∧ x3 = _x484 ∧ x4 = _x485 ∧ x5 = _x486 ∧ x6 = _x487 ∧ x1 = _x488 ∧ x2 = _x489 ∧ x3 = _x490 ∧ x4 = _x491 ∧ x5 = _x492 ∧ x6 = _x493 ∧ −1 ≤ _x494 − 1 ∧ _x484 ≤ 8 ∧ _x483 ≤ _x494 − 1 ∧ −1 ≤ _x495 − 1 ∧ _x484 ≤ _x495 − 1 ∧ 0 ≤ _x482 − 1 ∧ _x483 = _x488 ∧ _x484 = _x489 ∧ 0 = _x490 f8384_0_possibleValues_GE 31 f8384_0_possibleValues_GE: x1 = _x496 ∧ x2 = _x497 ∧ x3 = _x498 ∧ x4 = _x499 ∧ x5 = _x500 ∧ x6 = _x501 ∧ x1 = _x502 ∧ x2 = _x503 ∧ x3 = _x504 ∧ x4 = _x505 ∧ x5 = _x506 ∧ x6 = _x507 ∧ _x498 + 1 = _x504 ∧ _x497 = _x503 ∧ _x496 = _x502 ∧ _x498 ≤ 8 f8384_0_possibleValues_GE 32 f8739_0_possibleValues_GE: x1 = _x508 ∧ x2 = _x509 ∧ x3 = _x510 ∧ x4 = _x511 ∧ x5 = _x512 ∧ x6 = _x513 ∧ x1 = _x514 ∧ x2 = _x515 ∧ x3 = _x516 ∧ x4 = _x517 ∧ x5 = _x518 ∧ x6 = _x519 ∧ 0 = _x516 ∧ _x509 = _x515 ∧ _x508 = _x514 ∧ 8 ≤ _x510 − 1 f8739_0_possibleValues_GE 33 f8739_0_possibleValues_GE: x1 = _x520 ∧ x2 = _x521 ∧ x3 = _x522 ∧ x4 = _x523 ∧ x5 = _x524 ∧ x6 = _x525 ∧ x1 = _x526 ∧ x2 = _x527 ∧ x3 = _x528 ∧ x4 = _x529 ∧ x5 = _x530 ∧ x6 = _x531 ∧ −1 ≤ _x532 − 1 ∧ _x522 ≤ 8 ∧ _x520 ≤ _x532 − 1 ∧ −1 ≤ _x533 − 1 ∧ _x522 ≤ _x533 − 1 ∧ _x520 = _x526 ∧ _x521 = _x527 ∧ _x522 + 1 = _x528 f8739_0_possibleValues_GE 34 f8739_0_possibleValues_GE: x1 = _x534 ∧ x2 = _x535 ∧ x3 = _x536 ∧ x4 = _x537 ∧ x5 = _x538 ∧ x6 = _x539 ∧ x1 = _x540 ∧ x2 = _x541 ∧ x3 = _x542 ∧ x4 = _x543 ∧ x5 = _x544 ∧ x6 = _x545 ∧ −1 ≤ _x546 − 1 ∧ _x536 ≤ 8 ∧ _x534 ≤ _x546 − 1 ∧ −1 ≤ _x547 − 1 ∧ _x536 ≤ _x547 − 1 ∧ _x548 ≤ −1 ∧ −1 ≤ _x549 − 1 ∧ _x534 ≤ _x549 − 1 ∧ −1 ≤ _x550 − 1 ∧ _x536 ≤ _x550 − 1 ∧ _x551 ≤ 9 ∧ _x534 = _x540 ∧ _x535 = _x541 ∧ _x536 + 1 = _x542 f8739_0_possibleValues_GE 35 f8739_0_possibleValues_GE: x1 = _x552 ∧ x2 = _x553 ∧ x3 = _x554 ∧ x4 = _x555 ∧ x5 = _x556 ∧ x6 = _x557 ∧ x1 = _x558 ∧ x2 = _x559 ∧ x3 = _x560 ∧ x4 = _x561 ∧ x5 = _x562 ∧ x6 = _x563 ∧ −1 ≤ _x564 − 1 ∧ _x554 ≤ 8 ∧ _x552 ≤ _x564 − 1 ∧ −1 ≤ _x565 − 1 ∧ _x554 ≤ _x565 − 1 ∧ 0 ≤ _x566 − 1 ∧ −1 ≤ _x567 − 1 ∧ _x552 ≤ _x567 − 1 ∧ −1 ≤ _x568 − 1 ∧ _x554 ≤ _x568 − 1 ∧ _x569 ≤ 9 ∧ _x552 = _x558 ∧ _x553 = _x559 ∧ _x554 + 1 = _x560 f8739_0_possibleValues_GE 36 f9214_0_possibleValues_GE: x1 = _x570 ∧ x2 = _x571 ∧ x3 = _x572 ∧ x4 = _x573 ∧ x5 = _x574 ∧ x6 = _x575 ∧ x1 = _x576 ∧ x2 = _x577 ∧ x3 = _x578 ∧ x4 = _x579 ∧ x5 = _x580 ∧ x6 = _x581 ∧ 0 = _x578 ∧ _x571 = _x577 ∧ _x570 = _x576 ∧ 8 ≤ _x572 − 1 f9214_0_possibleValues_GE 37 f9214_0_possibleValues_GE': x1 = _x582 ∧ x2 = _x583 ∧ x3 = _x584 ∧ x4 = _x585 ∧ x5 = _x586 ∧ x6 = _x587 ∧ x1 = _x588 ∧ x2 = _x589 ∧ x3 = _x590 ∧ x4 = _x591 ∧ x5 = _x592 ∧ x6 = _x593 ∧ 0 ≤ _x582 − 3⋅_x594 ∧ 8 ≤ _x584 − 1 ∧ −1 ≤ _x582 − 1 ∧ 0 ≤ _x583 − 3⋅_x595 ∧ −1 ≤ _x583 − 1 ∧ _x582 = _x588 ∧ _x583 = _x589 ∧ _x584 = _x590 f9214_0_possibleValues_GE' 38 f9340_0_possibleValues_GE: x1 = _x596 ∧ x2 = _x597 ∧ x3 = _x598 ∧ x4 = _x599 ∧ x5 = _x600 ∧ x6 = _x601 ∧ x1 = _x602 ∧ x2 = _x603 ∧ x3 = _x604 ∧ x4 = _x605 ∧ x5 = _x606 ∧ x6 = _x607 ∧ 0 ≤ _x596 − 3⋅_x608 ∧ 8 ≤ _x598 − 1 ∧ −1 ≤ _x596 − 1 ∧ −1 ≤ _x597 − 1 ∧ 0 ≤ _x597 − 3⋅_x609 ∧ _x596 − 3⋅_x608 ≤ 2 ∧ _x597 − 3⋅_x609 ≤ 2 ∧ 0 ≤ _x597 − 3⋅_x610 ∧ _x597 − 3⋅_x610 ≤ 2 ∧ 0 ≤ _x597 − 3⋅_x611 ∧ _x597 − 3⋅_x611 ≤ 2 ∧ 0 ≤ _x596 − 3⋅_x612 ∧ _x596 − 3⋅_x612 ≤ 2 ∧ _x596 − 3⋅_x613 ≤ 2 ∧ 0 ≤ _x596 − 3⋅_x613 ∧ _x597 − _x597 − 3⋅_x610 = _x602 ∧ _x597 − _x597 − 3⋅_x611 + 3 = _x603 ∧ _x596 − _x596 − 3⋅_x612 = _x604 ∧ _x596 − _x596 − 3⋅_x613 + 3 = _x605 f9214_0_possibleValues_GE 39 f9214_0_possibleValues_GE: x1 = _x614 ∧ x2 = _x615 ∧ x3 = _x616 ∧ x4 = _x617 ∧ x5 = _x618 ∧ x6 = _x619 ∧ x1 = _x620 ∧ x2 = _x621 ∧ x3 = _x622 ∧ x4 = _x623 ∧ x5 = _x624 ∧ x6 = _x625 ∧ −1 ≤ _x626 − 1 ∧ _x616 ≤ 8 ∧ _x616 ≤ _x626 − 1 ∧ −1 ≤ _x627 − 1 ∧ _x615 ≤ _x627 − 1 ∧ _x614 = _x620 ∧ _x615 = _x621 ∧ _x616 + 1 = _x622 f9214_0_possibleValues_GE 40 f9214_0_possibleValues_GE: x1 = _x628 ∧ x2 = _x629 ∧ x3 = _x630 ∧ x4 = _x631 ∧ x5 = _x632 ∧ x6 = _x633 ∧ x1 = _x634 ∧ x2 = _x635 ∧ x3 = _x636 ∧ x4 = _x637 ∧ x5 = _x638 ∧ x6 = _x639 ∧ −1 ≤ _x640 − 1 ∧ _x630 ≤ 8 ∧ _x630 ≤ _x640 − 1 ∧ −1 ≤ _x641 − 1 ∧ _x629 ≤ _x641 − 1 ∧ _x642 ≤ −1 ∧ −1 ≤ _x643 − 1 ∧ _x630 ≤ _x643 − 1 ∧ −1 ≤ _x644 − 1 ∧ _x629 ≤ _x644 − 1 ∧ _x645 ≤ 9 ∧ _x628 = _x634 ∧ _x629 = _x635 ∧ _x630 + 1 = _x636 f9214_0_possibleValues_GE 41 f9214_0_possibleValues_GE: x1 = _x646 ∧ x2 = _x647 ∧ x3 = _x648 ∧ x4 = _x649 ∧ x5 = _x650 ∧ x6 = _x651 ∧ x1 = _x652 ∧ x2 = _x653 ∧ x3 = _x654 ∧ x4 = _x655 ∧ x5 = _x656 ∧ x6 = _x657 ∧ −1 ≤ _x658 − 1 ∧ _x648 ≤ 8 ∧ _x648 ≤ _x658 − 1 ∧ −1 ≤ _x659 − 1 ∧ _x647 ≤ _x659 − 1 ∧ 0 ≤ _x660 − 1 ∧ −1 ≤ _x661 − 1 ∧ _x648 ≤ _x661 − 1 ∧ −1 ≤ _x662 − 1 ∧ _x647 ≤ _x662 − 1 ∧ _x663 ≤ 9 ∧ _x646 = _x652 ∧ _x647 = _x653 ∧ _x648 + 1 = _x654 f9340_0_possibleValues_GE 42 f9691_0_possibleValues_GE: x1 = _x664 ∧ x2 = _x665 ∧ x3 = _x666 ∧ x4 = _x667 ∧ x5 = _x668 ∧ x6 = _x669 ∧ x1 = _x670 ∧ x2 = _x671 ∧ x3 = _x672 ∧ x4 = _x673 ∧ x5 = _x674 ∧ x6 = _x675 ∧ _x665 = _x675 ∧ _x664 = _x674 ∧ _x664 = _x673 ∧ _x666 = _x672 ∧ _x667 = _x671 ∧ _x664 = _x670 ∧ _x666 ≤ _x667 − 1 f9691_0_possibleValues_GE 43 f9340_0_possibleValues_GE: x1 = _x676 ∧ x2 = _x677 ∧ x3 = _x678 ∧ x4 = _x679 ∧ x5 = _x680 ∧ x6 = _x681 ∧ x1 = _x682 ∧ x2 = _x683 ∧ x3 = _x684 ∧ x4 = _x685 ∧ x5 = _x686 ∧ x6 = _x687 ∧ _x677 = _x685 ∧ _x678 + 1 = _x684 ∧ _x681 = _x683 ∧ _x676 = _x682 ∧ _x679 = _x680 ∧ _x681 ≤ _x679 f9691_0_possibleValues_GE 44 f9691_0_possibleValues_GE: x1 = _x688 ∧ x2 = _x689 ∧ x3 = _x690 ∧ x4 = _x691 ∧ x5 = _x692 ∧ x6 = _x693 ∧ x1 = _x694 ∧ x2 = _x695 ∧ x3 = _x696 ∧ x4 = _x697 ∧ x5 = _x698 ∧ x6 = _x699 ∧ −1 ≤ _x700 − 1 ∧ _x691 ≤ _x693 − 1 ∧ _x690 ≤ _x700 − 1 ∧ −1 ≤ _x701 − 1 ∧ _x691 ≤ _x701 − 1 ∧ _x691 = _x692 ∧ _x688 = _x694 ∧ _x689 = _x695 ∧ _x690 = _x696 ∧ _x691 + 1 = _x697 ∧ _x691 + 1 = _x698 ∧ _x693 = _x699 f9691_0_possibleValues_GE 45 f9691_0_possibleValues_GE: x1 = _x702 ∧ x2 = _x703 ∧ x3 = _x704 ∧ x4 = _x705 ∧ x5 = _x706 ∧ x6 = _x707 ∧ x1 = _x708 ∧ x2 = _x709 ∧ x3 = _x710 ∧ x4 = _x711 ∧ x5 = _x712 ∧ x6 = _x713 ∧ −1 ≤ _x714 − 1 ∧ _x705 ≤ _x707 − 1 ∧ _x704 ≤ _x714 − 1 ∧ −1 ≤ _x715 − 1 ∧ _x705 ≤ _x715 − 1 ∧ _x716 ≤ −1 ∧ −1 ≤ _x717 − 1 ∧ _x704 ≤ _x717 − 1 ∧ −1 ≤ _x718 − 1 ∧ _x705 ≤ _x718 − 1 ∧ _x719 ≤ 9 ∧ _x705 = _x706 ∧ _x702 = _x708 ∧ _x703 = _x709 ∧ _x704 = _x710 ∧ _x705 + 1 = _x711 ∧ _x705 + 1 = _x712 ∧ _x707 = _x713 f9691_0_possibleValues_GE 46 f9691_0_possibleValues_GE: x1 = _x720 ∧ x2 = _x721 ∧ x3 = _x722 ∧ x4 = _x723 ∧ x5 = _x724 ∧ x6 = _x725 ∧ x1 = _x726 ∧ x2 = _x727 ∧ x3 = _x728 ∧ x4 = _x729 ∧ x5 = _x730 ∧ x6 = _x731 ∧ −1 ≤ _x732 − 1 ∧ _x723 ≤ _x725 − 1 ∧ _x722 ≤ _x732 − 1 ∧ −1 ≤ _x733 − 1 ∧ _x723 ≤ _x733 − 1 ∧ 0 ≤ _x734 − 1 ∧ −1 ≤ _x735 − 1 ∧ _x722 ≤ _x735 − 1 ∧ −1 ≤ _x736 − 1 ∧ _x723 ≤ _x736 − 1 ∧ _x737 ≤ 9 ∧ _x723 = _x724 ∧ _x720 = _x726 ∧ _x721 = _x727 ∧ _x722 = _x728 ∧ _x723 + 1 = _x729 ∧ _x723 + 1 = _x730 ∧ _x725 = _x731 __init 47 f1_0_main_Load: x1 = _x738 ∧ x2 = _x739 ∧ x3 = _x740 ∧ x4 = _x741 ∧ x5 = _x742 ∧ x6 = _x743 ∧ x1 = _x744 ∧ x2 = _x745 ∧ x3 = _x746 ∧ x4 = _x747 ∧ x5 = _x748 ∧ x6 = _x749 ∧ 0 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 f913_0__init__GE f913_0__init__GE f913_0__init__GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f9340_0_possibleValues_GE f9340_0_possibleValues_GE f9340_0_possibleValues_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f8234_0_resolve_aux_GE f8234_0_resolve_aux_GE f8234_0_resolve_aux_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f9691_0_possibleValues_GE f9691_0_possibleValues_GE f9691_0_possibleValues_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 __init __init __init: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f9214_0_possibleValues_GE f9214_0_possibleValues_GE f9214_0_possibleValues_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f8739_0_possibleValues_GE f8739_0_possibleValues_GE f8739_0_possibleValues_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f10650_0_resolve_aux_GE f10650_0_resolve_aux_GE f10650_0_resolve_aux_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f1158_0__init__GE f1158_0__init__GE f1158_0__init__GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f7719_0_resolve_aux_LE f7719_0_resolve_aux_LE f7719_0_resolve_aux_LE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f10649_0_resolve_aux_GE f10649_0_resolve_aux_GE f10649_0_resolve_aux_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f9214_0_possibleValues_GE' f9214_0_possibleValues_GE' f9214_0_possibleValues_GE': x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f1907_0_resolve_GE f1907_0_resolve_GE f1907_0_resolve_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f2103_0_resolve_GE f2103_0_resolve_GE f2103_0_resolve_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f8467_0_resolve_aux_GE f8467_0_resolve_aux_GE f8467_0_resolve_aux_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f1_0_main_Load f1_0_main_Load f1_0_main_Load: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 f8384_0_possibleValues_GE f8384_0_possibleValues_GE f8384_0_possibleValues_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
and for every transition t, a duplicate t is considered.

### 2 SCC Decomposition

We consider subproblems for each of the 7 SCC(s) of the program graph.

### 2.1 SCC Subproblem 1/7

Here we consider the SCC { f913_0__init__GE, f1158_0__init__GE }.

### 2.1.1 Transition Removal

We remove transition 2 using the following ranking functions, which are bounded by −16.

 f913_0__init__GE: −2⋅x2 f1158_0__init__GE: −2⋅x2 − 1

### 2.1.2 Transition Removal

We remove transition 3 using the following ranking functions, which are bounded by 0.

 f1158_0__init__GE: 0 f913_0__init__GE: −1

### 2.1.3 Transition Removal

We remove transition 4 using the following ranking functions, which are bounded by −8.

 f1158_0__init__GE: − x3

### 2.1.4 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

### 2.2 SCC Subproblem 2/7

Here we consider the SCC { f1907_0_resolve_GE, f2103_0_resolve_GE }.

### 2.2.1 Transition Removal

We remove transition 7 using the following ranking functions, which are bounded by −14.

 f1907_0_resolve_GE: −2⋅x4 + 2 f2103_0_resolve_GE: −2⋅x3 + 1

### 2.2.2 Transition Removal

We remove transition 8 using the following ranking functions, which are bounded by 0.

 f2103_0_resolve_GE: 0 f1907_0_resolve_GE: −1

### 2.2.3 Transition Removal

We remove transitions 9, 10, 11 using the following ranking functions, which are bounded by 0.

 f2103_0_resolve_GE: 8 − x4

### 2.2.4 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

### 2.3 SCC Subproblem 3/7

Here we consider the SCC { f10650_0_resolve_aux_GE, f7719_0_resolve_aux_LE, f10649_0_resolve_aux_GE, f8467_0_resolve_aux_GE, f8234_0_resolve_aux_GE }.

### 2.3.1 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by 0.

 f7719_0_resolve_aux_LE: −1 + x1 f8234_0_resolve_aux_GE: −2 + x1 f10650_0_resolve_aux_GE: −2 + x1 f8467_0_resolve_aux_GE: −2 + x1 f10649_0_resolve_aux_GE: −2 + x1

### 2.3.2 Transition Removal

We remove transitions 18, 17 using the following ranking functions, which are bounded by 0.

 f10650_0_resolve_aux_GE: −1 − x1 f7719_0_resolve_aux_LE: −2 − x1 f8467_0_resolve_aux_GE: −1 + x1 f10649_0_resolve_aux_GE: −1 − x1 f8234_0_resolve_aux_GE: −1 + x1

### 2.3.3 Transition Removal

We remove transition 13 using the following ranking functions, which are bounded by 0.

 f10650_0_resolve_aux_GE: −1 − x1 f7719_0_resolve_aux_LE: −2 − x1 f10649_0_resolve_aux_GE: −5 + x1 + x2 f8467_0_resolve_aux_GE: 7 − x2 f8234_0_resolve_aux_GE: 8 − x3

### 2.3.4 Transition Removal

We remove transitions 15, 16 using the following ranking functions, which are bounded by 0.

 f10650_0_resolve_aux_GE: −1 − x1 f7719_0_resolve_aux_LE: −2 − x1 f10649_0_resolve_aux_GE: −5 + x1 + x2 f8467_0_resolve_aux_GE: 8 − x3 f8234_0_resolve_aux_GE: 8 − x2

### 2.3.5 Transition Removal

We remove transition 14 using the following ranking functions, which are bounded by 0.

 f10650_0_resolve_aux_GE: −1 − x1 f7719_0_resolve_aux_LE: −2 − x1 f10649_0_resolve_aux_GE: −5 + x1 + x2 f8467_0_resolve_aux_GE: 0 f8234_0_resolve_aux_GE: −1

### 2.3.6 Transition Removal

We remove transitions 24, 23 using the following ranking functions, which are bounded by 0.

 f10650_0_resolve_aux_GE: −1 + x1 f7719_0_resolve_aux_LE: −1 + x1 f10649_0_resolve_aux_GE: −4 + x1 + x2

### 2.3.7 Transition Removal

We remove transitions 20, 27, 28 using the following ranking functions, which are bounded by 0.

 f10650_0_resolve_aux_GE: 8 − x4 f10649_0_resolve_aux_GE: −4 + x1 + x2 f7719_0_resolve_aux_LE: −1 + x1

### 2.3.8 Transition Removal

We remove transitions 22, 21 using the following ranking functions, which are bounded by 0.

 f10649_0_resolve_aux_GE: −3 + x1 + x2 f7719_0_resolve_aux_LE: −1 + x1

### 2.3.9 Transition Removal

We remove transitions 19, 25, 26 using the following ranking functions, which are bounded by 0.

 f10649_0_resolve_aux_GE: 8 − x4

### 2.3.10 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

### 2.4 SCC Subproblem 4/7

Here we consider the SCC { f8384_0_possibleValues_GE }.

### 2.4.1 Transition Removal

We remove transition 31 using the following ranking functions, which are bounded by 0.

 f8384_0_possibleValues_GE: 8 − x3

### 2.4.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

### 2.5 SCC Subproblem 5/7

Here we consider the SCC { f8739_0_possibleValues_GE }.

### 2.5.1 Transition Removal

We remove transitions 33, 34, 35 using the following ranking functions, which are bounded by −8.

 f8739_0_possibleValues_GE: − x3

### 2.5.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

### 2.6 SCC Subproblem 6/7

Here we consider the SCC { f9214_0_possibleValues_GE }.

### 2.6.1 Transition Removal

We remove transitions 39, 40, 41 using the following ranking functions, which are bounded by 0.

 f9214_0_possibleValues_GE: 8 − x3

### 2.6.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

### 2.7 SCC Subproblem 7/7

Here we consider the SCC { f9340_0_possibleValues_GE, f9691_0_possibleValues_GE }.

### 2.7.1 Transition Removal

We remove transition 42 using the following ranking functions, which are bounded by 0.

 f9340_0_possibleValues_GE: − x3 + x4 f9691_0_possibleValues_GE: −1 + x2 − x3

### 2.7.2 Transition Removal

We remove transition 43 using the following ranking functions, which are bounded by 0.

 f9691_0_possibleValues_GE: 0 f9340_0_possibleValues_GE: −1

### 2.7.3 Transition Removal

We remove transitions 44, 45, 46 using the following ranking functions, which are bounded by 0.

 f9691_0_possibleValues_GE: − x5 + x6

### 2.7.4 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

## Tool configuration

AProVE

• version: AProVE Commit ID: unknown
• strategy: Statistics for single proof: 100.00 % (37 real / 0 unknown / 0 assumptions / 37 total proof steps)