LTS Termination Proof

by AProVE

Input

• Initial Location: f1099_0_entry_LE, f411_0_createList_Load, f423_0_createList_Return, f1201_0_entry_GT, f1228_0_createList_LE, f787_0_createList_Load, f1_0_main_Load, f813_0_random_ArrayAccess, __init
• Transitions: (pre-variables and post-variables)

  f411_0_createList_Load	1	f787_0_createList_Load:		x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x7 = _arg7 ∧ x8 = _arg8 ∧ x9 = _arg9 ∧ x10 = _arg10 ∧ x11 = _arg11 ∧ x12 = _arg12 ∧ x13 = _arg13 ∧ x14 = _arg14 ∧ x15 = _arg15 ∧ x16 = _arg16 ∧ x17 = _arg17 ∧ x18 = _arg18 ∧ x19 = _arg19 ∧ x20 = _arg20 ∧ x21 = _arg21 ∧ x22 = _arg22 ∧ x23 = _arg23 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ x7 = _arg7P ∧ x8 = _arg8P ∧ x9 = _arg9P ∧ x10 = _arg10P ∧ x11 = _arg11P ∧ x12 = _arg12P ∧ x13 = _arg13P ∧ x14 = _arg14P ∧ x15 = _arg15P ∧ x16 = _arg16P ∧ x17 = _arg17P ∧ x18 = _arg18P ∧ x19 = _arg19P ∧ x20 = _arg20P ∧ x21 = _arg21P ∧ x22 = _arg22P ∧ x23 = _arg23P ∧ _arg7 = _arg21P ∧ _arg6 = _arg18P ∧ _arg5 = _arg17P ∧ _arg4 = _arg15P ∧ _arg3 = _arg14P ∧ _arg3 = _arg13P ∧ 0 = _arg9P ∧ 0 = _arg8P ∧ 0 = _arg7P ∧ _arg4 = _arg5P ∧ 0 = _arg4P ∧ 0 = _arg3P ∧ _arg1 = _arg1P ∧ _arg7 + 3 ≤ _arg2 ∧ _arg6 + 5 ≤ _arg2 ∧ 9 ≤ _arg2P − 1 ∧ 9 ≤ _arg2 − 1
  f423_0_createList_Return	2	f813_0_random_ArrayAccess:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ x8 = _x7 ∧ x9 = _x8 ∧ x10 = _x9 ∧ x11 = _x10 ∧ x12 = _x11 ∧ x13 = _x12 ∧ x14 = _x13 ∧ x15 = _x14 ∧ x16 = _x15 ∧ x17 = _x16 ∧ x18 = _x17 ∧ x19 = _x18 ∧ x20 = _x19 ∧ x21 = _x20 ∧ x22 = _x21 ∧ x23 = _x22 ∧ x1 = _x23 ∧ x2 = _x24 ∧ x3 = _x25 ∧ x4 = _x26 ∧ x5 = _x27 ∧ x6 = _x28 ∧ x7 = _x29 ∧ x8 = _x30 ∧ x9 = _x31 ∧ x10 = _x32 ∧ x11 = _x33 ∧ x12 = _x34 ∧ x13 = _x35 ∧ x14 = _x36 ∧ x15 = _x37 ∧ x16 = _x39 ∧ x17 = _x41 ∧ x18 = _x42 ∧ x19 = _x43 ∧ x20 = _x44 ∧ x21 = _x45 ∧ x22 = _x46 ∧ x23 = _x47 ∧ _x8 = _x30 ∧ _x5 = _x27 ∧ _x3 = _x25 ∧ _x2 = _x24 ∧ _x7 + 7 ≤ _x1 ∧ _x8 + 3 ≤ _x1 ∧ _x6 + 7 ≤ _x1 ∧ _x5 + 5 ≤ _x1 ∧ 6 ≤ _x23 − 1 ∧ 6 ≤ _x1 − 1 ∧ 0 ≤ _x − 1
  f1_0_main_Load	3	f813_0_random_ArrayAccess:		x1 = _x48 ∧ x2 = _x50 ∧ x3 = _x51 ∧ x4 = _x52 ∧ x5 = _x53 ∧ x6 = _x55 ∧ x7 = _x56 ∧ x8 = _x57 ∧ x9 = _x59 ∧ x10 = _x61 ∧ x11 = _x62 ∧ x12 = _x63 ∧ x13 = _x64 ∧ x14 = _x65 ∧ x15 = _x66 ∧ x16 = _x67 ∧ x17 = _x68 ∧ x18 = _x70 ∧ x19 = _x71 ∧ x20 = _x72 ∧ x21 = _x73 ∧ x22 = _x75 ∧ x23 = _x76 ∧ x1 = _x77 ∧ x2 = _x79 ∧ x3 = _x80 ∧ x4 = _x81 ∧ x5 = _x82 ∧ x6 = _x83 ∧ x7 = _x84 ∧ x8 = _x85 ∧ x9 = _x86 ∧ x10 = _x87 ∧ x11 = _x88 ∧ x12 = _x89 ∧ x13 = _x90 ∧ x14 = _x91 ∧ x15 = _x92 ∧ x16 = _x93 ∧ x17 = _x94 ∧ x18 = _x95 ∧ x19 = _x96 ∧ x20 = _x97 ∧ x21 = _x98 ∧ x22 = _x99 ∧ x23 = _x100 ∧ −1 ≤ _x101 − 1 ∧ 0 ≤ _x50 − 1 ∧ 0 ≤ _x48 − 1 ∧ 6 ≤ _x77 − 1 ∧ _x50 = _x81
  f813_0_random_ArrayAccess	4	f1099_0_entry_LE:		x1 = _x102 ∧ x2 = _x103 ∧ x3 = _x104 ∧ x4 = _x105 ∧ x5 = _x106 ∧ x6 = _x107 ∧ x7 = _x108 ∧ x8 = _x109 ∧ x9 = _x110 ∧ x10 = _x111 ∧ x11 = _x113 ∧ x12 = _x114 ∧ x13 = _x115 ∧ x14 = _x116 ∧ x15 = _x117 ∧ x16 = _x118 ∧ x17 = _x119 ∧ x18 = _x120 ∧ x19 = _x121 ∧ x20 = _x122 ∧ x21 = _x123 ∧ x22 = _x124 ∧ x23 = _x125 ∧ x1 = _x126 ∧ x2 = _x127 ∧ x3 = _x128 ∧ x4 = _x129 ∧ x5 = _x130 ∧ x6 = _x131 ∧ x7 = _x132 ∧ x8 = _x133 ∧ x9 = _x134 ∧ x10 = _x135 ∧ x11 = _x136 ∧ x12 = _x137 ∧ x13 = _x138 ∧ x14 = _x139 ∧ x15 = _x140 ∧ x16 = _x141 ∧ x17 = _x142 ∧ x18 = _x143 ∧ x19 = _x144 ∧ x20 = _x145 ∧ x21 = _x146 ∧ x22 = _x147 ∧ x23 = _x148 ∧ _x149 ≤ _x105 − 1 ∧ 0 ≤ _x149 − 1 ∧ −1 ≤ _x127 − 1 ∧ _x150 ≤ _x127 ∧ _x127 ≤ _x106 − 1 ∧ 6 ≤ _x102 − 1 ∧ _x106 + 5 ≤ _x102 ∧ _x107 + 7 ≤ _x102 ∧ _x109 + 3 ≤ _x102 ∧ _x108 + 7 ≤ _x102 ∧ _x106 = _x126 ∧ _x104 = _x128
  f1099_0_entry_LE	5	f1099_0_entry_LE:		x1 = _x151 ∧ x2 = _x152 ∧ x3 = _x154 ∧ x4 = _x155 ∧ x5 = _x156 ∧ x6 = _x157 ∧ x7 = _x158 ∧ x8 = _x159 ∧ x9 = _x160 ∧ x10 = _x161 ∧ x11 = _x162 ∧ x12 = _x163 ∧ x13 = _x164 ∧ x14 = _x165 ∧ x15 = _x166 ∧ x16 = _x167 ∧ x17 = _x168 ∧ x18 = _x169 ∧ x19 = _x170 ∧ x20 = _x171 ∧ x21 = _x172 ∧ x22 = _x173 ∧ x23 = _x174 ∧ x1 = _x175 ∧ x2 = _x176 ∧ x3 = _x177 ∧ x4 = _x178 ∧ x5 = _x179 ∧ x6 = _x180 ∧ x7 = _x181 ∧ x8 = _x182 ∧ x9 = _x183 ∧ x10 = _x184 ∧ x11 = _x185 ∧ x12 = _x186 ∧ x13 = _x187 ∧ x14 = _x188 ∧ x15 = _x189 ∧ x16 = _x190 ∧ x17 = _x191 ∧ x18 = _x192 ∧ x19 = _x193 ∧ x20 = _x194 ∧ x21 = _x195 ∧ x22 = _x196 ∧ x23 = _x197 ∧ −1 ≤ _x154 − 1 ∧ 0 ≤ _x198 − 1 ∧ _x198 ≤ _x154 − 1 ∧ _x152 ≤ _x151 − 1 ∧ _x198 ≤ _x177 − 1 ∧ _x151 − 1 = _x175 ∧ _x152 = _x176
  f1099_0_entry_LE	6	f1099_0_entry_LE:		x1 = _x199 ∧ x2 = _x200 ∧ x3 = _x201 ∧ x4 = _x202 ∧ x5 = _x203 ∧ x6 = _x204 ∧ x7 = _x205 ∧ x8 = _x206 ∧ x9 = _x207 ∧ x10 = _x208 ∧ x11 = _x209 ∧ x12 = _x210 ∧ x13 = _x211 ∧ x14 = _x212 ∧ x15 = _x213 ∧ x16 = _x214 ∧ x17 = _x215 ∧ x18 = _x216 ∧ x19 = _x217 ∧ x20 = _x218 ∧ x21 = _x219 ∧ x22 = _x220 ∧ x23 = _x221 ∧ x1 = _x222 ∧ x2 = _x223 ∧ x3 = _x224 ∧ x4 = _x225 ∧ x5 = _x226 ∧ x6 = _x227 ∧ x7 = _x228 ∧ x8 = _x229 ∧ x9 = _x230 ∧ x10 = _x231 ∧ x11 = _x232 ∧ x12 = _x233 ∧ x13 = _x234 ∧ x14 = _x235 ∧ x15 = _x236 ∧ x16 = _x237 ∧ x17 = _x238 ∧ x18 = _x239 ∧ x19 = _x240 ∧ x20 = _x241 ∧ x21 = _x242 ∧ x22 = _x243 ∧ x23 = _x244 ∧ _x200 ≤ _x199 − 1 ∧ _x245 ≤ _x201 − 1 ∧ −1 ≤ _x201 − 1 ∧ _x199 − 1 = _x222 ∧ _x200 = _x223 ∧ 1 = _x224
  f813_0_random_ArrayAccess	7	f1201_0_entry_GT:		x1 = _x246 ∧ x2 = _x247 ∧ x3 = _x248 ∧ x4 = _x249 ∧ x5 = _x250 ∧ x6 = _x251 ∧ x7 = _x252 ∧ x8 = _x253 ∧ x9 = _x254 ∧ x10 = _x255 ∧ x11 = _x256 ∧ x12 = _x257 ∧ x13 = _x258 ∧ x14 = _x259 ∧ x15 = _x260 ∧ x16 = _x261 ∧ x17 = _x262 ∧ x18 = _x263 ∧ x19 = _x264 ∧ x20 = _x265 ∧ x21 = _x266 ∧ x22 = _x267 ∧ x23 = _x268 ∧ x1 = _x269 ∧ x2 = _x270 ∧ x3 = _x271 ∧ x4 = _x272 ∧ x5 = _x273 ∧ x6 = _x274 ∧ x7 = _x275 ∧ x8 = _x276 ∧ x9 = _x277 ∧ x10 = _x278 ∧ x11 = _x279 ∧ x12 = _x280 ∧ x13 = _x281 ∧ x14 = _x282 ∧ x15 = _x283 ∧ x16 = _x284 ∧ x17 = _x285 ∧ x18 = _x286 ∧ x19 = _x287 ∧ x20 = _x288 ∧ x21 = _x289 ∧ x22 = _x290 ∧ x23 = _x291 ∧ _x292 ≤ _x249 − 1 ∧ 0 ≤ _x292 − 1 ∧ −1 ≤ _x270 − 1 ∧ _x270 ≤ _x293 − 1 ∧ _x270 ≤ _x250 − 1 ∧ 6 ≤ _x246 − 1 ∧ _x250 + 5 ≤ _x246 ∧ _x251 + 7 ≤ _x246 ∧ _x253 + 3 ≤ _x246 ∧ _x252 + 7 ≤ _x246 ∧ 0 = _x269 ∧ _x247 = _x271
  f1201_0_entry_GT	8	f1201_0_entry_GT:		x1 = _x294 ∧ x2 = _x295 ∧ x3 = _x296 ∧ x4 = _x297 ∧ x5 = _x298 ∧ x6 = _x299 ∧ x7 = _x300 ∧ x8 = _x301 ∧ x9 = _x302 ∧ x10 = _x303 ∧ x11 = _x304 ∧ x12 = _x305 ∧ x13 = _x306 ∧ x14 = _x307 ∧ x15 = _x308 ∧ x16 = _x309 ∧ x17 = _x310 ∧ x18 = _x311 ∧ x19 = _x312 ∧ x20 = _x313 ∧ x21 = _x314 ∧ x22 = _x315 ∧ x23 = _x316 ∧ x1 = _x317 ∧ x2 = _x318 ∧ x3 = _x319 ∧ x4 = _x320 ∧ x5 = _x321 ∧ x6 = _x322 ∧ x7 = _x323 ∧ x8 = _x324 ∧ x9 = _x325 ∧ x10 = _x326 ∧ x11 = _x327 ∧ x12 = _x328 ∧ x13 = _x329 ∧ x14 = _x330 ∧ x15 = _x331 ∧ x16 = _x332 ∧ x17 = _x333 ∧ x18 = _x334 ∧ x19 = _x335 ∧ x20 = _x336 ∧ x21 = _x337 ∧ x22 = _x338 ∧ x23 = _x339 ∧ −1 ≤ _x296 − 1 ∧ 0 ≤ _x340 − 1 ∧ _x340 ≤ _x296 − 1 ∧ _x294 ≤ _x295 ∧ _x340 ≤ _x319 − 1 ∧ _x294 + 1 = _x317 ∧ _x295 = _x318
  f1201_0_entry_GT	9	f1201_0_entry_GT:		x1 = _x341 ∧ x2 = _x342 ∧ x3 = _x343 ∧ x4 = _x344 ∧ x5 = _x345 ∧ x6 = _x346 ∧ x7 = _x347 ∧ x8 = _x348 ∧ x9 = _x349 ∧ x10 = _x350 ∧ x11 = _x351 ∧ x12 = _x352 ∧ x13 = _x353 ∧ x14 = _x354 ∧ x15 = _x355 ∧ x16 = _x356 ∧ x17 = _x357 ∧ x18 = _x358 ∧ x19 = _x359 ∧ x20 = _x360 ∧ x21 = _x361 ∧ x22 = _x362 ∧ x23 = _x363 ∧ x1 = _x364 ∧ x2 = _x365 ∧ x3 = _x366 ∧ x4 = _x367 ∧ x5 = _x368 ∧ x6 = _x369 ∧ x7 = _x370 ∧ x8 = _x371 ∧ x9 = _x372 ∧ x10 = _x373 ∧ x11 = _x374 ∧ x12 = _x375 ∧ x13 = _x376 ∧ x14 = _x377 ∧ x15 = _x378 ∧ x16 = _x379 ∧ x17 = _x380 ∧ x18 = _x381 ∧ x19 = _x382 ∧ x20 = _x383 ∧ x21 = _x384 ∧ x22 = _x385 ∧ x23 = _x386 ∧ _x341 ≤ _x342 ∧ _x387 ≤ _x343 − 1 ∧ −1 ≤ _x343 − 1 ∧ _x341 + 1 = _x364 ∧ _x342 = _x365 ∧ 1 = _x366
  f1_0_main_Load	10	f411_0_createList_Load:		x1 = _x388 ∧ x2 = _x389 ∧ x3 = _x390 ∧ x4 = _x391 ∧ x5 = _x392 ∧ x6 = _x393 ∧ x7 = _x394 ∧ x8 = _x395 ∧ x9 = _x396 ∧ x10 = _x397 ∧ x11 = _x398 ∧ x12 = _x399 ∧ x13 = _x400 ∧ x14 = _x401 ∧ x15 = _x402 ∧ x16 = _x403 ∧ x17 = _x404 ∧ x18 = _x405 ∧ x19 = _x406 ∧ x20 = _x407 ∧ x21 = _x408 ∧ x22 = _x409 ∧ x23 = _x410 ∧ x1 = _x411 ∧ x2 = _x412 ∧ x3 = _x413 ∧ x4 = _x414 ∧ x5 = _x415 ∧ x6 = _x416 ∧ x7 = _x417 ∧ x8 = _x418 ∧ x9 = _x419 ∧ x10 = _x420 ∧ x11 = _x421 ∧ x12 = _x422 ∧ x13 = _x423 ∧ x14 = _x424 ∧ x15 = _x425 ∧ x16 = _x426 ∧ x17 = _x427 ∧ x18 = _x428 ∧ x19 = _x429 ∧ x20 = _x430 ∧ x21 = _x431 ∧ x22 = _x432 ∧ x23 = _x433 ∧ 0 = _x417 ∧ 0 = _x416 ∧ 1 = _x415 ∧ 7 ≤ _x412 − 1 ∧ 0 ≤ _x388 − 1 ∧ _x412 − 7 ≤ _x388 ∧ 0 ≤ _x389 − 1 ∧ −1 ≤ _x411 − 1
  f787_0_createList_Load	11	f1228_0_createList_LE:		x1 = _x434 ∧ x2 = _x435 ∧ x3 = _x436 ∧ x4 = _x437 ∧ x5 = _x438 ∧ x6 = _x439 ∧ x7 = _x440 ∧ x8 = _x441 ∧ x9 = _x442 ∧ x10 = _x443 ∧ x11 = _x444 ∧ x12 = _x445 ∧ x13 = _x446 ∧ x14 = _x447 ∧ x15 = _x448 ∧ x16 = _x449 ∧ x17 = _x450 ∧ x18 = _x451 ∧ x19 = _x452 ∧ x20 = _x453 ∧ x21 = _x454 ∧ x22 = _x455 ∧ x23 = _x456 ∧ x1 = _x457 ∧ x2 = _x458 ∧ x3 = _x459 ∧ x4 = _x460 ∧ x5 = _x461 ∧ x6 = _x462 ∧ x7 = _x463 ∧ x8 = _x464 ∧ x9 = _x465 ∧ x10 = _x466 ∧ x11 = _x467 ∧ x12 = _x468 ∧ x13 = _x469 ∧ x14 = _x470 ∧ x15 = _x471 ∧ x16 = _x472 ∧ x17 = _x473 ∧ x18 = _x474 ∧ x19 = _x475 ∧ x20 = _x476 ∧ x21 = _x477 ∧ x22 = _x478 ∧ x23 = _x479 ∧ _x454 = _x479 ∧ _x451 = _x473 ∧ _x450 = _x472 ∧ _x448 = _x471 ∧ _x447 = _x470 ∧ _x446 = _x469 ∧ _x445 = _x468 ∧ _x442 = _x467 ∧ _x441 = _x466 ∧ _x440 = _x465 ∧ _x439 = _x464 ∧ _x436 = _x463 ∧ _x443 = _x462 ∧ _x444 = _x461 ∧ _x438 = _x460 ∧ _x437 = _x459 ∧ _x434 = _x458 ∧ _x454 + 3 ≤ _x435 ∧ _x453 + 9 ≤ _x435 ∧ _x452 + 9 ≤ _x435 ∧ _x451 + 5 ≤ _x435 ∧ 11 ≤ _x457 − 1 ∧ 11 ≤ _x435 − 1
  f1228_0_createList_LE	12	f1228_0_createList_LE:		x1 = _x480 ∧ x2 = _x481 ∧ x3 = _x482 ∧ x4 = _x483 ∧ x5 = _x484 ∧ x6 = _x485 ∧ x7 = _x486 ∧ x8 = _x487 ∧ x9 = _x488 ∧ x10 = _x489 ∧ x11 = _x490 ∧ x12 = _x491 ∧ x13 = _x492 ∧ x14 = _x493 ∧ x15 = _x494 ∧ x16 = _x495 ∧ x17 = _x496 ∧ x18 = _x497 ∧ x19 = _x498 ∧ x20 = _x499 ∧ x21 = _x500 ∧ x22 = _x501 ∧ x23 = _x502 ∧ x1 = _x503 ∧ x2 = _x504 ∧ x3 = _x505 ∧ x4 = _x506 ∧ x5 = _x507 ∧ x6 = _x508 ∧ x7 = _x509 ∧ x8 = _x510 ∧ x9 = _x511 ∧ x10 = _x512 ∧ x11 = _x513 ∧ x12 = _x514 ∧ x13 = _x515 ∧ x14 = _x516 ∧ x15 = _x517 ∧ x16 = _x518 ∧ x17 = _x519 ∧ x18 = _x520 ∧ x19 = _x521 ∧ x20 = _x522 ∧ x21 = _x523 ∧ x22 = _x524 ∧ x23 = _x525 ∧ 0 ≤ _x481 − 1 ∧ −1 ≤ _x526 − 1 ∧ 0 ≤ _x495 − 1 ∧ _x495 ≤ _x526 − 1 ∧ 0 ≤ _x483 − 1 ∧ 0 ≤ _x482 − 1 ∧ 0 ≤ _x486 − 1 ∧ 0 ≤ _x485 − 1 ∧ 0 ≤ _x484 − 1 ∧ 0 ≤ _x493 − 1 ∧ −1 ≤ _x527 − 1 ∧ 0 ≤ _x488 − 1 ∧ 0 ≤ _x491 − 1 ∧ 0 ≤ _x489 − 1 ∧ 0 ≤ _x494 − 1 ∧ 0 ≤ _x492 − 1 ∧ 0 ≤ _x490 − 1 ∧ 0 ≤ _x487 − 1 ∧ −1 ≤ _x502 − 1 ∧ −1 ≤ _x496 − 1 ∧ 11 ≤ _x480 − 1 ∧ 11 ≤ _x503 − 1 ∧ _x496 + 5 ≤ _x480 ∧ _x497 + 9 ≤ _x480 ∧ _x498 + 9 ≤ _x480 ∧ _x499 + 9 ≤ _x480 ∧ _x500 + 11 ≤ _x480 ∧ _x502 + 3 ≤ _x480 ∧ _x501 + 11 ≤ _x480 ∧ _x481 − 1 = _x504 ∧ _x482 = _x505 ∧ _x483 = _x506 ∧ _x495 + 1 = _x518 ∧ _x496 + 1 = _x519 ∧ _x502 + 1 = _x525
  __init	13	f1_0_main_Load:		x1 = _x528 ∧ x2 = _x529 ∧ x3 = _x530 ∧ x4 = _x531 ∧ x5 = _x532 ∧ x6 = _x533 ∧ x7 = _x534 ∧ x8 = _x535 ∧ x9 = _x536 ∧ x10 = _x537 ∧ x11 = _x538 ∧ x12 = _x539 ∧ x13 = _x540 ∧ x14 = _x541 ∧ x15 = _x542 ∧ x16 = _x543 ∧ x17 = _x544 ∧ x18 = _x545 ∧ x19 = _x546 ∧ x20 = _x547 ∧ x21 = _x548 ∧ x22 = _x549 ∧ x23 = _x550 ∧ x1 = _x551 ∧ x2 = _x552 ∧ x3 = _x553 ∧ x4 = _x554 ∧ x5 = _x555 ∧ x6 = _x556 ∧ x7 = _x557 ∧ x8 = _x558 ∧ x9 = _x559 ∧ x10 = _x560 ∧ x11 = _x561 ∧ x12 = _x562 ∧ x13 = _x563 ∧ x14 = _x564 ∧ x15 = _x565 ∧ x16 = _x566 ∧ x17 = _x567 ∧ x18 = _x568 ∧ x19 = _x569 ∧ x20 = _x570 ∧ x21 = _x571 ∧ x22 = _x572 ∧ x23 = _x573 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

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

2.1 SCC Subproblem 1/3

Here we consider the SCC { f1201_0_entry_GT }.

2.1.1 Transition Removal

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

2.1.2 Trivial Cooperation Program

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

2.2 SCC Subproblem 2/3

Here we consider the SCC { f1099_0_entry_LE }.

2.2.1 Transition Removal

We remove transitions 5, 6 using the following ranking functions, which are bounded by 0.

2.2.2 Trivial Cooperation Program

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

2.3 SCC Subproblem 3/3

Here we consider the SCC { f1228_0_createList_LE }.

2.3.1 Transition Removal

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

2.3.2 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 % (10 real / 0 unknown / 0 assumptions / 10 total proof steps)