# LTS Termination Proof

by AProVE

## Input

Integer Transition System
• Initial Location: f703_0_main_InvokeMethod, f1232_0_sortedHigh_InvokeMethod, f1140_0_sortedHigh_NONNULL, f1309_0_sortedHigh_InvokeMethod, f1000_0_quicksort_InvokeMethod, f392_0_createList_GT, __init, f730_0_quicksort_NONNULL, f501_0_createList_InvokeMethod, f790_0_sortedLow_NONNULL, f1022_0_sortedLow_InvokeMethod, f89_0_main_InvokeMethod, f1_0_main_Load
• Transitions: (pre-variables and post-variables)  f1_0_main_Load 1 f392_0_createList_GT: x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ 0 = _arg3P ∧ 0 = _arg2P ∧ 0 = _arg1P ∧ 0 = _arg2 ∧ 0 ≤ _arg1 − 1 f1_0_main_Load 2 f89_0_main_InvokeMethod: x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x1 = _x5 ∧ x2 = _x6 ∧ x3 = _x7 ∧ x4 = _x8 ∧ x5 = _x9 ∧ 0 = _x6 ∧ 0 ≤ _x5 − 1 ∧ 0 ≤ _x − 1 ∧ 0 ≤ _x1 − 1 ∧ _x5 ≤ _x f1_0_main_Load 3 f89_0_main_InvokeMethod: x1 = _x10 ∧ x2 = _x11 ∧ x3 = _x12 ∧ x4 = _x13 ∧ x5 = _x14 ∧ x1 = _x15 ∧ x2 = _x16 ∧ x3 = _x17 ∧ x4 = _x19 ∧ x5 = _x20 ∧ 0 ≤ _x15 − 1 ∧ 0 ≤ _x10 − 1 ∧ _x15 ≤ _x10 ∧ 0 ≤ _x11 − 1 ∧ −1 ≤ _x16 − 1 f89_0_main_InvokeMethod 4 f392_0_createList_GT: x1 = _x21 ∧ x2 = _x22 ∧ x3 = _x24 ∧ x4 = _x25 ∧ x5 = _x26 ∧ x1 = _x27 ∧ x2 = _x28 ∧ x3 = _x30 ∧ x4 = _x31 ∧ x5 = _x32 ∧ 1 = _x30 ∧ _x22 = _x27 ∧ 0 ≤ _x28 − 1 ∧ 0 ≤ _x21 − 1 f1_0_main_Load 5 f730_0_quicksort_NONNULL: x1 = _x33 ∧ x2 = _x34 ∧ x3 = _x36 ∧ x4 = _x37 ∧ x5 = _x38 ∧ x1 = _x39 ∧ x2 = _x41 ∧ x3 = _x42 ∧ x4 = _x43 ∧ x5 = _x44 ∧ 0 = _x34 ∧ −1 ≤ _x39 − 1 ∧ 0 ≤ _x33 − 1 ∧ _x39 + 1 ≤ _x33 f89_0_main_InvokeMethod 6 f730_0_quicksort_NONNULL: x1 = _x45 ∧ x2 = _x46 ∧ x3 = _x47 ∧ x4 = _x48 ∧ x5 = _x49 ∧ x1 = _x50 ∧ x2 = _x51 ∧ x3 = _x52 ∧ x4 = _x53 ∧ x5 = _x55 ∧ _x50 + 1 ≤ _x45 ∧ 0 ≤ _x56 − 1 ∧ 0 ≤ _x45 − 1 ∧ −1 ≤ _x50 − 1 ∧ 0 = _x46 f1_0_main_Load 7 f730_0_quicksort_NONNULL: x1 = _x57 ∧ x2 = _x58 ∧ x3 = _x59 ∧ x4 = _x60 ∧ x5 = _x61 ∧ x1 = _x62 ∧ x2 = _x63 ∧ x3 = _x64 ∧ x4 = _x65 ∧ x5 = _x66 ∧ 0 = _x58 ∧ 1 ≤ _x62 − 1 ∧ 0 ≤ _x57 − 1 ∧ _x62 − 1 ≤ _x57 f89_0_main_InvokeMethod 8 f703_0_main_InvokeMethod: x1 = _x67 ∧ x2 = _x68 ∧ x3 = _x69 ∧ x4 = _x70 ∧ x5 = _x71 ∧ x1 = _x72 ∧ x2 = _x73 ∧ x3 = _x74 ∧ x4 = _x75 ∧ x5 = _x76 ∧ _x72 ≤ _x67 ∧ 0 ≤ _x77 − 1 ∧ 0 ≤ _x67 − 1 ∧ 0 ≤ _x72 − 1 ∧ 2 ≤ _x73 − 1 ∧ 0 = _x74 f89_0_main_InvokeMethod 9 f703_0_main_InvokeMethod: x1 = _x78 ∧ x2 = _x79 ∧ x3 = _x80 ∧ x4 = _x81 ∧ x5 = _x82 ∧ x1 = _x83 ∧ x2 = _x84 ∧ x3 = _x85 ∧ x4 = _x86 ∧ x5 = _x87 ∧ _x83 ≤ _x78 ∧ 0 ≤ _x88 − 1 ∧ 0 ≤ _x78 − 1 ∧ 0 ≤ _x83 − 1 ∧ 2 ≤ _x84 − 1 f89_0_main_InvokeMethod 10 f703_0_main_InvokeMethod: x1 = _x89 ∧ x2 = _x90 ∧ x3 = _x91 ∧ x4 = _x92 ∧ x5 = _x93 ∧ x1 = _x94 ∧ x2 = _x95 ∧ x3 = _x96 ∧ x4 = _x97 ∧ x5 = _x98 ∧ _x94 ≤ _x89 ∧ 0 ≤ _x99 − 1 ∧ 0 ≤ _x89 − 1 ∧ 0 ≤ _x94 − 1 ∧ 1 ≤ _x95 − 1 f89_0_main_InvokeMethod 11 f703_0_main_InvokeMethod: x1 = _x100 ∧ x2 = _x101 ∧ x3 = _x102 ∧ x4 = _x103 ∧ x5 = _x104 ∧ x1 = _x106 ∧ x2 = _x107 ∧ x3 = _x108 ∧ x4 = _x109 ∧ x5 = _x111 ∧ _x106 ≤ _x100 ∧ 0 ≤ _x112 − 1 ∧ _x107 − 1 ≤ _x100 ∧ 0 ≤ _x100 − 1 ∧ 0 ≤ _x106 − 1 ∧ 1 ≤ _x107 − 1 ∧ 0 = _x108 f703_0_main_InvokeMethod 12 f730_0_quicksort_NONNULL: x1 = _x113 ∧ x2 = _x114 ∧ x3 = _x116 ∧ x4 = _x117 ∧ x5 = _x118 ∧ x1 = _x119 ∧ x2 = _x120 ∧ x3 = _x121 ∧ x4 = _x122 ∧ x5 = _x123 ∧ _x119 ≤ _x114 ∧ 0 ≤ _x124 − 1 ∧ 0 ≤ _x113 − 1 ∧ 0 ≤ _x114 − 1 ∧ 0 ≤ _x119 − 1 ∧ _x116 + 2 ≤ _x114 f392_0_createList_GT 13 f392_0_createList_GT: x1 = _x125 ∧ x2 = _x126 ∧ x3 = _x127 ∧ x4 = _x128 ∧ x5 = _x129 ∧ x1 = _x130 ∧ x2 = _x131 ∧ x3 = _x132 ∧ x4 = _x133 ∧ x5 = _x134 ∧ _x127 = _x132 ∧ _x126 = _x131 ∧ _x125 − 1 = _x130 ∧ _x126 ≤ _x127 ∧ _x125 − 1 ≤ _x125 − 1 ∧ −1 ≤ _x126 − 1 ∧ 0 ≤ _x125 − 1 f392_0_createList_GT 14 f501_0_createList_InvokeMethod: x1 = _x135 ∧ x2 = _x136 ∧ x3 = _x137 ∧ x4 = _x138 ∧ x5 = _x139 ∧ x1 = _x141 ∧ x2 = _x142 ∧ x3 = _x143 ∧ x4 = _x144 ∧ x5 = _x146 ∧ _x137 + 1 = _x144 ∧ _x136 = _x143 ∧ _x135 − 1 = _x142 ∧ _x135 = _x141 ∧ _x137 ≤ _x136 − 1 ∧ −1 ≤ _x137 − 1 ∧ −1 ≤ _x136 − 1 ∧ 0 ≤ _x135 − 1 f392_0_createList_GT 15 f501_0_createList_InvokeMethod: x1 = _x147 ∧ x2 = _x148 ∧ x3 = _x149 ∧ x4 = _x150 ∧ x5 = _x151 ∧ x1 = _x152 ∧ x2 = _x153 ∧ x3 = _x154 ∧ x4 = _x155 ∧ x5 = _x156 ∧ 0 ≤ _x147 − 1 ∧ −1 ≤ _x148 − 1 ∧ _x149 ≤ _x148 − 1 ∧ −1 ≤ _x157 − 1 ∧ −1 ≤ _x149 − 1 ∧ _x147 = _x152 ∧ _x147 − 1 = _x153 ∧ _x148 = _x154 ∧ _x149 + 1 = _x155 f501_0_createList_InvokeMethod 16 f392_0_createList_GT: x1 = _x158 ∧ x2 = _x159 ∧ x3 = _x160 ∧ x4 = _x161 ∧ x5 = _x162 ∧ x1 = _x163 ∧ x2 = _x165 ∧ x3 = _x166 ∧ x4 = _x167 ∧ x5 = _x168 ∧ _x161 = _x166 ∧ _x160 = _x165 ∧ _x159 = _x163 ∧ _x159 ≤ _x158 − 1 ∧ _x161 ≤ _x160 ∧ 0 ≤ _x160 − 1 ∧ 0 ≤ _x161 − 1 ∧ 0 ≤ _x158 − 1 f730_0_quicksort_NONNULL 17 f790_0_sortedLow_NONNULL: x1 = _x169 ∧ x2 = _x170 ∧ x3 = _x171 ∧ x4 = _x172 ∧ x5 = _x173 ∧ x1 = _x174 ∧ x2 = _x175 ∧ x3 = _x176 ∧ x4 = _x177 ∧ x5 = _x178 ∧ _x174 + 2 ≤ _x169 ∧ −1 ≤ _x175 − 1 ∧ 0 ≤ _x169 − 1 ∧ _x175 + 1 ≤ _x169 f730_0_quicksort_NONNULL 18 f1140_0_sortedHigh_NONNULL: x1 = _x179 ∧ x2 = _x180 ∧ x3 = _x181 ∧ x4 = _x182 ∧ x5 = _x183 ∧ x1 = _x184 ∧ x2 = _x185 ∧ x3 = _x186 ∧ x4 = _x187 ∧ x5 = _x188 ∧ _x184 + 2 ≤ _x179 ∧ −1 ≤ _x185 − 1 ∧ 1 ≤ _x179 − 1 ∧ _x185 + 2 ≤ _x179 f730_0_quicksort_NONNULL 19 f1000_0_quicksort_InvokeMethod: x1 = _x189 ∧ x2 = _x190 ∧ x3 = _x191 ∧ x4 = _x192 ∧ x5 = _x193 ∧ x1 = _x194 ∧ x2 = _x196 ∧ x3 = _x197 ∧ x4 = _x198 ∧ x5 = _x199 ∧ _x199 + 4 ≤ _x189 ∧ _x198 + 2 ≤ _x189 ∧ 1 ≤ _x196 − 1 ∧ 3 ≤ _x194 − 1 ∧ 3 ≤ _x189 − 1 ∧ _x196 + 2 ≤ _x189 ∧ _x194 ≤ _x189 f730_0_quicksort_NONNULL 20 f1000_0_quicksort_InvokeMethod: x1 = _x200 ∧ x2 = _x201 ∧ x3 = _x202 ∧ x4 = _x203 ∧ x5 = _x204 ∧ x1 = _x205 ∧ x2 = _x206 ∧ x3 = _x207 ∧ x4 = _x208 ∧ x5 = _x209 ∧ _x209 + 4 ≤ _x200 ∧ _x208 + 2 ≤ _x200 ∧ 2 ≤ _x206 − 1 ∧ 4 ≤ _x205 − 1 ∧ 4 ≤ _x200 − 1 ∧ _x206 + 2 ≤ _x200 ∧ _x205 ≤ _x200 f1000_0_quicksort_InvokeMethod 21 f1140_0_sortedHigh_NONNULL: x1 = _x210 ∧ x2 = _x211 ∧ x3 = _x212 ∧ x4 = _x213 ∧ x5 = _x214 ∧ x1 = _x215 ∧ x2 = _x216 ∧ x3 = _x217 ∧ x4 = _x218 ∧ x5 = _x219 ∧ _x212 = _x217 ∧ _x213 = _x215 ∧ _x214 + 2 ≤ _x211 ∧ _x213 + 2 ≤ _x210 ∧ _x214 + 4 ≤ _x210 ∧ 0 ≤ _x216 − 1 ∧ 0 ≤ _x211 − 1 ∧ 2 ≤ _x210 − 1 ∧ _x216 ≤ _x211 ∧ _x216 + 2 ≤ _x210 f1000_0_quicksort_InvokeMethod 22 f1287_0_quicksort_InvokeMethod: x1 = _x220 ∧ x2 = _x221 ∧ x3 = _x222 ∧ x4 = _x223 ∧ x5 = _x224 ∧ x1 = _x225 ∧ x2 = _x226 ∧ x3 = _x227 ∧ x4 = _x228 ∧ x5 = _x229 ∧ _x224 + 2 ≤ _x221 ∧ _x223 + 2 ≤ _x220 ∧ _x224 + 4 ≤ _x220 ∧ 4 ≤ _x225 − 1 ∧ 2 ≤ _x221 − 1 ∧ 4 ≤ _x220 − 1 ∧ _x225 ≤ _x220 f1000_0_quicksort_InvokeMethod 23 f1287_0_quicksort_InvokeMethod: x1 = _x230 ∧ x2 = _x231 ∧ x3 = _x232 ∧ x4 = _x233 ∧ x5 = _x234 ∧ x1 = _x235 ∧ x2 = _x236 ∧ x3 = _x237 ∧ x4 = _x238 ∧ x5 = _x239 ∧ _x234 + 2 ≤ _x231 ∧ _x233 + 2 ≤ _x230 ∧ _x234 + 4 ≤ _x230 ∧ 3 ≤ _x235 − 1 ∧ 1 ≤ _x231 − 1 ∧ 3 ≤ _x230 − 1 ∧ _x235 ≤ _x230 f790_0_sortedLow_NONNULL 24 f790_0_sortedLow_NONNULL: x1 = _x240 ∧ x2 = _x241 ∧ x3 = _x242 ∧ x4 = _x243 ∧ x5 = _x244 ∧ x1 = _x245 ∧ x2 = _x246 ∧ x3 = _x247 ∧ x4 = _x248 ∧ x5 = _x249 ∧ _x246 + 1 ≤ _x241 ∧ _x240 ≤ _x250 − 1 ∧ 0 ≤ _x241 − 1 ∧ −1 ≤ _x246 − 1 ∧ _x240 = _x245 ∧ _x242 = _x247 f790_0_sortedLow_NONNULL 25 f790_0_sortedLow_NONNULL: x1 = _x251 ∧ x2 = _x252 ∧ x3 = _x253 ∧ x4 = _x254 ∧ x5 = _x255 ∧ x1 = _x256 ∧ x2 = _x257 ∧ x3 = _x258 ∧ x4 = _x259 ∧ x5 = _x260 ∧ _x257 + 1 ≤ _x252 ∧ _x261 ≤ _x251 ∧ 0 ≤ _x252 − 1 ∧ −1 ≤ _x257 − 1 ∧ _x251 = _x256 ∧ _x253 = _x258 f790_0_sortedLow_NONNULL 26 f730_0_quicksort_NONNULL: x1 = _x262 ∧ x2 = _x263 ∧ x3 = _x264 ∧ x4 = _x265 ∧ x5 = _x266 ∧ x1 = _x267 ∧ x2 = _x268 ∧ x3 = _x269 ∧ x4 = _x270 ∧ x5 = _x271 ∧ _x267 ≤ _x263 ∧ _x272 ≤ _x262 ∧ 1 ≤ _x263 − 1 ∧ 1 ≤ _x267 − 1 f790_0_sortedLow_NONNULL 27 f1022_0_sortedLow_InvokeMethod: x1 = _x273 ∧ x2 = _x274 ∧ x3 = _x275 ∧ x4 = _x276 ∧ x5 = _x277 ∧ x1 = _x278 ∧ x2 = _x279 ∧ x3 = _x280 ∧ x4 = _x281 ∧ x5 = _x282 ∧ _x275 = _x280 ∧ _x281 + 4 ≤ _x274 ∧ _x282 + 2 ≤ _x274 ∧ 1 ≤ _x279 − 1 ∧ 3 ≤ _x278 − 1 ∧ 3 ≤ _x274 − 1 ∧ _x279 ≤ _x274 ∧ _x282 ≤ _x273 ∧ _x278 ≤ _x274 f790_0_sortedLow_NONNULL 28 f1022_0_sortedLow_InvokeMethod: x1 = _x283 ∧ x2 = _x284 ∧ x3 = _x285 ∧ x4 = _x286 ∧ x5 = _x287 ∧ x1 = _x288 ∧ x2 = _x289 ∧ x3 = _x290 ∧ x4 = _x291 ∧ x5 = _x292 ∧ _x285 = _x290 ∧ _x291 + 4 ≤ _x284 ∧ _x292 + 2 ≤ _x284 ∧ 1 ≤ _x289 − 1 ∧ 4 ≤ _x288 − 1 ∧ 4 ≤ _x284 − 1 ∧ _x289 ≤ _x284 ∧ _x292 ≤ _x283 ∧ _x288 ≤ _x284 f1022_0_sortedLow_InvokeMethod 29 f730_0_quicksort_NONNULL: x1 = _x293 ∧ x2 = _x294 ∧ x3 = _x295 ∧ x4 = _x296 ∧ x5 = _x297 ∧ x1 = _x298 ∧ x2 = _x299 ∧ x3 = _x300 ∧ x4 = _x301 ∧ x5 = _x302 ∧ _x297 + 2 ≤ _x294 ∧ _x297 + 2 ≤ _x293 ∧ _x296 + 4 ≤ _x293 ∧ 1 ≤ _x298 − 1 ∧ 1 ≤ _x294 − 1 ∧ 2 ≤ _x293 − 1 ∧ _x298 ≤ _x294 ∧ _x298 ≤ _x293 f1140_0_sortedHigh_NONNULL 30 f1140_0_sortedHigh_NONNULL: x1 = _x303 ∧ x2 = _x304 ∧ x3 = _x305 ∧ x4 = _x306 ∧ x5 = _x307 ∧ x1 = _x308 ∧ x2 = _x309 ∧ x3 = _x310 ∧ x4 = _x311 ∧ x5 = _x312 ∧ _x309 + 1 ≤ _x304 ∧ _x313 ≤ _x303 ∧ 0 ≤ _x304 − 1 ∧ −1 ≤ _x309 − 1 ∧ _x303 = _x308 ∧ _x305 = _x310 f1140_0_sortedHigh_NONNULL 31 f1140_0_sortedHigh_NONNULL: x1 = _x314 ∧ x2 = _x315 ∧ x3 = _x316 ∧ x4 = _x317 ∧ x5 = _x318 ∧ x1 = _x319 ∧ x2 = _x320 ∧ x3 = _x321 ∧ x4 = _x322 ∧ x5 = _x323 ∧ _x320 + 1 ≤ _x315 ∧ _x314 ≤ _x324 − 1 ∧ 0 ≤ _x315 − 1 ∧ −1 ≤ _x320 − 1 ∧ _x314 = _x319 ∧ _x316 = _x321 f1140_0_sortedHigh_NONNULL 32 f1232_0_sortedHigh_InvokeMethod: x1 = _x325 ∧ x2 = _x326 ∧ x3 = _x327 ∧ x4 = _x328 ∧ x5 = _x329 ∧ x1 = _x330 ∧ x2 = _x331 ∧ x3 = _x332 ∧ x4 = _x333 ∧ x5 = _x334 ∧ _x327 = _x332 ∧ _x333 + 4 ≤ _x326 ∧ _x334 + 2 ≤ _x326 ∧ 1 ≤ _x331 − 1 ∧ 3 ≤ _x330 − 1 ∧ 3 ≤ _x326 − 1 ∧ _x331 ≤ _x326 ∧ _x325 ≤ _x334 − 1 ∧ _x330 ≤ _x326 f1140_0_sortedHigh_NONNULL 33 f1232_0_sortedHigh_InvokeMethod: x1 = _x335 ∧ x2 = _x336 ∧ x3 = _x337 ∧ x4 = _x338 ∧ x5 = _x339 ∧ x1 = _x340 ∧ x2 = _x341 ∧ x3 = _x342 ∧ x4 = _x343 ∧ x5 = _x344 ∧ _x337 = _x342 ∧ _x343 + 4 ≤ _x336 ∧ _x344 + 2 ≤ _x336 ∧ 1 ≤ _x341 − 1 ∧ 4 ≤ _x340 − 1 ∧ 4 ≤ _x336 − 1 ∧ _x341 ≤ _x336 ∧ _x335 ≤ _x344 − 1 ∧ _x340 ≤ _x336 f1140_0_sortedHigh_NONNULL 34 f730_0_quicksort_NONNULL: x1 = _x345 ∧ x2 = _x346 ∧ x3 = _x347 ∧ x4 = _x348 ∧ x5 = _x349 ∧ x1 = _x350 ∧ x2 = _x351 ∧ x3 = _x352 ∧ x4 = _x353 ∧ x5 = _x354 ∧ _x350 ≤ _x346 ∧ _x345 ≤ _x355 − 1 ∧ 1 ≤ _x346 − 1 ∧ 1 ≤ _x350 − 1 f1232_0_sortedHigh_InvokeMethod 35 f730_0_quicksort_NONNULL: x1 = _x356 ∧ x2 = _x357 ∧ x3 = _x358 ∧ x4 = _x359 ∧ x5 = _x360 ∧ x1 = _x361 ∧ x2 = _x362 ∧ x3 = _x363 ∧ x4 = _x364 ∧ x5 = _x365 ∧ _x360 + 2 ≤ _x357 ∧ _x360 + 2 ≤ _x356 ∧ _x359 + 4 ≤ _x356 ∧ 1 ≤ _x361 − 1 ∧ 1 ≤ _x357 − 1 ∧ 2 ≤ _x356 − 1 ∧ _x361 ≤ _x357 ∧ _x361 ≤ _x356 f1140_0_sortedHigh_NONNULL 36 f1309_0_sortedHigh_InvokeMethod: x1 = _x366 ∧ x2 = _x367 ∧ x3 = _x368 ∧ x4 = _x369 ∧ x5 = _x370 ∧ x1 = _x371 ∧ x2 = _x372 ∧ x3 = _x373 ∧ x4 = _x374 ∧ x5 = _x375 ∧ _x368 = _x373 ∧ _x374 + 4 ≤ _x367 ∧ _x375 + 2 ≤ _x367 ∧ 1 ≤ _x372 − 1 ∧ 3 ≤ _x371 − 1 ∧ 3 ≤ _x367 − 1 ∧ _x372 ≤ _x367 ∧ _x366 ≤ _x375 − 1 ∧ _x371 ≤ _x367 f1140_0_sortedHigh_NONNULL 37 f1309_0_sortedHigh_InvokeMethod: x1 = _x376 ∧ x2 = _x377 ∧ x3 = _x378 ∧ x4 = _x379 ∧ x5 = _x380 ∧ x1 = _x381 ∧ x2 = _x382 ∧ x3 = _x383 ∧ x4 = _x384 ∧ x5 = _x385 ∧ _x378 = _x383 ∧ _x384 + 4 ≤ _x377 ∧ _x385 + 2 ≤ _x377 ∧ 1 ≤ _x382 − 1 ∧ 4 ≤ _x381 − 1 ∧ 4 ≤ _x377 − 1 ∧ _x382 ≤ _x377 ∧ _x376 ≤ _x385 − 1 ∧ _x381 ≤ _x377 f1309_0_sortedHigh_InvokeMethod 38 f730_0_quicksort_NONNULL: x1 = _x386 ∧ x2 = _x387 ∧ x3 = _x388 ∧ x4 = _x389 ∧ x5 = _x390 ∧ x1 = _x391 ∧ x2 = _x392 ∧ x3 = _x393 ∧ x4 = _x394 ∧ x5 = _x395 ∧ _x390 + 2 ≤ _x387 ∧ _x390 + 2 ≤ _x386 ∧ _x389 + 4 ≤ _x386 ∧ 1 ≤ _x391 − 1 ∧ 1 ≤ _x387 − 1 ∧ 2 ≤ _x386 − 1 ∧ _x391 ≤ _x387 ∧ _x391 ≤ _x386 __init 39 f1_0_main_Load: x1 = _x396 ∧ x2 = _x397 ∧ x3 = _x398 ∧ x4 = _x399 ∧ x5 = _x400 ∧ x1 = _x401 ∧ x2 = _x402 ∧ x3 = _x403 ∧ x4 = _x404 ∧ x5 = _x405 ∧ 0 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 f703_0_main_InvokeMethod f703_0_main_InvokeMethod f703_0_main_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f1232_0_sortedHigh_InvokeMethod f1232_0_sortedHigh_InvokeMethod f1232_0_sortedHigh_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f1140_0_sortedHigh_NONNULL f1140_0_sortedHigh_NONNULL f1140_0_sortedHigh_NONNULL: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f1309_0_sortedHigh_InvokeMethod f1309_0_sortedHigh_InvokeMethod f1309_0_sortedHigh_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f1000_0_quicksort_InvokeMethod f1000_0_quicksort_InvokeMethod f1000_0_quicksort_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f392_0_createList_GT f392_0_createList_GT f392_0_createList_GT: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 __init __init __init: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f730_0_quicksort_NONNULL f730_0_quicksort_NONNULL f730_0_quicksort_NONNULL: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f501_0_createList_InvokeMethod f501_0_createList_InvokeMethod f501_0_createList_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f790_0_sortedLow_NONNULL f790_0_sortedLow_NONNULL f790_0_sortedLow_NONNULL: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f1022_0_sortedLow_InvokeMethod f1022_0_sortedLow_InvokeMethod f1022_0_sortedLow_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f89_0_main_InvokeMethod f89_0_main_InvokeMethod f89_0_main_InvokeMethod: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 f1_0_main_Load f1_0_main_Load f1_0_main_Load: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5
and for every transition t, a duplicate t is considered.

### 2 SCC Decomposition

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

### 2.1 SCC Subproblem 1/2

Here we consider the SCC { f1232_0_sortedHigh_InvokeMethod, f790_0_sortedLow_NONNULL, f1140_0_sortedHigh_NONNULL, f1309_0_sortedHigh_InvokeMethod, f1022_0_sortedLow_InvokeMethod, f1000_0_quicksort_InvokeMethod, f730_0_quicksort_NONNULL }.

### 2.1.1 Transition Removal

We remove transitions 17, 34, 18, 35, 33, 32, 21, 20, 19, 38, 37, 36, 30, 31, 29, 28, 27, 26, 24, 25 using the following ranking functions, which are bounded by 0.

 f730_0_quicksort_NONNULL: −1 + 3⋅x1 f790_0_sortedLow_NONNULL: 1 + 3⋅x2 f1140_0_sortedHigh_NONNULL: 1 + 3⋅x2 f1232_0_sortedHigh_InvokeMethod: 3⋅x1 f1000_0_quicksort_InvokeMethod: −4 + 3⋅x1 f1309_0_sortedHigh_InvokeMethod: 3⋅x1 f1022_0_sortedLow_InvokeMethod: 3⋅x1

### 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/2

Here we consider the SCC { f501_0_createList_InvokeMethod, f392_0_createList_GT }.

### 2.2.1 Transition Removal

We remove transitions 13, 16, 15, 14 using the following ranking functions, which are bounded by 0.

 f392_0_createList_GT: 2⋅x1 f501_0_createList_InvokeMethod: −1 + 2⋅x1

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