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
l24 l24 l24: 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
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 { l22, l1, l3, l31, l18, l30, l0, l2 }.

2.1.1 Transition Removal

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

l0: −1 − x3 + x7
l1: −1 − x3 + x7
l3: −1 − x3 + x7
l31: −1 − x3 + x7
l2: −1 − x3 + x7
l18: − x3 + x7
l22: − x3 + x7
l30: −1 − x3 + x7

2.1.2 Transition Removal

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

l0: 0
l1: −1 − x5 + x7
l3: 0
l31: 0
l2: 0
l22: −1 − x5 + x7
l18: −1 − x5 + x7
l30: −1 − x5 + x7

2.1.3 Transition Removal

We remove transitions 30, 42, 45, 44, 43 using the following ranking functions, which are bounded by 0.

l3: −1 + 3⋅x2 + 4⋅x3 + 5⋅x4 − x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x11
l0: −1 + 3⋅x2 + 4⋅x3 + 5⋅x4 − x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x11
l31: −2 + 3⋅x2 + 4⋅x3 + 5⋅x4 − x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x11
l2: −2 + 3⋅x2 + 4⋅x3 + 5⋅x4 − x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x11
l22: 0
l18: −1
l30: 1
l1: 2

2.1.4 Transition Removal

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

l3: −4⋅x5 + 4⋅x7 + 3
l0: −4⋅x5 + 4⋅x7 + 2
l31: −4⋅x5 + 4⋅x7
l2: −4⋅x5 + 4⋅x7 + 1

2.1.5 Transition Removal

We remove transitions 3, 46, 48, 47 using the following ranking functions, which are bounded by 0.

l3: 0
l0: −1
l31: 1
l2: 2

2.1.6 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, l7, l24, l11, l13, l20, l17, l21, l9, l14, l23, l4, l25, l6, l10, l8, l27, l16, l15, l12, l19, l26 }.

2.2.1 Transition Removal

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

l5: − x3 + x7
l27: − x3 + x7
l4: − x3 + x7
l9: − x3 + x7
l6: − x3 + x7
l7: − x3 + x7
l8: − x3 + x7
l10: − x3 + x7
l11: − x3 + x7
l14: − x3 + x7
l12: − x3 + x7
l13: − x3 + x7
l21: − x3 + x7
l16: − x3 + x7
l26: − x3 + x7
l24: − x3 + x7
l23: − x3 + x7
l25: − x3 + x7
l15: −1 − x3 + x7
l17: −1 − x3 + x7
l19: −1 − x3 + x7
l20: −1 − x3 + x7

2.2.2 Transition Removal

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

l5: 1 − 2⋅x5 + 2⋅x7
l27: 1 − 2⋅x5 + 2⋅x7
l4: −1 − 2⋅x5 + 2⋅x7
l9: −2⋅x5 + 2⋅x7
l6: −1 − 2⋅x5 + 2⋅x7
l7: −1 − 2⋅x5 + 2⋅x7
l8: −1 − 2⋅x5 + 2⋅x7
l10: −2⋅x5 + 2⋅x7
l11: −2⋅x5 + 2⋅x7
l14: −2⋅x5 + 2⋅x7
l12: −2⋅x5 + 2⋅x7
l13: −2⋅x5 + 2⋅x7
l21: −2⋅x5 + 2⋅x7
l16: −2⋅x5 + 2⋅x7
l26: −2⋅x5 + 2⋅x7
l24: −2⋅x5 + 2⋅x7
l23: −2⋅x5 + 2⋅x7
l25: −2⋅x5 + 2⋅x7
l15: −2⋅x5 + 2⋅x7
l17: −2⋅x5 + 2⋅x7
l19: −2⋅x5 + 2⋅x7
l20: −2⋅x5 + 2⋅x7

2.2.3 Transition Removal

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

l5: −1 − x3 − x5 − 2⋅x6 + 4⋅x7
l27: −1 − x3 − x5 − 2⋅x6 + 4⋅x7
l4: −2 − x3 − x5 − 2⋅x6 + 4⋅x7
l6: −2 − x3 − x5 − 2⋅x6 + 4⋅x7
l7: −2 − x3 − x5 − 2⋅x6 + 4⋅x7
l8: −2 − x3 − x5 − 2⋅x6 + 4⋅x7
l9: −5 − x3 + 2⋅x5 − 2⋅x6 + x7
l10: −5 − x3 + 2⋅x5 − 2⋅x6 + x7
l11: −5 − x3 + 2⋅x5 − 2⋅x6 + x7
l14: −3 − x3 + 2⋅x5 − 2⋅x6 + x7
l12: −5 − x3 + 2⋅x5 − 2⋅x6 + x7
l13: −3 − x3 + 2⋅x5 − 2⋅x6 + x7
l21: −4 + 2⋅x5 − 2⋅x6
l16: −4 + 2⋅x5 − 2⋅x6
l26: −4 + 2⋅x5 − 2⋅x6
l24: −4 + 2⋅x5 − 2⋅x6
l23: −4 + 2⋅x5 − 2⋅x6
l25: −4 + 2⋅x5 − 2⋅x6
l15: −4 + 2⋅x5 − 2⋅x6
l17: −4 + 2⋅x5 − 2⋅x6
l19: 11
l20: 11

2.2.4 Transition Removal

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

l5: −4 − x1 − 5⋅x3 − 2⋅x5 − x6 + x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l27: −4 − x1 − 5⋅x3 − 2⋅x5 − x6 + x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l4: −6 − x1 − 5⋅x3 − 2⋅x5 − x6 + x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l6: −6 − x1 − 5⋅x3 − 2⋅x5 − x6 + x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l7: −1 − x1 − 5⋅x3 − 2⋅x5 − x6 + x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l8: −1 − x1 − 5⋅x3 − 2⋅x5 − x6 + x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l9: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l10: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l11: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l14: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l12: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l13: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l21: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l16: −4 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l26: −4 − x3 − 3⋅x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l24: −4 − x3 − 3⋅x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l23: −5 − x3 − 3⋅x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l25: −4 − x3 − 3⋅x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l15: −9 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l17: −9 − x1 − 5⋅x3 + x5 − x6 − 2⋅x7 + 2⋅x9 + 3⋅x10 + 4⋅x11
l20: −1 + x5 − x6
l19: −1 + x5 − x6

2.2.5 Transition Removal

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

l5: −2 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l27: −2 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l4: −5 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l6: −5 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l7: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l8: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l9: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l10: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l11: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l14: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l12: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l13: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l21: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l16: −4 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l26: −4 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l24: −3 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l23: −4 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l25: −4 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l15: −5 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l17: −5 − x1 − x3 − 3⋅x5 − 3⋅x6 + 2⋅x7 + 3⋅x9 + 4⋅x10 + 5⋅x11
l20: 0
l19: −1

2.2.6 Transition Removal

We remove transitions 40, 4, 5, 8, 10 using the following ranking functions, which are bounded by 0.

l5: 0
l27: −1
l4: 1
l6: 2
l7: 2
l8: 3
l9: −1 + 5⋅x5 − 5⋅x7
l10: −1 + 5⋅x5 − 5⋅x7
l11: −1 + 5⋅x5 − 5⋅x7
l14: −1 + 5⋅x5 − 5⋅x7
l12: −1 + 5⋅x5 − 5⋅x7
l13: −1 + 5⋅x5 − 5⋅x7
l21: −1 + 5⋅x5 − 5⋅x7
l16: −1 + 5⋅x5 − 5⋅x7
l26: −1 + 5⋅x5 − 5⋅x7
l24: −1 + 5⋅x5 − 5⋅x7
l23: −1 + 5⋅x5 − 5⋅x7
l25: −1 + 5⋅x5 − 5⋅x7
l15: −1 + 5⋅x5 − 5⋅x7
l17: −1 + 5⋅x5 − 5⋅x7

2.2.7 Transition Removal

We remove transitions 12, 13, 17, 14, 19, 18, 28, 31, 35, 20, 22, 21 using the following ranking functions, which are bounded by 0.

l7: −1 + 8⋅x1 + 9⋅x2 − x3 + 10⋅x4 + 11⋅x5 + 12⋅x6 + 13⋅x7 + 14⋅x8 + 15⋅x9 + 16⋅x10 + 17⋅x11
l6: −1 + 8⋅x1 + 9⋅x2 − x3 + 10⋅x4 + 11⋅x5 + 12⋅x6 + 13⋅x7 + 14⋅x8 + 15⋅x9 + 16⋅x10 + 17⋅x11
l10: 0
l9: −1
l11: 1
l14: 3
l12: 2
l13: 2
l21: 4
l16: 5
l26: 6
l24: 6
l23: 6
l25: 6
l15: 6
l17: 7

2.2.8 Transition Removal

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

l7: −1 + 2⋅x1 + 3⋅x2 − x3 + 4⋅x4 + 5⋅x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11
l6: −1 + 2⋅x1 + 3⋅x2 − x3 + 4⋅x4 + 5⋅x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11
l13: − x6 + x7
l12: − x6 + x7
l24: −1 + 12⋅x1 + 13⋅x2 − 2⋅x3 + 14⋅x4 + x5 + 15⋅x7 + 16⋅x9 + 17⋅x10 + 18⋅x11
l26: −3 + 12⋅x1 + 13⋅x2 − 2⋅x3 + 14⋅x4 + x5 + 15⋅x7 + 16⋅x9 + 17⋅x10 + 18⋅x11
l23: −3 + 12⋅x1 + 13⋅x2 − 2⋅x3 + 14⋅x4 + x5 + 15⋅x7 + 16⋅x9 + 17⋅x10 + 18⋅x11
l25: −3 + 12⋅x1 + 13⋅x2 − 2⋅x3 + 14⋅x4 + x5 + 15⋅x7 + 16⋅x9 + 17⋅x10 + 18⋅x11

2.2.9 Transition Removal

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

l7: −1 + 2⋅x1 + 3⋅x2 − x3 + 4⋅x4 + 5⋅x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11
l6: −2 + 2⋅x1 + 3⋅x2 − x3 + 4⋅x4 + 5⋅x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11
l13: 1
l12: 0
l24: −1 − x3 + x5
l26: −1 − x3 + x5
l23: −2 − x3 + x5
l25: −2 − x3 + x5

2.2.10 Transition Removal

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

l7: −1 + 2⋅x1 + 3⋅x2 − x3 + 4⋅x4 + 5⋅x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11
l6: −2 + 2⋅x1 + 3⋅x2 − x3 + 4⋅x4 + 5⋅x5 + 6⋅x6 + 7⋅x7 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11
l24: −2 + x3 − x6
l26: −2 + x3 − x6
l23: −1 + x3 − x6
l25: −1 + x3 − x6

2.2.11 Transition Removal

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

l7: −1 + 3⋅x1 + 4⋅x2 − x3 + 5⋅x4 + 6⋅x5 + 7⋅x6 + 8⋅x7 + 9⋅x8 + 10⋅x9 + 11⋅x10 + 12⋅x11
l6: −2 + 3⋅x1 + 4⋅x2 − x3 + 5⋅x4 + 6⋅x5 + 7⋅x6 + 8⋅x7 + 9⋅x8 + 10⋅x9 + 11⋅x10 + 12⋅x11
l24: 0
l26: −1
l23: 1
l25: 2

2.2.12 Transition Removal

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

l7: −2⋅x3 + 2⋅x7 + 1
l6: −2⋅x3 + 2⋅x7

2.2.13 Transition Removal

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

l7: 0
l6: −1

2.2.14 Trivial Cooperation Program

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

Tool configuration

AProVE