LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
l5 l5 l5: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l22 l22 l22: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l1 l1 l1: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l13 l13 l13: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l31 l31 l31: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l18 l18 l18: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l17 l17 l17: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l21 l21 l21: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l9 l9 l9: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l14 l14 l14: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l25 l25 l25: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l6 l6 l6: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l8 l8 l8: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l27 l27 l27: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
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
l12 l12 l12: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l19 l19 l19: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l26 l26 l26: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l7 l7 l7: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l11 l11 l11: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l3 l3 l3: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l20 l20 l20: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l32 l32 l32: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l28 l28 l28: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
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
l23 l23 l23: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l4 l4 l4: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l10 l10 l10: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l29 l29 l29: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l15 l15 l15: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l16 l16 l16: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
l30 l30 l30: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11
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 { l25, l1, l29, l27, l30, l0, l28, l26 }.

2.1.1 Transition Removal

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

l0: −1 − x3 + x7
l1: −1 − x3 + x7
l30: − x3 + x7
l26: − x3 + x7
l25: −1 − x3 + x7
l27: −1 − x3 + x7
l28: −1 − x3 + x7
l29: −1 − x3 + x7

2.1.2 Transition Removal

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

l0: − x5 + x7
l1: − x5 + x7
l26: − x5 + x7
l30: − x5 + x7
l25: − x5 + x7
l27: − x5 + x7
l28: −1 − x5 + x7
l29: −1 − x5 + x7

2.1.3 Transition Removal

We remove transitions 1, 47, 35, 38, 37, 36, 43, 39, 42, 41 using the following ranking functions, which are bounded by 0.

l0: 4
l1: 3
l26: 0
l30: −1
l25: 1
l27: 2
l28: 5
l29: 6

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 { l5, l22, l7, l11, l3, l13, l20, l18, l17, l2, l21, l9, l14, l23, l4, l6, l10, l8, l15, l16, l12, l19 }.

2.2.1 Transition Removal

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

l2: − x3 + x7
l3: − x3 + x7
l4: − x3 + x7
l8: − x3 + x7
l5: − x3 + x7
l6: − x3 + x7
l7: − x3 + x7
l11: − x3 + x7
l12: − x3 + x7
l17: − x3 + x7
l15: − x3 + x7
l16: − x3 + x7
l21: − x3 + x7
l19: − x3 + x7
l10: − x3 + x7
l9: − x3 + x7
l14: − x3 + x7
l13: − x3 + x7
l18: −1 − x3 + x7
l20: −1 − x3 + x7
l22: −1 − x3 + x7
l23: −1 − x3 + x7

2.2.2 Transition Removal

We remove transitions 7, 9, 34 using the following ranking functions, which are bounded by 0.

l2: 1 − 2⋅x5 + 2⋅x7
l3: 1 − 2⋅x5 + 2⋅x7
l4: −1 − 2⋅x5 + 2⋅x7
l8: −2⋅x5 + 2⋅x7
l5: −1 − 2⋅x5 + 2⋅x7
l6: −1 − 2⋅x5 + 2⋅x7
l7: −1 − 2⋅x5 + 2⋅x7
l11: −2⋅x5 + 2⋅x7
l12: −2⋅x5 + 2⋅x7
l17: −2⋅x5 + 2⋅x7
l15: −2⋅x5 + 2⋅x7
l16: −2⋅x5 + 2⋅x7
l21: −2⋅x5 + 2⋅x7
l19: −2⋅x5 + 2⋅x7
l10: −2⋅x5 + 2⋅x7
l9: −2⋅x5 + 2⋅x7
l14: −2⋅x5 + 2⋅x7
l13: −2⋅x5 + 2⋅x7
l18: −2⋅x5 + 2⋅x7
l20: −2⋅x5 + 2⋅x7
l22: −2⋅x5 + 2⋅x7
l23: −2⋅x5 + 2⋅x7

2.2.3 Transition Removal

We remove transitions 25, 22, 30, 19, 21, 20, 23 using the following ranking functions, which are bounded by 0.

l2: −1 − x3 − x5 + 2⋅x7
l3: −1 − x3 − x5 + 2⋅x7
l4: −2 − x3 − x5 + 2⋅x7
l5: −2 − x3 − x5 + 2⋅x7
l6: −2 − x3 − x5 + 2⋅x7
l7: −2 − x3 − x5 + 2⋅x7
l8: −3 − x3 + x7
l11: −3 − x3 + x7
l12: −3 − x3 + x7
l17: −3 − x3 + x7
l15: −3 − x3 + x7
l16: −3 − x3 + x7
l21: 0
l19: 1
l10: 2
l9: 2
l14: 2
l13: 2
l18: 2
l20: 3
l22: 4
l23: 4

2.2.4 Transition Removal

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

l2: −2 + 2⋅x1 − 2⋅x3 + x4 + x5 − x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l3: −2 + 2⋅x1 − 2⋅x3 + x4 + x5 − x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l4: −1 + 2⋅x1 − 2⋅x3 + x4 + x5 − x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l5: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l6: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l7: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l8: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l11: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l12: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l17: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l15: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l16: −4 + 2⋅x1 + x3 + x4 + x5 − x6 − 2⋅x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l9: −1 − x3 + x5
l10: −1 − x3 + x5
l14: −2 − x3 + x5
l13: −2 − x3 + x5
l23: −1 + 7⋅x1 + 8⋅x2 + 9⋅x3 + 10⋅x4 − x5 + 11⋅x7 + 12⋅x9 + 13⋅x10 + 14⋅x11
l22: −1 + 7⋅x1 + 8⋅x2 + 9⋅x3 + 10⋅x4 − x5 + 11⋅x7 + 12⋅x9 + 13⋅x10 + 14⋅x11

2.2.5 Transition Removal

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

l2: −1 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l3: −1 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l4: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l5: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l6: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l7: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l8: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l11: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l12: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l17: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l15: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l16: −3 + 2⋅x1 + x3 + x4 − 2⋅x5 − 2⋅x6 + x7 + 3⋅x8 + 4⋅x9 + 5⋅x10 + 6⋅x11
l9: −2 + 7⋅x1 + 8⋅x2 + x3 + 9⋅x4 + 10⋅x5 − 2⋅x6 + 11⋅x7 + 12⋅x9 + 13⋅x10 + 14⋅x11
l10: −2 + 7⋅x1 + 8⋅x2 + x3 + 9⋅x4 + 10⋅x5 − 2⋅x6 + 11⋅x7 + 12⋅x9 + 13⋅x10 + 14⋅x11
l14: −1 + 7⋅x1 + 8⋅x2 − x3 + 9⋅x4 + 10⋅x5 + 11⋅x7 + 12⋅x9 + 13⋅x10 + 14⋅x11
l13: −1 + 7⋅x1 + 8⋅x2 − x3 + 9⋅x4 + 10⋅x5 + 11⋅x7 + 12⋅x9 + 13⋅x10 + 14⋅x11
l23: −1 + x5 − x6
l22: −1 + x5 − x6

2.2.6 Transition Removal

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

l2: 3 − x3 − x5 − x6 + 3⋅x7
l3: 3 − x3 − x5 − x6 + 3⋅x7
l4: 2 − x3 − x5 − x6 + 3⋅x7
l5: 1 − x5 − x6 + 2⋅x7
l6: 1 − x5 − x6 + 2⋅x7
l7: 1 − x5 − x6 + 2⋅x7
l8: − x6 + x7
l11: − x6 + x7
l12: − x6 + x7
l17: − x6 + x7
l15: − x6 + x7
l16: − x6 + x7
l9: −2 + 4⋅x1 + 5⋅x2 + x3 + 6⋅x4 + 7⋅x5 − 2⋅x6 + 8⋅x7 + 9⋅x9 + 10⋅x10 + 11⋅x11
l10: −2 + 4⋅x1 + 5⋅x2 + x3 + 6⋅x4 + 7⋅x5 − 2⋅x6 + 8⋅x7 + 9⋅x9 + 10⋅x10 + 11⋅x11
l14: −1 + 4⋅x1 + 5⋅x2 − x3 + 6⋅x4 + 7⋅x5 + 8⋅x7 + 9⋅x9 + 10⋅x10 + 11⋅x11
l13: −1 + 4⋅x1 + 5⋅x2 − x3 + 6⋅x4 + 7⋅x5 + 8⋅x7 + 9⋅x9 + 10⋅x10 + 11⋅x11
l23: −1 + 12⋅x1 + 13⋅x2 + 14⋅x3 + 15⋅x4 + 16⋅x5 + 17⋅x6 + 18⋅x7 + 19⋅x8 + 20⋅x9 + 21⋅x10 + 22⋅x11
l22: −1 + 12⋅x1 + 13⋅x2 + 14⋅x3 + 15⋅x4 + 16⋅x5 + 17⋅x6 + 18⋅x7 + 19⋅x8 + 20⋅x9 + 21⋅x10 + 22⋅x11

2.2.7 Transition Removal

We remove transitions 2, 3, 4, 40, 6, 8, 11, 12, 16, 14, 32, 18, 17, 29, 27 using the following ranking functions, which are bounded by 0.

l2: 0
l3: −1
l4: 1
l5: 2
l6: 3
l7: 4
l8: 5
l11: 6
l12: 7
l17: 10
l15: 8
l16: 9
l9: −2 + x3 − x6
l10: −2 + x3 − x6
l14: −1 + x3 − x6
l13: −1 + x3 − x6
l23: 1
l22: 0

2.2.8 Transition Removal

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

l9: 0
l10: −1
l14: 1
l13: 2

2.2.9 Trivial Cooperation Program

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

Tool configuration

AProVE