LTS Termination Proof

by AProVE

Input

• Initial Location: f2521_0_main_InvokeMethod, f701_0_createTree_Return, f355_0_createTree_Return, f845_0_alternate_NONNULL, f1242_0_alternate_InvokeMethod, f2589_0_main_InvokeMethod, f2712_0_createTree_LE, f702_0_createTree_Return, f2530_0_main_InvokeMethod, f2504_0_createTree_LE, f756_0_copy_NONNULL, f61_0_createTree_Return, f252_0_main_InvokeMethod, __init, f2588_0_createTree_NONNULL, f1172_0_createNode_Return, f741_0_random_GT, f2671_0_createTree_FieldAccess, f2777_0_createTree_FieldAccess, f1247_0_copy_InvokeMethod, f875_0_createTree_NE, f1_0_main_Load
• Transitions: (pre-variables and post-variables)

  f1_0_main_Load	1	f252_0_main_InvokeMethod:		x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x7 = _arg7 ∧ x8 = _arg8 ∧ x9 = _arg9 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ x7 = _arg7P ∧ x8 = _arg8P ∧ x9 = _arg9P ∧ 0 = _arg2P ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ _arg1P ≤ _arg1
  f1_0_main_Load	2	f252_0_main_InvokeMethod:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ x8 = _x7 ∧ x9 = _x8 ∧ x1 = _x9 ∧ x2 = _x10 ∧ x3 = _x11 ∧ x4 = _x12 ∧ x5 = _x13 ∧ x6 = _x14 ∧ x7 = _x15 ∧ x8 = _x16 ∧ x9 = _x17 ∧ 0 ≤ _x9 − 1 ∧ 0 ≤ _x − 1 ∧ _x9 ≤ _x
  f61_0_createTree_Return	3	f252_0_main_InvokeMethod:		x1 = _x18 ∧ x2 = _x19 ∧ x3 = _x20 ∧ x4 = _x21 ∧ x5 = _x22 ∧ x6 = _x23 ∧ x7 = _x24 ∧ x8 = _x25 ∧ x9 = _x26 ∧ x1 = _x27 ∧ x2 = _x28 ∧ x3 = _x29 ∧ x4 = _x30 ∧ x5 = _x31 ∧ x6 = _x32 ∧ x7 = _x33 ∧ x8 = _x34 ∧ x9 = _x35 ∧ 0 = _x28 ∧ 0 ≤ _x27 − 1
  f252_0_main_InvokeMethod	4	f355_0_createTree_Return:		x1 = _x36 ∧ x2 = _x37 ∧ x3 = _x38 ∧ x4 = _x39 ∧ x5 = _x40 ∧ x6 = _x41 ∧ x7 = _x42 ∧ x8 = _x43 ∧ x9 = _x44 ∧ x1 = _x45 ∧ x2 = _x46 ∧ x3 = _x47 ∧ x4 = _x48 ∧ x5 = _x49 ∧ x6 = _x50 ∧ x7 = _x51 ∧ x8 = _x52 ∧ x9 = _x53 ∧ 0 ≤ _x45 − 1 ∧ 0 ≤ _x36 − 1 ∧ _x45 ≤ _x36
  f355_0_createTree_Return	5	f845_0_alternate_NONNULL:		x1 = _x54 ∧ x2 = _x55 ∧ x3 = _x56 ∧ x4 = _x57 ∧ x5 = _x58 ∧ x6 = _x59 ∧ x7 = _x60 ∧ x8 = _x61 ∧ x9 = _x62 ∧ x1 = _x63 ∧ x2 = _x64 ∧ x3 = _x65 ∧ x4 = _x66 ∧ x5 = _x67 ∧ x6 = _x68 ∧ x7 = _x69 ∧ x8 = _x70 ∧ x9 = _x71 ∧ −1 ≤ _x66 − 1 ∧ −1 ≤ _x65 − 1 ∧ −1 ≤ _x64 − 1 ∧ −1 ≤ _x63 − 1 ∧ 0 ≤ _x54 − 1 ∧ _x66 + 1 ≤ _x54 ∧ _x65 + 1 ≤ _x54 ∧ _x64 + 1 ≤ _x54 ∧ _x63 + 1 ≤ _x54
  f1_0_main_Load	6	f2521_0_main_InvokeMethod:		x1 = _x72 ∧ x2 = _x73 ∧ x3 = _x74 ∧ x4 = _x75 ∧ x5 = _x76 ∧ x6 = _x77 ∧ x7 = _x78 ∧ x8 = _x80 ∧ x9 = _x81 ∧ x1 = _x83 ∧ x2 = _x84 ∧ x3 = _x85 ∧ x4 = _x86 ∧ x5 = _x87 ∧ x6 = _x89 ∧ x7 = _x91 ∧ x8 = _x92 ∧ x9 = _x93 ∧ 0 ≤ _x84 − 1 ∧ 0 ≤ _x83 − 1 ∧ 0 ≤ _x72 − 1 ∧ _x83 ≤ _x72
  f701_0_createTree_Return	7	f2521_0_main_InvokeMethod:		x1 = _x94 ∧ x2 = _x95 ∧ x3 = _x96 ∧ x4 = _x97 ∧ x5 = _x98 ∧ x6 = _x99 ∧ x7 = _x100 ∧ x8 = _x101 ∧ x9 = _x102 ∧ x1 = _x103 ∧ x2 = _x104 ∧ x3 = _x105 ∧ x4 = _x106 ∧ x5 = _x107 ∧ x6 = _x108 ∧ x7 = _x109 ∧ x8 = _x110 ∧ x9 = _x111 ∧ _x97 = _x106 ∧ _x96 = _x105 ∧ _x97 + 2 ≤ _x95 ∧ 1 ≤ _x104 − 1 ∧ 0 ≤ _x103 − 1 ∧ 1 ≤ _x95 − 1 ∧ 0 ≤ _x94 − 1 ∧ _x104 ≤ _x95 ∧ _x103 + 1 ≤ _x95 ∧ _x103 ≤ _x94
  f252_0_main_InvokeMethod	8	f2530_0_main_InvokeMethod:		x1 = _x112 ∧ x2 = _x113 ∧ x3 = _x114 ∧ x4 = _x115 ∧ x5 = _x116 ∧ x6 = _x117 ∧ x7 = _x118 ∧ x8 = _x119 ∧ x9 = _x120 ∧ x1 = _x121 ∧ x2 = _x122 ∧ x3 = _x123 ∧ x4 = _x124 ∧ x5 = _x125 ∧ x6 = _x126 ∧ x7 = _x127 ∧ x8 = _x128 ∧ x9 = _x129 ∧ 0 ≤ _x122 − 1 ∧ 0 ≤ _x121 − 1 ∧ 0 ≤ _x112 − 1 ∧ _x121 ≤ _x112
  f702_0_createTree_Return	9	f2530_0_main_InvokeMethod:		x1 = _x130 ∧ x2 = _x131 ∧ x3 = _x132 ∧ x4 = _x133 ∧ x5 = _x134 ∧ x6 = _x135 ∧ x7 = _x136 ∧ x8 = _x137 ∧ x9 = _x138 ∧ x1 = _x139 ∧ x2 = _x140 ∧ x3 = _x141 ∧ x4 = _x142 ∧ x5 = _x143 ∧ x6 = _x144 ∧ x7 = _x145 ∧ x8 = _x146 ∧ x9 = _x147 ∧ _x132 = _x141 ∧ _x132 + 2 ≤ _x131 ∧ 1 ≤ _x140 − 1 ∧ 0 ≤ _x139 − 1 ∧ 1 ≤ _x131 − 1 ∧ 0 ≤ _x130 − 1 ∧ _x140 ≤ _x131 ∧ _x139 + 1 ≤ _x131 ∧ _x139 ≤ _x130
  f2530_0_main_InvokeMethod	10	f845_0_alternate_NONNULL:		x1 = _x148 ∧ x2 = _x149 ∧ x3 = _x150 ∧ x4 = _x151 ∧ x5 = _x152 ∧ x6 = _x153 ∧ x7 = _x154 ∧ x8 = _x155 ∧ x9 = _x156 ∧ x1 = _x157 ∧ x2 = _x158 ∧ x3 = _x159 ∧ x4 = _x160 ∧ x5 = _x161 ∧ x6 = _x162 ∧ x7 = _x163 ∧ x8 = _x164 ∧ x9 = _x165 ∧ _x150 + 2 ≤ _x149 ∧ −1 ≤ _x160 − 1 ∧ 0 ≤ _x159 − 1 ∧ −1 ≤ _x158 − 1 ∧ −1 ≤ _x157 − 1 ∧ 0 ≤ _x149 − 1 ∧ 0 ≤ _x148 − 1 ∧ _x160 + 1 ≤ _x149 ∧ _x160 + 1 ≤ _x148 ∧ _x159 ≤ _x149 ∧ _x158 + 1 ≤ _x149 ∧ _x158 + 1 ≤ _x148 ∧ _x157 + 1 ≤ _x149 ∧ _x157 + 1 ≤ _x148
  f2521_0_main_InvokeMethod	11	f2589_0_main_InvokeMethod:		x1 = _x166 ∧ x2 = _x167 ∧ x3 = _x168 ∧ x4 = _x169 ∧ x5 = _x170 ∧ x6 = _x171 ∧ x7 = _x172 ∧ x8 = _x173 ∧ x9 = _x174 ∧ x1 = _x175 ∧ x2 = _x176 ∧ x3 = _x177 ∧ x4 = _x178 ∧ x5 = _x179 ∧ x6 = _x180 ∧ x7 = _x181 ∧ x8 = _x182 ∧ x9 = _x183 ∧ _x169 = _x177 ∧ _x169 + 2 ≤ _x167 ∧ _x178 + 2 ≤ _x167 ∧ 0 ≤ _x176 − 1 ∧ 0 ≤ _x175 − 1 ∧ 0 ≤ _x167 − 1 ∧ 0 ≤ _x166 − 1 ∧ _x176 ≤ _x167 ∧ _x175 ≤ _x167 ∧ _x175 ≤ _x166
  f2589_0_main_InvokeMethod	12	f845_0_alternate_NONNULL:		x1 = _x184 ∧ x2 = _x185 ∧ x3 = _x186 ∧ x4 = _x187 ∧ x5 = _x188 ∧ x6 = _x189 ∧ x7 = _x190 ∧ x8 = _x191 ∧ x9 = _x192 ∧ x1 = _x193 ∧ x2 = _x194 ∧ x3 = _x195 ∧ x4 = _x196 ∧ x5 = _x197 ∧ x6 = _x198 ∧ x7 = _x199 ∧ x8 = _x200 ∧ x9 = _x201 ∧ _x186 + 2 ≤ _x185 ∧ _x187 + 2 ≤ _x185 ∧ 0 ≤ _x196 − 1 ∧ −1 ≤ _x195 − 1 ∧ 0 ≤ _x194 − 1 ∧ 0 ≤ _x193 − 1 ∧ 0 ≤ _x185 − 1 ∧ 0 ≤ _x184 − 1 ∧ _x196 ≤ _x185 ∧ _x195 + 1 ≤ _x185 ∧ _x195 + 1 ≤ _x184 ∧ _x194 ≤ _x185 ∧ _x193 ≤ _x185
  f2521_0_main_InvokeMethod	13	f845_0_alternate_NONNULL:		x1 = _x202 ∧ x2 = _x203 ∧ x3 = _x204 ∧ x4 = _x205 ∧ x5 = _x206 ∧ x6 = _x207 ∧ x7 = _x208 ∧ x8 = _x209 ∧ x9 = _x210 ∧ x1 = _x211 ∧ x2 = _x212 ∧ x3 = _x213 ∧ x4 = _x214 ∧ x5 = _x215 ∧ x6 = _x216 ∧ x7 = _x217 ∧ x8 = _x218 ∧ x9 = _x219 ∧ _x205 + 2 ≤ _x203 ∧ 0 ≤ _x214 − 1 ∧ 0 ≤ _x213 − 1 ∧ 0 ≤ _x212 − 1 ∧ 0 ≤ _x211 − 1 ∧ 0 ≤ _x203 − 1 ∧ 0 ≤ _x202 − 1 ∧ _x214 ≤ _x203 ∧ _x212 ≤ _x203 ∧ _x211 ≤ _x203
  f1_0_main_Load	14	f741_0_random_GT:		x1 = _x220 ∧ x2 = _x221 ∧ x3 = _x222 ∧ x4 = _x223 ∧ x5 = _x224 ∧ x6 = _x225 ∧ x7 = _x226 ∧ x8 = _x227 ∧ x9 = _x228 ∧ x1 = _x229 ∧ x2 = _x230 ∧ x3 = _x231 ∧ x4 = _x232 ∧ x5 = _x233 ∧ x6 = _x234 ∧ x7 = _x235 ∧ x8 = _x236 ∧ x9 = _x237 ∧ −1 ≤ _x221 − 1 ∧ 0 ≤ _x220 − 1
  f252_0_main_InvokeMethod	15	f741_0_random_GT:		x1 = _x238 ∧ x2 = _x239 ∧ x3 = _x240 ∧ x4 = _x241 ∧ x5 = _x242 ∧ x6 = _x243 ∧ x7 = _x244 ∧ x8 = _x245 ∧ x9 = _x246 ∧ x1 = _x247 ∧ x2 = _x248 ∧ x3 = _x249 ∧ x4 = _x250 ∧ x5 = _x251 ∧ x6 = _x252 ∧ x7 = _x253 ∧ x8 = _x254 ∧ x9 = _x255 ∧ 0 ≤ _x238 − 1 ∧ −1 ≤ _x256 − 1
  f2521_0_main_InvokeMethod	16	f741_0_random_GT:		x1 = _x257 ∧ x2 = _x258 ∧ x3 = _x259 ∧ x4 = _x260 ∧ x5 = _x261 ∧ x6 = _x262 ∧ x7 = _x263 ∧ x8 = _x264 ∧ x9 = _x265 ∧ x1 = _x266 ∧ x2 = _x267 ∧ x3 = _x268 ∧ x4 = _x269 ∧ x5 = _x270 ∧ x6 = _x271 ∧ x7 = _x272 ∧ x8 = _x273 ∧ x9 = _x274 ∧ 0 ≤ _x257 − 1 ∧ −1 ≤ _x275 − 1 ∧ 0 ≤ _x258 − 1 ∧ _x260 + 2 ≤ _x258
  f741_0_random_GT	17	f875_0_createTree_NE:		x1 = _x276 ∧ x2 = _x277 ∧ x3 = _x278 ∧ x4 = _x279 ∧ x5 = _x280 ∧ x6 = _x281 ∧ x7 = _x282 ∧ x8 = _x283 ∧ x9 = _x284 ∧ x1 = _x285 ∧ x2 = _x286 ∧ x3 = _x287 ∧ x4 = _x288 ∧ x5 = _x289 ∧ x6 = _x290 ∧ x7 = _x291 ∧ x8 = _x292 ∧ x9 = _x293 ∧ −1 ≤ _x294 − 1 ∧ _x294 ≤ _x286 − 1 ∧ 0 = _x285 ∧ _x294 + 1 = _x287
  f741_0_random_GT	18	f875_0_createTree_NE:		x1 = _x295 ∧ x2 = _x296 ∧ x3 = _x297 ∧ x4 = _x298 ∧ x5 = _x299 ∧ x6 = _x300 ∧ x7 = _x301 ∧ x8 = _x302 ∧ x9 = _x303 ∧ x1 = _x304 ∧ x2 = _x305 ∧ x3 = _x306 ∧ x4 = _x307 ∧ x5 = _x308 ∧ x6 = _x309 ∧ x7 = _x310 ∧ x8 = _x311 ∧ x9 = _x312 ∧ _x313 ≤ _x305 − 1 ∧ −1 ≤ _x304 − 1 ∧ −1 ≤ _x313 − 1 ∧ _x313 + 1 = _x306
  f1172_0_createNode_Return	19	f2504_0_createTree_LE:		x1 = _x314 ∧ x2 = _x315 ∧ x3 = _x316 ∧ x4 = _x317 ∧ x5 = _x318 ∧ x6 = _x319 ∧ x7 = _x320 ∧ x8 = _x321 ∧ x9 = _x322 ∧ x1 = _x323 ∧ x2 = _x324 ∧ x3 = _x325 ∧ x4 = _x326 ∧ x5 = _x327 ∧ x6 = _x328 ∧ x7 = _x329 ∧ x8 = _x330 ∧ x9 = _x331 ∧ _x316 = _x327 ∧ _x315 = _x326 ∧ _x314 = _x325 ∧ 1 ≤ _x323 − 1 ∧ 1 ≤ _x324 − 1
  f875_0_createTree_NE	20	f2504_0_createTree_LE:		x1 = _x332 ∧ x2 = _x333 ∧ x3 = _x334 ∧ x4 = _x335 ∧ x5 = _x336 ∧ x6 = _x337 ∧ x7 = _x338 ∧ x8 = _x339 ∧ x9 = _x340 ∧ x1 = _x341 ∧ x2 = _x342 ∧ x3 = _x343 ∧ x4 = _x344 ∧ x5 = _x345 ∧ x6 = _x346 ∧ x7 = _x347 ∧ x8 = _x348 ∧ x9 = _x349 ∧ _x334 = _x345 ∧ _x333 = _x344 ∧ _x332 = _x343 ∧ 1 ≤ _x341 − 1 ∧ 1 ≤ _x342 − 1 ∧ 0 ≤ _x334 − 1 ∧ 0 ≤ _x332 − 1
  f875_0_createTree_NE	21	f2504_0_createTree_LE:		x1 = _x350 ∧ x2 = _x351 ∧ x3 = _x352 ∧ x4 = _x353 ∧ x5 = _x354 ∧ x6 = _x355 ∧ x7 = _x356 ∧ x8 = _x357 ∧ x9 = _x358 ∧ x1 = _x359 ∧ x2 = _x360 ∧ x3 = _x361 ∧ x4 = _x362 ∧ x5 = _x363 ∧ x6 = _x364 ∧ x7 = _x365 ∧ x8 = _x366 ∧ x9 = _x367 ∧ _x351 = _x362 ∧ _x350 = _x361 ∧ 1 ≤ _x359 − 1 ∧ 1 ≤ _x360 − 1 ∧ 0 ≤ _x352 − 1 ∧ 0 ≤ _x350 − 1
  f2504_0_createTree_LE	22	f2588_0_createTree_NONNULL:		x1 = _x368 ∧ x2 = _x369 ∧ x3 = _x370 ∧ x4 = _x371 ∧ x5 = _x372 ∧ x6 = _x373 ∧ x7 = _x374 ∧ x8 = _x375 ∧ x9 = _x376 ∧ x1 = _x377 ∧ x2 = _x378 ∧ x3 = _x379 ∧ x4 = _x380 ∧ x5 = _x381 ∧ x6 = _x382 ∧ x7 = _x383 ∧ x8 = _x384 ∧ x9 = _x385 ∧ _x372 = _x382 ∧ _x371 = _x381 ∧ _x370 = _x377 ∧ _x385 + 2 ≤ _x369 ∧ _x384 + 2 ≤ _x368 ∧ _x383 + 2 ≤ _x368 ∧ −1 ≤ _x380 − 1 ∧ 0 ≤ _x379 − 1 ∧ 0 ≤ _x378 − 1 ∧ 0 ≤ _x369 − 1 ∧ 0 ≤ _x368 − 1 ∧ _x380 + 1 ≤ _x369 ∧ _x379 ≤ _x369 ∧ _x378 ≤ _x368 ∧ 0 ≤ _x370 − 1 ∧ −1 ≤ _x371 − 1 ∧ _x371 ≤ _x372
  f2588_0_createTree_NONNULL	23	f2504_0_createTree_LE:		x1 = _x386 ∧ x2 = _x387 ∧ x3 = _x388 ∧ x4 = _x389 ∧ x5 = _x390 ∧ x6 = _x391 ∧ x7 = _x392 ∧ x8 = _x393 ∧ x9 = _x394 ∧ x1 = _x395 ∧ x2 = _x396 ∧ x3 = _x397 ∧ x4 = _x398 ∧ x5 = _x399 ∧ x6 = _x400 ∧ x7 = _x401 ∧ x8 = _x402 ∧ x9 = _x403 ∧ _x391 = _x399 ∧ _x390 = _x398 ∧ _x386 − 1 = _x397 ∧ _x394 + 2 ≤ _x388 ∧ _x393 + 2 ≤ _x387 ∧ _x392 + 2 ≤ _x387 ∧ 0 ≤ _x396 − 1 ∧ 0 ≤ _x395 − 1 ∧ 0 ≤ _x389 − 1 ∧ 2 ≤ _x388 − 1 ∧ 0 ≤ _x387 − 1 ∧ _x396 ≤ _x389 ∧ _x396 + 2 ≤ _x388 ∧ _x395 ≤ _x387
  f2588_0_createTree_NONNULL	24	f2671_0_createTree_FieldAccess:		x1 = _x404 ∧ x2 = _x405 ∧ x3 = _x406 ∧ x4 = _x407 ∧ x5 = _x408 ∧ x6 = _x409 ∧ x7 = _x410 ∧ x8 = _x411 ∧ x9 = _x412 ∧ x1 = _x413 ∧ x2 = _x414 ∧ x3 = _x415 ∧ x4 = _x416 ∧ x5 = _x417 ∧ x6 = _x418 ∧ x7 = _x419 ∧ x8 = _x420 ∧ x9 = _x421 ∧ _x412 = _x419 ∧ _x411 = _x418 ∧ _x409 = _x417 ∧ _x408 = _x416 ∧ _x404 = _x413 ∧ _x412 + 2 ≤ _x406 ∧ _x411 + 2 ≤ _x405 ∧ _x410 + 2 ≤ _x405 ∧ 1 ≤ _x415 − 1 ∧ 0 ≤ _x414 − 1 ∧ −1 ≤ _x407 − 1 ∧ 1 ≤ _x406 − 1 ∧ 0 ≤ _x405 − 1 ∧ _x415 ≤ _x406 ∧ _x414 ≤ _x405 ∧ 0 ≤ _x404 − 1 ∧ _x408 ≤ _x409
  f2588_0_createTree_NONNULL	25	f2671_0_createTree_FieldAccess:		x1 = _x422 ∧ x2 = _x423 ∧ x3 = _x424 ∧ x4 = _x425 ∧ x5 = _x426 ∧ x6 = _x427 ∧ x7 = _x428 ∧ x8 = _x429 ∧ x9 = _x430 ∧ x1 = _x431 ∧ x2 = _x432 ∧ x3 = _x433 ∧ x4 = _x434 ∧ x5 = _x435 ∧ x6 = _x436 ∧ x7 = _x437 ∧ x8 = _x438 ∧ x9 = _x439 ∧ _x430 = _x437 ∧ _x429 = _x436 ∧ _x426 = _x434 ∧ _x422 = _x431 ∧ _x430 + 2 ≤ _x424 ∧ _x429 + 2 ≤ _x423 ∧ _x428 + 2 ≤ _x423 ∧ 1 ≤ _x433 − 1 ∧ 0 ≤ _x432 − 1 ∧ −1 ≤ _x425 − 1 ∧ 1 ≤ _x424 − 1 ∧ 0 ≤ _x423 − 1 ∧ _x433 ≤ _x424 ∧ _x432 ≤ _x423 ∧ 0 ≤ _x422 − 1 ∧ _x426 ≤ _x427
  f2504_0_createTree_LE	26	f2712_0_createTree_LE:		x1 = _x440 ∧ x2 = _x441 ∧ x3 = _x442 ∧ x4 = _x443 ∧ x5 = _x444 ∧ x6 = _x445 ∧ x7 = _x446 ∧ x8 = _x447 ∧ x9 = _x448 ∧ x1 = _x449 ∧ x2 = _x450 ∧ x3 = _x451 ∧ x4 = _x452 ∧ x5 = _x453 ∧ x6 = _x454 ∧ x7 = _x455 ∧ x8 = _x456 ∧ x9 = _x457 ∧ _x444 + 1 = _x454 ∧ _x443 = _x453 ∧ 0 = _x452 ∧ _x442 = _x449 ∧ _x456 + 2 ≤ _x440 ∧ _x455 + 2 ≤ _x440 ∧ 0 ≤ _x451 − 1 ∧ 0 ≤ _x450 − 1 ∧ 0 ≤ _x441 − 1 ∧ 0 ≤ _x440 − 1 ∧ _x451 ≤ _x441 ∧ _x450 ≤ _x440 ∧ −1 ≤ _x444 − 1 ∧ _x444 ≤ _x443 − 1 ∧ −1 ≤ _x443 − 1 ∧ 0 ≤ _x442 − 1
  f2504_0_createTree_LE	27	f2712_0_createTree_LE:		x1 = _x458 ∧ x2 = _x459 ∧ x3 = _x460 ∧ x4 = _x461 ∧ x5 = _x462 ∧ x6 = _x463 ∧ x7 = _x464 ∧ x8 = _x465 ∧ x9 = _x466 ∧ x1 = _x467 ∧ x2 = _x468 ∧ x3 = _x469 ∧ x4 = _x470 ∧ x5 = _x471 ∧ x6 = _x472 ∧ x7 = _x473 ∧ x8 = _x474 ∧ x9 = _x475 ∧ _x462 + 1 = _x472 ∧ _x461 = _x471 ∧ _x460 = _x467 ∧ _x474 + 2 ≤ _x458 ∧ _x473 + 2 ≤ _x458 ∧ 0 ≤ _x469 − 1 ∧ 0 ≤ _x468 − 1 ∧ 0 ≤ _x459 − 1 ∧ 0 ≤ _x458 − 1 ∧ _x469 ≤ _x459 ∧ _x468 ≤ _x458 ∧ −1 ≤ _x470 − 1 ∧ −1 ≤ _x462 − 1 ∧ _x462 ≤ _x461 − 1 ∧ −1 ≤ _x461 − 1 ∧ 0 ≤ _x460 − 1
  f2671_0_createTree_FieldAccess	28	f2504_0_createTree_LE:		x1 = _x476 ∧ x2 = _x477 ∧ x3 = _x478 ∧ x4 = _x479 ∧ x5 = _x480 ∧ x6 = _x481 ∧ x7 = _x482 ∧ x8 = _x483 ∧ x9 = _x484 ∧ x1 = _x485 ∧ x2 = _x486 ∧ x3 = _x487 ∧ x4 = _x488 ∧ x5 = _x489 ∧ x6 = _x490 ∧ x7 = _x491 ∧ x8 = _x492 ∧ x9 = _x493 ∧ _x480 = _x489 ∧ _x479 = _x488 ∧ _x476 − 1 = _x487 ∧ _x482 + 2 ≤ _x478 ∧ _x481 + 2 ≤ _x477 ∧ 0 ≤ _x486 − 1 ∧ 0 ≤ _x485 − 1 ∧ 1 ≤ _x478 − 1 ∧ 0 ≤ _x477 − 1
  f2671_0_createTree_FieldAccess	29	f2504_0_createTree_LE:		x1 = _x494 ∧ x2 = _x495 ∧ x3 = _x496 ∧ x4 = _x497 ∧ x5 = _x498 ∧ x6 = _x499 ∧ x7 = _x500 ∧ x8 = _x501 ∧ x9 = _x502 ∧ x1 = _x503 ∧ x2 = _x504 ∧ x3 = _x505 ∧ x4 = _x506 ∧ x5 = _x507 ∧ x6 = _x508 ∧ x7 = _x509 ∧ x8 = _x510 ∧ x9 = _x511 ∧ _x498 = _x507 ∧ _x497 = _x506 ∧ _x494 − 1 = _x505 ∧ _x499 = _x500 ∧ _x499 + 2 ≤ _x496 ∧ _x499 + 2 ≤ _x495 ∧ 3 ≤ _x504 − 1 ∧ 3 ≤ _x503 − 1 ∧ 1 ≤ _x496 − 1 ∧ 1 ≤ _x495 − 1 ∧ _x504 − 2 ≤ _x496 ∧ _x504 − 2 ≤ _x495 ∧ _x503 − 2 ≤ _x496 ∧ _x503 − 2 ≤ _x495
  f2712_0_createTree_LE	30	f2588_0_createTree_NONNULL:		x1 = _x512 ∧ x2 = _x513 ∧ x3 = _x514 ∧ x4 = _x515 ∧ x5 = _x516 ∧ x6 = _x517 ∧ x7 = _x518 ∧ x8 = _x519 ∧ x9 = _x520 ∧ x1 = _x521 ∧ x2 = _x522 ∧ x3 = _x523 ∧ x4 = _x524 ∧ x5 = _x525 ∧ x6 = _x526 ∧ x7 = _x527 ∧ x8 = _x528 ∧ x9 = _x529 ∧ _x519 = _x528 ∧ _x518 = _x527 ∧ _x517 = _x526 ∧ _x516 = _x525 ∧ _x512 = _x521 ∧ 0 = _x515 ∧ _x529 + 2 ≤ _x514 ∧ _x519 + 2 ≤ _x513 ∧ _x518 + 2 ≤ _x513 ∧ −1 ≤ _x524 − 1 ∧ 0 ≤ _x523 − 1 ∧ 0 ≤ _x522 − 1 ∧ 0 ≤ _x514 − 1 ∧ 0 ≤ _x513 − 1 ∧ _x524 + 1 ≤ _x514 ∧ _x523 ≤ _x514 ∧ _x522 ≤ _x513
  f2712_0_createTree_LE	31	f2504_0_createTree_LE:		x1 = _x530 ∧ x2 = _x531 ∧ x3 = _x532 ∧ x4 = _x533 ∧ x5 = _x534 ∧ x6 = _x535 ∧ x7 = _x536 ∧ x8 = _x537 ∧ x9 = _x538 ∧ x1 = _x539 ∧ x2 = _x540 ∧ x3 = _x541 ∧ x4 = _x542 ∧ x5 = _x543 ∧ x6 = _x544 ∧ x7 = _x545 ∧ x8 = _x546 ∧ x9 = _x547 ∧ _x535 = _x543 ∧ _x534 = _x542 ∧ _x530 − 1 = _x541 ∧ _x537 + 2 ≤ _x531 ∧ _x536 + 2 ≤ _x531 ∧ 0 ≤ _x540 − 1 ∧ 0 ≤ _x539 − 1 ∧ 2 ≤ _x532 − 1 ∧ 0 ≤ _x531 − 1 ∧ _x540 + 2 ≤ _x532 ∧ 0 ≤ _x533 − 1 ∧ _x539 ≤ _x531
  f2712_0_createTree_LE	32	f2777_0_createTree_FieldAccess:		x1 = _x548 ∧ x2 = _x549 ∧ x3 = _x550 ∧ x4 = _x551 ∧ x5 = _x552 ∧ x6 = _x553 ∧ x7 = _x554 ∧ x8 = _x555 ∧ x9 = _x556 ∧ x1 = _x557 ∧ x2 = _x558 ∧ x3 = _x559 ∧ x4 = _x560 ∧ x5 = _x561 ∧ x6 = _x562 ∧ x7 = _x563 ∧ x8 = _x564 ∧ x9 = _x565 ∧ _x554 = _x562 ∧ _x553 = _x561 ∧ _x552 = _x560 ∧ _x548 = _x557 ∧ _x563 + 2 ≤ _x550 ∧ _x555 + 2 ≤ _x549 ∧ _x554 + 2 ≤ _x549 ∧ 1 ≤ _x559 − 1 ∧ 0 ≤ _x558 − 1 ∧ 1 ≤ _x550 − 1 ∧ 0 ≤ _x549 − 1 ∧ _x559 ≤ _x550 ∧ _x558 ≤ _x549 ∧ 0 ≤ _x548 − 1 ∧ 0 ≤ _x553 − 1 ∧ 0 ≤ _x551 − 1
  f2712_0_createTree_LE	33	f2777_0_createTree_FieldAccess:		x1 = _x566 ∧ x2 = _x567 ∧ x3 = _x568 ∧ x4 = _x569 ∧ x5 = _x570 ∧ x6 = _x571 ∧ x7 = _x572 ∧ x8 = _x573 ∧ x9 = _x574 ∧ x1 = _x575 ∧ x2 = _x576 ∧ x3 = _x577 ∧ x4 = _x578 ∧ x5 = _x579 ∧ x6 = _x580 ∧ x7 = _x581 ∧ x8 = _x582 ∧ x9 = _x583 ∧ _x572 = _x580 ∧ _x570 = _x578 ∧ _x566 = _x575 ∧ _x581 + 2 ≤ _x568 ∧ _x573 + 2 ≤ _x567 ∧ _x572 + 2 ≤ _x567 ∧ 1 ≤ _x577 − 1 ∧ 0 ≤ _x576 − 1 ∧ 1 ≤ _x568 − 1 ∧ 0 ≤ _x567 − 1 ∧ _x577 ≤ _x568 ∧ _x576 ≤ _x567 ∧ 0 ≤ _x566 − 1 ∧ 0 ≤ _x571 − 1 ∧ 0 ≤ _x569 − 1
  f2777_0_createTree_FieldAccess	34	f2504_0_createTree_LE:		x1 = _x584 ∧ x2 = _x585 ∧ x3 = _x586 ∧ x4 = _x587 ∧ x5 = _x588 ∧ x6 = _x589 ∧ x7 = _x590 ∧ x8 = _x591 ∧ x9 = _x592 ∧ x1 = _x593 ∧ x2 = _x594 ∧ x3 = _x595 ∧ x4 = _x596 ∧ x5 = _x597 ∧ x6 = _x598 ∧ x7 = _x599 ∧ x8 = _x600 ∧ x9 = _x601 ∧ _x588 = _x597 ∧ _x587 = _x596 ∧ _x584 − 1 = _x595 ∧ _x590 + 2 ≤ _x586 ∧ _x589 + 2 ≤ _x585 ∧ 0 ≤ _x594 − 1 ∧ 0 ≤ _x593 − 1 ∧ 1 ≤ _x586 − 1 ∧ 0 ≤ _x585 − 1
  f2777_0_createTree_FieldAccess	35	f2504_0_createTree_LE:		x1 = _x602 ∧ x2 = _x603 ∧ x3 = _x604 ∧ x4 = _x605 ∧ x5 = _x606 ∧ x6 = _x607 ∧ x7 = _x608 ∧ x8 = _x609 ∧ x9 = _x610 ∧ x1 = _x611 ∧ x2 = _x612 ∧ x3 = _x613 ∧ x4 = _x614 ∧ x5 = _x615 ∧ x6 = _x616 ∧ x7 = _x617 ∧ x8 = _x618 ∧ x9 = _x619 ∧ _x606 = _x615 ∧ _x605 = _x614 ∧ _x602 − 1 = _x613 ∧ _x607 = _x608 ∧ _x607 + 2 ≤ _x604 ∧ _x607 + 2 ≤ _x603 ∧ 3 ≤ _x612 − 1 ∧ 3 ≤ _x611 − 1 ∧ 1 ≤ _x604 − 1 ∧ 1 ≤ _x603 − 1 ∧ _x612 − 2 ≤ _x604 ∧ _x612 − 2 ≤ _x603 ∧ _x611 − 2 ≤ _x604 ∧ _x611 − 2 ≤ _x603
  f845_0_alternate_NONNULL	36	f756_0_copy_NONNULL:		x1 = _x620 ∧ x2 = _x621 ∧ x3 = _x622 ∧ x4 = _x623 ∧ x5 = _x624 ∧ x6 = _x625 ∧ x7 = _x626 ∧ x8 = _x627 ∧ x9 = _x628 ∧ x1 = _x629 ∧ x2 = _x630 ∧ x3 = _x631 ∧ x4 = _x632 ∧ x5 = _x633 ∧ x6 = _x634 ∧ x7 = _x635 ∧ x8 = _x636 ∧ x9 = _x637 ∧ −1 ≤ _x629 − 1 ∧ −1 ≤ _x623 − 1 ∧ −1 ≤ _x622 − 1 ∧ −1 ≤ _x621 − 1 ∧ −1 ≤ _x620 − 1 ∧ _x629 ≤ _x622
  f845_0_alternate_NONNULL	37	f756_0_copy_NONNULL:		x1 = _x638 ∧ x2 = _x639 ∧ x3 = _x640 ∧ x4 = _x641 ∧ x5 = _x642 ∧ x6 = _x643 ∧ x7 = _x644 ∧ x8 = _x645 ∧ x9 = _x646 ∧ x1 = _x647 ∧ x2 = _x648 ∧ x3 = _x649 ∧ x4 = _x650 ∧ x5 = _x651 ∧ x6 = _x652 ∧ x7 = _x653 ∧ x8 = _x654 ∧ x9 = _x655 ∧ −1 ≤ _x647 − 1 ∧ 0 ≤ _x641 − 1 ∧ −1 ≤ _x640 − 1 ∧ 0 ≤ _x639 − 1 ∧ 0 ≤ _x638 − 1 ∧ _x647 + 1 ≤ _x641 ∧ _x647 + 1 ≤ _x639 ∧ _x647 + 1 ≤ _x638
  f845_0_alternate_NONNULL	38	f845_0_alternate_NONNULL:		x1 = _x656 ∧ x2 = _x657 ∧ x3 = _x658 ∧ x4 = _x659 ∧ x5 = _x660 ∧ x6 = _x661 ∧ x7 = _x662 ∧ x8 = _x663 ∧ x9 = _x664 ∧ x1 = _x665 ∧ x2 = _x666 ∧ x3 = _x667 ∧ x4 = _x668 ∧ x5 = _x669 ∧ x6 = _x670 ∧ x7 = _x671 ∧ x8 = _x672 ∧ x9 = _x673 ∧ −1 ≤ _x668 − 1 ∧ −1 ≤ _x667 − 1 ∧ −1 ≤ _x666 − 1 ∧ −1 ≤ _x665 − 1 ∧ 1 ≤ _x659 − 1 ∧ −1 ≤ _x658 − 1 ∧ 1 ≤ _x657 − 1 ∧ 1 ≤ _x656 − 1 ∧ _x668 ≤ _x658 ∧ _x667 + 2 ≤ _x659 ∧ _x667 + 2 ≤ _x657 ∧ _x667 + 2 ≤ _x656 ∧ _x666 ≤ _x658 ∧ _x665 ≤ _x658
  f845_0_alternate_NONNULL	39	f1242_0_alternate_InvokeMethod:		x1 = _x674 ∧ x2 = _x675 ∧ x3 = _x676 ∧ x4 = _x677 ∧ x5 = _x678 ∧ x6 = _x679 ∧ x7 = _x680 ∧ x8 = _x681 ∧ x9 = _x682 ∧ x1 = _x683 ∧ x2 = _x684 ∧ x3 = _x685 ∧ x4 = _x686 ∧ x5 = _x687 ∧ x6 = _x688 ∧ x7 = _x689 ∧ x8 = _x690 ∧ x9 = _x691 ∧ −1 ≤ _x688 − 1 ∧ −1 ≤ _x686 − 1 ∧ −1 ≤ _x685 − 1 ∧ 2 ≤ _x684 − 1 ∧ 4 ≤ _x683 − 1 ∧ 4 ≤ _x677 − 1 ∧ −1 ≤ _x676 − 1 ∧ 4 ≤ _x675 − 1 ∧ 4 ≤ _x674 − 1 ∧ _x688 + 2 ≤ _x677 ∧ _x688 + 2 ≤ _x675 ∧ _x688 + 2 ≤ _x674 ∧ _x686 + 2 ≤ _x677 ∧ _x686 + 2 ≤ _x675 ∧ _x686 + 2 ≤ _x674 ∧ _x685 ≤ _x676 ∧ _x683 ≤ _x677 ∧ _x683 ≤ _x675 ∧ _x683 ≤ _x674
  f845_0_alternate_NONNULL	40	f1242_0_alternate_InvokeMethod:		x1 = _x692 ∧ x2 = _x693 ∧ x3 = _x694 ∧ x4 = _x695 ∧ x5 = _x696 ∧ x6 = _x697 ∧ x7 = _x698 ∧ x8 = _x699 ∧ x9 = _x700 ∧ x1 = _x701 ∧ x2 = _x702 ∧ x3 = _x703 ∧ x4 = _x704 ∧ x5 = _x705 ∧ x6 = _x706 ∧ x7 = _x707 ∧ x8 = _x708 ∧ x9 = _x709 ∧ −1 ≤ _x706 − 1 ∧ −1 ≤ _x704 − 1 ∧ −1 ≤ _x703 − 1 ∧ 1 ≤ _x702 − 1 ∧ 3 ≤ _x701 − 1 ∧ 3 ≤ _x695 − 1 ∧ −1 ≤ _x694 − 1 ∧ 3 ≤ _x693 − 1 ∧ 3 ≤ _x692 − 1 ∧ _x706 + 2 ≤ _x695 ∧ _x706 + 2 ≤ _x693 ∧ _x706 + 2 ≤ _x692 ∧ _x704 + 2 ≤ _x695 ∧ _x704 + 2 ≤ _x693 ∧ _x704 + 2 ≤ _x692 ∧ _x703 ≤ _x694 ∧ _x702 + 2 ≤ _x695 ∧ _x702 − 2 ≤ _x694 ∧ _x702 + 2 ≤ _x693 ∧ _x702 + 2 ≤ _x692 ∧ _x701 ≤ _x695 ∧ _x701 ≤ _x693 ∧ _x701 ≤ _x692
  f1242_0_alternate_InvokeMethod	41	f845_0_alternate_NONNULL:		x1 = _x710 ∧ x2 = _x711 ∧ x3 = _x712 ∧ x4 = _x713 ∧ x5 = _x714 ∧ x6 = _x715 ∧ x7 = _x716 ∧ x8 = _x717 ∧ x9 = _x718 ∧ x1 = _x719 ∧ x2 = _x720 ∧ x3 = _x721 ∧ x4 = _x722 ∧ x5 = _x723 ∧ x6 = _x724 ∧ x7 = _x725 ∧ x8 = _x726 ∧ x9 = _x727 ∧ −1 ≤ _x722 − 1 ∧ −1 ≤ _x721 − 1 ∧ −1 ≤ _x720 − 1 ∧ −1 ≤ _x719 − 1 ∧ −1 ≤ _x715 − 1 ∧ −1 ≤ _x713 − 1 ∧ −1 ≤ _x712 − 1 ∧ 0 ≤ _x711 − 1 ∧ 2 ≤ _x710 − 1 ∧ _x722 ≤ _x712 ∧ _x721 ≤ _x715 ∧ _x721 ≤ _x713 ∧ _x721 + 2 ≤ _x710 ∧ _x720 ≤ _x712 ∧ _x719 ≤ _x712
  f756_0_copy_NONNULL	42	f756_0_copy_NONNULL:		x1 = _x728 ∧ x2 = _x729 ∧ x3 = _x730 ∧ x4 = _x731 ∧ x5 = _x732 ∧ x6 = _x733 ∧ x7 = _x734 ∧ x8 = _x735 ∧ x9 = _x736 ∧ x1 = _x737 ∧ x2 = _x738 ∧ x3 = _x739 ∧ x4 = _x740 ∧ x5 = _x741 ∧ x6 = _x742 ∧ x7 = _x743 ∧ x8 = _x744 ∧ x9 = _x745 ∧ −1 ≤ _x737 − 1 ∧ 0 ≤ _x728 − 1 ∧ _x737 + 1 ≤ _x728
  f756_0_copy_NONNULL	43	f756_0_copy_NONNULL:		x1 = _x746 ∧ x2 = _x747 ∧ x3 = _x748 ∧ x4 = _x749 ∧ x5 = _x750 ∧ x6 = _x751 ∧ x7 = _x752 ∧ x8 = _x753 ∧ x9 = _x754 ∧ x1 = _x755 ∧ x2 = _x756 ∧ x3 = _x757 ∧ x4 = _x758 ∧ x5 = _x759 ∧ x6 = _x760 ∧ x7 = _x761 ∧ x8 = _x762 ∧ x9 = _x763 ∧ −1 ≤ _x755 − 1 ∧ 1 ≤ _x746 − 1 ∧ _x755 + 2 ≤ _x746
  f756_0_copy_NONNULL	44	f1247_0_copy_InvokeMethod:		x1 = _x764 ∧ x2 = _x765 ∧ x3 = _x766 ∧ x4 = _x767 ∧ x5 = _x768 ∧ x6 = _x769 ∧ x7 = _x770 ∧ x8 = _x771 ∧ x9 = _x772 ∧ x1 = _x773 ∧ x2 = _x774 ∧ x3 = _x775 ∧ x4 = _x776 ∧ x5 = _x777 ∧ x6 = _x778 ∧ x7 = _x779 ∧ x8 = _x780 ∧ x9 = _x781 ∧ −1 ≤ _x775 − 1 ∧ −1 ≤ _x774 − 1 ∧ 4 ≤ _x773 − 1 ∧ 4 ≤ _x764 − 1 ∧ _x775 + 2 ≤ _x764 ∧ _x774 + 2 ≤ _x764 ∧ _x773 ≤ _x764
  f756_0_copy_NONNULL	45	f1247_0_copy_InvokeMethod:		x1 = _x782 ∧ x2 = _x783 ∧ x3 = _x784 ∧ x4 = _x785 ∧ x5 = _x786 ∧ x6 = _x787 ∧ x7 = _x788 ∧ x8 = _x789 ∧ x9 = _x790 ∧ x1 = _x791 ∧ x2 = _x792 ∧ x3 = _x793 ∧ x4 = _x794 ∧ x5 = _x795 ∧ x6 = _x796 ∧ x7 = _x797 ∧ x8 = _x798 ∧ x9 = _x799 ∧ −1 ≤ _x793 − 1 ∧ −1 ≤ _x792 − 1 ∧ 3 ≤ _x791 − 1 ∧ 3 ≤ _x782 − 1 ∧ _x793 + 2 ≤ _x782 ∧ _x792 + 2 ≤ _x782 ∧ _x791 ≤ _x782
  f1247_0_copy_InvokeMethod	46	f756_0_copy_NONNULL:		x1 = _x800 ∧ x2 = _x801 ∧ x3 = _x802 ∧ x4 = _x803 ∧ x5 = _x804 ∧ x6 = _x805 ∧ x7 = _x806 ∧ x8 = _x807 ∧ x9 = _x808 ∧ x1 = _x809 ∧ x2 = _x810 ∧ x3 = _x811 ∧ x4 = _x812 ∧ x5 = _x813 ∧ x6 = _x814 ∧ x7 = _x815 ∧ x8 = _x816 ∧ x9 = _x817 ∧ −1 ≤ _x809 − 1 ∧ −1 ≤ _x802 − 1 ∧ −1 ≤ _x801 − 1 ∧ 2 ≤ _x800 − 1 ∧ _x809 ≤ _x802 ∧ _x809 ≤ _x801 ∧ _x809 + 2 ≤ _x800
  f875_0_createTree_NE	47	f2035_0_random_GT:		x1 = _x818 ∧ x2 = _x819 ∧ x3 = _x820 ∧ x4 = _x821 ∧ x5 = _x822 ∧ x6 = _x823 ∧ x7 = _x824 ∧ x8 = _x825 ∧ x9 = _x826 ∧ x1 = _x827 ∧ x2 = _x828 ∧ x3 = _x829 ∧ x4 = _x830 ∧ x5 = _x831 ∧ x6 = _x832 ∧ x7 = _x833 ∧ x8 = _x834 ∧ x9 = _x835 ∧ _x820 = _x829 ∧ _x819 = _x828 ∧ 0 ≤ _x820 − 1 ∧ −1 ≤ _x819 − 1 ∧ 0 ≤ _x818 − 1
  f2588_0_createTree_NONNULL	48	f2035_0_random_GT:		x1 = _x836 ∧ x2 = _x837 ∧ x3 = _x838 ∧ x4 = _x839 ∧ x5 = _x840 ∧ x6 = _x841 ∧ x7 = _x842 ∧ x8 = _x843 ∧ x9 = _x844 ∧ x1 = _x845 ∧ x2 = _x846 ∧ x3 = _x847 ∧ x4 = _x848 ∧ x5 = _x849 ∧ x6 = _x850 ∧ x7 = _x851 ∧ x8 = _x852 ∧ x9 = _x853 ∧ _x841 = _x847 ∧ _x840 = _x846 ∧ _x844 + 2 ≤ _x838 ∧ _x843 + 2 ≤ _x837 ∧ _x842 + 2 ≤ _x837 ∧ −1 ≤ _x839 − 1 ∧ 1 ≤ _x838 − 1 ∧ 0 ≤ _x837 − 1 ∧ 0 ≤ _x836 − 1 ∧ _x840 ≤ _x841 ∧ −1 ≤ _x840 − 1
  f2712_0_createTree_LE	49	f2035_0_random_GT:		x1 = _x854 ∧ x2 = _x855 ∧ x3 = _x856 ∧ x4 = _x857 ∧ x5 = _x858 ∧ x6 = _x859 ∧ x7 = _x860 ∧ x8 = _x861 ∧ x9 = _x862 ∧ x1 = _x863 ∧ x2 = _x864 ∧ x3 = _x865 ∧ x4 = _x866 ∧ x5 = _x867 ∧ x6 = _x868 ∧ x7 = _x869 ∧ x8 = _x870 ∧ x9 = _x871 ∧ _x859 = _x865 ∧ _x858 = _x864 ∧ _x861 + 2 ≤ _x855 ∧ _x860 + 2 ≤ _x855 ∧ 1 ≤ _x856 − 1 ∧ 0 ≤ _x855 − 1 ∧ 0 ≤ _x857 − 1 ∧ −1 ≤ _x858 − 1 ∧ 0 ≤ _x859 − 1 ∧ 0 ≤ _x854 − 1
  __init	50	f1_0_main_Load:		x1 = _x872 ∧ x2 = _x873 ∧ x3 = _x874 ∧ x4 = _x875 ∧ x5 = _x876 ∧ x6 = _x877 ∧ x7 = _x878 ∧ x8 = _x879 ∧ x9 = _x880 ∧ x1 = _x881 ∧ x2 = _x882 ∧ x3 = _x883 ∧ x4 = _x884 ∧ x5 = _x885 ∧ x6 = _x886 ∧ x7 = _x887 ∧ x8 = _x888 ∧ x9 = _x889 ∧ 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 { f2671_0_createTree_FieldAccess, f2777_0_createTree_FieldAccess, f2712_0_createTree_LE, f2504_0_createTree_LE, f2588_0_createTree_NONNULL }.

2.1.1 Transition Removal

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

2.1.2 Transition Removal

We remove transitions 23, 30, 31, 35, 34, 33, 32, 29, 28, 25, 24 using the following ranking functions, which are bounded by 0.

2.1.3 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 { f845_0_alternate_NONNULL, f1242_0_alternate_InvokeMethod }.

2.2.1 Transition Removal

We remove transitions 38, 41, 40, 39 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 { f1247_0_copy_InvokeMethod, f756_0_copy_NONNULL }.

2.3.1 Transition Removal

We remove transitions 42, 43, 46, 45, 44 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 % (12 real / 0 unknown / 0 assumptions / 12 total proof steps)