LTS Termination Proof

by AProVE

Input

• 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

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.

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.

2.2.2 Transition Removal

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

2.2.3 Transition Removal

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

2.2.4 Transition Removal

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

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)