LTS Termination Proof

Input

Integer Transition System

Initial Location: l0, l2

Transitions: (pre-variables and post-variables)

l0	1	l1:		x1 = _i1HAT0 ∧ x2 = _i2HAT0 ∧ x3 = _i3HAT0 ∧ x4 = _i4HAT0 ∧ x5 = _i5HAT0 ∧ x6 = _i6HAT0 ∧ x7 = _i7HAT0 ∧ x8 = _i8HAT0 ∧ x9 = _n17HAT0 ∧ x10 = _n21HAT0 ∧ x11 = _n25HAT0 ∧ x12 = _n29HAT0 ∧ x13 = _n33HAT0 ∧ x14 = _n37HAT0 ∧ x15 = _n41HAT0 ∧ x16 = _n45HAT0 ∧ x17 = _ret18HAT0 ∧ x18 = _ret22HAT0 ∧ x19 = _ret26HAT0 ∧ x20 = _ret30HAT0 ∧ x21 = _ret34HAT0 ∧ x22 = _ret38HAT0 ∧ x23 = _ret42HAT0 ∧ x24 = _ret46HAT0 ∧ x25 = _ret_fn120HAT0 ∧ x26 = _ret_fn124HAT0 ∧ x27 = _ret_fn128HAT0 ∧ x28 = _ret_fn132HAT0 ∧ x29 = _ret_fn136HAT0 ∧ x30 = _ret_fn140HAT0 ∧ x31 = _ret_fn144HAT0 ∧ x32 = _ret_fn148HAT0 ∧ x33 = _tmp19HAT0 ∧ x34 = _tmp23HAT0 ∧ x35 = _tmp27HAT0 ∧ x36 = _tmp31HAT0 ∧ x37 = _tmp35HAT0 ∧ x38 = _tmp39HAT0 ∧ x39 = _tmp43HAT0 ∧ x40 = _tmp47HAT0 ∧ x41 = _tmpHAT0 ∧ x42 = _tmp___0HAT0 ∧ x43 = _tmp___1HAT0 ∧ x44 = _tmp___2HAT0 ∧ x45 = _tmp___3HAT0 ∧ x46 = _tmp___4HAT0 ∧ x47 = _tmp___5HAT0 ∧ x48 = _tmp___6HAT0 ∧ x1 = _i1HATpost ∧ x2 = _i2HATpost ∧ x3 = _i3HATpost ∧ x4 = _i4HATpost ∧ x5 = _i5HATpost ∧ x6 = _i6HATpost ∧ x7 = _i7HATpost ∧ x8 = _i8HATpost ∧ x9 = _n17HATpost ∧ x10 = _n21HATpost ∧ x11 = _n25HATpost ∧ x12 = _n29HATpost ∧ x13 = _n33HATpost ∧ x14 = _n37HATpost ∧ x15 = _n41HATpost ∧ x16 = _n45HATpost ∧ x17 = _ret18HATpost ∧ x18 = _ret22HATpost ∧ x19 = _ret26HATpost ∧ x20 = _ret30HATpost ∧ x21 = _ret34HATpost ∧ x22 = _ret38HATpost ∧ x23 = _ret42HATpost ∧ x24 = _ret46HATpost ∧ x25 = _ret_fn120HATpost ∧ x26 = _ret_fn124HATpost ∧ x27 = _ret_fn128HATpost ∧ x28 = _ret_fn132HATpost ∧ x29 = _ret_fn136HATpost ∧ x30 = _ret_fn140HATpost ∧ x31 = _ret_fn144HATpost ∧ x32 = _ret_fn148HATpost ∧ x33 = _tmp19HATpost ∧ x34 = _tmp23HATpost ∧ x35 = _tmp27HATpost ∧ x36 = _tmp31HATpost ∧ x37 = _tmp35HATpost ∧ x38 = _tmp39HATpost ∧ x39 = _tmp43HATpost ∧ x40 = _tmp47HATpost ∧ x41 = _tmpHATpost ∧ x42 = _tmp___0HATpost ∧ x43 = _tmp___1HATpost ∧ x44 = _tmp___2HATpost ∧ x45 = _tmp___3HATpost ∧ x46 = _tmp___4HATpost ∧ x47 = _tmp___5HATpost ∧ x48 = _tmp___6HATpost ∧ _i8HATpost = _tmp___6HATpost ∧ _tmp___6HATpost = _ret_fn148HATpost ∧ _ret_fn148HATpost = _ret46HATpost ∧ _ret46HATpost = _tmp47HATpost ∧ _tmp47HATpost = _tmp47HATpost ∧ _n45HATpost = 2 ∧ _i7HATpost = _tmp___5HATpost ∧ _tmp___5HATpost = _ret_fn144HATpost ∧ _ret_fn144HATpost = _ret42HATpost ∧ _ret42HATpost = _tmp43HATpost ∧ _tmp43HATpost = _tmp43HATpost ∧ _n41HATpost = 2 ∧ _i6HATpost = _tmp___4HATpost ∧ _tmp___4HATpost = _ret_fn140HATpost ∧ _ret_fn140HATpost = _ret38HATpost ∧ _ret38HATpost = _tmp39HATpost ∧ _tmp39HATpost = _tmp39HATpost ∧ _n37HATpost = 2 ∧ _i5HATpost = _tmp___3HATpost ∧ _tmp___3HATpost = _ret_fn136HATpost ∧ _ret_fn136HATpost = _ret34HATpost ∧ _ret34HATpost = _tmp35HATpost ∧ _tmp35HATpost = _tmp35HATpost ∧ _n33HATpost = 2 ∧ _i4HATpost = _tmp___2HATpost ∧ _tmp___2HATpost = _ret_fn132HATpost ∧ _ret_fn132HATpost = _ret30HATpost ∧ _ret30HATpost = _tmp31HATpost ∧ _tmp31HATpost = _tmp31HATpost ∧ _n29HATpost = 2 ∧ _i3HATpost = _tmp___1HATpost ∧ _tmp___1HATpost = _ret_fn128HATpost ∧ _ret_fn128HATpost = _ret26HATpost ∧ _ret26HATpost = _tmp27HATpost ∧ _tmp27HATpost = _tmp27HATpost ∧ _n25HATpost = 2 ∧ _i2HATpost = _tmp___0HATpost ∧ _tmp___0HATpost = _ret_fn124HATpost ∧ _ret_fn124HATpost = _ret22HATpost ∧ _ret22HATpost = _tmp23HATpost ∧ _tmp23HATpost = _tmp23HATpost ∧ _n21HATpost = 2 ∧ _i1HATpost = _tmpHATpost ∧ _tmpHATpost = _ret_fn120HATpost ∧ _ret_fn120HATpost = _ret18HATpost ∧ _ret18HATpost = _tmp19HATpost ∧ _tmp19HATpost = _tmp19HATpost ∧ _n17HATpost = 2
l2	2	l0:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ x8 = _x7 ∧ x9 = _x8 ∧ x10 = _x9 ∧ x11 = _x10 ∧ x12 = _x11 ∧ x13 = _x12 ∧ x14 = _x13 ∧ x15 = _x14 ∧ x16 = _x15 ∧ x17 = _x16 ∧ x18 = _x17 ∧ x19 = _x18 ∧ x20 = _x19 ∧ x21 = _x20 ∧ x22 = _x21 ∧ x23 = _x22 ∧ x24 = _x23 ∧ x25 = _x24 ∧ x26 = _x25 ∧ x27 = _x26 ∧ x28 = _x27 ∧ x29 = _x28 ∧ x30 = _x29 ∧ x31 = _x30 ∧ x32 = _x31 ∧ x33 = _x32 ∧ x34 = _x33 ∧ x35 = _x34 ∧ x36 = _x35 ∧ x37 = _x36 ∧ x38 = _x37 ∧ x39 = _x38 ∧ x40 = _x39 ∧ x41 = _x40 ∧ x42 = _x41 ∧ x43 = _x42 ∧ x44 = _x43 ∧ x45 = _x44 ∧ x46 = _x45 ∧ x47 = _x46 ∧ x48 = _x47 ∧ x1 = _x48 ∧ x2 = _x49 ∧ x3 = _x50 ∧ x4 = _x51 ∧ x5 = _x52 ∧ x6 = _x53 ∧ x7 = _x54 ∧ x8 = _x55 ∧ x9 = _x56 ∧ x10 = _x57 ∧ x11 = _x58 ∧ x12 = _x59 ∧ x13 = _x60 ∧ x14 = _x61 ∧ x15 = _x62 ∧ x16 = _x63 ∧ x17 = _x64 ∧ x18 = _x65 ∧ x19 = _x66 ∧ x20 = _x67 ∧ x21 = _x68 ∧ x22 = _x69 ∧ x23 = _x70 ∧ x24 = _x71 ∧ x25 = _x72 ∧ x26 = _x73 ∧ x27 = _x74 ∧ x28 = _x75 ∧ x29 = _x76 ∧ x30 = _x77 ∧ x31 = _x78 ∧ x32 = _x79 ∧ x33 = _x80 ∧ x34 = _x81 ∧ x35 = _x82 ∧ x36 = _x83 ∧ x37 = _x84 ∧ x38 = _x85 ∧ x39 = _x86 ∧ x40 = _x87 ∧ x41 = _x88 ∧ x42 = _x89 ∧ x43 = _x90 ∧ x44 = _x91 ∧ x45 = _x92 ∧ x46 = _x93 ∧ x47 = _x94 ∧ x48 = _x95 ∧ _x47 = _x95 ∧ _x46 = _x94 ∧ _x45 = _x93 ∧ _x44 = _x92 ∧ _x43 = _x91 ∧ _x42 = _x90 ∧ _x41 = _x89 ∧ _x39 = _x87 ∧ _x38 = _x86 ∧ _x37 = _x85 ∧ _x36 = _x84 ∧ _x35 = _x83 ∧ _x34 = _x82 ∧ _x33 = _x81 ∧ _x32 = _x80 ∧ _x40 = _x88 ∧ _x31 = _x79 ∧ _x30 = _x78 ∧ _x29 = _x77 ∧ _x28 = _x76 ∧ _x27 = _x75 ∧ _x26 = _x74 ∧ _x25 = _x73 ∧ _x24 = _x72 ∧ _x23 = _x71 ∧ _x22 = _x70 ∧ _x21 = _x69 ∧ _x20 = _x68 ∧ _x19 = _x67 ∧ _x18 = _x66 ∧ _x17 = _x65 ∧ _x16 = _x64 ∧ _x15 = _x63 ∧ _x14 = _x62 ∧ _x13 = _x61 ∧ _x12 = _x60 ∧ _x11 = _x59 ∧ _x10 = _x58 ∧ _x9 = _x57 ∧ _x8 = _x56 ∧ _x7 = _x55 ∧ _x6 = _x54 ∧ _x5 = _x53 ∧ _x4 = _x52 ∧ _x3 = _x51 ∧ _x2 = _x50 ∧ _x1 = _x49 ∧ _x = _x48

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

l0	l0	l0:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48
l2	l2	l2:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48

and for every transition t, a duplicate t is considered.

2 SCC Decomposition

There exist no SCC in the program graph.

Tool configuration

version: AProVE Commit ID: unknown
strategy: Statistics for single proof: 100.00 % (2 real / 0 unknown / 0 assumptions / 2 total proof steps)