LTS Termination Proof

Input

Integer Transition System

Initial Location: f179_0_main_GT, f350_0_fact_GT, f1_0_main_ConstantStackPush, f535_0_main_GT, f535_0_main_GT', __init

Transitions: (pre-variables and post-variables)

f1_0_main_ConstantStackPush	1	f179_0_main_GT:	x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ _arg2 = _arg3P ∧ 0 = _arg2P ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ −1 ≤ _arg2 − 1 ∧ _arg1P ≤ _arg1
f179_0_main_GT	2	f535_0_main_GT:	x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x1 = _x4 ∧ x2 = _x5 ∧ x3 = _x6 ∧ x4 = _x7 ∧ _x2 = _x7 ∧ 0 = _x6 ∧ _x1 = _x5 ∧ 0 ≤ _x4 − 1 ∧ 0 ≤ _x − 1 ∧ _x4 ≤ _x ∧ −1 ≤ _x2 − 1 ∧ _x1 ≤ _x2
f535_0_main_GT	3	f179_0_main_GT:	x1 = _x8 ∧ x2 = _x9 ∧ x3 = _x10 ∧ x4 = _x11 ∧ x1 = _x12 ∧ x2 = _x13 ∧ x3 = _x14 ∧ x4 = _x15 ∧ _x11 = _x14 ∧ _x9 + 1 = _x13 ∧ 0 ≤ _x12 − 1 ∧ 0 ≤ _x8 − 1 ∧ _x12 ≤ _x8 ∧ −1 ≤ _x11 − 1 ∧ _x11 ≤ _x10 − 1
f535_0_main_GT	4	f350_0_fact_GT:	x1 = _x16 ∧ x2 = _x17 ∧ x3 = _x18 ∧ x4 = _x19 ∧ x1 = _x20 ∧ x2 = _x21 ∧ x3 = _x22 ∧ x4 = _x23 ∧ _x18 = _x20 ∧ 0 ≤ _x16 − 1 ∧ _x17 ≤ _x18 − 1 ∧ _x18 ≤ _x19 ∧ _x17 ≤ _x19 ∧ 0 ≤ _x18 − 1
f535_0_main_GT	5	f350_0_fact_GT:	x1 = _x25 ∧ x2 = _x26 ∧ x3 = _x27 ∧ x4 = _x28 ∧ x1 = _x29 ∧ x2 = _x30 ∧ x3 = _x31 ∧ x4 = _x33 ∧ _x26 = _x29 ∧ 0 ≤ _x25 − 1 ∧ _x27 ≤ _x26 ∧ _x27 ≤ _x28 ∧ _x26 ≤ _x28
f535_0_main_GT	6	f350_0_fact_GT:	x1 = _x34 ∧ x2 = _x35 ∧ x3 = _x36 ∧ x4 = _x37 ∧ x1 = _x38 ∧ x2 = _x39 ∧ x3 = _x40 ∧ x4 = _x41 ∧ 0 ≤ _x36 − 1 ∧ _x35 ≤ _x37 ∧ _x36 ≤ _x37 ∧ 0 ≤ _x45 − 1 ∧ _x35 ≤ _x36 − 1 ∧ 0 ≤ _x34 − 1 ∧ _x35 = _x38
f535_0_main_GT	7	f350_0_fact_GT:	x1 = _x46 ∧ x2 = _x47 ∧ x3 = _x48 ∧ x4 = _x49 ∧ x1 = _x50 ∧ x2 = _x51 ∧ x3 = _x52 ∧ x4 = _x53 ∧ _x48 = _x50 ∧ 0 = _x47 ∧ 0 ≤ _x46 − 1 ∧ _x48 ≤ 0 ∧ _x48 ≤ _x49 ∧ −1 ≤ _x49 − 1
f535_0_main_GT	8	f350_0_fact_GT:	x1 = _x54 ∧ x2 = _x55 ∧ x3 = _x58 ∧ x4 = _x59 ∧ x1 = _x60 ∧ x2 = _x61 ∧ x3 = _x65 ∧ x4 = _x66 ∧ _x55 ≤ _x59 ∧ _x58 ≤ _x59 ∧ 0 ≤ _x55 − 1 ∧ 0 ≤ _x67 − 1 ∧ _x58 ≤ _x55 ∧ 0 ≤ _x54 − 1 ∧ _x58 = _x60
f535_0_main_GT	9	f350_0_fact_GT:	x1 = _x68 ∧ x2 = _x69 ∧ x3 = _x70 ∧ x4 = _x71 ∧ x1 = _x72 ∧ x2 = _x73 ∧ x3 = _x74 ∧ x4 = _x75 ∧ 0 ≤ _x70 − 1 ∧ −1 ≤ _x71 − 1 ∧ _x70 ≤ _x71 ∧ 0 ≤ _x76 − 1 ∧ 0 ≤ _x77 − 1 ∧ 0 ≤ _x68 − 1 ∧ 0 = _x69 ∧ _x70 = _x72
f535_0_main_GT	10	f350_0_fact_GT:	x1 = _x78 ∧ x2 = _x79 ∧ x3 = _x80 ∧ x4 = _x81 ∧ x1 = _x82 ∧ x2 = _x83 ∧ x3 = _x84 ∧ x4 = _x85 ∧ 0 ≤ _x80 − 1 ∧ _x79 ≤ _x81 ∧ _x80 ≤ _x81 ∧ 0 ≤ _x86 − 1 ∧ _x79 ≤ _x80 − 1 ∧ 0 ≤ _x87 − 1 ∧ 0 ≤ _x88 − 1 ∧ 0 ≤ _x79 − 1 ∧ 0 ≤ _x78 − 1 ∧ _x80 − _x79 = _x82
f535_0_main_GT	11	f350_0_fact_GT:	x1 = _x89 ∧ x2 = _x90 ∧ x3 = _x91 ∧ x4 = _x92 ∧ x1 = _x93 ∧ x2 = _x94 ∧ x3 = _x95 ∧ x4 = _x99 ∧ 0 − _x91 = _x93 ∧ 0 = _x90 ∧ 0 ≤ _x89 − 1 ∧ _x91 ≤ 0 ∧ _x91 ≤ _x92 ∧ −1 ≤ _x92 − 1
f535_0_main_GT	12	f350_0_fact_GT:	x1 = _x100 ∧ x2 = _x102 ∧ x3 = _x103 ∧ x4 = _x104 ∧ x1 = _x105 ∧ x2 = _x110 ∧ x3 = _x111 ∧ x4 = _x113 ∧ _x103 ≤ _x104 ∧ 0 ≤ _x103 − 1 ∧ −1 ≤ _x104 − 1 ∧ _x103 ≤ 0 ∧ 0 ≤ _x114 − 1 ∧ 0 ≤ _x100 − 1 ∧ 0 = _x102 ∧ 0 − _x103 = _x105
f535_0_main_GT	13	f350_0_fact_GT:	x1 = _x115 ∧ x2 = _x116 ∧ x3 = _x121 ∧ x4 = _x122 ∧ x1 = _x123 ∧ x2 = _x124 ∧ x3 = _x125 ∧ x4 = _x126 ∧ _x116 ≤ _x122 ∧ _x121 ≤ _x122 ∧ 0 ≤ _x116 − 1 ∧ 0 ≤ _x127 − 1 ∧ _x121 ≤ _x116 ∧ 1 ≤ _x116 − _x121 ∧ 0 ≤ _x128 − 1 ∧ _x121 ≤ 0 ∧ 0 ≤ _x115 − 1 ∧ _x116 − _x121 = _x123
f535_0_main_GT	14	f350_0_fact_GT:	x1 = _x129 ∧ x2 = _x130 ∧ x3 = _x131 ∧ x4 = _x133 ∧ x1 = _x134 ∧ x2 = _x135 ∧ x3 = _x136 ∧ x4 = _x138 ∧ _x130 ≤ _x133 ∧ _x131 ≤ _x133 ∧ 0 ≤ _x130 − 1 ∧ 0 ≤ _x139 − 1 ∧ _x131 ≤ _x130 ∧ 0 ≤ _x140 − 1 ∧ 0 ≤ _x141 − 1 ∧ 0 ≤ _x131 − 1 ∧ 0 ≤ _x129 − 1 ∧ _x130 − _x131 = _x134
f535_0_main_GT	15	f535_0_main_GT':	x1 = _x142 ∧ x2 = _x145 ∧ x3 = _x146 ∧ x4 = _x147 ∧ x1 = _x148 ∧ x2 = _x150 ∧ x3 = _x151 ∧ x4 = _x152 ∧ −1 ≤ _x147 − 1 ∧ _x146 ≤ _x147 ∧ _x146 ≤ 0 ∧ _x153 ≤ _x142 ∧ 0 ≤ _x142 − 1 ∧ 0 ≤ _x153 − 1 ∧ 0 = _x145 ∧ _x142 = _x148 ∧ 0 = _x150 ∧ _x146 = _x151 ∧ _x147 = _x152
f535_0_main_GT'	16	f535_0_main_GT:	x1 = _x154 ∧ x2 = _x157 ∧ x3 = _x158 ∧ x4 = _x159 ∧ x1 = _x160 ∧ x2 = _x164 ∧ x3 = _x165 ∧ x4 = _x166 ∧ −1 ≤ _x159 − 1 ∧ _x158 ≤ _x159 ∧ _x158 ≤ 0 ∧ _x160 ≤ _x154 ∧ 0 ≤ _x154 − 1 ∧ 0 ≤ _x160 − 1 ∧ 1 − _x167⋅_x168 ≤ _x167 − 1 ∧ _x167⋅_x168 ≤ 1 ∧ 0 = _x157 ∧ 0 = _x164 ∧ _x158 + 1 = _x165 ∧ _x159 = _x166
f535_0_main_GT	17	f535_0_main_GT':	x1 = _x174 ∧ x2 = _x175 ∧ x3 = _x176 ∧ x4 = _x177 ∧ x1 = _x180 ∧ x2 = _x181 ∧ x3 = _x182 ∧ x4 = _x183 ∧ −1 ≤ _x177 − 1 ∧ _x184 ≤ _x174 ∧ 0 ≤ _x174 − 1 ∧ 0 ≤ _x184 − 1 ∧ 0 = _x175 ∧ 0 = _x176 ∧ _x174 = _x180 ∧ 0 = _x181 ∧ 0 = _x182 ∧ _x177 = _x183
f535_0_main_GT'	18	f535_0_main_GT:	x1 = _x188 ∧ x2 = _x189 ∧ x3 = _x190 ∧ x4 = _x191 ∧ x1 = _x192 ∧ x2 = _x198 ∧ x3 = _x199 ∧ x4 = _x200 ∧ −1 ≤ _x191 − 1 ∧ _x192 ≤ _x188 ∧ 0 ≤ _x188 − 1 ∧ 0 ≤ _x192 − 1 ∧ 1 − _x201⋅_x202 ≤ _x201 − 1 ∧ _x201⋅_x202 ≤ 1 ∧ 0 = _x189 ∧ 0 = _x190 ∧ 0 = _x198 ∧ 1 = _x199 ∧ _x191 = _x200
f535_0_main_GT	19	f535_0_main_GT':	x1 = _x209 ∧ x2 = _x210 ∧ x3 = _x211 ∧ x4 = _x212 ∧ x1 = _x213 ∧ x2 = _x220 ∧ x3 = _x221 ∧ x4 = _x222 ∧ 0 ≤ _x211 − 1 ∧ −1 ≤ _x212 − 1 ∧ _x211 ≤ _x212 ∧ 0 ≤ _x223 − 1 ∧ 0 ≤ _x224 − 1 ∧ _x225 ≤ _x209 ∧ 0 ≤ _x209 − 1 ∧ 0 ≤ _x225 − 1 ∧ 0 = _x210 ∧ _x209 = _x213 ∧ 0 = _x220 ∧ _x211 = _x221 ∧ _x212 = _x222
f535_0_main_GT'	20	f535_0_main_GT:	x1 = _x226 ∧ x2 = _x227 ∧ x3 = _x228 ∧ x4 = _x229 ∧ x1 = _x230 ∧ x2 = _x231 ∧ x3 = _x232 ∧ x4 = _x233 ∧ 0 ≤ _x228 − 1 ∧ −1 ≤ _x229 − 1 ∧ _x228 ≤ _x229 ∧ 0 ≤ _x234 − 1 ∧ 0 ≤ _x235 − 1 ∧ _x230 ≤ _x226 ∧ 0 ≤ _x226 − 1 ∧ 0 ≤ _x230 − 1 ∧ _x236 − _x237⋅_x238 ≤ _x237 − 1 ∧ 0 ≤ _x236 − _x237⋅_x238 ∧ 0 = _x227 ∧ 0 = _x231 ∧ _x228 + 1 = _x232 ∧ _x229 = _x233
f535_0_main_GT	21	f535_0_main_GT':	x1 = _x239 ∧ x2 = _x240 ∧ x3 = _x241 ∧ x4 = _x242 ∧ x1 = _x243 ∧ x2 = _x244 ∧ x3 = _x245 ∧ x4 = _x246 ∧ _x241 ≤ _x242 ∧ 0 ≤ _x241 − 1 ∧ −1 ≤ _x242 − 1 ∧ _x241 ≤ 0 ∧ 0 ≤ _x247 − 1 ∧ _x248 ≤ _x239 ∧ 0 ≤ _x239 − 1 ∧ 0 ≤ _x248 − 1 ∧ 0 = _x240 ∧ _x239 = _x243 ∧ 0 = _x244 ∧ _x241 = _x245 ∧ _x242 = _x246
f535_0_main_GT'	22	f535_0_main_GT:	x1 = _x249 ∧ x2 = _x250 ∧ x3 = _x251 ∧ x4 = _x252 ∧ x1 = _x253 ∧ x2 = _x254 ∧ x3 = _x255 ∧ x4 = _x256 ∧ _x251 ≤ _x252 ∧ 0 ≤ _x251 − 1 ∧ −1 ≤ _x252 − 1 ∧ _x251 ≤ 0 ∧ 0 ≤ _x257 − 1 ∧ _x253 ≤ _x249 ∧ 0 ≤ _x249 − 1 ∧ 0 ≤ _x253 − 1 ∧ 1 − _x258⋅_x259 ≤ _x258 − 1 ∧ _x258⋅_x259 ≤ 1 ∧ 0 = _x250 ∧ 0 = _x254 ∧ _x251 + 1 = _x255 ∧ _x252 = _x256
f535_0_main_GT	23	f535_0_main_GT':	x1 = _x260 ∧ x2 = _x261 ∧ x3 = _x262 ∧ x4 = _x263 ∧ x1 = _x264 ∧ x2 = _x265 ∧ x3 = _x266 ∧ x4 = _x267 ∧ _x261 ≤ _x263 ∧ _x262 ≤ _x263 ∧ 0 ≤ _x261 − 1 ∧ 0 ≤ _x268 − 1 ∧ _x262 ≤ _x261 ∧ 1 ≤ _x261 − _x262 ∧ 0 ≤ _x269 − 1 ∧ _x262 ≤ 0 ∧ −1 ≤ _x263 − 1 ∧ _x270 ≤ _x260 ∧ 0 ≤ _x260 − 1 ∧ 0 ≤ _x270 − 1 ∧ _x260 = _x264 ∧ _x261 = _x265 ∧ _x262 = _x266 ∧ _x263 = _x267
f535_0_main_GT'	24	f535_0_main_GT:	x1 = _x271 ∧ x2 = _x272 ∧ x3 = _x273 ∧ x4 = _x274 ∧ x1 = _x275 ∧ x2 = _x276 ∧ x3 = _x277 ∧ x4 = _x278 ∧ _x272 ≤ _x274 ∧ _x273 ≤ _x274 ∧ 0 ≤ _x272 − 1 ∧ 0 ≤ _x279 − 1 ∧ _x273 ≤ _x272 ∧ 1 ≤ _x272 − _x273 ∧ 0 ≤ _x280 − 1 ∧ _x273 ≤ 0 ∧ −1 ≤ _x274 − 1 ∧ _x275 ≤ _x271 ∧ 0 ≤ _x271 − 1 ∧ 0 ≤ _x275 − 1 ∧ _x281 − _x282⋅_x283 ≤ _x282 − 1 ∧ 0 ≤ _x281 − _x282⋅_x283 ∧ _x272 = _x276 ∧ _x273 + 1 = _x277 ∧ _x274 = _x278
f535_0_main_GT	25	f535_0_main_GT':	x1 = _x284 ∧ x2 = _x285 ∧ x3 = _x286 ∧ x4 = _x287 ∧ x1 = _x288 ∧ x2 = _x289 ∧ x3 = _x290 ∧ x4 = _x291 ∧ 0 ≤ _x286 − 1 ∧ _x285 ≤ _x287 ∧ _x286 ≤ _x287 ∧ 0 ≤ _x292 − 1 ∧ _x285 ≤ _x286 − 1 ∧ 0 ≤ _x293 − 1 ∧ 0 ≤ _x294 − 1 ∧ 0 ≤ _x285 − 1 ∧ −1 ≤ _x287 − 1 ∧ _x295 ≤ _x284 ∧ 0 ≤ _x284 − 1 ∧ 0 ≤ _x295 − 1 ∧ _x284 = _x288 ∧ _x285 = _x289 ∧ _x286 = _x290 ∧ _x287 = _x291
f535_0_main_GT'	26	f535_0_main_GT:	x1 = _x296 ∧ x2 = _x297 ∧ x3 = _x298 ∧ x4 = _x299 ∧ x1 = _x300 ∧ x2 = _x301 ∧ x3 = _x302 ∧ x4 = _x303 ∧ 0 ≤ _x298 − 1 ∧ _x297 ≤ _x299 ∧ _x298 ≤ _x299 ∧ 0 ≤ _x304 − 1 ∧ _x297 ≤ _x298 − 1 ∧ 0 ≤ _x305 − 1 ∧ 0 ≤ _x306 − 1 ∧ 0 ≤ _x297 − 1 ∧ −1 ≤ _x299 − 1 ∧ _x300 ≤ _x296 ∧ 0 ≤ _x296 − 1 ∧ 0 ≤ _x300 − 1 ∧ _x307 − _x308⋅_x309 ≤ _x308 − 1 ∧ 0 ≤ _x307 − _x308⋅_x309 ∧ _x297 = _x301 ∧ _x298 + 1 = _x302 ∧ _x299 = _x303
f535_0_main_GT	27	f535_0_main_GT':	x1 = _x310 ∧ x2 = _x311 ∧ x3 = _x312 ∧ x4 = _x313 ∧ x1 = _x314 ∧ x2 = _x315 ∧ x3 = _x316 ∧ x4 = _x317 ∧ _x311 ≤ _x313 ∧ _x312 ≤ _x313 ∧ 0 ≤ _x311 − 1 ∧ 0 ≤ _x318 − 1 ∧ _x312 ≤ _x311 ∧ 0 ≤ _x319 − 1 ∧ 0 ≤ _x320 − 1 ∧ 0 ≤ _x312 − 1 ∧ −1 ≤ _x313 − 1 ∧ _x321 ≤ _x310 ∧ 0 ≤ _x310 − 1 ∧ 0 ≤ _x321 − 1 ∧ _x310 = _x314 ∧ _x311 = _x315 ∧ _x312 = _x316 ∧ _x313 = _x317
f535_0_main_GT'	28	f535_0_main_GT:	x1 = _x322 ∧ x2 = _x323 ∧ x3 = _x324 ∧ x4 = _x325 ∧ x1 = _x326 ∧ x2 = _x327 ∧ x3 = _x328 ∧ x4 = _x329 ∧ _x323 ≤ _x325 ∧ _x324 ≤ _x325 ∧ 0 ≤ _x323 − 1 ∧ 0 ≤ _x330 − 1 ∧ _x324 ≤ _x323 ∧ 0 ≤ _x331 − 1 ∧ 0 ≤ _x332 − 1 ∧ 0 ≤ _x324 − 1 ∧ −1 ≤ _x325 − 1 ∧ _x326 ≤ _x322 ∧ 0 ≤ _x322 − 1 ∧ 0 ≤ _x326 − 1 ∧ _x333 − _x334⋅_x335 ≤ _x334 − 1 ∧ 0 ≤ _x333 − _x334⋅_x335 ∧ _x323 = _x327 ∧ _x324 + 1 = _x328 ∧ _x325 = _x329
f350_0_fact_GT	29	f350_0_fact_GT:	x1 = _x336 ∧ x2 = _x337 ∧ x3 = _x338 ∧ x4 = _x339 ∧ x1 = _x340 ∧ x2 = _x341 ∧ x3 = _x342 ∧ x4 = _x343 ∧ _x336 − 1 = _x340 ∧ _x336 − 1 ≤ _x336 − 1 ∧ 0 ≤ _x336 − 1
__init	30	f1_0_main_ConstantStackPush:	x1 = _x344 ∧ x2 = _x345 ∧ x3 = _x346 ∧ x4 = _x347 ∧ x1 = _x348 ∧ x2 = _x349 ∧ x3 = _x350 ∧ x4 = _x351 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

f179_0_main_GT	f179_0_main_GT	f179_0_main_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f350_0_fact_GT	f350_0_fact_GT	f350_0_fact_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f1_0_main_ConstantStackPush	f1_0_main_ConstantStackPush	f1_0_main_ConstantStackPush:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f535_0_main_GT	f535_0_main_GT	f535_0_main_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f535_0_main_GT'	f535_0_main_GT'	f535_0_main_GT':	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
__init	__init	__init:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4

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 { f179_0_main_GT, f535_0_main_GT, f535_0_main_GT' }.

2.1.1 Transition Removal

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

f179_0_main_GT:	− x2 + x3
f535_0_main_GT:	−1 − x2 + x4
f535_0_main_GT':	−1 − x2 + x4

2.1.2 Transition Removal

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

f535_0_main_GT:	0
f179_0_main_GT:	−1
f535_0_main_GT':	0

2.1.3 Transition Removal

We remove transitions 16, 15, 18, 17, 20, 19, 22, 21, 24, 23, 26, 25, 28, 27 using the following ranking functions, which are bounded by 0.

f535_0_main_GT':	−2⋅x3 + 2⋅x4
f535_0_main_GT:	1 − 2⋅x3 + 2⋅x4

2.1.4 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 { f350_0_fact_GT }.

2.2.1 Transition Removal

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

f350_0_fact_GT:

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