by AProVE
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 |
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 | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 |
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 | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 |
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 | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 |
f2789_0_createCollection_InvokeMethod | f2789_0_createCollection_InvokeMethod | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 |
__init | __init | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 |
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 | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 |
We consider subproblems for each of the 4 SCC(s) of the program graph.
Here we consider the SCC {
, }.We remove transitions
, , , , , , , , , , , , , , , , , using the following ranking functions, which are bounded by 0.: | 1 − 2⋅x2 + 2⋅x3 |
: | 2⋅x1 − 2⋅x2 |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.
Here we consider the SCC {
}.We remove transitions
, , using the following ranking functions, which are bounded by 0.: | x2 |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.
Here we consider the SCC {
}.We remove transitions
, using the following ranking functions, which are bounded by 0.: | x2 |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.
Here we consider the SCC {
}.We remove transition
using the following ranking functions, which are bounded by 0.: | x1 + x2 |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.