LTS Termination Proof

by AProVE

Input

• Initial Location: f3543_0_random_ArrayAccess, f4196_0_put_NULL, f4179_0_removeEntryForKey_NULL, f609_0_createMap_Return, f4838_0_transfer_GE, f4304_0_put_EQ, f3465_0_createMap_LE, f4933_0_transfer_ArrayAccess, f4319_0_removeEntryForKey_EQ, f1_0_main_Load, __init
• Transitions: (pre-variables and post-variables)

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

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

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

2.1 SCC Subproblem 1/4

Here we consider the SCC { f3465_0_createMap_LE }.

2.1.1 Transition Removal

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

Here we consider the SCC { f4196_0_put_NULL, f4304_0_put_EQ }.

2.2.1 Transition Removal

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

Here we consider the SCC { f4838_0_transfer_GE, f4933_0_transfer_ArrayAccess }.

2.3.1 Transition Removal

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

2.3.2 Transition Removal

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

2.3.3 Transition Removal

We remove transitions 28, 26 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/4

Here we consider the SCC { f4179_0_removeEntryForKey_NULL, f4319_0_removeEntryForKey_EQ }.

2.4.1 Transition Removal

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

2.4.2 Transition Removal

We remove transitions 6, 7, 11, 12, 13, 9 using the following ranking functions, which are bounded by 0.

2.4.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 % (17 real / 0 unknown / 0 assumptions / 17 total proof steps)