LTS Termination Proof

Input

Integer Transition System

Initial Location: f319_0_main_GE, f862_0_cos_GT, f861_0_sin_GT, f165_0_main_GE, f862_0_cos_GT', f1_0_main_ConstantStackPush, f1049_0_fact_Return', f165_0_main_GE', f544_0_exp_GT', __init, f1011_0_power_GT, f1048_0_fact_Return, f765_0_fact_Return, f544_0_exp_GT, f861_0_sin_GT', f1113_0_fact_GT, f1049_0_fact_Return

Transitions: (pre-variables and post-variables)

f1_0_main_ConstantStackPush	1	f165_0_main_GE:	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
f165_0_main_GE	2	f165_0_main_GE':	x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x1 = _x4 ∧ x2 = _x5 ∧ x3 = _x6 ∧ x4 = _x7 ∧ _x1 − 2⋅_x8 = 1 ∧ _x1 ≤ _x2 − 1 ∧ 0 ≤ _x1 − 5⋅_x9 − 1 ∧ 0 ≤ _x1 − 3⋅_x10 − 1 ∧ _x11 ≤ _x ∧ 0 ≤ _x − 1 ∧ 0 ≤ _x11 − 1 ∧ _x = _x4 ∧ _x1 = _x5 ∧ _x2 = _x6
f165_0_main_GE'	3	f319_0_main_GE:	x1 = _x12 ∧ x2 = _x13 ∧ x3 = _x14 ∧ x4 = _x15 ∧ x1 = _x16 ∧ x2 = _x17 ∧ x3 = _x18 ∧ x4 = _x19 ∧ 0 ≤ _x13 − 5⋅_x20 − 1 ∧ 0 ≤ _x13 − 3⋅_x21 − 1 ∧ _x13 − 2⋅_x22 = 1 ∧ _x13 ≤ _x14 − 1 ∧ _x16 ≤ _x12 ∧ 0 ≤ _x12 − 1 ∧ 0 ≤ _x16 − 1 ∧ 0 ≤ _x13 − 2⋅_x22 ∧ _x13 − 2⋅_x22 ≤ 1 ∧ _x13 − 3⋅_x21 ≤ 2 ∧ _x13 − 5⋅_x20 ≤ 4 ∧ _x13 = _x17 ∧ 0 = _x18 ∧ _x14 = _x19
f319_0_main_GE	4	f319_0_main_GE:	x1 = _x23 ∧ x2 = _x24 ∧ x3 = _x25 ∧ x4 = _x26 ∧ x1 = _x27 ∧ x2 = _x28 ∧ x3 = _x29 ∧ x4 = _x30 ∧ _x26 = _x30 ∧ _x25 + 1 = _x29 ∧ _x24 = _x28 ∧ 0 ≤ _x27 − 1 ∧ 0 ≤ _x23 − 1 ∧ _x25 ≤ 99 ∧ _x27 ≤ _x23
f319_0_main_GE	5	f165_0_main_GE:	x1 = _x31 ∧ x2 = _x32 ∧ x3 = _x33 ∧ x4 = _x34 ∧ x1 = _x35 ∧ x2 = _x36 ∧ x3 = _x38 ∧ x4 = _x39 ∧ _x34 = _x38 ∧ _x32 + 1 = _x36 ∧ 0 ≤ _x35 − 1 ∧ 0 ≤ _x31 − 1 ∧ _x35 ≤ _x31 ∧ 99 ≤ _x33 − 1 ∧ −1 ≤ _x34 − 1
f165_0_main_GE	6	f165_0_main_GE':	x1 = _x40 ∧ x2 = _x41 ∧ x3 = _x42 ∧ x4 = _x43 ∧ x1 = _x44 ∧ x2 = _x45 ∧ x3 = _x46 ∧ x4 = _x47 ∧ _x41 ≤ _x42 − 1 ∧ 0 ≤ _x42 − 1 ∧ _x41 − 2⋅_x48 = 1 ∧ 0 ≤ _x41 − 3⋅_x49 − 1 ∧ _x41 − 5⋅_x50 = 0 ∧ _x52 ≤ _x40 ∧ 0 ≤ _x40 − 1 ∧ 0 ≤ _x52 − 1 ∧ _x40 = _x44 ∧ _x41 = _x45 ∧ _x42 = _x46
f165_0_main_GE'	7	f165_0_main_GE:	x1 = _x53 ∧ x2 = _x55 ∧ x3 = _x56 ∧ x4 = _x57 ∧ x1 = _x58 ∧ x2 = _x59 ∧ x3 = _x60 ∧ x4 = _x61 ∧ 0 ≤ _x55 − 3⋅_x62 − 1 ∧ _x55 ≤ _x56 − 1 ∧ 0 ≤ _x56 − 1 ∧ _x55 − 2⋅_x63 = 1 ∧ _x55 − 5⋅_x65 = 0 ∧ _x58 ≤ _x53 ∧ 0 ≤ _x53 − 1 ∧ 0 ≤ _x58 − 1 ∧ 0 ≤ _x55 − 2⋅_x63 ∧ _x55 − 2⋅_x63 ≤ 1 ∧ _x55 − 3⋅_x62 ≤ 2 ∧ _x55 − 5⋅_x65 ≤ 4 ∧ 0 ≤ _x55 − 5⋅_x65 ∧ _x55 + 1 = _x59 ∧ _x56 = _x60
f165_0_main_GE	8	f165_0_main_GE':	x1 = _x67 ∧ x2 = _x68 ∧ x3 = _x70 ∧ x4 = _x71 ∧ x1 = _x72 ∧ x2 = _x73 ∧ x3 = _x74 ∧ x4 = _x75 ∧ _x68 ≤ _x70 − 1 ∧ 0 ≤ _x70 − 1 ∧ _x68 − 2⋅_x76 = 0 ∧ _x77 ≤ _x67 ∧ 0 ≤ _x67 − 1 ∧ 0 ≤ _x77 − 1 ∧ _x67 = _x72 ∧ _x68 = _x73 ∧ _x70 = _x74
f165_0_main_GE'	9	f165_0_main_GE:	x1 = _x78 ∧ x2 = _x79 ∧ x3 = _x80 ∧ x4 = _x81 ∧ x1 = _x82 ∧ x2 = _x83 ∧ x3 = _x84 ∧ x4 = _x85 ∧ _x79 ≤ _x80 − 1 ∧ 0 ≤ _x80 − 1 ∧ _x79 − 2⋅_x86 = 0 ∧ _x82 ≤ _x78 ∧ 0 ≤ _x78 − 1 ∧ 0 ≤ _x82 − 1 ∧ _x79 − 2⋅_x86 ≤ 1 ∧ 0 ≤ _x79 − 2⋅_x86 ∧ _x79 + 1 = _x83 ∧ _x80 = _x84
f165_0_main_GE	10	f165_0_main_GE':	x1 = _x87 ∧ x2 = _x88 ∧ x3 = _x90 ∧ x4 = _x91 ∧ x1 = _x92 ∧ x2 = _x93 ∧ x3 = _x94 ∧ x4 = _x95 ∧ _x88 ≤ _x90 − 1 ∧ 0 ≤ _x90 − 1 ∧ _x88 − 2⋅_x98 = 1 ∧ _x88 − 3⋅_x99 = 0 ∧ _x100 ≤ _x87 ∧ 0 ≤ _x87 − 1 ∧ 0 ≤ _x100 − 1 ∧ _x87 = _x92 ∧ _x88 = _x93 ∧ _x90 = _x94
f165_0_main_GE'	11	f165_0_main_GE:	x1 = _x105 ∧ x2 = _x106 ∧ x3 = _x107 ∧ x4 = _x108 ∧ x1 = _x112 ∧ x2 = _x113 ∧ x3 = _x114 ∧ x4 = _x117 ∧ _x106 ≤ _x107 − 1 ∧ 0 ≤ _x107 − 1 ∧ _x106 − 2⋅_x118 = 1 ∧ _x106 − 3⋅_x119 = 0 ∧ _x112 ≤ _x105 ∧ 0 ≤ _x105 − 1 ∧ 0 ≤ _x112 − 1 ∧ 0 ≤ _x106 − 2⋅_x118 ∧ _x106 − 2⋅_x118 ≤ 1 ∧ _x106 − 3⋅_x119 ≤ 2 ∧ 0 ≤ _x106 − 3⋅_x119 ∧ _x106 + 1 = _x113 ∧ _x107 = _x114
f165_0_main_GE	12	f165_0_main_GE':	x1 = _x120 ∧ x2 = _x122 ∧ x3 = _x123 ∧ x4 = _x124 ∧ x1 = _x128 ∧ x2 = _x129 ∧ x3 = _x130 ∧ x4 = _x131 ∧ _x122 ≤ _x123 − 1 ∧ 0 ≤ _x123 − 1 ∧ _x122 − 2⋅_x134 = 0 ∧ 0 ≤ _x120 − 1 ∧ _x120 = _x128 ∧ _x122 = _x129 ∧ _x123 = _x130
f165_0_main_GE'	13	f861_0_sin_GT:	x1 = _x135 ∧ x2 = _x136 ∧ x3 = _x138 ∧ x4 = _x139 ∧ x1 = _x140 ∧ x2 = _x142 ∧ x3 = _x143 ∧ x4 = _x149 ∧ _x136 ≤ _x138 − 1 ∧ 0 ≤ _x138 − 1 ∧ _x136 − 2⋅_x150 = 0 ∧ 0 ≤ _x135 − 1 ∧ _x136 − 2⋅_x150 ≤ 1 ∧ 0 ≤ _x136 − 2⋅_x150 ∧ 3 = _x140 ∧ _x136 = _x142
f1048_0_fact_Return	14	f861_0_sin_GT:	x1 = _x151 ∧ x2 = _x154 ∧ x3 = _x155 ∧ x4 = _x156 ∧ x1 = _x159 ∧ x2 = _x160 ∧ x3 = _x164 ∧ x4 = _x165 ∧ _x151 = _x160 ∧ _x154 + 2 = _x159
f861_0_sin_GT	15	f861_0_sin_GT':	x1 = _x167 ∧ x2 = _x168 ∧ x3 = _x173 ∧ x4 = _x174 ∧ x1 = _x175 ∧ x2 = _x179 ∧ x3 = _x180 ∧ x4 = _x181 ∧ 0 ≤ _x185 − 1 ∧ _x167 ≤ _x168 ∧ _x167 = _x175 ∧ _x168 = _x179
f861_0_sin_GT'	16	f861_0_sin_GT:	x1 = _x186 ∧ x2 = _x187 ∧ x3 = _x191 ∧ x4 = _x192 ∧ x1 = _x193 ∧ x2 = _x194 ∧ x3 = _x195 ∧ x4 = _x197 ∧ _x186 ≤ _x187 ∧ 0 ≤ _x198 − 1 ∧ 0 ≤ _x186 − 2⋅_x199 ∧ _x186 − 2⋅_x199 ≤ 1 ∧ _x200⋅_x201 − _x198⋅_x202 ≤ _x198 − 1 ∧ 0 ≤ _x200⋅_x201 − _x198⋅_x202 ∧ _x186 + 2 = _x193 ∧ _x187 = _x194
f165_0_main_GE	17	f165_0_main_GE':	x1 = _x203 ∧ x2 = _x204 ∧ x3 = _x205 ∧ x4 = _x206 ∧ x1 = _x207 ∧ x2 = _x209 ∧ x3 = _x210 ∧ x4 = _x212 ∧ _x204 ≤ _x205 − 1 ∧ 0 ≤ _x205 − 1 ∧ _x204 − 2⋅_x213 = 1 ∧ _x204 − 3⋅_x214 = 0 ∧ 0 ≤ _x203 − 1 ∧ _x203 = _x207 ∧ _x204 = _x209 ∧ _x205 = _x210
f165_0_main_GE'	18	f862_0_cos_GT:	x1 = _x215 ∧ x2 = _x216 ∧ x3 = _x218 ∧ x4 = _x219 ∧ x1 = _x220 ∧ x2 = _x221 ∧ x3 = _x222 ∧ x4 = _x223 ∧ _x216 ≤ _x218 − 1 ∧ 0 ≤ _x218 − 1 ∧ _x216 − 2⋅_x224 = 1 ∧ _x216 − 3⋅_x225 = 0 ∧ 0 ≤ _x215 − 1 ∧ 0 ≤ _x216 − 2⋅_x224 ∧ _x216 − 2⋅_x224 ≤ 1 ∧ _x216 − 3⋅_x225 ≤ 2 ∧ 0 ≤ _x216 − 3⋅_x225 ∧ 2 = _x220 ∧ _x216 = _x221
f1049_0_fact_Return	19	f1049_0_fact_Return':	x1 = _x226 ∧ x2 = _x227 ∧ x3 = _x228 ∧ x4 = _x229 ∧ x1 = _x230 ∧ x2 = _x231 ∧ x3 = _x232 ∧ x4 = _x233 ∧ _x227 = _x231 ∧ _x226 = _x230
f1049_0_fact_Return'	20	f862_0_cos_GT:	x1 = _x234 ∧ x2 = _x235 ∧ x3 = _x236 ∧ x4 = _x237 ∧ x1 = _x238 ∧ x2 = _x239 ∧ x3 = _x240 ∧ x4 = _x241 ∧ _x242 − _x243⋅_x244 ≤ _x243 − 1 ∧ 0 ≤ _x242 − _x243⋅_x244 ∧ _x235 + 2 = _x238 ∧ _x234 = _x239
f862_0_cos_GT	21	f862_0_cos_GT':	x1 = _x245 ∧ x2 = _x246 ∧ x3 = _x247 ∧ x4 = _x248 ∧ x1 = _x249 ∧ x2 = _x250 ∧ x3 = _x251 ∧ x4 = _x252 ∧ 1 ≤ _x245 − 1 ∧ 0 ≤ _x253 − 1 ∧ 1 ≤ _x246 − 1 ∧ _x245 ≤ _x246 ∧ _x253 ≤ _x245 − 1 ∧ _x245 = _x249 ∧ _x246 = _x250
f862_0_cos_GT'	22	f862_0_cos_GT:	x1 = _x254 ∧ x2 = _x255 ∧ x3 = _x256 ∧ x4 = _x257 ∧ x1 = _x258 ∧ x2 = _x259 ∧ x3 = _x260 ∧ x4 = _x261 ∧ 1 ≤ _x254 − 1 ∧ 0 ≤ _x262 − 1 ∧ 1 ≤ _x255 − 1 ∧ _x262 ≤ _x254 − 1 ∧ _x254 ≤ _x255 ∧ 0 ≤ _x254 − 2⋅_x262 ∧ _x254 − 2⋅_x262 ≤ 1 ∧ _x263 − _x264⋅_x265 ≤ _x264 − 1 ∧ 0 ≤ _x263 − _x264⋅_x265 ∧ _x254 + 2 = _x258 ∧ _x255 = _x259
f165_0_main_GE	23	f165_0_main_GE':	x1 = _x266 ∧ x2 = _x267 ∧ x3 = _x268 ∧ x4 = _x269 ∧ x1 = _x270 ∧ x2 = _x271 ∧ x3 = _x272 ∧ x4 = _x273 ∧ _x267 ≤ _x268 − 1 ∧ 0 ≤ _x268 − 1 ∧ _x267 − 2⋅_x274 = 1 ∧ 0 ≤ _x267 − 3⋅_x275 − 1 ∧ _x267 − 5⋅_x276 = 0 ∧ 0 ≤ _x266 − 1 ∧ _x266 = _x270 ∧ _x267 = _x271 ∧ _x268 = _x272
f165_0_main_GE'	24	f544_0_exp_GT:	x1 = _x277 ∧ x2 = _x278 ∧ x3 = _x279 ∧ x4 = _x280 ∧ x1 = _x281 ∧ x2 = _x282 ∧ x3 = _x283 ∧ x4 = _x284 ∧ 0 ≤ _x278 − 3⋅_x285 − 1 ∧ _x278 ≤ _x279 − 1 ∧ 0 ≤ _x279 − 1 ∧ _x278 − 2⋅_x286 = 1 ∧ _x278 − 5⋅_x287 = 0 ∧ 0 ≤ _x277 − 1 ∧ 0 ≤ _x278 − 2⋅_x286 ∧ _x278 − 2⋅_x286 ≤ 1 ∧ _x278 − 3⋅_x285 ≤ 2 ∧ _x278 − 5⋅_x287 ≤ 4 ∧ 0 ≤ _x278 − 5⋅_x287 ∧ _x279 = _x281 ∧ 0 = _x282 ∧ _x278 = _x283
f765_0_fact_Return	25	f544_0_exp_GT:	x1 = _x288 ∧ x2 = _x289 ∧ x3 = _x290 ∧ x4 = _x291 ∧ x1 = _x292 ∧ x2 = _x293 ∧ x3 = _x294 ∧ x4 = _x295 ∧ _x289 = _x294 ∧ _x290 + 1 = _x293 ∧ _x288 = _x292
f544_0_exp_GT	26	f544_0_exp_GT':	x1 = _x296 ∧ x2 = _x297 ∧ x3 = _x298 ∧ x4 = _x299 ∧ x1 = _x300 ∧ x2 = _x301 ∧ x3 = _x302 ∧ x4 = _x303 ∧ 0 ≤ _x296 − 1 ∧ −1 ≤ _x298 − 1 ∧ _x297 ≤ _x298 ∧ 0 ≤ _x304 − 1 ∧ _x296 = _x300 ∧ _x297 = _x301 ∧ _x298 = _x302
f544_0_exp_GT'	27	f544_0_exp_GT:	x1 = _x305 ∧ x2 = _x306 ∧ x3 = _x307 ∧ x4 = _x308 ∧ x1 = _x309 ∧ x2 = _x310 ∧ x3 = _x311 ∧ x4 = _x312 ∧ 0 ≤ _x305 − 1 ∧ −1 ≤ _x307 − 1 ∧ 0 ≤ _x313 − 1 ∧ _x306 ≤ _x307 ∧ _x314 − _x313⋅_x315 ≤ _x313 − 1 ∧ 0 ≤ _x314 − _x313⋅_x315 ∧ _x305 = _x309 ∧ _x306 + 1 = _x310 ∧ _x307 = _x311
f861_0_sin_GT	28	f861_0_sin_GT':	x1 = _x316 ∧ x2 = _x317 ∧ x3 = _x318 ∧ x4 = _x319 ∧ x1 = _x320 ∧ x2 = _x321 ∧ x3 = _x322 ∧ x4 = _x323 ∧ _x317 = _x321 ∧ _x316 = _x320 ∧ _x316 ≤ _x317
f861_0_sin_GT'	29	f1011_0_power_GT:	x1 = _x324 ∧ x2 = _x325 ∧ x3 = _x326 ∧ x4 = _x327 ∧ x1 = _x328 ∧ x2 = _x329 ∧ x3 = _x330 ∧ x4 = _x331 ∧ 1 = _x328 ∧ 0 ≤ _x324 − 2⋅_x329 ∧ _x324 − 2⋅_x329 ≤ 1 ∧ _x324 ≤ _x325
f861_0_sin_GT'	30	f1011_0_power_GT:	x1 = _x332 ∧ x2 = _x333 ∧ x3 = _x334 ∧ x4 = _x335 ∧ x1 = _x336 ∧ x2 = _x337 ∧ x3 = _x338 ∧ x4 = _x339 ∧ _x332 ≤ _x333 ∧ _x332 − 2⋅_x340 ≤ 1 ∧ 0 ≤ _x332 − 2⋅_x340 ∧ 1 = _x336 ∧ _x332 = _x337
f862_0_cos_GT'	31	f1011_0_power_GT:	x1 = _x341 ∧ x2 = _x342 ∧ x3 = _x343 ∧ x4 = _x344 ∧ x1 = _x345 ∧ x2 = _x346 ∧ x3 = _x347 ∧ x4 = _x348 ∧ 1 = _x345 ∧ 0 ≤ _x341 − 2⋅_x346 ∧ _x341 − 2⋅_x346 ≤ 1 ∧ _x341 ≤ _x342 ∧ _x346 ≤ _x341 − 1 ∧ 1 ≤ _x342 − 1 ∧ 0 ≤ _x346 − 1 ∧ 1 ≤ _x341 − 1
f862_0_cos_GT'	32	f1011_0_power_GT:	x1 = _x349 ∧ x2 = _x350 ∧ x3 = _x351 ∧ x4 = _x352 ∧ x1 = _x353 ∧ x2 = _x354 ∧ x3 = _x355 ∧ x4 = _x356 ∧ 1 ≤ _x349 − 1 ∧ 0 ≤ _x357 − 1 ∧ 1 ≤ _x350 − 1 ∧ _x357 ≤ _x349 − 1 ∧ _x349 ≤ _x350 ∧ _x349 − 2⋅_x357 ≤ 1 ∧ 0 ≤ _x349 − 2⋅_x357 ∧ 1 = _x353 ∧ _x349 = _x354
f544_0_exp_GT	33	f1011_0_power_GT:	x1 = _x358 ∧ x2 = _x359 ∧ x3 = _x360 ∧ x4 = _x361 ∧ x1 = _x362 ∧ x2 = _x363 ∧ x3 = _x364 ∧ x4 = _x365 ∧ _x359 = _x363 ∧ 1 = _x362 ∧ −1 ≤ _x360 − 1 ∧ _x359 ≤ _x360 ∧ 0 ≤ _x358 − 1
f1011_0_power_GT	34	f1011_0_power_GT:	x1 = _x366 ∧ x2 = _x367 ∧ x3 = _x368 ∧ x4 = _x369 ∧ x1 = _x370 ∧ x2 = _x371 ∧ x3 = _x372 ∧ x4 = _x373 ∧ _x367 = _x371 ∧ _x366 + 1 = _x370 ∧ _x366 ≤ _x367
f861_0_sin_GT'	35	f1113_0_fact_GT:	x1 = _x374 ∧ x2 = _x375 ∧ x3 = _x376 ∧ x4 = _x377 ∧ x1 = _x378 ∧ x2 = _x379 ∧ x3 = _x380 ∧ x4 = _x381 ∧ _x374 ≤ _x375 ∧ _x374 − 2⋅_x382 ≤ 1 ∧ 0 ≤ _x374 − 2⋅_x382 ∧ 1 = _x378 ∧ 1 = _x379 ∧ 1 = _x380 ∧ _x374 = _x381
f862_0_cos_GT'	36	f1113_0_fact_GT:	x1 = _x383 ∧ x2 = _x384 ∧ x3 = _x385 ∧ x4 = _x386 ∧ x1 = _x387 ∧ x2 = _x388 ∧ x3 = _x389 ∧ x4 = _x390 ∧ 1 ≤ _x383 − 1 ∧ 0 ≤ _x391 − 1 ∧ 1 ≤ _x384 − 1 ∧ _x391 ≤ _x383 − 1 ∧ _x383 ≤ _x384 ∧ _x383 − 2⋅_x391 ≤ 1 ∧ 0 ≤ _x383 − 2⋅_x391 ∧ 1 = _x387 ∧ 1 = _x388 ∧ 1 = _x389 ∧ _x383 = _x390
f544_0_exp_GT	37	f1113_0_fact_GT:	x1 = _x392 ∧ x2 = _x393 ∧ x3 = _x394 ∧ x4 = _x395 ∧ x1 = _x396 ∧ x2 = _x397 ∧ x3 = _x398 ∧ x4 = _x399 ∧ _x393 = _x399 ∧ 1 = _x398 ∧ 1 = _x397 ∧ 1 = _x396 ∧ −1 ≤ _x394 − 1 ∧ _x393 ≤ _x394 ∧ 0 ≤ _x392 − 1
f1113_0_fact_GT	38	f1113_0_fact_GT:	x1 = _x400 ∧ x2 = _x401 ∧ x3 = _x402 ∧ x4 = _x403 ∧ x1 = _x404 ∧ x2 = _x405 ∧ x3 = _x406 ∧ x4 = _x407 ∧ _x403 = _x407 ∧ _x401 + 1 = _x406 ∧ _x401 + 1 = _x405 ∧ _x400⋅_x401 = _x404 ∧ _x401 = _x402 ∧ 0 ≤ _x401 − 1 ∧ 0 ≤ _x400 − 1 ∧ _x401 ≤ _x403
__init	39	f1_0_main_ConstantStackPush:	x1 = _x408 ∧ x2 = _x409 ∧ x3 = _x410 ∧ x4 = _x411 ∧ x1 = _x412 ∧ x2 = _x413 ∧ x3 = _x414 ∧ x4 = _x415 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

f319_0_main_GE	f319_0_main_GE	f319_0_main_GE:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f862_0_cos_GT	f862_0_cos_GT	f862_0_cos_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f861_0_sin_GT	f861_0_sin_GT	f861_0_sin_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f165_0_main_GE	f165_0_main_GE	f165_0_main_GE:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f862_0_cos_GT'	f862_0_cos_GT'	f862_0_cos_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
f1049_0_fact_Return'	f1049_0_fact_Return'	f1049_0_fact_Return':	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f165_0_main_GE'	f165_0_main_GE'	f165_0_main_GE':	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f544_0_exp_GT'	f544_0_exp_GT'	f544_0_exp_GT':	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
__init	__init	__init:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f1011_0_power_GT	f1011_0_power_GT	f1011_0_power_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f1048_0_fact_Return	f1048_0_fact_Return	f1048_0_fact_Return:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f765_0_fact_Return	f765_0_fact_Return	f765_0_fact_Return:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f544_0_exp_GT	f544_0_exp_GT	f544_0_exp_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f861_0_sin_GT'	f861_0_sin_GT'	f861_0_sin_GT':	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f1113_0_fact_GT	f1113_0_fact_GT	f1113_0_fact_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4
f1049_0_fact_Return	f1049_0_fact_Return	f1049_0_fact_Return:	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 6 SCC(s) of the program graph.

2.1 SCC Subproblem 1/6

Here we consider the SCC { f319_0_main_GE, f165_0_main_GE, f165_0_main_GE' }.

2.1.1 Transition Removal

We remove transitions 2, 3, 6, 7, 8, 9, 10, 11, 23, 17, 12 using the following ranking functions, which are bounded by 0.

f165_0_main_GE:	1 − 2⋅x2 + 2⋅x3
f165_0_main_GE':	−2⋅x2 + 2⋅x3
f319_0_main_GE:	−1 − 2⋅x2 + 2⋅x4

2.1.2 Transition Removal

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

f319_0_main_GE:	x4
f165_0_main_GE:	−1 + x3

2.1.3 Transition Removal

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

f319_0_main_GE:

99 − x3

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/6

Here we consider the SCC { f544_0_exp_GT, f544_0_exp_GT' }.

2.2.1 Transition Removal

We remove transitions 26, 27 using the following ranking functions, which are bounded by −1.

f544_0_exp_GT:	2⋅x3 − 2⋅x2
f544_0_exp_GT':	−2⋅x2 + 2⋅x3 − 1

2.2.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.3 SCC Subproblem 3/6

Here we consider the SCC { f862_0_cos_GT, f862_0_cos_GT' }.

2.3.1 Transition Removal

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

f862_0_cos_GT:	1 − x1 + x2
f862_0_cos_GT':	− x1 + x2

2.3.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.4 SCC Subproblem 4/6

Here we consider the SCC { f861_0_sin_GT', f861_0_sin_GT }.

2.4.1 Transition Removal

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

f861_0_sin_GT:	− x1 + x2 + 1
f861_0_sin_GT':	− x1 + x2

2.4.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.5 SCC Subproblem 5/6

Here we consider the SCC { f1113_0_fact_GT }.

2.5.1 Transition Removal

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

f1113_0_fact_GT:

− x3 + x4

2.5.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.6 SCC Subproblem 6/6

Here we consider the SCC { f1011_0_power_GT }.

2.6.1 Transition Removal

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

f1011_0_power_GT:

− x1 + x2

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