LTS Termination Proof

by AProVE

Input

• Initial Location: f532_0_createMap_Return, f5950_0_nextEntry_GE, f5790_0_hasNext_NULL, f4279_0_createMap_LE, f5935_0_transfer_ArrayAccess, f4729_0__init__LE, f5797_0_transfer_GE, f4900_0_put_NULL, f1_0_main_Load, f4935_0__init__GE, __init, f5022_0_put_EQ
• Transitions: (pre-variables and post-variables)

  f1_0_main_Load	1	f4729_0__init__LE:		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 ∧ 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 ∧ −1 ≤ _x7 − 1 ∧ 0 ≤ _arg2 − 1 ∧ 0 ≤ _arg1 − 1 ∧ 5 ≤ _arg1P − 1 ∧ 3 ≤ _arg2P − 1 ∧ 0 = _arg3P
  f532_0_createMap_Return	2	f4729_0__init__LE:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ x8 = _x8 ∧ x9 = _x9 ∧ x10 = _x10 ∧ x11 = _x11 ∧ x12 = _x12 ∧ x13 = _x13 ∧ x1 = _x14 ∧ x2 = _x15 ∧ x3 = _x16 ∧ x4 = _x17 ∧ x5 = _x18 ∧ x6 = _x19 ∧ x7 = _x20 ∧ x8 = _x21 ∧ x9 = _x22 ∧ x10 = _x23 ∧ x11 = _x24 ∧ x12 = _x25 ∧ x13 = _x26 ∧ 12 = _x19 ∧ 16 = _x18 ∧ _x1 = _x17 ∧ 0 = _x16 ∧ 12 = _x3 ∧ 16 = _x2 ∧ _x1 + 3 ≤ _x ∧ 14 ≤ _x15 − 1 ∧ 16 ≤ _x14 − 1 ∧ 14 ≤ _x − 1 ∧ _x15 ≤ _x ∧ _x14 − 2 ≤ _x
  f4729_0__init__LE	3	f4935_0__init__GE:		x1 = _x27 ∧ x2 = _x28 ∧ x3 = _x29 ∧ x4 = _x30 ∧ x5 = _x31 ∧ x6 = _x32 ∧ x7 = _x33 ∧ x8 = _x34 ∧ x9 = _x35 ∧ x10 = _x36 ∧ x11 = _x37 ∧ x12 = _x38 ∧ x13 = _x39 ∧ x1 = _x40 ∧ x2 = _x41 ∧ x3 = _x42 ∧ x4 = _x43 ∧ x5 = _x44 ∧ x6 = _x45 ∧ x7 = _x46 ∧ x8 = _x47 ∧ x9 = _x48 ∧ x10 = _x49 ∧ x11 = _x50 ∧ x12 = _x51 ∧ x13 = _x52 ∧ _x31 = _x45 ∧ _x32 = _x44 ∧ _x30 = _x43 ∧ 0 = _x42 ∧ 0 = _x29 ∧ _x32 + 3 ≤ _x28 ∧ _x30 + 3 ≤ _x28 ∧ _x32 + 5 ≤ _x27 ∧ _x30 + 5 ≤ _x27 ∧ 0 ≤ _x41 − 1 ∧ 5 ≤ _x40 − 1 ∧ 3 ≤ _x28 − 1 ∧ 5 ≤ _x27 − 1 ∧ _x41 + 3 ≤ _x28 ∧ _x41 + 5 ≤ _x27 ∧ _x40 − 2 ≤ _x28 ∧ _x40 ≤ _x27 ∧ −1 ≤ _x31 − 1 ∧ 0 ≤ _x30 − 1
  f4935_0__init__GE	4	f4935_0__init__GE:		x1 = _x53 ∧ x2 = _x54 ∧ x3 = _x55 ∧ x4 = _x56 ∧ x5 = _x57 ∧ x6 = _x58 ∧ x7 = _x59 ∧ x8 = _x60 ∧ x9 = _x61 ∧ x10 = _x62 ∧ x11 = _x63 ∧ x12 = _x64 ∧ x13 = _x65 ∧ x1 = _x66 ∧ x2 = _x67 ∧ x3 = _x68 ∧ x4 = _x69 ∧ x5 = _x70 ∧ x6 = _x71 ∧ x7 = _x72 ∧ x8 = _x73 ∧ x9 = _x74 ∧ x10 = _x75 ∧ x11 = _x76 ∧ x12 = _x77 ∧ x13 = _x78 ∧ _x58 = _x71 ∧ _x57 = _x70 ∧ _x56 = _x69 ∧ _x55 + 1 = _x68 ∧ _x57 + 5 ≤ _x53 ∧ _x56 + 5 ≤ _x53 ∧ _x55 + 2 ≤ _x53 ∧ 0 ≤ _x67 − 1 ∧ 5 ≤ _x66 − 1 ∧ 0 ≤ _x54 − 1 ∧ 5 ≤ _x53 − 1 ∧ _x67 ≤ _x54 ∧ _x67 + 5 ≤ _x53 ∧ _x66 − 1 ≤ _x53 ∧ −1 ≤ _x58 − 1 ∧ −1 ≤ _x55 − 1 ∧ _x55 ≤ _x58 − 1
  f4935_0__init__GE	5	f5790_0_hasNext_NULL:		x1 = _x79 ∧ x2 = _x80 ∧ x3 = _x81 ∧ x4 = _x82 ∧ x5 = _x83 ∧ x6 = _x84 ∧ x7 = _x85 ∧ x8 = _x86 ∧ x9 = _x87 ∧ x10 = _x88 ∧ x11 = _x89 ∧ x12 = _x90 ∧ x13 = _x91 ∧ x1 = _x92 ∧ x2 = _x93 ∧ x3 = _x94 ∧ x4 = _x95 ∧ x5 = _x96 ∧ x6 = _x97 ∧ x7 = _x100 ∧ x8 = _x101 ∧ x9 = _x102 ∧ x10 = _x103 ∧ x11 = _x104 ∧ x12 = _x105 ∧ x13 = _x106 ∧ _x83 = _x97 ∧ _x84 = _x96 ∧ _x82 = _x95 ∧ _x81 = _x94 ∧ _x83 + 5 ≤ _x79 ∧ _x82 + 5 ≤ _x79 ∧ _x81 + 2 ≤ _x79 ∧ −1 ≤ _x93 − 1 ∧ 5 ≤ _x92 − 1 ∧ 0 ≤ _x80 − 1 ∧ 5 ≤ _x79 − 1 ∧ _x93 + 1 ≤ _x80 ∧ _x93 + 6 ≤ _x79 ∧ _x84 ≤ _x81 ∧ _x92 ≤ _x79
  f4935_0__init__GE	6	f5790_0_hasNext_NULL:		x1 = _x107 ∧ x2 = _x108 ∧ x3 = _x109 ∧ x4 = _x110 ∧ x5 = _x113 ∧ x6 = _x114 ∧ x7 = _x115 ∧ x8 = _x116 ∧ x9 = _x117 ∧ x10 = _x118 ∧ x11 = _x119 ∧ x12 = _x120 ∧ x13 = _x121 ∧ x1 = _x122 ∧ x2 = _x123 ∧ x3 = _x124 ∧ x4 = _x125 ∧ x5 = _x126 ∧ x6 = _x127 ∧ x7 = _x128 ∧ x8 = _x129 ∧ x9 = _x130 ∧ x10 = _x131 ∧ x11 = _x132 ∧ x12 = _x133 ∧ x13 = _x134 ∧ _x113 = _x127 ∧ _x114 = _x126 ∧ _x110 = _x125 ∧ _x109 + 1 = _x124 ∧ _x113 + 5 ≤ _x107 ∧ _x110 + 5 ≤ _x107 ∧ _x109 + 2 ≤ _x107 ∧ 0 ≤ _x123 − 1 ∧ 5 ≤ _x122 − 1 ∧ 0 ≤ _x108 − 1 ∧ 5 ≤ _x107 − 1 ∧ −1 ≤ _x109 − 1 ∧ _x109 ≤ _x114 − 1
  f5790_0_hasNext_NULL	7	f5950_0_nextEntry_GE:		x1 = _x135 ∧ x2 = _x136 ∧ x3 = _x137 ∧ x4 = _x138 ∧ x5 = _x139 ∧ x6 = _x140 ∧ x7 = _x141 ∧ x8 = _x142 ∧ x9 = _x143 ∧ x10 = _x144 ∧ x11 = _x145 ∧ x12 = _x146 ∧ x13 = _x147 ∧ x1 = _x148 ∧ x2 = _x149 ∧ x3 = _x151 ∧ x4 = _x152 ∧ x5 = _x153 ∧ x6 = _x154 ∧ x7 = _x155 ∧ x8 = _x156 ∧ x9 = _x157 ∧ x10 = _x158 ∧ x11 = _x159 ∧ x12 = _x160 ∧ x13 = _x161 ∧ _x139 = _x154 ∧ _x140 = _x153 ∧ _x138 = _x152 ∧ _x137 = _x151 ∧ _x140 + 5 ≤ _x135 ∧ _x138 + 5 ≤ _x135 ∧ _x137 + 2 ≤ _x135 ∧ 0 ≤ _x149 − 1 ∧ 5 ≤ _x148 − 1 ∧ 1 ≤ _x136 − 1 ∧ 5 ≤ _x135 − 1 ∧ _x149 + 1 ≤ _x136 ∧ _x149 + 5 ≤ _x135 ∧ −1 ≤ _x139 − 1 ∧ _x148 ≤ _x135
  f5790_0_hasNext_NULL	8	f5790_0_hasNext_NULL:		x1 = _x162 ∧ x2 = _x163 ∧ x3 = _x164 ∧ x4 = _x165 ∧ x5 = _x166 ∧ x6 = _x167 ∧ x7 = _x168 ∧ x8 = _x169 ∧ x9 = _x170 ∧ x10 = _x171 ∧ x11 = _x172 ∧ x12 = _x173 ∧ x13 = _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 ∧ _x167 = _x180 ∧ _x166 = _x179 ∧ _x165 = _x178 ∧ _x164 = _x177 ∧ _x167 + 5 ≤ _x162 ∧ _x165 + 5 ≤ _x162 ∧ _x164 + 2 ≤ _x162 ∧ 0 ≤ _x176 − 1 ∧ 5 ≤ _x175 − 1 ∧ 2 ≤ _x163 − 1 ∧ 5 ≤ _x162 − 1 ∧ _x176 + 2 ≤ _x163 ∧ _x176 + 4 ≤ _x162 ∧ _x175 ≤ _x162
  f5950_0_nextEntry_GE	9	f5790_0_hasNext_NULL:		x1 = _x188 ∧ x2 = _x189 ∧ x3 = _x190 ∧ x4 = _x191 ∧ x5 = _x192 ∧ x6 = _x193 ∧ x7 = _x194 ∧ x8 = _x195 ∧ x9 = _x196 ∧ x10 = _x197 ∧ x11 = _x198 ∧ x12 = _x199 ∧ x13 = _x200 ∧ x1 = _x201 ∧ x2 = _x202 ∧ x3 = _x203 ∧ x4 = _x204 ∧ x5 = _x205 ∧ x6 = _x206 ∧ x7 = _x207 ∧ x8 = _x208 ∧ x9 = _x209 ∧ x10 = _x210 ∧ x11 = _x211 ∧ x12 = _x212 ∧ x13 = _x213 ∧ _x192 = _x206 ∧ _x193 = _x205 ∧ _x191 = _x204 ∧ _x190 = _x203 ∧ _x192 + 5 ≤ _x188 ∧ _x191 + 5 ≤ _x188 ∧ _x190 + 2 ≤ _x188 ∧ −1 ≤ _x202 − 1 ∧ 5 ≤ _x201 − 1 ∧ 0 ≤ _x189 − 1 ∧ 5 ≤ _x188 − 1 ∧ _x202 + 1 ≤ _x189 ∧ _x202 + 6 ≤ _x188 ∧ _x193 ≤ _x190 ∧ _x201 ≤ _x188
  f5950_0_nextEntry_GE	10	f5950_0_nextEntry_GE:		x1 = _x214 ∧ x2 = _x215 ∧ x3 = _x216 ∧ x4 = _x217 ∧ x5 = _x218 ∧ x6 = _x219 ∧ x7 = _x220 ∧ x8 = _x221 ∧ x9 = _x222 ∧ x10 = _x223 ∧ x11 = _x224 ∧ x12 = _x225 ∧ x13 = _x226 ∧ x1 = _x227 ∧ x2 = _x228 ∧ x3 = _x229 ∧ x4 = _x230 ∧ x5 = _x231 ∧ x6 = _x232 ∧ x7 = _x233 ∧ x8 = _x234 ∧ x9 = _x235 ∧ x10 = _x236 ∧ x11 = _x237 ∧ x12 = _x238 ∧ x13 = _x239 ∧ _x219 = _x232 ∧ _x218 = _x231 ∧ _x217 = _x230 ∧ _x216 + 1 = _x229 ∧ _x218 + 5 ≤ _x214 ∧ _x217 + 5 ≤ _x214 ∧ _x216 + 2 ≤ _x214 ∧ 0 ≤ _x228 − 1 ∧ 5 ≤ _x227 − 1 ∧ 0 ≤ _x215 − 1 ∧ 5 ≤ _x214 − 1 ∧ _x228 ≤ _x215 ∧ _x228 + 5 ≤ _x214 ∧ _x227 − 1 ≤ _x214 ∧ _x216 ≤ _x219 − 1 ∧ −1 ≤ _x219 − 1
  f5950_0_nextEntry_GE	11	f5790_0_hasNext_NULL:		x1 = _x240 ∧ x2 = _x241 ∧ x3 = _x242 ∧ x4 = _x243 ∧ x5 = _x244 ∧ x6 = _x245 ∧ x7 = _x246 ∧ x8 = _x247 ∧ x9 = _x248 ∧ x10 = _x249 ∧ x11 = _x250 ∧ x12 = _x251 ∧ x13 = _x252 ∧ x1 = _x253 ∧ x2 = _x254 ∧ x3 = _x255 ∧ x4 = _x256 ∧ x5 = _x257 ∧ x6 = _x258 ∧ x7 = _x259 ∧ x8 = _x260 ∧ x9 = _x261 ∧ x10 = _x262 ∧ x11 = _x263 ∧ x12 = _x264 ∧ x13 = _x265 ∧ _x244 = _x258 ∧ _x245 = _x257 ∧ _x243 = _x256 ∧ _x242 + 1 = _x255 ∧ _x244 + 5 ≤ _x240 ∧ _x243 + 5 ≤ _x240 ∧ _x242 + 2 ≤ _x240 ∧ 0 ≤ _x254 − 1 ∧ 5 ≤ _x253 − 1 ∧ 0 ≤ _x241 − 1 ∧ _x242 ≤ _x245 − 1 ∧ 5 ≤ _x240 − 1
  f1_0_main_Load	12	f4279_0_createMap_LE:		x1 = _x266 ∧ x2 = _x267 ∧ x3 = _x268 ∧ x4 = _x269 ∧ x5 = _x270 ∧ x6 = _x271 ∧ x7 = _x272 ∧ x8 = _x273 ∧ x9 = _x274 ∧ x10 = _x275 ∧ x11 = _x276 ∧ x12 = _x277 ∧ x13 = _x278 ∧ x1 = _x279 ∧ x2 = _x280 ∧ x3 = _x281 ∧ x4 = _x282 ∧ x5 = _x283 ∧ x6 = _x284 ∧ x7 = _x286 ∧ x8 = _x287 ∧ x9 = _x288 ∧ x10 = _x289 ∧ x11 = _x290 ∧ x12 = _x291 ∧ x13 = _x292 ∧ 12 = _x286 ∧ 16 = _x284 ∧ 0 = _x283 ∧ 1 = _x282 ∧ _x267 = _x281 ∧ 14 ≤ _x279 − 1 ∧ 0 ≤ _x266 − 1 ∧ _x279 − 14 ≤ _x266 ∧ 0 ≤ _x267 − 1 ∧ −1 ≤ _x280 − 1
  f4279_0_createMap_LE	13	f4279_0_createMap_LE:		x1 = _x293 ∧ x2 = _x294 ∧ x3 = _x295 ∧ x4 = _x296 ∧ x5 = _x297 ∧ x6 = _x298 ∧ x7 = _x299 ∧ x8 = _x300 ∧ x9 = _x301 ∧ x10 = _x302 ∧ x11 = _x303 ∧ x12 = _x304 ∧ x13 = _x305 ∧ x1 = _x306 ∧ x2 = _x307 ∧ x3 = _x308 ∧ x4 = _x309 ∧ x5 = _x310 ∧ x6 = _x311 ∧ x7 = _x312 ∧ x8 = _x313 ∧ x9 = _x314 ∧ x10 = _x315 ∧ x11 = _x316 ∧ x12 = _x317 ∧ x13 = _x318 ∧ 0 ≤ _x294 − 1 ∧ _x296 + 1 ≤ _x295 − 1 ∧ −1 ≤ _x295 − 1 ∧ −1 ≤ _x296 − 1 ∧ −1 ≤ _x319 − 1 ∧ −1 ≤ _x320 − 1 ∧ 1 ≤ _x298 − 1 ∧ 3 ≤ _x293 − 1 ∧ 3 ≤ _x306 − 1 ∧ _x297 + 3 ≤ _x293 ∧ _x299 + 3 ≤ _x293 ∧ _x294 − 1 = _x307 ∧ _x295 = _x308 ∧ _x296 + 2 = _x309
  f4279_0_createMap_LE	14	f4900_0_put_NULL:		x1 = _x321 ∧ x2 = _x322 ∧ x3 = _x323 ∧ x4 = _x324 ∧ x5 = _x325 ∧ x6 = _x326 ∧ x7 = _x327 ∧ x8 = _x328 ∧ x9 = _x329 ∧ x10 = _x330 ∧ x11 = _x331 ∧ x12 = _x332 ∧ x13 = _x333 ∧ x1 = _x334 ∧ x2 = _x335 ∧ x3 = _x336 ∧ x4 = _x337 ∧ x5 = _x338 ∧ x6 = _x339 ∧ x7 = _x340 ∧ x8 = _x341 ∧ x9 = _x342 ∧ x10 = _x343 ∧ x11 = _x344 ∧ x12 = _x345 ∧ x13 = _x346 ∧ _x324 + 1 ≤ _x323 − 1 ∧ 1 ≤ _x326 − 1 ∧ 0 ≤ _x322 − 1 ∧ −1 ≤ _x323 − 1 ∧ −1 ≤ _x324 − 1 ∧ −1 ≤ _x347 − 1 ∧ −1 ≤ _x348 − 1 ∧ _x336 ≤ _x326 − 1 ∧ _x334 ≤ _x321 ∧ 3 ≤ _x321 − 1 ∧ 3 ≤ _x334 − 1 ∧ −1 ≤ _x337 − 1 ∧ _x325 + 3 ≤ _x321 ∧ _x327 + 3 ≤ _x321 ∧ _x323 = _x338 ∧ _x324 + 2 = _x339 ∧ _x325 = _x340 ∧ _x326 = _x341 ∧ _x327 = _x342
  f4900_0_put_NULL	15	f5022_0_put_EQ:		x1 = _x349 ∧ x2 = _x350 ∧ x3 = _x351 ∧ x4 = _x352 ∧ x5 = _x353 ∧ x6 = _x354 ∧ x7 = _x355 ∧ x8 = _x356 ∧ x9 = _x357 ∧ x10 = _x358 ∧ x11 = _x359 ∧ x12 = _x360 ∧ x13 = _x361 ∧ x1 = _x362 ∧ x2 = _x363 ∧ x3 = _x364 ∧ x4 = _x365 ∧ x5 = _x366 ∧ x6 = _x367 ∧ x7 = _x368 ∧ x8 = _x369 ∧ x9 = _x370 ∧ x10 = _x371 ∧ x11 = _x372 ∧ x12 = _x373 ∧ x13 = _x374 ∧ _x350 = _x371 ∧ _x357 = _x368 ∧ _x356 = _x367 ∧ _x355 = _x366 ∧ 0 = _x365 ∧ _x351 = _x363 ∧ _x370 + 4 ≤ _x352 ∧ _x350 + 2 ≤ _x352 ∧ _x357 + 3 ≤ _x349 ∧ _x355 + 3 ≤ _x349 ∧ −1 ≤ _x369 − 1 ∧ 2 ≤ _x364 − 1 ∧ 3 ≤ _x362 − 1 ∧ 2 ≤ _x352 − 1 ∧ 3 ≤ _x349 − 1 ∧ _x369 + 2 ≤ _x352 ∧ _x364 ≤ _x352 ∧ 1 ≤ _x356 − 1 ∧ _x362 ≤ _x349
  f4900_0_put_NULL	16	f5022_0_put_EQ:		x1 = _x375 ∧ x2 = _x376 ∧ x3 = _x377 ∧ x4 = _x378 ∧ x5 = _x379 ∧ x6 = _x380 ∧ x7 = _x381 ∧ x8 = _x382 ∧ x9 = _x383 ∧ x10 = _x384 ∧ x11 = _x385 ∧ x12 = _x386 ∧ x13 = _x387 ∧ 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 ∧ _x376 = _x397 ∧ _x383 = _x394 ∧ _x382 = _x393 ∧ _x381 = _x392 ∧ 1 = _x391 ∧ _x377 = _x389 ∧ _x396 + 4 ≤ _x378 ∧ _x376 + 2 ≤ _x378 ∧ _x383 + 3 ≤ _x375 ∧ _x381 + 3 ≤ _x375 ∧ −1 ≤ _x395 − 1 ∧ 2 ≤ _x390 − 1 ∧ 3 ≤ _x388 − 1 ∧ 2 ≤ _x378 − 1 ∧ 3 ≤ _x375 − 1 ∧ _x395 + 2 ≤ _x378 ∧ _x390 ≤ _x378 ∧ 1 ≤ _x382 − 1 ∧ _x388 ≤ _x375
  f4900_0_put_NULL	17	f4900_0_put_NULL:		x1 = _x401 ∧ x2 = _x402 ∧ x3 = _x403 ∧ x4 = _x404 ∧ x5 = _x405 ∧ x6 = _x406 ∧ x7 = _x407 ∧ x8 = _x408 ∧ x9 = _x409 ∧ x10 = _x410 ∧ x11 = _x411 ∧ x12 = _x412 ∧ x13 = _x413 ∧ x1 = _x414 ∧ x2 = _x415 ∧ x3 = _x416 ∧ x4 = _x417 ∧ x5 = _x418 ∧ x6 = _x419 ∧ x7 = _x420 ∧ x8 = _x421 ∧ x9 = _x422 ∧ x10 = _x423 ∧ x11 = _x424 ∧ x12 = _x425 ∧ x13 = _x426 ∧ _x414 ≤ _x401 ∧ _x427 ≤ _x402 − 1 ∧ _x417 + 1 ≤ _x404 ∧ 3 ≤ _x401 − 1 ∧ 0 ≤ _x404 − 1 ∧ 3 ≤ _x414 − 1 ∧ −1 ≤ _x417 − 1 ∧ _x407 + 3 ≤ _x401 ∧ _x409 + 3 ≤ _x401 ∧ _x402 = _x415 ∧ _x403 = _x416 ∧ _x405 = _x418 ∧ _x406 = _x419 ∧ _x407 = _x420 ∧ _x408 = _x421 ∧ _x409 = _x422
  f4900_0_put_NULL	18	f4900_0_put_NULL:		x1 = _x428 ∧ x2 = _x429 ∧ x3 = _x430 ∧ x4 = _x431 ∧ x5 = _x432 ∧ x6 = _x433 ∧ x7 = _x434 ∧ x8 = _x435 ∧ x9 = _x436 ∧ x10 = _x437 ∧ x11 = _x438 ∧ x12 = _x439 ∧ x13 = _x440 ∧ x1 = _x441 ∧ x2 = _x442 ∧ x3 = _x443 ∧ x4 = _x444 ∧ x5 = _x445 ∧ x6 = _x446 ∧ x7 = _x447 ∧ x8 = _x448 ∧ x9 = _x449 ∧ x10 = _x450 ∧ x11 = _x451 ∧ x12 = _x452 ∧ x13 = _x453 ∧ _x441 ≤ _x428 ∧ _x429 ≤ _x454 − 1 ∧ _x444 + 1 ≤ _x431 ∧ 3 ≤ _x428 − 1 ∧ 0 ≤ _x431 − 1 ∧ 3 ≤ _x441 − 1 ∧ −1 ≤ _x444 − 1 ∧ _x434 + 3 ≤ _x428 ∧ _x436 + 3 ≤ _x428 ∧ _x429 = _x442 ∧ _x430 = _x443 ∧ _x432 = _x445 ∧ _x433 = _x446 ∧ _x434 = _x447 ∧ _x435 = _x448 ∧ _x436 = _x449
  f4900_0_put_NULL	19	f4900_0_put_NULL:		x1 = _x455 ∧ x2 = _x456 ∧ x3 = _x457 ∧ x4 = _x458 ∧ x5 = _x459 ∧ x6 = _x460 ∧ x7 = _x461 ∧ x8 = _x462 ∧ x9 = _x463 ∧ x10 = _x464 ∧ x11 = _x465 ∧ x12 = _x466 ∧ x13 = _x467 ∧ x1 = _x468 ∧ x2 = _x469 ∧ x3 = _x470 ∧ x4 = _x471 ∧ x5 = _x472 ∧ x6 = _x473 ∧ x7 = _x474 ∧ x8 = _x475 ∧ x9 = _x476 ∧ x10 = _x477 ∧ x11 = _x478 ∧ x12 = _x479 ∧ x13 = _x480 ∧ _x463 = _x476 ∧ _x462 = _x475 ∧ _x461 = _x474 ∧ _x460 = _x473 ∧ _x459 = _x472 ∧ _x457 = _x470 ∧ _x456 = _x469 ∧ _x456 + 2 ≤ _x458 ∧ _x463 + 3 ≤ _x455 ∧ _x461 + 3 ≤ _x455 ∧ −1 ≤ _x471 − 1 ∧ 3 ≤ _x468 − 1 ∧ 1 ≤ _x458 − 1 ∧ 3 ≤ _x455 − 1 ∧ _x471 + 2 ≤ _x458 ∧ 1 ≤ _x462 − 1 ∧ _x468 ≤ _x455
  f4900_0_put_NULL	20	f4900_0_put_NULL:		x1 = _x481 ∧ x2 = _x482 ∧ x3 = _x483 ∧ x4 = _x484 ∧ x5 = _x485 ∧ x6 = _x486 ∧ x7 = _x487 ∧ x8 = _x488 ∧ x9 = _x489 ∧ x10 = _x490 ∧ x11 = _x491 ∧ x12 = _x492 ∧ x13 = _x493 ∧ x1 = _x494 ∧ x2 = _x495 ∧ x3 = _x496 ∧ x4 = _x497 ∧ x5 = _x498 ∧ x6 = _x499 ∧ x7 = _x500 ∧ x8 = _x501 ∧ x9 = _x502 ∧ x10 = _x503 ∧ x11 = _x504 ∧ x12 = _x505 ∧ x13 = _x506 ∧ _x489 = _x502 ∧ _x488 = _x501 ∧ _x487 = _x500 ∧ _x486 = _x499 ∧ _x485 = _x498 ∧ _x483 = _x496 ∧ _x482 = _x495 ∧ _x482 + 2 ≤ _x484 ∧ _x489 + 3 ≤ _x481 ∧ _x487 + 3 ≤ _x481 ∧ −1 ≤ _x497 − 1 ∧ 3 ≤ _x494 − 1 ∧ 2 ≤ _x484 − 1 ∧ 3 ≤ _x481 − 1 ∧ _x497 + 2 ≤ _x484 ∧ 1 ≤ _x488 − 1 ∧ _x494 ≤ _x481
  f5022_0_put_EQ	21	f4900_0_put_NULL:		x1 = _x507 ∧ x2 = _x508 ∧ x3 = _x509 ∧ x4 = _x510 ∧ x5 = _x511 ∧ x6 = _x512 ∧ x7 = _x513 ∧ x8 = _x514 ∧ x9 = _x515 ∧ x10 = _x516 ∧ x11 = _x517 ∧ x12 = _x518 ∧ x13 = _x519 ∧ x1 = _x520 ∧ x2 = _x521 ∧ x3 = _x522 ∧ x4 = _x523 ∧ x5 = _x524 ∧ x6 = _x525 ∧ x7 = _x526 ∧ x8 = _x527 ∧ x9 = _x528 ∧ x10 = _x529 ∧ x11 = _x530 ∧ x12 = _x531 ∧ x13 = _x532 ∧ _x513 = _x528 ∧ _x512 = _x527 ∧ _x511 = _x526 ∧ _x508 = _x522 ∧ _x516 = _x521 ∧ 0 = _x510 ∧ _x516 + 2 ≤ _x509 ∧ _x515 + 4 ≤ _x509 ∧ _x513 + 3 ≤ _x507 ∧ _x511 + 3 ≤ _x507 ∧ −1 ≤ _x523 − 1 ∧ 3 ≤ _x520 − 1 ∧ −1 ≤ _x514 − 1 ∧ 2 ≤ _x509 − 1 ∧ 3 ≤ _x507 − 1 ∧ _x523 ≤ _x514 ∧ _x523 + 2 ≤ _x509 ∧ _x520 ≤ _x507
  f4900_0_put_NULL	22	f5797_0_transfer_GE:		x1 = _x533 ∧ x2 = _x534 ∧ x3 = _x535 ∧ x4 = _x536 ∧ x5 = _x537 ∧ x6 = _x538 ∧ x7 = _x539 ∧ x8 = _x540 ∧ x9 = _x541 ∧ x10 = _x542 ∧ x11 = _x543 ∧ x12 = _x544 ∧ x13 = _x545 ∧ x1 = _x546 ∧ x2 = _x547 ∧ x3 = _x548 ∧ x4 = _x549 ∧ x5 = _x550 ∧ x6 = _x551 ∧ x7 = _x552 ∧ x8 = _x553 ∧ x9 = _x554 ∧ x10 = _x555 ∧ x11 = _x556 ∧ x12 = _x557 ∧ x13 = _x558 ∧ _x540 = _x553 ∧ 2⋅_x540 = _x552 ∧ _x541 = _x551 ∧ _x539 + 1 = _x550 ∧ 0 = _x549 ∧ _x541 + 3 ≤ _x533 ∧ _x539 + 3 ≤ _x533 ∧ 0 ≤ _x548 − 1 ∧ 0 ≤ _x547 − 1 ∧ 3 ≤ _x546 − 1 ∧ −1 ≤ _x536 − 1 ∧ 3 ≤ _x533 − 1 ∧ _x548 − 1 ≤ _x536 ∧ _x548 + 3 ≤ _x533 ∧ _x547 − 1 ≤ _x536 ∧ _x547 + 3 ≤ _x533 ∧ _x546 − 1 ≤ _x533 ∧ _x540 ≤ 1073741823 ∧ 0 ≤ 2⋅_x540 ∧ _x541 ≤ _x539 ∧ 1 ≤ _x540 − 1 ∧ _x535 ≤ _x540 − 1
  f4900_0_put_NULL	23	f5797_0_transfer_GE:		x1 = _x559 ∧ x2 = _x560 ∧ x3 = _x561 ∧ x4 = _x562 ∧ x5 = _x563 ∧ x6 = _x564 ∧ x7 = _x565 ∧ x8 = _x566 ∧ x9 = _x567 ∧ x10 = _x568 ∧ x11 = _x569 ∧ x12 = _x570 ∧ x13 = _x571 ∧ x1 = _x572 ∧ x2 = _x573 ∧ x3 = _x574 ∧ x4 = _x575 ∧ x5 = _x576 ∧ x6 = _x577 ∧ x7 = _x578 ∧ x8 = _x579 ∧ x9 = _x580 ∧ x10 = _x581 ∧ x11 = _x582 ∧ x12 = _x583 ∧ x13 = _x584 ∧ _x566 = _x579 ∧ 2⋅_x566 = _x578 ∧ _x567 = _x577 ∧ _x565 + 1 = _x576 ∧ 0 = _x575 ∧ _x567 + 3 ≤ _x559 ∧ _x565 + 3 ≤ _x559 ∧ 0 ≤ _x574 − 1 ∧ 0 ≤ _x573 − 1 ∧ 3 ≤ _x572 − 1 ∧ −1 ≤ _x562 − 1 ∧ 3 ≤ _x559 − 1 ∧ _x574 − 1 ≤ _x562 ∧ _x574 + 3 ≤ _x559 ∧ _x573 − 1 ≤ _x562 ∧ _x573 + 3 ≤ _x559 ∧ _x572 − 1 ≤ _x559 ∧ _x567 ≤ _x565 ∧ 0 ≤ 2⋅_x566 ∧ 1073741824 ≤ _x566 − 1 ∧ _x561 ≤ _x566 − 1
  f5797_0_transfer_GE	24	f5935_0_transfer_ArrayAccess:		x1 = _x585 ∧ x2 = _x586 ∧ x3 = _x587 ∧ x4 = _x588 ∧ x5 = _x589 ∧ x6 = _x590 ∧ x7 = _x591 ∧ x8 = _x592 ∧ x9 = _x593 ∧ x10 = _x594 ∧ x11 = _x595 ∧ x12 = _x596 ∧ x13 = _x597 ∧ x1 = _x598 ∧ x2 = _x599 ∧ x3 = _x600 ∧ x4 = _x601 ∧ x5 = _x602 ∧ x6 = _x603 ∧ x7 = _x604 ∧ x8 = _x605 ∧ x9 = _x606 ∧ x10 = _x607 ∧ x11 = _x608 ∧ x12 = _x609 ∧ x13 = _x610 ∧ _x591 = _x610 ∧ _x592 = _x607 ∧ _x590 = _x606 ∧ _x589 = _x605 ∧ _x588 = _x600 ∧ _x590 + 3 ≤ _x585 ∧ _x589 + 3 ≤ _x585 ∧ 0 ≤ _x603 − 1 ∧ 0 ≤ _x602 − 1 ∧ −1 ≤ _x601 − 1 ∧ 0 ≤ _x599 − 1 ∧ 3 ≤ _x598 − 1 ∧ 0 ≤ _x587 − 1 ∧ 0 ≤ _x586 − 1 ∧ 3 ≤ _x585 − 1 ∧ _x603 ≤ _x587 ∧ _x603 ≤ _x586 ∧ _x603 + 3 ≤ _x585 ∧ _x599 ≤ _x587 ∧ _x599 ≤ _x586 ∧ _x599 + 3 ≤ _x585 ∧ _x598 ≤ _x585 ∧ _x588 ≤ _x592 − 1 ∧ 0 ≤ _x591 − 1
  f5935_0_transfer_ArrayAccess	25	f5935_0_transfer_ArrayAccess:		x1 = _x611 ∧ x2 = _x612 ∧ x3 = _x613 ∧ x4 = _x614 ∧ x5 = _x615 ∧ x6 = _x616 ∧ x7 = _x617 ∧ x8 = _x618 ∧ x9 = _x619 ∧ x10 = _x620 ∧ x11 = _x621 ∧ x12 = _x622 ∧ x13 = _x623 ∧ x1 = _x624 ∧ x2 = _x625 ∧ x3 = _x626 ∧ x4 = _x627 ∧ x5 = _x628 ∧ x6 = _x629 ∧ x7 = _x630 ∧ x8 = _x631 ∧ x9 = _x632 ∧ x10 = _x633 ∧ x11 = _x634 ∧ x12 = _x635 ∧ x13 = _x636 ∧ _x623 = _x636 ∧ _x620 = _x633 ∧ _x619 = _x632 ∧ _x618 = _x631 ∧ _x613 = _x626 ∧ _x622 + 2 ≤ _x615 ∧ _x621 + 2 ≤ _x615 ∧ _x635 + 4 ≤ _x615 ∧ _x634 + 4 ≤ _x615 ∧ _x635 + 2 ≤ _x614 ∧ _x634 + 2 ≤ _x614 ∧ _x619 + 3 ≤ _x611 ∧ _x618 + 3 ≤ _x611 ∧ 0 ≤ _x629 − 1 ∧ 0 ≤ _x628 − 1 ∧ −1 ≤ _x627 − 1 ∧ 0 ≤ _x625 − 1 ∧ 3 ≤ _x624 − 1 ∧ 0 ≤ _x616 − 1 ∧ 2 ≤ _x615 − 1 ∧ 0 ≤ _x614 − 1 ∧ 0 ≤ _x612 − 1 ∧ 3 ≤ _x611 − 1 ∧ _x629 ≤ _x616 ∧ _x629 + 2 ≤ _x615 ∧ _x629 ≤ _x614 ∧ _x629 ≤ _x612 ∧ _x629 + 3 ≤ _x611 ∧ _x628 + 2 ≤ _x615 ∧ _x628 ≤ _x614 ∧ _x627 + 3 ≤ _x615 ∧ _x627 + 1 ≤ _x614 ∧ _x625 ≤ _x616 ∧ _x625 + 2 ≤ _x615 ∧ _x625 ≤ _x614 ∧ _x625 ≤ _x612 ∧ _x625 + 3 ≤ _x611 ∧ _x624 ≤ _x611 ∧ 0 ≤ _x623 − 1 ∧ _x617 ≤ _x623 − 1
  f5797_0_transfer_GE	26	f5797_0_transfer_GE:		x1 = _x637 ∧ x2 = _x638 ∧ x3 = _x639 ∧ x4 = _x640 ∧ x5 = _x641 ∧ x6 = _x642 ∧ x7 = _x643 ∧ x8 = _x644 ∧ x9 = _x645 ∧ x10 = _x646 ∧ x11 = _x647 ∧ x12 = _x648 ∧ x13 = _x649 ∧ x1 = _x650 ∧ x2 = _x651 ∧ x3 = _x652 ∧ x4 = _x653 ∧ x5 = _x654 ∧ x6 = _x655 ∧ x7 = _x656 ∧ x8 = _x657 ∧ x9 = _x658 ∧ x10 = _x659 ∧ x11 = _x660 ∧ x12 = _x661 ∧ x13 = _x662 ∧ _x644 = _x657 ∧ _x643 = _x656 ∧ _x642 = _x655 ∧ _x641 = _x654 ∧ _x640 + 1 = _x653 ∧ _x642 + 3 ≤ _x637 ∧ _x641 + 3 ≤ _x637 ∧ 0 ≤ _x652 − 1 ∧ 0 ≤ _x651 − 1 ∧ 3 ≤ _x650 − 1 ∧ 0 ≤ _x639 − 1 ∧ 0 ≤ _x638 − 1 ∧ 3 ≤ _x637 − 1 ∧ _x652 ≤ _x639 ∧ _x652 ≤ _x638 ∧ _x652 + 3 ≤ _x637 ∧ _x651 ≤ _x639 ∧ _x651 ≤ _x638 ∧ _x651 + 3 ≤ _x637 ∧ _x650 ≤ _x637 ∧ _x640 ≤ _x644 − 1 ∧ −1 ≤ _x644 − 1
  f5935_0_transfer_ArrayAccess	27	f5797_0_transfer_GE:		x1 = _x663 ∧ x2 = _x664 ∧ x3 = _x665 ∧ x4 = _x666 ∧ x5 = _x667 ∧ x6 = _x668 ∧ x7 = _x669 ∧ x8 = _x670 ∧ x9 = _x671 ∧ x10 = _x672 ∧ x11 = _x673 ∧ x12 = _x674 ∧ x13 = _x675 ∧ x1 = _x676 ∧ x2 = _x677 ∧ x3 = _x678 ∧ x4 = _x679 ∧ x5 = _x680 ∧ x6 = _x681 ∧ x7 = _x682 ∧ x8 = _x683 ∧ x9 = _x684 ∧ x10 = _x685 ∧ x11 = _x686 ∧ x12 = _x687 ∧ x13 = _x688 ∧ _x672 = _x683 ∧ _x675 = _x682 ∧ _x671 = _x681 ∧ _x670 = _x680 ∧ _x665 + 1 = _x679 ∧ _x674 + 2 ≤ _x667 ∧ _x673 + 2 ≤ _x667 ∧ _x671 + 3 ≤ _x663 ∧ _x670 + 3 ≤ _x663 ∧ 0 ≤ _x678 − 1 ∧ 0 ≤ _x677 − 1 ∧ 3 ≤ _x676 − 1 ∧ 0 ≤ _x668 − 1 ∧ 1 ≤ _x667 − 1 ∧ −1 ≤ _x666 − 1 ∧ 0 ≤ _x664 − 1 ∧ 3 ≤ _x663 − 1 ∧ _x678 ≤ _x668 ∧ _x678 + 1 ≤ _x667 ∧ _x678 − 1 ≤ _x666 ∧ _x678 ≤ _x664 ∧ _x678 + 3 ≤ _x663 ∧ _x677 ≤ _x668 ∧ _x677 + 1 ≤ _x667 ∧ _x677 − 1 ≤ _x666 ∧ _x677 ≤ _x664 ∧ _x677 + 3 ≤ _x663 ∧ _x676 ≤ _x663 ∧ _x669 ≤ _x675 − 1 ∧ −1 ≤ _x672 − 1
  __init	28	f1_0_main_Load:		x1 = _x689 ∧ x2 = _x690 ∧ x3 = _x691 ∧ x4 = _x692 ∧ x5 = _x693 ∧ x6 = _x694 ∧ x7 = _x695 ∧ x8 = _x696 ∧ x9 = _x697 ∧ x10 = _x698 ∧ x11 = _x699 ∧ x12 = _x700 ∧ x13 = _x701 ∧ x1 = _x702 ∧ x2 = _x703 ∧ x3 = _x704 ∧ x4 = _x705 ∧ x5 = _x706 ∧ x6 = _x707 ∧ x7 = _x708 ∧ x8 = _x709 ∧ x9 = _x710 ∧ x10 = _x711 ∧ x11 = _x712 ∧ x12 = _x713 ∧ x13 = _x714 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

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

2.1 SCC Subproblem 1/5

Here we consider the SCC { f4279_0_createMap_LE }.

2.1.1 Transition Removal

We remove transition 13 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/5

Here we consider the SCC { f4900_0_put_NULL, f5022_0_put_EQ }.

2.2.1 Transition Removal

We remove transitions 15, 17, 18, 19, 20, 21, 16 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/5

Here we consider the SCC { f5935_0_transfer_ArrayAccess, f5797_0_transfer_GE }.

2.3.1 Transition Removal

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

2.3.2 Transition Removal

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

2.3.3 Transition Removal

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

2.3.4 Trivial Cooperation Program

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

2.4 SCC Subproblem 4/5

Here we consider the SCC { f4935_0__init__GE }.

2.4.1 Transition Removal

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

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/5

Here we consider the SCC { f5950_0_nextEntry_GE, f5790_0_hasNext_NULL }.

2.5.1 Transition Removal

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

2.5.2 Transition Removal

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

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