LTS Termination Proof

by AProVE

Input

Integer Transition System
• Initial Location: f2753_0_insert_NONNULL, f1598_0_main_InvokeMethod, f2353_0_createCollection_GE, f1_0_main_Load, f2751_0_insert_NONNULL, f202_0_createCollection_Return, f2789_0_createCollection_InvokeMethod, __init, f89_0_createCollection_LE, f1863_0_minimum_NONNULL
• Transitions: (pre-variables and post-variables)  f1_0_main_Load 1 f1598_0_main_InvokeMethod: x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x7 = _arg7 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ x7 = _arg7P ∧ 0 ≤ _arg2P − 1 ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ _arg1P ≤ _arg1 f202_0_createCollection_Return 2 f1598_0_main_InvokeMethod: x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ x1 = _x7 ∧ x2 = _x8 ∧ x3 = _x9 ∧ x4 = _x10 ∧ x5 = _x11 ∧ x6 = _x12 ∧ x7 = _x13 ∧ 1 ≤ _x8 − 1 ∧ 0 ≤ _x7 − 1 ∧ 0 ≤ _x − 1 ∧ _x8 − 1 ≤ _x ∧ _x7 ≤ _x f1_0_main_Load 3 f89_0_createCollection_LE: x1 = _x14 ∧ x2 = _x15 ∧ x3 = _x16 ∧ x4 = _x17 ∧ x5 = _x18 ∧ x6 = _x19 ∧ x7 = _x20 ∧ x1 = _x21 ∧ x2 = _x22 ∧ x3 = _x23 ∧ x4 = _x24 ∧ x5 = _x25 ∧ x6 = _x26 ∧ x7 = _x27 ∧ _x15 = _x22 ∧ 0 = _x21 ∧ 0 ≤ _x15 − 1 ∧ 0 ≤ _x14 − 1 f1_0_main_Load 4 f89_0_createCollection_LE: x1 = _x28 ∧ x2 = _x29 ∧ x3 = _x30 ∧ x4 = _x31 ∧ x5 = _x32 ∧ x6 = _x33 ∧ x7 = _x34 ∧ x1 = _x35 ∧ x2 = _x36 ∧ x3 = _x37 ∧ x4 = _x38 ∧ x5 = _x39 ∧ x6 = _x40 ∧ x7 = _x41 ∧ _x29 = _x36 ∧ 0 ≤ _x28 − 1 ∧ 0 ≤ _x29 − 1 ∧ −1 ≤ _x35 − 1 f1_0_main_Load 5 f2353_0_createCollection_GE: x1 = _x42 ∧ x2 = _x43 ∧ x3 = _x44 ∧ x4 = _x45 ∧ x5 = _x46 ∧ x6 = _x47 ∧ x7 = _x48 ∧ x1 = _x49 ∧ x2 = _x50 ∧ x3 = _x51 ∧ x4 = _x52 ∧ x5 = _x53 ∧ x6 = _x54 ∧ x7 = _x55 ∧ 0 = _x53 ∧ 0 = _x52 ∧ 0 = _x51 ∧ 0 = _x50 ∧ 0 = _x43 ∧ 1 ≤ _x49 − 1 ∧ 0 ≤ _x42 − 1 ∧ _x49 − 1 ≤ _x42 f89_0_createCollection_LE 6 f2353_0_createCollection_GE: x1 = _x56 ∧ x2 = _x57 ∧ x3 = _x58 ∧ x4 = _x59 ∧ x5 = _x60 ∧ x6 = _x61 ∧ x7 = _x62 ∧ x1 = _x63 ∧ x2 = _x64 ∧ x3 = _x65 ∧ x4 = _x66 ∧ x5 = _x67 ∧ x6 = _x68 ∧ x7 = _x69 ∧ 1 = _x67 ∧ 1 = _x66 ∧ 0 = _x65 ∧ 0 = _x64 ∧ 1 = _x57 ∧ 0 = _x56 ∧ 1 ≤ _x63 − 1 f89_0_createCollection_LE 7 f2353_0_createCollection_GE: x1 = _x70 ∧ x2 = _x71 ∧ x3 = _x72 ∧ x4 = _x73 ∧ x5 = _x74 ∧ x6 = _x75 ∧ x7 = _x76 ∧ x1 = _x77 ∧ x2 = _x78 ∧ x3 = _x79 ∧ x4 = _x80 ∧ x5 = _x81 ∧ x6 = _x82 ∧ x7 = _x83 ∧ 1 = _x81 ∧ 1 = _x80 ∧ 0 = _x79 ∧ 0 = _x78 ∧ 1 = _x71 ∧ 1 ≤ _x77 − 1 ∧ 0 ≤ _x70 − 1 f89_0_createCollection_LE 8 f2353_0_createCollection_GE: x1 = _x84 ∧ x2 = _x85 ∧ x3 = _x86 ∧ x4 = _x87 ∧ x5 = _x88 ∧ x6 = _x89 ∧ x7 = _x90 ∧ x1 = _x91 ∧ x2 = _x92 ∧ x3 = _x93 ∧ x4 = _x94 ∧ x5 = _x95 ∧ x6 = _x96 ∧ x7 = _x97 ∧ 2 = _x95 ∧ _x85 = _x94 ∧ 0 = _x93 ∧ 0 = _x92 ∧ 0 = _x84 ∧ 1 ≤ _x91 − 1 ∧ 1 ≤ _x85 − 1 f89_0_createCollection_LE 9 f2353_0_createCollection_GE: x1 = _x98 ∧ x2 = _x99 ∧ x3 = _x100 ∧ x4 = _x101 ∧ x5 = _x102 ∧ x6 = _x103 ∧ x7 = _x104 ∧ x1 = _x105 ∧ x2 = _x106 ∧ x3 = _x107 ∧ x4 = _x108 ∧ x5 = _x109 ∧ x6 = _x110 ∧ x7 = _x111 ∧ 2 = _x109 ∧ _x99 = _x108 ∧ 0 = _x106 ∧ 0 = _x98 ∧ 1 ≤ _x99 − 1 ∧ 1 ≤ _x105 − 1 ∧ −1 ≤ _x107 − 1 f89_0_createCollection_LE 10 f2353_0_createCollection_GE: x1 = _x112 ∧ x2 = _x113 ∧ x3 = _x114 ∧ x4 = _x115 ∧ x5 = _x116 ∧ x6 = _x117 ∧ x7 = _x118 ∧ x1 = _x119 ∧ x2 = _x120 ∧ x3 = _x121 ∧ x4 = _x122 ∧ x5 = _x123 ∧ x6 = _x124 ∧ x7 = _x125 ∧ 2 = _x123 ∧ _x113 = _x122 ∧ 0 = _x121 ∧ 0 = _x120 ∧ 1 ≤ _x113 − 1 ∧ 1 ≤ _x119 − 1 ∧ 0 ≤ _x112 − 1 f89_0_createCollection_LE 11 f2353_0_createCollection_GE: x1 = _x126 ∧ x2 = _x127 ∧ x3 = _x128 ∧ x4 = _x129 ∧ x5 = _x130 ∧ x6 = _x131 ∧ x7 = _x132 ∧ x1 = _x133 ∧ x2 = _x134 ∧ x3 = _x135 ∧ x4 = _x136 ∧ x5 = _x137 ∧ x6 = _x138 ∧ x7 = _x139 ∧ 2 = _x137 ∧ _x127 = _x136 ∧ 0 = _x134 ∧ 0 ≤ _x126 − 1 ∧ 1 ≤ _x133 − 1 ∧ 1 ≤ _x127 − 1 ∧ −1 ≤ _x135 − 1 f2353_0_createCollection_GE 12 f2751_0_insert_NONNULL: x1 = _x140 ∧ x2 = _x141 ∧ x3 = _x142 ∧ x4 = _x143 ∧ x5 = _x144 ∧ x6 = _x145 ∧ x7 = _x146 ∧ x1 = _x147 ∧ x2 = _x148 ∧ x3 = _x149 ∧ x4 = _x150 ∧ x5 = _x151 ∧ x6 = _x152 ∧ x7 = _x153 ∧ 0 = _x149 ∧ −1 ≤ _x148 − 1 ∧ 1 ≤ _x147 − 1 ∧ 1 ≤ _x140 − 1 ∧ _x148 + 2 ≤ _x140 ∧ _x147 ≤ _x140 ∧ 0 ≤ _x142 − 1 ∧ _x143 ≤ _x144 ∧ _x141 ≤ _x142 − 1 ∧ −1 ≤ _x143 − 1 f2353_0_createCollection_GE 13 f2751_0_insert_NONNULL: x1 = _x154 ∧ x2 = _x155 ∧ x3 = _x156 ∧ x4 = _x157 ∧ x5 = _x158 ∧ x6 = _x159 ∧ x7 = _x160 ∧ x1 = _x161 ∧ x2 = _x162 ∧ x3 = _x163 ∧ x4 = _x164 ∧ x5 = _x165 ∧ x6 = _x166 ∧ x7 = _x167 ∧ 0 = _x163 ∧ 0 ≤ _x162 − 1 ∧ 1 ≤ _x161 − 1 ∧ 2 ≤ _x154 − 1 ∧ _x162 + 2 ≤ _x154 ∧ _x161 + 1 ≤ _x154 ∧ 0 ≤ _x156 − 1 ∧ _x157 ≤ _x158 ∧ _x155 ≤ _x156 − 1 ∧ −1 ≤ _x157 − 1 f2353_0_createCollection_GE 14 f2753_0_insert_NONNULL: x1 = _x168 ∧ x2 = _x169 ∧ x3 = _x170 ∧ x4 = _x171 ∧ x5 = _x172 ∧ x6 = _x173 ∧ x7 = _x174 ∧ x1 = _x175 ∧ x2 = _x176 ∧ x3 = _x177 ∧ x4 = _x178 ∧ x5 = _x179 ∧ x6 = _x180 ∧ x7 = _x181 ∧ 0 = _x177 ∧ −1 ≤ _x176 − 1 ∧ 1 ≤ _x175 − 1 ∧ 1 ≤ _x168 − 1 ∧ _x176 + 2 ≤ _x168 ∧ _x175 ≤ _x168 ∧ 0 ≤ _x170 − 1 ∧ _x171 ≤ _x172 ∧ _x169 ≤ _x170 − 1 ∧ −1 ≤ _x171 − 1 f2353_0_createCollection_GE 15 f2753_0_insert_NONNULL: x1 = _x182 ∧ x2 = _x183 ∧ x3 = _x184 ∧ x4 = _x185 ∧ x5 = _x186 ∧ x6 = _x187 ∧ x7 = _x188 ∧ x1 = _x189 ∧ x2 = _x190 ∧ x3 = _x191 ∧ x4 = _x192 ∧ x5 = _x193 ∧ x6 = _x194 ∧ x7 = _x195 ∧ 0 = _x191 ∧ 0 ≤ _x190 − 1 ∧ 1 ≤ _x189 − 1 ∧ 2 ≤ _x182 − 1 ∧ _x190 + 2 ≤ _x182 ∧ _x189 + 1 ≤ _x182 ∧ 0 ≤ _x184 − 1 ∧ _x185 ≤ _x186 ∧ _x183 ≤ _x184 − 1 ∧ −1 ≤ _x185 − 1 f2353_0_createCollection_GE 16 f2789_0_createCollection_InvokeMethod: x1 = _x196 ∧ x2 = _x197 ∧ x3 = _x198 ∧ x4 = _x199 ∧ x5 = _x200 ∧ x6 = _x201 ∧ x7 = _x202 ∧ x1 = _x203 ∧ x2 = _x204 ∧ x3 = _x205 ∧ x4 = _x206 ∧ x5 = _x207 ∧ x6 = _x208 ∧ x7 = _x209 ∧ 0 = _x209 ∧ _x200 + 1 = _x208 ∧ _x199 = _x207 ∧ _x197 = _x204 ∧ _x198 = _x203 ∧ 1 ≤ _x206 − 1 ∧ 0 ≤ _x205 − 1 ∧ 0 ≤ _x196 − 1 ∧ _x206 − 1 ≤ _x196 ∧ _x205 ≤ _x196 ∧ −1 ≤ _x200 − 1 ∧ _x200 ≤ _x199 − 1 ∧ _x197 ≤ _x198 − 1 ∧ −1 ≤ _x199 − 1 f2353_0_createCollection_GE 17 f2789_0_createCollection_InvokeMethod: x1 = _x210 ∧ x2 = _x211 ∧ x3 = _x212 ∧ x4 = _x213 ∧ x5 = _x214 ∧ x6 = _x215 ∧ x7 = _x216 ∧ x1 = _x217 ∧ x2 = _x218 ∧ x3 = _x219 ∧ x4 = _x220 ∧ x5 = _x221 ∧ x6 = _x222 ∧ x7 = _x223 ∧ _x214 + 1 = _x222 ∧ _x213 = _x221 ∧ _x211 = _x218 ∧ _x212 = _x217 ∧ 0 ≤ _x220 − 1 ∧ 0 ≤ _x219 − 1 ∧ 0 ≤ _x210 − 1 ∧ _x219 ≤ _x210 ∧ −1 ≤ _x214 − 1 ∧ −1 ≤ _x223 − 1 ∧ _x214 ≤ _x213 − 1 ∧ _x211 ≤ _x212 − 1 ∧ −1 ≤ _x213 − 1 f2789_0_createCollection_InvokeMethod 18 f2751_0_insert_NONNULL: x1 = _x224 ∧ x2 = _x225 ∧ x3 = _x226 ∧ x4 = _x227 ∧ x5 = _x228 ∧ x6 = _x229 ∧ x7 = _x230 ∧ x1 = _x231 ∧ x2 = _x232 ∧ x3 = _x233 ∧ x4 = _x234 ∧ x5 = _x235 ∧ x6 = _x236 ∧ x7 = _x237 ∧ _x230 = _x233 ∧ _x230 + 2 ≤ _x227 ∧ −1 ≤ _x232 − 1 ∧ 0 ≤ _x231 − 1 ∧ 0 ≤ _x227 − 1 ∧ 1 ≤ _x226 − 1 ∧ _x232 + 1 ≤ _x227 ∧ _x232 + 2 ≤ _x226 ∧ _x231 ≤ _x227 ∧ 0 ≤ _x229 − 1 ∧ _x225 ≤ _x224 − 1 ∧ 0 ≤ _x224 − 1 f2789_0_createCollection_InvokeMethod 19 f2753_0_insert_NONNULL: x1 = _x238 ∧ x2 = _x239 ∧ x3 = _x240 ∧ x4 = _x241 ∧ x5 = _x242 ∧ x6 = _x243 ∧ x7 = _x244 ∧ x1 = _x245 ∧ x2 = _x246 ∧ x3 = _x247 ∧ x4 = _x248 ∧ x5 = _x249 ∧ x6 = _x250 ∧ x7 = _x251 ∧ _x244 = _x247 ∧ _x244 + 2 ≤ _x241 ∧ −1 ≤ _x246 − 1 ∧ 0 ≤ _x245 − 1 ∧ 0 ≤ _x241 − 1 ∧ 1 ≤ _x240 − 1 ∧ _x246 + 1 ≤ _x241 ∧ _x246 + 2 ≤ _x240 ∧ _x245 ≤ _x241 ∧ 0 ≤ _x243 − 1 ∧ _x239 ≤ _x238 − 1 ∧ 0 ≤ _x238 − 1 f2789_0_createCollection_InvokeMethod 20 f2751_0_insert_NONNULL: x1 = _x252 ∧ x2 = _x253 ∧ x3 = _x254 ∧ x4 = _x255 ∧ x5 = _x256 ∧ x6 = _x257 ∧ x7 = _x258 ∧ x1 = _x259 ∧ x2 = _x260 ∧ x3 = _x261 ∧ x4 = _x262 ∧ x5 = _x263 ∧ x6 = _x264 ∧ x7 = _x265 ∧ _x258 = _x261 ∧ _x258 + 2 ≤ _x255 ∧ 0 ≤ _x260 − 1 ∧ 0 ≤ _x259 − 1 ∧ 0 ≤ _x255 − 1 ∧ 2 ≤ _x254 − 1 ∧ _x260 + 2 ≤ _x254 ∧ _x259 ≤ _x255 ∧ 0 ≤ _x257 − 1 ∧ _x253 ≤ _x252 − 1 ∧ 0 ≤ _x252 − 1 f2789_0_createCollection_InvokeMethod 21 f2753_0_insert_NONNULL: x1 = _x266 ∧ x2 = _x267 ∧ x3 = _x268 ∧ x4 = _x269 ∧ x5 = _x270 ∧ x6 = _x271 ∧ x7 = _x272 ∧ x1 = _x273 ∧ x2 = _x274 ∧ x3 = _x275 ∧ x4 = _x276 ∧ x5 = _x277 ∧ x6 = _x278 ∧ x7 = _x279 ∧ _x272 = _x275 ∧ _x272 + 2 ≤ _x269 ∧ 0 ≤ _x274 − 1 ∧ 0 ≤ _x273 − 1 ∧ 0 ≤ _x269 − 1 ∧ 2 ≤ _x268 − 1 ∧ _x274 + 2 ≤ _x268 ∧ _x273 ≤ _x269 ∧ 0 ≤ _x271 − 1 ∧ _x267 ≤ _x266 − 1 ∧ 0 ≤ _x266 − 1 f2353_0_createCollection_GE 22 f2353_0_createCollection_GE: x1 = _x280 ∧ x2 = _x281 ∧ x3 = _x282 ∧ x4 = _x283 ∧ x5 = _x284 ∧ x6 = _x285 ∧ x7 = _x286 ∧ x1 = _x287 ∧ x2 = _x288 ∧ x3 = _x289 ∧ x4 = _x290 ∧ x5 = _x291 ∧ x6 = _x292 ∧ x7 = _x293 ∧ _x284 = _x291 ∧ _x283 = _x290 ∧ _x282 = _x289 ∧ _x281 + 1 = _x288 ∧ 4 ≤ _x287 − 1 ∧ 1 ≤ _x280 − 1 ∧ 0 ≤ _x282 − 1 ∧ _x283 ≤ _x284 ∧ _x281 ≤ _x282 − 1 ∧ −1 ≤ _x283 − 1 f2789_0_createCollection_InvokeMethod 23 f2353_0_createCollection_GE: x1 = _x294 ∧ x2 = _x295 ∧ x3 = _x296 ∧ x4 = _x297 ∧ x5 = _x298 ∧ x6 = _x299 ∧ x7 = _x300 ∧ x1 = _x301 ∧ x2 = _x302 ∧ x3 = _x303 ∧ x4 = _x304 ∧ x5 = _x305 ∧ x6 = _x306 ∧ x7 = _x307 ∧ _x299 = _x305 ∧ _x298 = _x304 ∧ _x294 = _x303 ∧ _x295 + 1 = _x302 ∧ _x300 + 2 ≤ _x297 ∧ 4 ≤ _x301 − 1 ∧ 0 ≤ _x297 − 1 ∧ 1 ≤ _x296 − 1 ∧ 0 ≤ _x299 − 1 ∧ _x295 ≤ _x294 − 1 ∧ 0 ≤ _x294 − 1 f2353_0_createCollection_GE 24 f2353_0_createCollection_GE: x1 = _x308 ∧ x2 = _x309 ∧ x3 = _x310 ∧ x4 = _x311 ∧ x5 = _x312 ∧ x6 = _x313 ∧ x7 = _x314 ∧ x1 = _x315 ∧ x2 = _x316 ∧ x3 = _x317 ∧ x4 = _x318 ∧ x5 = _x319 ∧ x6 = _x320 ∧ x7 = _x321 ∧ _x312 = _x319 ∧ _x311 = _x318 ∧ _x310 = _x317 ∧ _x309 + 1 = _x316 ∧ 7 ≤ _x315 − 1 ∧ 4 ≤ _x308 − 1 ∧ 0 ≤ _x310 − 1 ∧ _x311 ≤ _x312 ∧ _x309 ≤ _x310 − 1 ∧ −1 ≤ _x311 − 1 f2789_0_createCollection_InvokeMethod 25 f2353_0_createCollection_GE: x1 = _x322 ∧ x2 = _x323 ∧ x3 = _x324 ∧ x4 = _x325 ∧ x5 = _x326 ∧ x6 = _x327 ∧ x7 = _x328 ∧ x1 = _x329 ∧ x2 = _x330 ∧ x3 = _x331 ∧ x4 = _x332 ∧ x5 = _x333 ∧ x6 = _x334 ∧ x7 = _x335 ∧ _x327 = _x333 ∧ _x326 = _x332 ∧ _x322 = _x331 ∧ _x323 + 1 = _x330 ∧ _x328 + 2 ≤ _x325 ∧ 7 ≤ _x329 − 1 ∧ 0 ≤ _x325 − 1 ∧ 4 ≤ _x324 − 1 ∧ 0 ≤ _x327 − 1 ∧ _x323 ≤ _x322 − 1 ∧ 0 ≤ _x322 − 1 f2353_0_createCollection_GE 26 f2353_0_createCollection_GE: x1 = _x336 ∧ x2 = _x337 ∧ x3 = _x338 ∧ x4 = _x339 ∧ x5 = _x340 ∧ x6 = _x341 ∧ x7 = _x342 ∧ x1 = _x343 ∧ x2 = _x344 ∧ x3 = _x345 ∧ x4 = _x346 ∧ x5 = _x347 ∧ x6 = _x348 ∧ x7 = _x349 ∧ _x340 = _x347 ∧ _x339 = _x346 ∧ _x338 = _x345 ∧ _x337 + 1 = _x344 ∧ 8 ≤ _x343 − 1 ∧ 2 ≤ _x336 − 1 ∧ 0 ≤ _x338 − 1 ∧ _x339 ≤ _x340 ∧ _x337 ≤ _x338 − 1 ∧ −1 ≤ _x339 − 1 f2789_0_createCollection_InvokeMethod 27 f2353_0_createCollection_GE: x1 = _x350 ∧ x2 = _x351 ∧ x3 = _x352 ∧ x4 = _x353 ∧ x5 = _x354 ∧ x6 = _x355 ∧ x7 = _x356 ∧ x1 = _x357 ∧ x2 = _x358 ∧ x3 = _x359 ∧ x4 = _x360 ∧ x5 = _x361 ∧ x6 = _x362 ∧ x7 = _x363 ∧ _x355 = _x361 ∧ _x354 = _x360 ∧ _x350 = _x359 ∧ _x351 + 1 = _x358 ∧ _x356 + 2 ≤ _x353 ∧ 8 ≤ _x357 − 1 ∧ 0 ≤ _x353 − 1 ∧ 2 ≤ _x352 − 1 ∧ 0 ≤ _x355 − 1 ∧ _x351 ≤ _x350 − 1 ∧ 0 ≤ _x350 − 1 f2353_0_createCollection_GE 28 f2353_0_createCollection_GE: x1 = _x364 ∧ x2 = _x365 ∧ x3 = _x366 ∧ x4 = _x367 ∧ x5 = _x368 ∧ x6 = _x369 ∧ x7 = _x370 ∧ x1 = _x371 ∧ x2 = _x372 ∧ x3 = _x373 ∧ x4 = _x374 ∧ x5 = _x375 ∧ x6 = _x376 ∧ x7 = _x377 ∧ _x368 = _x375 ∧ _x367 = _x374 ∧ _x366 = _x373 ∧ _x365 + 1 = _x372 ∧ 10 ≤ _x371 − 1 ∧ 2 ≤ _x364 − 1 ∧ 0 ≤ _x366 − 1 ∧ _x367 ≤ _x368 ∧ _x365 ≤ _x366 − 1 ∧ −1 ≤ _x367 − 1 f2789_0_createCollection_InvokeMethod 29 f2353_0_createCollection_GE: x1 = _x378 ∧ x2 = _x379 ∧ x3 = _x380 ∧ x4 = _x381 ∧ x5 = _x382 ∧ x6 = _x383 ∧ x7 = _x384 ∧ x1 = _x385 ∧ x2 = _x386 ∧ x3 = _x387 ∧ x4 = _x388 ∧ x5 = _x389 ∧ x6 = _x390 ∧ x7 = _x391 ∧ _x383 = _x389 ∧ _x382 = _x388 ∧ _x378 = _x387 ∧ _x379 + 1 = _x386 ∧ _x384 + 2 ≤ _x381 ∧ 10 ≤ _x385 − 1 ∧ 0 ≤ _x381 − 1 ∧ 2 ≤ _x380 − 1 ∧ 0 ≤ _x383 − 1 ∧ _x379 ≤ _x378 − 1 ∧ 0 ≤ _x378 − 1 f2353_0_createCollection_GE 30 f2353_0_createCollection_GE: x1 = _x392 ∧ x2 = _x393 ∧ x3 = _x394 ∧ x4 = _x395 ∧ x5 = _x396 ∧ x6 = _x397 ∧ x7 = _x398 ∧ x1 = _x399 ∧ x2 = _x400 ∧ x3 = _x401 ∧ x4 = _x402 ∧ x5 = _x403 ∧ x6 = _x404 ∧ x7 = _x405 ∧ _x396 = _x403 ∧ _x395 = _x402 ∧ _x394 = _x401 ∧ _x393 + 1 = _x400 ∧ 7 ≤ _x399 − 1 ∧ 2 ≤ _x392 − 1 ∧ 0 ≤ _x394 − 1 ∧ _x395 ≤ _x396 ∧ _x393 ≤ _x394 − 1 ∧ −1 ≤ _x395 − 1 f2789_0_createCollection_InvokeMethod 31 f2353_0_createCollection_GE: x1 = _x406 ∧ x2 = _x407 ∧ x3 = _x408 ∧ x4 = _x409 ∧ x5 = _x410 ∧ x6 = _x411 ∧ x7 = _x412 ∧ x1 = _x413 ∧ x2 = _x414 ∧ x3 = _x415 ∧ x4 = _x416 ∧ x5 = _x417 ∧ x6 = _x418 ∧ x7 = _x419 ∧ _x411 = _x417 ∧ _x410 = _x416 ∧ _x406 = _x415 ∧ _x407 + 1 = _x414 ∧ _x412 + 2 ≤ _x409 ∧ 7 ≤ _x413 − 1 ∧ 0 ≤ _x409 − 1 ∧ 2 ≤ _x408 − 1 ∧ 0 ≤ _x411 − 1 ∧ _x407 ≤ _x406 − 1 ∧ 0 ≤ _x406 − 1 f2353_0_createCollection_GE 32 f2353_0_createCollection_GE: x1 = _x420 ∧ x2 = _x421 ∧ x3 = _x422 ∧ x4 = _x423 ∧ x5 = _x424 ∧ x6 = _x425 ∧ x7 = _x426 ∧ x1 = _x427 ∧ x2 = _x428 ∧ x3 = _x429 ∧ x4 = _x430 ∧ x5 = _x431 ∧ x6 = _x432 ∧ x7 = _x433 ∧ _x424 = _x431 ∧ _x423 = _x430 ∧ _x422 = _x429 ∧ _x421 + 1 = _x428 ∧ 8 ≤ _x427 − 1 ∧ 1 ≤ _x420 − 1 ∧ 0 ≤ _x422 − 1 ∧ _x423 ≤ _x424 ∧ _x421 ≤ _x422 − 1 ∧ −1 ≤ _x423 − 1 f2789_0_createCollection_InvokeMethod 33 f2353_0_createCollection_GE: x1 = _x434 ∧ x2 = _x435 ∧ x3 = _x436 ∧ x4 = _x437 ∧ x5 = _x438 ∧ x6 = _x439 ∧ x7 = _x440 ∧ x1 = _x441 ∧ x2 = _x442 ∧ x3 = _x443 ∧ x4 = _x444 ∧ x5 = _x445 ∧ x6 = _x446 ∧ x7 = _x447 ∧ _x439 = _x445 ∧ _x438 = _x444 ∧ _x434 = _x443 ∧ _x435 + 1 = _x442 ∧ _x440 + 2 ≤ _x437 ∧ 8 ≤ _x441 − 1 ∧ 0 ≤ _x437 − 1 ∧ 1 ≤ _x436 − 1 ∧ 0 ≤ _x439 − 1 ∧ _x435 ≤ _x434 − 1 ∧ 0 ≤ _x434 − 1 f2353_0_createCollection_GE 34 f2353_0_createCollection_GE: x1 = _x448 ∧ x2 = _x449 ∧ x3 = _x450 ∧ x4 = _x451 ∧ x5 = _x452 ∧ x6 = _x453 ∧ x7 = _x454 ∧ x1 = _x455 ∧ x2 = _x456 ∧ x3 = _x457 ∧ x4 = _x458 ∧ x5 = _x459 ∧ x6 = _x460 ∧ x7 = _x461 ∧ _x452 = _x459 ∧ _x451 = _x458 ∧ _x450 = _x457 ∧ _x449 + 1 = _x456 ∧ 10 ≤ _x455 − 1 ∧ 1 ≤ _x448 − 1 ∧ 0 ≤ _x450 − 1 ∧ _x451 ≤ _x452 ∧ _x449 ≤ _x450 − 1 ∧ −1 ≤ _x451 − 1 f2789_0_createCollection_InvokeMethod 35 f2353_0_createCollection_GE: x1 = _x462 ∧ x2 = _x463 ∧ x3 = _x464 ∧ x4 = _x465 ∧ x5 = _x466 ∧ x6 = _x467 ∧ x7 = _x468 ∧ x1 = _x469 ∧ x2 = _x470 ∧ x3 = _x471 ∧ x4 = _x472 ∧ x5 = _x473 ∧ x6 = _x474 ∧ x7 = _x475 ∧ _x467 = _x473 ∧ _x466 = _x472 ∧ _x462 = _x471 ∧ _x463 + 1 = _x470 ∧ _x468 + 2 ≤ _x465 ∧ 10 ≤ _x469 − 1 ∧ 0 ≤ _x465 − 1 ∧ 1 ≤ _x464 − 1 ∧ 0 ≤ _x467 − 1 ∧ _x463 ≤ _x462 − 1 ∧ 0 ≤ _x462 − 1 f2353_0_createCollection_GE 36 f2353_0_createCollection_GE: x1 = _x476 ∧ x2 = _x477 ∧ x3 = _x478 ∧ x4 = _x479 ∧ x5 = _x480 ∧ x6 = _x481 ∧ x7 = _x482 ∧ x1 = _x483 ∧ x2 = _x484 ∧ x3 = _x485 ∧ x4 = _x486 ∧ x5 = _x487 ∧ x6 = _x488 ∧ x7 = _x489 ∧ _x480 = _x487 ∧ _x479 = _x486 ∧ _x478 = _x485 ∧ _x477 + 1 = _x484 ∧ 7 ≤ _x483 − 1 ∧ 1 ≤ _x476 − 1 ∧ 0 ≤ _x478 − 1 ∧ _x479 ≤ _x480 ∧ _x477 ≤ _x478 − 1 ∧ −1 ≤ _x479 − 1 f2789_0_createCollection_InvokeMethod 37 f2353_0_createCollection_GE: x1 = _x490 ∧ x2 = _x491 ∧ x3 = _x492 ∧ x4 = _x493 ∧ x5 = _x494 ∧ x6 = _x495 ∧ x7 = _x496 ∧ x1 = _x497 ∧ x2 = _x498 ∧ x3 = _x499 ∧ x4 = _x500 ∧ x5 = _x501 ∧ x6 = _x502 ∧ x7 = _x503 ∧ _x495 = _x501 ∧ _x494 = _x500 ∧ _x490 = _x499 ∧ _x491 + 1 = _x498 ∧ _x496 + 2 ≤ _x493 ∧ 7 ≤ _x497 − 1 ∧ 0 ≤ _x493 − 1 ∧ 1 ≤ _x492 − 1 ∧ 0 ≤ _x495 − 1 ∧ _x491 ≤ _x490 − 1 ∧ 0 ≤ _x490 − 1 f2751_0_insert_NONNULL 38 f2751_0_insert_NONNULL: x1 = _x504 ∧ x2 = _x505 ∧ x3 = _x506 ∧ x4 = _x507 ∧ x5 = _x508 ∧ x6 = _x509 ∧ x7 = _x510 ∧ x1 = _x511 ∧ x2 = _x512 ∧ x3 = _x513 ∧ x4 = _x514 ∧ x5 = _x515 ∧ x6 = _x516 ∧ x7 = _x517 ∧ _x506 = _x513 ∧ _x506 + 2 ≤ _x504 ∧ −1 ≤ _x512 − 1 ∧ 0 ≤ _x511 − 1 ∧ 1 ≤ _x505 − 1 ∧ 0 ≤ _x504 − 1 ∧ _x512 + 2 ≤ _x505 ∧ _x511 ≤ _x504 f2751_0_insert_NONNULL 39 f2751_0_insert_NONNULL: x1 = _x518 ∧ x2 = _x519 ∧ x3 = _x520 ∧ x4 = _x521 ∧ x5 = _x522 ∧ x6 = _x523 ∧ x7 = _x524 ∧ x1 = _x525 ∧ x2 = _x526 ∧ x3 = _x527 ∧ x4 = _x528 ∧ x5 = _x529 ∧ x6 = _x530 ∧ x7 = _x531 ∧ _x525 ≤ _x518 ∧ _x532 ≤ _x520 ∧ _x526 + 3 ≤ _x519 ∧ 0 ≤ _x518 − 1 ∧ 2 ≤ _x519 − 1 ∧ 0 ≤ _x525 − 1 ∧ −1 ≤ _x526 − 1 ∧ _x520 + 2 ≤ _x518 ∧ _x520 = _x527 f2753_0_insert_NONNULL 40 f2753_0_insert_NONNULL: x1 = _x533 ∧ x2 = _x534 ∧ x3 = _x535 ∧ x4 = _x536 ∧ x5 = _x537 ∧ x6 = _x538 ∧ x7 = _x539 ∧ x1 = _x540 ∧ x2 = _x541 ∧ x3 = _x542 ∧ x4 = _x543 ∧ x5 = _x544 ∧ x6 = _x545 ∧ x7 = _x546 ∧ _x535 = _x542 ∧ _x535 + 2 ≤ _x533 ∧ −1 ≤ _x541 − 1 ∧ 0 ≤ _x540 − 1 ∧ 1 ≤ _x534 − 1 ∧ 0 ≤ _x533 − 1 ∧ _x541 + 2 ≤ _x534 ∧ _x540 ≤ _x533 f2753_0_insert_NONNULL 41 f2753_0_insert_NONNULL: x1 = _x547 ∧ x2 = _x548 ∧ x3 = _x549 ∧ x4 = _x550 ∧ x5 = _x551 ∧ x6 = _x552 ∧ x7 = _x553 ∧ x1 = _x554 ∧ x2 = _x555 ∧ x3 = _x556 ∧ x4 = _x557 ∧ x5 = _x558 ∧ x6 = _x559 ∧ x7 = _x560 ∧ _x554 ≤ _x547 ∧ _x561 ≤ _x549 ∧ _x555 + 3 ≤ _x548 ∧ 0 ≤ _x547 − 1 ∧ 2 ≤ _x548 − 1 ∧ 0 ≤ _x554 − 1 ∧ −1 ≤ _x555 − 1 ∧ _x549 + 2 ≤ _x547 ∧ _x549 = _x556 f2753_0_insert_NONNULL 42 f2753_0_insert_NONNULL: x1 = _x562 ∧ x2 = _x563 ∧ x3 = _x564 ∧ x4 = _x565 ∧ x5 = _x566 ∧ x6 = _x567 ∧ x7 = _x568 ∧ x1 = _x569 ∧ x2 = _x570 ∧ x3 = _x571 ∧ x4 = _x572 ∧ x5 = _x573 ∧ x6 = _x574 ∧ x7 = _x575 ∧ 0 ≤ _x576 − 1 ∧ _x564 ≤ _x576 − 1 ∧ _x569 ≤ _x562 ∧ _x570 + 3 ≤ _x563 ∧ 0 ≤ _x562 − 1 ∧ 2 ≤ _x563 − 1 ∧ 0 ≤ _x569 − 1 ∧ −1 ≤ _x570 − 1 ∧ _x564 + 2 ≤ _x562 ∧ _x564 = _x571 f1598_0_main_InvokeMethod 43 f1863_0_minimum_NONNULL: x1 = _x577 ∧ x2 = _x578 ∧ x3 = _x579 ∧ x4 = _x580 ∧ x5 = _x582 ∧ x6 = _x583 ∧ x7 = _x584 ∧ x1 = _x585 ∧ x2 = _x586 ∧ x3 = _x587 ∧ x4 = _x588 ∧ x5 = _x589 ∧ x6 = _x590 ∧ x7 = _x591 ∧ _x587 + 5 ≤ _x578 ∧ _x588 + 4 ≤ _x578 ∧ −1 ≤ _x586 − 1 ∧ 0 ≤ _x585 − 1 ∧ 2 ≤ _x578 − 1 ∧ 0 ≤ _x577 − 1 ∧ _x586 + 3 ≤ _x578 ∧ _x585 + 2 ≤ _x578 f1863_0_minimum_NONNULL 44 f1863_0_minimum_NONNULL: x1 = _x593 ∧ x2 = _x594 ∧ x3 = _x595 ∧ x4 = _x596 ∧ x5 = _x597 ∧ x6 = _x599 ∧ x7 = _x600 ∧ x1 = _x601 ∧ x2 = _x602 ∧ x3 = _x603 ∧ x4 = _x604 ∧ x5 = _x605 ∧ x6 = _x606 ∧ x7 = _x607 ∧ _x603 + 3 ≤ _x594 ∧ _x604 + 2 ≤ _x594 ∧ _x596 + 2 ≤ _x593 ∧ _x604 + 5 ≤ _x593 ∧ _x603 + 6 ≤ _x593 ∧ _x595 + 3 ≤ _x593 ∧ −1 ≤ _x602 − 1 ∧ 0 ≤ _x601 − 1 ∧ 0 ≤ _x594 − 1 ∧ 3 ≤ _x593 − 1 ∧ _x602 + 1 ≤ _x594 ∧ _x602 + 4 ≤ _x593 ∧ _x601 ≤ _x594 ∧ _x601 + 3 ≤ _x593 __init 45 f1_0_main_Load: x1 = _x608 ∧ x2 = _x609 ∧ x3 = _x610 ∧ x4 = _x611 ∧ x5 = _x612 ∧ x6 = _x613 ∧ x7 = _x614 ∧ x1 = _x615 ∧ x2 = _x616 ∧ x3 = _x617 ∧ x4 = _x618 ∧ x5 = _x619 ∧ x6 = _x620 ∧ x7 = _x621 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 f2753_0_insert_NONNULL f2753_0_insert_NONNULL f2753_0_insert_NONNULL: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f1598_0_main_InvokeMethod f1598_0_main_InvokeMethod f1598_0_main_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f2353_0_createCollection_GE f2353_0_createCollection_GE f2353_0_createCollection_GE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f1_0_main_Load f1_0_main_Load f1_0_main_Load: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f2751_0_insert_NONNULL f2751_0_insert_NONNULL f2751_0_insert_NONNULL: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f202_0_createCollection_Return f202_0_createCollection_Return f202_0_createCollection_Return: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f2789_0_createCollection_InvokeMethod f2789_0_createCollection_InvokeMethod f2789_0_createCollection_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 __init __init __init: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f89_0_createCollection_LE f89_0_createCollection_LE f89_0_createCollection_LE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f1863_0_minimum_NONNULL f1863_0_minimum_NONNULL f1863_0_minimum_NONNULL: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7
and for every transition t, a duplicate t is considered.

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 { f2353_0_createCollection_GE, f2789_0_createCollection_InvokeMethod }.

2.1.1 Transition Removal

We remove transitions 16, 22, 23, 17, 24, 26, 28, 30, 32, 34, 36, 37, 35, 33, 31, 29, 27, 25 using the following ranking functions, which are bounded by 0.

 f2353_0_createCollection_GE: 1 − 2⋅x2 + 2⋅x3 f2789_0_createCollection_InvokeMethod: 2⋅x1 − 2⋅x2

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 { f2753_0_insert_NONNULL }.

2.2.1 Transition Removal

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

 f2753_0_insert_NONNULL: x2

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 { f2751_0_insert_NONNULL }.

2.3.1 Transition Removal

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

 f2751_0_insert_NONNULL: x2

2.3.2 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 { f1863_0_minimum_NONNULL }.

2.4.1 Transition Removal

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

 f1863_0_minimum_NONNULL: x1 + x2

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