LTS Termination Proof

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)