# LTS Termination Proof

by AProVE

## Input

Integer Transition System
• Initial Location: f826_0_binarySearch_LE', f1076_0_binarySearch_EQ, f242_0_createArray_Return, f826_0_binarySearch_LE, f1078_0_binarySearch_EQ, f382_0_random_ArrayAccess, f1_0_main_Load, f464_0_createArray_GE, __init
• Transitions: (pre-variables and post-variables)  f242_0_createArray_Return 1 f382_0_random_ArrayAccess: 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 ∧ _arg4 = _arg3P ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg2 − 1 ∧ 0 ≤ _arg1 − 1 ∧ _arg1P ≤ _arg2 ∧ _arg1P ≤ _arg1 f1_0_main_Load 2 f382_0_random_ArrayAccess: 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 ∧ _x1 = _x8 ∧ 0 ≤ _x7 − 1 ∧ 0 ≤ _x − 1 ∧ _x7 ≤ _x f1_0_main_Load 3 f464_0_createArray_GE: x1 = _x14 ∧ x2 = _x15 ∧ x3 = _x16 ∧ x4 = _x17 ∧ x5 = _x18 ∧ x6 = _x19 ∧ x7 = _x20 ∧ x1 = _x21 ∧ x2 = _x23 ∧ x3 = _x24 ∧ x4 = _x25 ∧ x5 = _x26 ∧ x6 = _x27 ∧ x7 = _x29 ∧ 1 = _x25 ∧ _x15 = _x24 ∧ 0 = _x23 ∧ 0 ≤ _x21 − 1 ∧ 0 ≤ _x14 − 1 ∧ _x21 ≤ _x14 ∧ 0 ≤ _x15 − 1 ∧ −1 ≤ _x26 − 1 f464_0_createArray_GE 4 f464_0_createArray_GE: x1 = _x30 ∧ x2 = _x31 ∧ x3 = _x32 ∧ x4 = _x33 ∧ x5 = _x34 ∧ x6 = _x35 ∧ x7 = _x36 ∧ x1 = _x37 ∧ x2 = _x38 ∧ x3 = _x39 ∧ x4 = _x40 ∧ x5 = _x41 ∧ x6 = _x42 ∧ x7 = _x43 ∧ _x34 = _x41 ∧ _x33 + 1 = _x40 ∧ _x32 = _x39 ∧ _x31 + 1 = _x38 ∧ 0 ≤ _x37 − 1 ∧ 0 ≤ _x30 − 1 ∧ _x37 ≤ _x30 ∧ −1 ≤ _x34 − 1 ∧ _x31 ≤ _x34 − 1 ∧ 0 ≤ _x33 − 1 ∧ _x33 ≤ _x32 − 1 f382_0_random_ArrayAccess 5 f826_0_binarySearch_LE: x1 = _x44 ∧ x2 = _x45 ∧ x3 = _x46 ∧ x4 = _x47 ∧ x5 = _x48 ∧ x6 = _x49 ∧ x7 = _x50 ∧ x1 = _x51 ∧ x2 = _x52 ∧ x3 = _x53 ∧ x4 = _x54 ∧ x5 = _x55 ∧ x6 = _x56 ∧ x7 = _x57 ∧ _x58 ≤ _x45 − 1 ∧ 0 ≤ _x58 − 1 ∧ −1 ≤ _x53 − 1 ∧ 0 ≤ _x45 − 1 ∧ −1 ≤ _x46 − 1 ∧ 1 ≤ _x59 − 1 ∧ _x52 ≤ _x44 ∧ 0 ≤ _x44 − 1 ∧ 0 ≤ _x51 − 1 ∧ 0 ≤ _x52 − 1 ∧ 0 = _x54 ∧ _x46 = _x55 ∧ _x46 = _x56 f826_0_binarySearch_LE 6 f826_0_binarySearch_LE': x1 = _x60 ∧ x2 = _x61 ∧ x3 = _x62 ∧ x4 = _x63 ∧ x5 = _x64 ∧ x6 = _x65 ∧ x7 = _x66 ∧ x1 = _x67 ∧ x2 = _x68 ∧ x3 = _x69 ∧ x4 = _x70 ∧ x5 = _x71 ∧ x6 = _x73 ∧ x7 = _x74 ∧ _x75 ≤ _x64 − _x63 ∧ −1 ≤ _x63 − 1 ∧ −1 ≤ _x64 − 1 ∧ _x63 ≤ _x64 ∧ −1 ≤ _x75 − 1 ∧ _x63 + _x75 ≤ _x65 − 1 ∧ 1 ≤ _x76 − 1 ∧ 0 ≤ _x63 + _x75 ∧ _x63 + _x75 − 1 ≤ _x63 + _x75 − 1 ∧ _x77 ≤ _x62 − 1 ∧ _x78 ≤ _x60 ∧ _x78 ≤ _x61 ∧ _x79 ≤ _x60 ∧ _x79 ≤ _x61 ∧ 0 ≤ _x60 − 1 ∧ 0 ≤ _x61 − 1 ∧ 0 ≤ _x78 − 1 ∧ 0 ≤ _x79 − 1 ∧ _x60 = _x67 ∧ _x61 = _x68 ∧ _x62 = _x69 ∧ _x63 = _x70 ∧ _x64 = _x71 ∧ _x65 = _x73 f826_0_binarySearch_LE 7 f826_0_binarySearch_LE': x1 = _x80 ∧ x2 = _x81 ∧ x3 = _x82 ∧ x4 = _x84 ∧ x5 = _x85 ∧ x6 = _x86 ∧ x7 = _x87 ∧ x1 = _x88 ∧ x2 = _x89 ∧ x3 = _x90 ∧ x4 = _x91 ∧ x5 = _x92 ∧ x6 = _x93 ∧ x7 = _x95 ∧ _x96 ≤ _x85 − _x84 ∧ −1 ≤ _x84 − 1 ∧ −1 ≤ _x85 − 1 ∧ _x84 ≤ _x85 ∧ −1 ≤ _x96 − 1 ∧ _x84 + _x96 ≤ _x86 − 1 ∧ 1 ≤ _x97 − 1 ∧ 0 ≤ _x84 + _x96 ∧ _x84 + _x96 − 1 ≤ _x84 + _x96 − 1 ∧ _x82 ≤ _x98 − 1 ∧ _x99 ≤ _x80 ∧ _x99 ≤ _x81 ∧ _x100 ≤ _x80 ∧ _x100 ≤ _x81 ∧ 0 ≤ _x80 − 1 ∧ 0 ≤ _x81 − 1 ∧ 0 ≤ _x99 − 1 ∧ 0 ≤ _x100 − 1 ∧ _x80 = _x88 ∧ _x81 = _x89 ∧ _x82 = _x90 ∧ _x84 = _x91 ∧ _x85 = _x92 ∧ _x86 = _x93 f826_0_binarySearch_LE' 8 f826_0_binarySearch_LE: x1 = _x101 ∧ x2 = _x102 ∧ x3 = _x103 ∧ x4 = _x104 ∧ x5 = _x106 ∧ x6 = _x107 ∧ x7 = _x108 ∧ x1 = _x109 ∧ x2 = _x110 ∧ x3 = _x111 ∧ x4 = _x112 ∧ x5 = _x113 ∧ x6 = _x114 ∧ x7 = _x115 ∧ _x116 ≤ _x106 − _x104 ∧ −1 ≤ _x104 − 1 ∧ −1 ≤ _x106 − 1 ∧ _x104 ≤ _x106 ∧ −1 ≤ _x116 − 1 ∧ _x104 + _x116 ≤ _x107 − 1 ∧ 1 ≤ _x117 − 1 ∧ 0 ≤ _x104 + _x116 ∧ _x104 + _x116 − 1 ≤ _x104 + _x116 − 1 ∧ _x118 ≤ _x103 − 1 ∧ _x109 ≤ _x101 ∧ _x109 ≤ _x102 ∧ _x110 ≤ _x101 ∧ _x110 ≤ _x102 ∧ 0 ≤ _x101 − 1 ∧ 0 ≤ _x102 − 1 ∧ 0 ≤ _x109 − 1 ∧ 0 ≤ _x110 − 1 ∧ _x106 − _x104 − 2⋅_x116 ≤ 1 ∧ 0 ≤ _x106 − _x104 − 2⋅_x116 ∧ _x103 = _x111 ∧ _x104 = _x112 ∧ _x104 + _x116 − 1 = _x113 ∧ _x107 = _x114 f826_0_binarySearch_LE' 9 f826_0_binarySearch_LE: x1 = _x119 ∧ x2 = _x120 ∧ x3 = _x121 ∧ x4 = _x122 ∧ x5 = _x124 ∧ x6 = _x125 ∧ x7 = _x126 ∧ x1 = _x127 ∧ x2 = _x128 ∧ x3 = _x129 ∧ x4 = _x130 ∧ x5 = _x131 ∧ x6 = _x132 ∧ x7 = _x133 ∧ _x134 ≤ _x124 − _x122 ∧ −1 ≤ _x122 − 1 ∧ −1 ≤ _x124 − 1 ∧ _x122 ≤ _x124 ∧ −1 ≤ _x134 − 1 ∧ _x122 + _x134 ≤ _x125 − 1 ∧ 1 ≤ _x136 − 1 ∧ 0 ≤ _x122 + _x134 ∧ _x122 + _x134 − 1 ≤ _x122 + _x134 − 1 ∧ _x121 ≤ _x137 − 1 ∧ _x127 ≤ _x119 ∧ _x127 ≤ _x120 ∧ _x128 ≤ _x119 ∧ _x128 ≤ _x120 ∧ 0 ≤ _x119 − 1 ∧ 0 ≤ _x120 − 1 ∧ 0 ≤ _x127 − 1 ∧ 0 ≤ _x128 − 1 ∧ _x124 − _x122 − 2⋅_x134 ≤ 1 ∧ 0 ≤ _x124 − _x122 − 2⋅_x134 ∧ _x121 = _x129 ∧ _x122 = _x130 ∧ _x122 + _x134 − 1 = _x131 ∧ _x125 = _x132 f826_0_binarySearch_LE 10 f826_0_binarySearch_LE': x1 = _x138 ∧ x2 = _x139 ∧ x3 = _x140 ∧ x4 = _x141 ∧ x5 = _x142 ∧ x6 = _x143 ∧ x7 = _x144 ∧ x1 = _x150 ∧ x2 = _x151 ∧ x3 = _x152 ∧ x4 = _x153 ∧ x5 = _x154 ∧ x6 = _x155 ∧ x7 = _x156 ∧ _x157 ≤ _x142 − _x141 ∧ −1 ≤ _x141 − 1 ∧ −1 ≤ _x142 − 1 ∧ _x141 ≤ _x142 ∧ −1 ≤ _x157 − 1 ∧ _x141 + _x157 ≤ _x143 − 1 ∧ 1 ≤ _x161 − 1 ∧ 0 ≤ _x141 + _x157 ∧ _x141 + _x157 − 1 ≤ _x141 + _x157 − 1 ∧ _x162 ≤ _x140 − 1 ∧ _x163 ≤ _x138 ∧ _x163 ≤ _x139 ∧ 0 ≤ _x138 − 1 ∧ 0 ≤ _x139 − 1 ∧ 0 ≤ _x163 − 1 ∧ _x138 = _x150 ∧ _x139 = _x151 ∧ _x140 = _x152 ∧ _x141 = _x153 ∧ _x142 = _x154 ∧ _x143 = _x155 f826_0_binarySearch_LE 11 f826_0_binarySearch_LE': x1 = _x164 ∧ x2 = _x165 ∧ x3 = _x166 ∧ x4 = _x167 ∧ x5 = _x168 ∧ x6 = _x172 ∧ x7 = _x173 ∧ x1 = _x174 ∧ x2 = _x175 ∧ x3 = _x176 ∧ x4 = _x177 ∧ x5 = _x178 ∧ x6 = _x179 ∧ x7 = _x180 ∧ _x181 ≤ _x168 − _x167 ∧ −1 ≤ _x167 − 1 ∧ −1 ≤ _x168 − 1 ∧ _x167 ≤ _x168 ∧ −1 ≤ _x181 − 1 ∧ _x167 + _x181 ≤ _x172 − 1 ∧ 1 ≤ _x182 − 1 ∧ 0 ≤ _x167 + _x181 ∧ _x167 + _x181 − 1 ≤ _x167 + _x181 − 1 ∧ _x166 ≤ _x183 − 1 ∧ _x184 ≤ _x164 ∧ _x184 ≤ _x165 ∧ 0 ≤ _x164 − 1 ∧ 0 ≤ _x165 − 1 ∧ 0 ≤ _x184 − 1 ∧ _x164 = _x174 ∧ _x165 = _x175 ∧ _x166 = _x176 ∧ _x167 = _x177 ∧ _x168 = _x178 ∧ _x172 = _x179 f826_0_binarySearch_LE' 12 f1076_0_binarySearch_EQ: x1 = _x185 ∧ x2 = _x186 ∧ x3 = _x187 ∧ x4 = _x188 ∧ x5 = _x189 ∧ x6 = _x190 ∧ x7 = _x191 ∧ x1 = _x192 ∧ x2 = _x193 ∧ x3 = _x194 ∧ x4 = _x195 ∧ x5 = _x196 ∧ x6 = _x197 ∧ x7 = _x198 ∧ _x199 ≤ _x189 − _x188 ∧ −1 ≤ _x188 − 1 ∧ −1 ≤ _x189 − 1 ∧ _x188 ≤ _x189 ∧ −1 ≤ _x199 − 1 ∧ _x188 + _x199 ≤ _x190 − 1 ∧ 1 ≤ _x200 − 1 ∧ 0 ≤ _x188 + _x199 ∧ _x188 + _x199 − 1 ≤ _x188 + _x199 − 1 ∧ _x201 ≤ _x187 − 1 ∧ _x192 ≤ _x185 ∧ _x192 ≤ _x186 ∧ 0 ≤ _x185 − 1 ∧ 0 ≤ _x186 − 1 ∧ 0 ≤ _x192 − 1 ∧ _x189 − _x188 − 2⋅_x199 ≤ 1 ∧ 0 ≤ _x189 − _x188 − 2⋅_x199 ∧ _x187 = _x193 ∧ _x189 = _x194 ∧ _x188 + _x199 = _x195 ∧ 0 = _x196 ∧ _x190 = _x198 f826_0_binarySearch_LE' 13 f1076_0_binarySearch_EQ: x1 = _x202 ∧ x2 = _x203 ∧ x3 = _x204 ∧ x4 = _x205 ∧ x5 = _x206 ∧ x6 = _x207 ∧ x7 = _x208 ∧ x1 = _x209 ∧ x2 = _x210 ∧ x3 = _x211 ∧ x4 = _x212 ∧ x5 = _x213 ∧ x6 = _x214 ∧ x7 = _x215 ∧ _x216 ≤ _x206 − _x205 ∧ −1 ≤ _x205 − 1 ∧ −1 ≤ _x206 − 1 ∧ _x205 ≤ _x206 ∧ −1 ≤ _x216 − 1 ∧ _x205 + _x216 ≤ _x207 − 1 ∧ 1 ≤ _x217 − 1 ∧ 0 ≤ _x205 + _x216 ∧ _x205 + _x216 − 1 ≤ _x205 + _x216 − 1 ∧ _x204 ≤ _x218 − 1 ∧ _x209 ≤ _x202 ∧ _x209 ≤ _x203 ∧ 0 ≤ _x202 − 1 ∧ 0 ≤ _x203 − 1 ∧ 0 ≤ _x209 − 1 ∧ _x206 − _x205 − 2⋅_x216 ≤ 1 ∧ 0 ≤ _x206 − _x205 − 2⋅_x216 ∧ _x204 = _x210 ∧ _x206 = _x211 ∧ _x205 + _x216 = _x212 ∧ 0 = _x213 ∧ _x207 = _x215 f826_0_binarySearch_LE' 14 f1078_0_binarySearch_EQ: x1 = _x219 ∧ x2 = _x220 ∧ x3 = _x221 ∧ x4 = _x226 ∧ x5 = _x227 ∧ x6 = _x228 ∧ x7 = _x229 ∧ x1 = _x230 ∧ x2 = _x231 ∧ x3 = _x236 ∧ x4 = _x237 ∧ x5 = _x238 ∧ x6 = _x239 ∧ x7 = _x240 ∧ _x241 ≤ _x227 − _x226 ∧ −1 ≤ _x226 − 1 ∧ −1 ≤ _x227 − 1 ∧ _x226 ≤ _x227 ∧ −1 ≤ _x241 − 1 ∧ _x226 + _x241 ≤ _x228 − 1 ∧ 1 ≤ _x242 − 1 ∧ 0 ≤ _x226 + _x241 ∧ _x226 + _x241 − 1 ≤ _x226 + _x241 − 1 ∧ _x244 ≤ _x221 − 1 ∧ _x230 ≤ _x219 ∧ _x230 ≤ _x220 ∧ 0 ≤ _x219 − 1 ∧ 0 ≤ _x220 − 1 ∧ 0 ≤ _x230 − 1 ∧ _x227 − _x226 − 2⋅_x241 ≤ 1 ∧ 0 ≤ _x227 − _x226 − 2⋅_x241 ∧ _x221 = _x231 ∧ _x227 = _x236 ∧ _x226 + _x241 = _x237 ∧ 0 = _x238 ∧ _x228 = _x240 f826_0_binarySearch_LE' 15 f1078_0_binarySearch_EQ: x1 = _x247 ∧ x2 = _x248 ∧ x3 = _x249 ∧ x4 = _x250 ∧ x5 = _x251 ∧ x6 = _x252 ∧ x7 = _x253 ∧ x1 = _x255 ∧ x2 = _x258 ∧ x3 = _x259 ∧ x4 = _x260 ∧ x5 = _x261 ∧ x6 = _x262 ∧ x7 = _x263 ∧ _x264 ≤ _x251 − _x250 ∧ −1 ≤ _x250 − 1 ∧ −1 ≤ _x251 − 1 ∧ _x250 ≤ _x251 ∧ −1 ≤ _x264 − 1 ∧ _x250 + _x264 ≤ _x252 − 1 ∧ 1 ≤ _x265 − 1 ∧ 0 ≤ _x250 + _x264 ∧ _x250 + _x264 − 1 ≤ _x250 + _x264 − 1 ∧ _x249 ≤ _x266 − 1 ∧ _x255 ≤ _x247 ∧ _x255 ≤ _x248 ∧ 0 ≤ _x247 − 1 ∧ 0 ≤ _x248 − 1 ∧ 0 ≤ _x255 − 1 ∧ _x251 − _x250 − 2⋅_x264 ≤ 1 ∧ 0 ≤ _x251 − _x250 − 2⋅_x264 ∧ _x249 = _x258 ∧ _x251 = _x259 ∧ _x250 + _x264 = _x260 ∧ 0 = _x261 ∧ _x252 = _x263 f826_0_binarySearch_LE' 16 f1076_0_binarySearch_EQ: x1 = _x267 ∧ x2 = _x268 ∧ x3 = _x269 ∧ x4 = _x270 ∧ x5 = _x271 ∧ x6 = _x272 ∧ x7 = _x273 ∧ x1 = _x274 ∧ x2 = _x275 ∧ x3 = _x276 ∧ x4 = _x277 ∧ x5 = _x278 ∧ x6 = _x279 ∧ x7 = _x280 ∧ _x281 ≤ _x271 − _x270 ∧ −1 ≤ _x270 − 1 ∧ −1 ≤ _x271 − 1 ∧ _x270 ≤ _x271 ∧ −1 ≤ _x281 − 1 ∧ _x270 + _x281 ≤ _x272 − 1 ∧ 1 ≤ _x282 − 1 ∧ 0 ≤ _x270 + _x281 ∧ _x270 + _x281 − 1 ≤ _x270 + _x281 − 1 ∧ _x283 ≤ _x269 − 1 ∧ _x274 ≤ _x267 ∧ _x274 ≤ _x268 ∧ 0 ≤ _x267 − 1 ∧ 0 ≤ _x268 − 1 ∧ 0 ≤ _x274 − 1 ∧ _x271 − _x270 − 2⋅_x281 ≤ 1 ∧ 0 ≤ _x271 − _x270 − 2⋅_x281 ∧ _x269 = _x275 ∧ _x271 = _x276 ∧ _x270 + _x281 = _x277 ∧ 1 = _x278 ∧ _x272 = _x280 f826_0_binarySearch_LE' 17 f1076_0_binarySearch_EQ: x1 = _x284 ∧ x2 = _x286 ∧ x3 = _x289 ∧ x4 = _x290 ∧ x5 = _x291 ∧ x6 = _x292 ∧ x7 = _x293 ∧ x1 = _x294 ∧ x2 = _x295 ∧ x3 = _x297 ∧ x4 = _x300 ∧ x5 = _x301 ∧ x6 = _x302 ∧ x7 = _x303 ∧ _x304 ≤ _x291 − _x290 ∧ −1 ≤ _x290 − 1 ∧ −1 ≤ _x291 − 1 ∧ _x290 ≤ _x291 ∧ −1 ≤ _x304 − 1 ∧ _x290 + _x304 ≤ _x292 − 1 ∧ 1 ≤ _x305 − 1 ∧ 0 ≤ _x290 + _x304 ∧ _x290 + _x304 − 1 ≤ _x290 + _x304 − 1 ∧ _x289 ≤ _x306 − 1 ∧ _x294 ≤ _x284 ∧ _x294 ≤ _x286 ∧ 0 ≤ _x284 − 1 ∧ 0 ≤ _x286 − 1 ∧ 0 ≤ _x294 − 1 ∧ _x291 − _x290 − 2⋅_x304 ≤ 1 ∧ 0 ≤ _x291 − _x290 − 2⋅_x304 ∧ _x289 = _x295 ∧ _x291 = _x297 ∧ _x290 + _x304 = _x300 ∧ 1 = _x301 ∧ _x292 = _x303 f826_0_binarySearch_LE' 18 f1078_0_binarySearch_EQ: x1 = _x307 ∧ x2 = _x308 ∧ x3 = _x309 ∧ x4 = _x310 ∧ x5 = _x311 ∧ x6 = _x312 ∧ x7 = _x313 ∧ x1 = _x314 ∧ x2 = _x315 ∧ x3 = _x316 ∧ x4 = _x317 ∧ x5 = _x318 ∧ x6 = _x319 ∧ x7 = _x320 ∧ _x321 ≤ _x311 − _x310 ∧ −1 ≤ _x310 − 1 ∧ −1 ≤ _x311 − 1 ∧ _x310 ≤ _x311 ∧ −1 ≤ _x321 − 1 ∧ _x310 + _x321 ≤ _x312 − 1 ∧ 1 ≤ _x322 − 1 ∧ 0 ≤ _x310 + _x321 ∧ _x310 + _x321 − 1 ≤ _x310 + _x321 − 1 ∧ _x323 ≤ _x309 − 1 ∧ _x314 ≤ _x307 ∧ _x314 ≤ _x308 ∧ 0 ≤ _x307 − 1 ∧ 0 ≤ _x308 − 1 ∧ 0 ≤ _x314 − 1 ∧ _x311 − _x310 − 2⋅_x321 ≤ 1 ∧ 0 ≤ _x311 − _x310 − 2⋅_x321 ∧ _x309 = _x315 ∧ _x311 = _x316 ∧ _x310 + _x321 = _x317 ∧ 1 = _x318 ∧ _x312 = _x320 f826_0_binarySearch_LE' 19 f1078_0_binarySearch_EQ: x1 = _x324 ∧ x2 = _x325 ∧ x3 = _x326 ∧ x4 = _x328 ∧ x5 = _x331 ∧ x6 = _x332 ∧ x7 = _x333 ∧ x1 = _x334 ∧ x2 = _x335 ∧ x3 = _x336 ∧ x4 = _x337 ∧ x5 = _x339 ∧ x6 = _x342 ∧ x7 = _x343 ∧ _x344 ≤ _x331 − _x328 ∧ −1 ≤ _x328 − 1 ∧ −1 ≤ _x331 − 1 ∧ _x328 ≤ _x331 ∧ −1 ≤ _x344 − 1 ∧ _x328 + _x344 ≤ _x332 − 1 ∧ 1 ≤ _x345 − 1 ∧ 0 ≤ _x328 + _x344 ∧ _x328 + _x344 − 1 ≤ _x328 + _x344 − 1 ∧ _x326 ≤ _x346 − 1 ∧ _x334 ≤ _x324 ∧ _x334 ≤ _x325 ∧ 0 ≤ _x324 − 1 ∧ 0 ≤ _x325 − 1 ∧ 0 ≤ _x334 − 1 ∧ _x331 − _x328 − 2⋅_x344 ≤ 1 ∧ 0 ≤ _x331 − _x328 − 2⋅_x344 ∧ _x326 = _x335 ∧ _x331 = _x336 ∧ _x328 + _x344 = _x337 ∧ 1 = _x339 ∧ _x332 = _x343 f1078_0_binarySearch_EQ 20 f826_0_binarySearch_LE: x1 = _x347 ∧ x2 = _x348 ∧ x3 = _x349 ∧ x4 = _x350 ∧ x5 = _x351 ∧ x6 = _x352 ∧ x7 = _x353 ∧ x1 = _x354 ∧ x2 = _x355 ∧ x3 = _x356 ∧ x4 = _x357 ∧ x5 = _x358 ∧ x6 = _x359 ∧ x7 = _x360 ∧ 1 ≤ _x361 − 1 ∧ −1 ≤ _x350 − 1 ∧ _x354 ≤ _x347 ∧ _x355 ≤ _x347 ∧ 0 ≤ _x347 − 1 ∧ 0 ≤ _x354 − 1 ∧ 0 ≤ _x355 − 1 ∧ 0 = _x351 ∧ _x348 = _x356 ∧ _x350 + 1 = _x357 ∧ _x349 = _x358 ∧ _x353 = _x359 f1076_0_binarySearch_EQ 21 f826_0_binarySearch_LE: x1 = _x362 ∧ x2 = _x363 ∧ x3 = _x364 ∧ x4 = _x365 ∧ x5 = _x366 ∧ x6 = _x367 ∧ x7 = _x368 ∧ x1 = _x370 ∧ x2 = _x373 ∧ x3 = _x374 ∧ x4 = _x375 ∧ x5 = _x376 ∧ x6 = _x377 ∧ x7 = _x378 ∧ 1 ≤ _x379 − 1 ∧ −1 ≤ _x365 − 1 ∧ _x370 ≤ _x362 ∧ _x373 ≤ _x362 ∧ 0 ≤ _x362 − 1 ∧ 0 ≤ _x370 − 1 ∧ 0 ≤ _x373 − 1 ∧ 0 = _x366 ∧ _x363 = _x374 ∧ _x365 + 1 = _x375 ∧ _x364 = _x376 ∧ _x368 = _x377 f826_0_binarySearch_LE' 22 f1076_0_binarySearch_EQ: x1 = _x381 ∧ x2 = _x384 ∧ x3 = _x385 ∧ x4 = _x386 ∧ x5 = _x387 ∧ x6 = _x388 ∧ x7 = _x389 ∧ x1 = _x390 ∧ x2 = _x391 ∧ x3 = _x392 ∧ x4 = _x394 ∧ x5 = _x395 ∧ x6 = _x396 ∧ x7 = _x397 ∧ _x398 ≤ _x387 − _x386 ∧ −1 ≤ _x386 − 1 ∧ −1 ≤ _x387 − 1 ∧ _x386 ≤ _x387 ∧ −1 ≤ _x398 − 1 ∧ _x386 + _x398 ≤ _x388 − 1 ∧ 1 ≤ _x399 − 1 ∧ 0 ≤ _x386 + _x398 ∧ _x386 + _x398 − 1 ≤ _x386 + _x398 − 1 ∧ _x400 ≤ _x385 − 1 ∧ _x390 ≤ _x381 ∧ _x390 ≤ _x384 ∧ 0 ≤ _x381 − 1 ∧ 0 ≤ _x384 − 1 ∧ 0 ≤ _x390 − 1 ∧ _x387 − _x386 − 2⋅_x398 ≤ 1 ∧ 0 ≤ _x387 − _x386 − 2⋅_x398 ∧ _x385 = _x391 ∧ _x387 = _x392 ∧ _x386 + _x398 = _x394 ∧ _x388 = _x397 f826_0_binarySearch_LE' 23 f1076_0_binarySearch_EQ: x1 = _x401 ∧ x2 = _x402 ∧ x3 = _x403 ∧ x4 = _x404 ∧ x5 = _x405 ∧ x6 = _x406 ∧ x7 = _x407 ∧ x1 = _x408 ∧ x2 = _x409 ∧ x3 = _x410 ∧ x4 = _x411 ∧ x5 = _x412 ∧ x6 = _x413 ∧ x7 = _x414 ∧ _x415 ≤ _x405 − _x404 ∧ −1 ≤ _x404 − 1 ∧ −1 ≤ _x405 − 1 ∧ _x404 ≤ _x405 ∧ −1 ≤ _x415 − 1 ∧ _x404 + _x415 ≤ _x406 − 1 ∧ 1 ≤ _x416 − 1 ∧ 0 ≤ _x404 + _x415 ∧ _x404 + _x415 − 1 ≤ _x404 + _x415 − 1 ∧ _x403 ≤ _x417 − 1 ∧ _x408 ≤ _x401 ∧ _x408 ≤ _x402 ∧ 0 ≤ _x401 − 1 ∧ 0 ≤ _x402 − 1 ∧ 0 ≤ _x408 − 1 ∧ _x405 − _x404 − 2⋅_x415 ≤ 1 ∧ 0 ≤ _x405 − _x404 − 2⋅_x415 ∧ _x403 = _x409 ∧ _x405 = _x410 ∧ _x404 + _x415 = _x411 ∧ _x406 = _x414 f826_0_binarySearch_LE' 24 f1078_0_binarySearch_EQ: x1 = _x418 ∧ x2 = _x419 ∧ x3 = _x420 ∧ x4 = _x422 ∧ x5 = _x423 ∧ x6 = _x426 ∧ x7 = _x427 ∧ x1 = _x428 ∧ x2 = _x429 ∧ x3 = _x430 ∧ x4 = _x431 ∧ x5 = _x432 ∧ x6 = _x434 ∧ x7 = _x435 ∧ _x438 ≤ _x423 − _x422 ∧ −1 ≤ _x422 − 1 ∧ −1 ≤ _x423 − 1 ∧ _x422 ≤ _x423 ∧ −1 ≤ _x438 − 1 ∧ _x422 + _x438 ≤ _x426 − 1 ∧ 1 ≤ _x439 − 1 ∧ 0 ≤ _x422 + _x438 ∧ _x422 + _x438 − 1 ≤ _x422 + _x438 − 1 ∧ _x440 ≤ _x420 − 1 ∧ _x428 ≤ _x418 ∧ _x428 ≤ _x419 ∧ 0 ≤ _x418 − 1 ∧ 0 ≤ _x419 − 1 ∧ 0 ≤ _x428 − 1 ∧ _x423 − _x422 − 2⋅_x438 ≤ 1 ∧ 0 ≤ _x423 − _x422 − 2⋅_x438 ∧ _x420 = _x429 ∧ _x423 = _x430 ∧ _x422 + _x438 = _x431 ∧ _x426 = _x435 f826_0_binarySearch_LE' 25 f1078_0_binarySearch_EQ: x1 = _x441 ∧ x2 = _x442 ∧ x3 = _x443 ∧ x4 = _x444 ∧ x5 = _x445 ∧ x6 = _x446 ∧ x7 = _x447 ∧ x1 = _x448 ∧ x2 = _x449 ∧ x3 = _x450 ∧ x4 = _x451 ∧ x5 = _x452 ∧ x6 = _x453 ∧ x7 = _x454 ∧ _x455 ≤ _x445 − _x444 ∧ −1 ≤ _x444 − 1 ∧ −1 ≤ _x445 − 1 ∧ _x444 ≤ _x445 ∧ −1 ≤ _x455 − 1 ∧ _x444 + _x455 ≤ _x446 − 1 ∧ 1 ≤ _x456 − 1 ∧ 0 ≤ _x444 + _x455 ∧ _x444 + _x455 − 1 ≤ _x444 + _x455 − 1 ∧ _x443 ≤ _x457 − 1 ∧ _x448 ≤ _x441 ∧ _x448 ≤ _x442 ∧ 0 ≤ _x441 − 1 ∧ 0 ≤ _x442 − 1 ∧ 0 ≤ _x448 − 1 ∧ _x445 − _x444 − 2⋅_x455 ≤ 1 ∧ 0 ≤ _x445 − _x444 − 2⋅_x455 ∧ _x443 = _x449 ∧ _x445 = _x450 ∧ _x444 + _x455 = _x451 ∧ _x446 = _x454 __init 26 f1_0_main_Load: x1 = _x458 ∧ x2 = _x459 ∧ x3 = _x460 ∧ x4 = _x461 ∧ x5 = _x462 ∧ x6 = _x463 ∧ x7 = _x464 ∧ x1 = _x466 ∧ x2 = _x467 ∧ x3 = _x470 ∧ x4 = _x471 ∧ x5 = _x472 ∧ x6 = _x473 ∧ x7 = _x474 ∧ 0 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 f826_0_binarySearch_LE' f826_0_binarySearch_LE' f826_0_binarySearch_LE': x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f1076_0_binarySearch_EQ f1076_0_binarySearch_EQ f1076_0_binarySearch_EQ: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f242_0_createArray_Return f242_0_createArray_Return f242_0_createArray_Return: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f826_0_binarySearch_LE f826_0_binarySearch_LE f826_0_binarySearch_LE: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f1078_0_binarySearch_EQ f1078_0_binarySearch_EQ f1078_0_binarySearch_EQ: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 f382_0_random_ArrayAccess f382_0_random_ArrayAccess f382_0_random_ArrayAccess: 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 f464_0_createArray_GE f464_0_createArray_GE f464_0_createArray_GE: 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
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 { f464_0_createArray_GE }.

### 2.1.1 Transition Removal

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

 f464_0_createArray_GE: − x4 + x3

### 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 { f826_0_binarySearch_LE', f1076_0_binarySearch_EQ, f826_0_binarySearch_LE, f1078_0_binarySearch_EQ }.

### 2.2.1 Transition Removal

We remove transitions 6, 8, 7, 9, 10, 25, 24, 19, 18, 15, 14, 23, 22, 17, 16, 12 using the following ranking functions, which are bounded by 0.

 f826_0_binarySearch_LE: −3⋅x4 + 2⋅x5 + 2⋅x6 + 2 f826_0_binarySearch_LE': −3⋅x4 + 2⋅x5 + 2⋅x6 + 1 f1078_0_binarySearch_EQ: −3⋅x4 + 2⋅x3 + 2⋅x7 f1076_0_binarySearch_EQ: −3⋅x4 + 2⋅x3 + 2⋅x7

### 2.2.2 Transition Removal

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

 f1078_0_binarySearch_EQ: 0⋅x5 f826_0_binarySearch_LE: −1 f826_0_binarySearch_LE': −1 f1076_0_binarySearch_EQ: −1 + 0⋅x5

### 2.2.3 Transition Removal

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

 f826_0_binarySearch_LE: −3⋅x4 + 3⋅x6 f826_0_binarySearch_LE': −3⋅x4 + 3⋅x6 − 1 f1076_0_binarySearch_EQ: −3⋅x4 + 3⋅x7 − 2

### 2.2.4 Transition Removal

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

 f1076_0_binarySearch_EQ: 0⋅x5 f826_0_binarySearch_LE: −1

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