LTS Termination Proof

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:

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:

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)