LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f3654_0_remove_FieldAccess f3654_0_remove_FieldAccess f3654_0_remove_FieldAccess: 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 = x25
f3652_0_remove_FieldAccess f3652_0_remove_FieldAccess f3652_0_remove_FieldAccess: 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 = x25
f526_0_createList_Load f526_0_createList_Load f526_0_createList_Load: 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 = x25
f3554_0_entry_LE f3554_0_entry_LE f3554_0_entry_LE: 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 = x25
f4208_0_remove_EQ f4208_0_remove_EQ f4208_0_remove_EQ: 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 = x25
f3401_0_equals_Return f3401_0_equals_Return f3401_0_equals_Return: 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 = x25
f558_0_createList_Return f558_0_createList_Return f558_0_createList_Return: 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 = x25
__init __init __init: 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 = x25
f4139_0_remove_EQ f4139_0_remove_EQ f4139_0_remove_EQ: 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 = x25
f996_0_createList_Load f996_0_createList_Load f996_0_createList_Load: 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 = x25
f3307_0_remove_EQ f3307_0_remove_EQ f3307_0_remove_EQ: 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 = x25
f4555_0_remove_EQ f4555_0_remove_EQ f4555_0_remove_EQ: 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 = x25
f2756_0_random_ArrayAccess f2756_0_random_ArrayAccess f2756_0_random_ArrayAccess: 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 = x25
f4554_0_remove_EQ f4554_0_remove_EQ f4554_0_remove_EQ: 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 = x25
f2651_0_createList_LE f2651_0_createList_LE f2651_0_createList_LE: 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 = x25
f4378_0_remove_FieldAccess f4378_0_remove_FieldAccess f4378_0_remove_FieldAccess: 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 = x25
f4457_0_remove_FieldAccess f4457_0_remove_FieldAccess f4457_0_remove_FieldAccess: 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 = x25
f4209_0_remove_EQ f4209_0_remove_EQ f4209_0_remove_EQ: 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 = x25
f4374_0_remove_FieldAccess f4374_0_remove_FieldAccess f4374_0_remove_FieldAccess: 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 = x25
f3653_0_remove_FieldAccess f3653_0_remove_FieldAccess f3653_0_remove_FieldAccess: 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 = x25
f3415_0_equals_Return f3415_0_equals_Return f3415_0_equals_Return: 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 = x25
f4376_0_remove_FieldAccess f4376_0_remove_FieldAccess f4376_0_remove_FieldAccess: 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 = x25
f3651_0_remove_FieldAccess f3651_0_remove_FieldAccess f3651_0_remove_FieldAccess: 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 = x25
f4140_0_remove_EQ f4140_0_remove_EQ f4140_0_remove_EQ: 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 = x25
f4372_0_remove_FieldAccess f4372_0_remove_FieldAccess f4372_0_remove_FieldAccess: 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 = x25
f4553_0_remove_EQ f4553_0_remove_EQ f4553_0_remove_EQ: 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 = x25
f3891_0_main_CheckCast f3891_0_main_CheckCast f3891_0_main_CheckCast: 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 = x25
f3394_0_equals_Return f3394_0_equals_Return f3394_0_equals_Return: 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 = x25
f3306_0_remove_EQ f3306_0_remove_EQ f3306_0_remove_EQ: 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 = x25
f4556_0_remove_EQ f4556_0_remove_EQ f4556_0_remove_EQ: 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 = x25
f3793_0_entry_GT f3793_0_entry_GT f3793_0_entry_GT: 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 = x25
f1_0_main_Load f1_0_main_Load f1_0_main_Load: 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 = x25
f3408_0_equals_Return f3408_0_equals_Return f3408_0_equals_Return: 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 = x25
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

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

2.1 SCC Subproblem 1/9

Here we consider the SCC { f3793_0_entry_GT }.

2.1.1 Transition Removal

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

f3793_0_entry_GT: x4 + x5

2.1.2 Trivial Cooperation Program

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

2.2 SCC Subproblem 2/9

Here we consider the SCC { f3554_0_entry_LE }.

2.2.1 Transition Removal

We remove transitions 27, 28, 29, 30, 31 using the following ranking functions, which are bounded by 0.

f3554_0_entry_LE: x4x5

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

Here we consider the SCC { f4556_0_remove_EQ, f4555_0_remove_EQ, f4209_0_remove_EQ }.

2.3.1 Transition Removal

We remove transitions 76, 77, 83, 82, 85 using the following ranking functions, which are bounded by 0.

f4209_0_remove_EQ: −2 + x7 + x9
f4555_0_remove_EQ: −2 + x7 + x9
f4556_0_remove_EQ: −1 − x4 + x5 + x7

2.3.2 Transition Removal

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

f4555_0_remove_EQ: x4 + 3⋅x6 + 3⋅x11 + 2⋅x7 + 2⋅x9
f4209_0_remove_EQ: 2⋅x7 + 2⋅x9 + 3⋅x10 − 1
f4556_0_remove_EQ: 3⋅x10 + 2⋅x5 + 2⋅x7

2.3.3 Transition Removal

We remove transitions 90, 91 using the following ranking functions, which are bounded by 0.

f4555_0_remove_EQ: 0⋅x4
f4209_0_remove_EQ: −1
f4556_0_remove_EQ: 0⋅x4

2.3.4 Trivial Cooperation Program

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

2.4 SCC Subproblem 4/9

Here we consider the SCC { f4208_0_remove_EQ, f4553_0_remove_EQ, f4554_0_remove_EQ }.

2.4.1 Transition Removal

We remove transitions 74, 75, 79, 78, 81 using the following ranking functions, which are bounded by 0.

f4208_0_remove_EQ: −2 + x7 + x9
f4553_0_remove_EQ: −2 + x7 + x9
f4554_0_remove_EQ: −1 − x4 + x5 + x7

2.4.2 Transition Removal

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

f4553_0_remove_EQ: −2 + 0⋅x4 + x7 + x9
f4208_0_remove_EQ: −2 + x7 + x9
f4554_0_remove_EQ: −2 + 0⋅x4 + x5 + x7

2.4.3 Transition Removal

We remove transitions 88, 89 using the following ranking functions, which are bounded by 0.

f4553_0_remove_EQ: 0⋅x4
f4208_0_remove_EQ: −1
f4554_0_remove_EQ: 0⋅x4

2.4.4 Trivial Cooperation Program

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

2.5 SCC Subproblem 5/9

Here we consider the SCC { f4140_0_remove_EQ }.

2.5.1 Transition Removal

We remove transitions 52, 53 using the following ranking functions, which are bounded by 0.

f4140_0_remove_EQ: x5

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

Here we consider the SCC { f4139_0_remove_EQ }.

2.6.1 Transition Removal

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

f4139_0_remove_EQ: x5

2.6.2 Trivial Cooperation Program

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

2.7 SCC Subproblem 7/9

Here we consider the SCC { f3415_0_equals_Return, f3307_0_remove_EQ, f3408_0_equals_Return }.

2.7.1 Transition Removal

We remove transitions 10, 11, 13, 12, 64, 65 using the following ranking functions, which are bounded by 0.

f3307_0_remove_EQ: −1 + x6 + x8
f3408_0_equals_Return: −1 + x7 + x9
f3415_0_equals_Return: −1 + x5 + x7

2.7.2 Transition Removal

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

f3408_0_equals_Return: 0⋅x4
f3307_0_remove_EQ: −1
f3415_0_equals_Return: 0⋅x4

2.7.3 Trivial Cooperation Program

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

2.8 SCC Subproblem 8/9

Here we consider the SCC { f3306_0_remove_EQ, f3401_0_equals_Return, f3394_0_equals_Return }.

2.8.1 Transition Removal

We remove transitions 6, 7, 9, 8, 62, 63 using the following ranking functions, which are bounded by 0.

f3306_0_remove_EQ: −1 + x6 + x8
f3394_0_equals_Return: −1 + x7 + x9
f3401_0_equals_Return: −1 + x5 + x7

2.8.2 Transition Removal

We remove transitions 18, 19 using the following ranking functions, which are bounded by 0.

f3394_0_equals_Return: 0⋅x4
f3306_0_remove_EQ: −1
f3401_0_equals_Return: 0⋅x4

2.8.3 Trivial Cooperation Program

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

2.9 SCC Subproblem 9/9

Here we consider the SCC { f2651_0_createList_LE }.

2.9.1 Transition Removal

We remove transitions 98, 99 using the following ranking functions, which are bounded by 0.

f2651_0_createList_LE: x2

2.9.2 Trivial Cooperation Program

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

Tool configuration

AProVE