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 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l22 l22 l22: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l48 l48 l48: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l18 l18 l18: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l17 l17 l17: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l35 l35 l35: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l21 l21 l21: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l6 l6 l6: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l34 l34 l34: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l46 l46 l46: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l19 l19 l19: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l33 l33 l33: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l40 l40 l40: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l47 l47 l47: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l37 l37 l37: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l11 l11 l11: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l49 l49 l49: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l32 l32 l32: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l28 l28 l28: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l2 l2 l2: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l23 l23 l23: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l4 l4 l4: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l44 l44 l44: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l16 l16 l16: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l30 l30 l30: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l39 l39 l39: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l43 l43 l43: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l1 l1 l1: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l13 l13 l13: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l31 l31 l31: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l9 l9 l9: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l14 l14 l14: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l25 l25 l25: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l8 l8 l8: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l27 l27 l27: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l0 l0 l0: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l12 l12 l12: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l26 l26 l26: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l7 l7 l7: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l24 l24 l24: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l3 l3 l3: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l41 l41 l41: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l20 l20 l20: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l45 l45 l45: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l38 l38 l38: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l10 l10 l10: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l36 l36 l36: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l29 l29 l29: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l15 l15 l15: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
l50 l50 l50: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

We consider subproblems for each of the 5 SCC(s) of the program graph.

2.1 SCC Subproblem 1/5

Here we consider the SCC { l39, l38, l37, l36, l40 }.

2.1.1 Transition Removal

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

l36: −5⋅x5 + 5⋅x14 − 2
l37: −5⋅x5 + 5⋅x14 − 3
l39: −5⋅x5 + 5⋅x14 − 1
l40: −5⋅x5 + 5⋅x14
l38: −5⋅x5 + 5⋅x14 + 1

2.1.2 Transition Removal

We remove transitions 52, 56, 55, 61, 54, 57 using the following ranking functions, which are bounded by 0.

l36: 2
l37: 1
l39: 3
l38: 0
l40: −1

2.1.3 Trivial Cooperation Program

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

2.2 SCC Subproblem 2/5

Here we consider the SCC { l34, l35 }.

2.2.1 Transition Removal

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

l34: x5 + x13
l35: x5 + x13

2.2.2 Transition Removal

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

l35: 0
l34: −1

2.2.3 Trivial Cooperation Program

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

2.3 SCC Subproblem 3/5

Here we consider the SCC { l31, l32 }.

2.3.1 Transition Removal

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

l31: x5 + x13
l32: x5 + x13

2.3.2 Transition Removal

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

l32: 0
l31: −1

2.3.3 Trivial Cooperation Program

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

2.4 SCC Subproblem 4/5

Here we consider the SCC { l5, l22, l43, l1, l13, l48, l18, l17, l21, l9, l14, l25, l6, l8, l46, l27, l0, l12, l19, l26, l47, l7, l24, l11, l3, l20, l28, l45, l2, l23, l4, l10, l44, l29, l15, l16 }.

2.4.1 Transition Removal

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

l0: −1 − x5 + x13
l1: −1 − x5 + x13
l4: −1 − x5 + x13
l5: −1 − x5 + x13
l3: −1 − x5 + x13
l6: x5 + x13
l12: x5 + x13
l44: −1 − x5 + x13
l45: −1 − x5 + x13
l43: −1 − x5 + x13
l47: −1 − x5 + x13
l48: −1 − x5 + x13
l46: −1 − x5 + x13
l2: −1 − x5 + x13
l9: x5 + x13
l13: x5 + x13
l8: x5 + x13
l15: x5 + x13
l16: x5 + x13
l14: x5 + x13
l19: x5 + x13
l20: x5 + x13
l11: x5 + x13
l10: x5 + x13
l29: x5 + x13
l7: x5 + x13
l24: x5 + x13
l26: x5 + x13
l27: x5 + x13
l22: x5 + x13
l21: x5 + x13
l18: x5 + x13
l17: x5 + x13
l28: x5 + x13
l23: x5 + x13
l25: x5 + x13

2.4.2 Transition Removal

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

l0: −1 + x8x9
l1: −1 + x8x9
l4: −1 + x8x9
l5: −1 + x8x9
l3: −1 + x8x9
l12: −1 + x8x9
l6: −1 + x8x9
l44: −1 + x8x9
l45: −1 + x8x9
l43: −1 + x8x9
l47: −1 + x8x9
l48: −1 + x8x9
l46: −1 + x8x9
l2: −1 + x8x9
l9: −1 + x8x9
l13: −1 + x8x9
l8: −1 + x8x9
l15: −1 + x8x9
l16: −1 + x8x9
l14: −1 + x8x9
l19: −1 + x8x9
l20: −1 + x8x9
l11: −1 + x8x9
l10: −1 + x8x9
l29: x8x9
l7: x8x9
l24: −1 + x8x9
l26: −1 + x8x9
l27: −1 + x8x9
l22: −1 + x8x9
l21: −1 + x8x9
l18: −1 + x8x9
l17: −1 + x8x9
l28: −1 + x8x9
l23: −1 + x8x9
l25: −1 + x8x9

2.4.3 Transition Removal

We remove transitions 1, 5, 8, 4, 7, 6, 53, 67, 70, 65, 69, 68, 72, 75, 71, 74, 73, 77, 76, 2, 3, 13, 16, 11, 15, 14, 18, 21, 17, 20, 19, 23, 40, 78, 9 using the following ranking functions, which are bounded by 0.

l0: 11
l1: 10
l4: 12
l5: 14
l3: 13
l12: 2
l6: 1
l44: 3
l45: 5
l43: 4
l47: 6
l48: 8
l46: 7
l2: 9
l9: 3
l13: 5
l8: 4
l15: 6
l16: 8
l14: 7
l19: 9
l20: 9
l11: 10
l10: 10
l7: 0
l29: −1
l24: 10
l26: 10
l27: 10
l22: 10
l21: 10
l18: 10
l17: 10
l28: 10
l23: 10
l25: 10

2.4.4 Transition Removal

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

l20: x5 + x14
l19: x5 + x14
l10: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l11: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l24: −3 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l26: −3 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l27: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l22: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l21: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l18: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l17: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l28: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l23: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27
l25: −2 + 4⋅x1 + 5⋅x2 + 6⋅x3 + 7⋅x4 − 2⋅x5x6 + 8⋅x8 + 9⋅x9 + 10⋅x10 + 11⋅x11 + x12 + 3⋅x13x14x15 + 12⋅x16 + 13⋅x17 + 14⋅x18 + 15⋅x19 + 16⋅x20 + 17⋅x21 + 18⋅x22 + 19⋅x23 + 20⋅x24 + 21⋅x25 + 22⋅x26 + 23⋅x27

2.4.5 Transition Removal

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

l20: 1
l19: 0
l10: x5 + x12
l11: x5 + x12
l24: x5 + x12
l26: x5 + x12
l27: x5 + x12
l22: x5 + x12
l21: x5 + x12
l18: x5 + x12
l17: x5 + x12
l28: x5 + x12
l23: x5 + x12
l25: x5 + x12

2.4.6 Transition Removal

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

l10: x6
l11: x6
l24: −1 − x6
l26: −1 − x6
l27: −1 − x6
l22: −1 − x6
l21: −1 − x6
l18: −1 − x6
l17: −1 − x6
l28: −1 − x6
l23: −1 − x6
l25: −1 − x6

2.4.7 Transition Removal

We remove transitions 12, 28, 29, 31, 32, 25, 35, 22, 39, 38, 26, 34, 37 using the following ranking functions, which are bounded by 0.

l10: 0
l11: −1
l24: 1
l26: 2
l27: 3
l22: 4
l21: 5
l18: 6
l17: 7
l28: 8
l23: 6
l25: 7

2.4.8 Trivial Cooperation Program

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

2.5 SCC Subproblem 5/5

Here we consider the SCC { l41, l30 }.

2.5.1 Transition Removal

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

l30: −2⋅x5 + 2⋅x13 + 1
l41: −2⋅x5 + 2⋅x13

2.5.2 Transition Removal

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

l30: 0
l41: −1

2.5.3 Trivial Cooperation Program

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

Tool configuration

AProVE