LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f563_0_createList_Return f563_0_createList_Return f563_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
f3914_0_main_CheckCast f3914_0_main_CheckCast f3914_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
f4904_0_indexOf_EQ f4904_0_indexOf_EQ f4904_0_indexOf_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
f3920_0_indexOf_EQ f3920_0_indexOf_EQ f3920_0_indexOf_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
f4015_0_equals_Return f4015_0_equals_Return f4015_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
f4821_0_indexOf_EQ f4821_0_indexOf_EQ f4821_0_indexOf_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
f3555_0_entry_LE f3555_0_entry_LE f3555_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
f3801_0_entry_GT f3801_0_entry_GT f3801_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
f4900_0_indexOf_EQ f4900_0_indexOf_EQ f4900_0_indexOf_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
f4902_0_indexOf_EQ f4902_0_indexOf_EQ f4902_0_indexOf_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
__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
f4029_0_equals_Return f4029_0_equals_Return f4029_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
f2767_0_random_ArrayAccess f2767_0_random_ArrayAccess f2767_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
f4822_0_indexOf_EQ f4822_0_indexOf_EQ f4822_0_indexOf_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
f998_0_createList_Load f998_0_createList_Load f998_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
f4022_0_equals_Return f4022_0_equals_Return f4022_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
f4566_0_indexOf_EQ f4566_0_indexOf_EQ f4566_0_indexOf_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
f3921_0_indexOf_EQ f3921_0_indexOf_EQ f3921_0_indexOf_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
f4906_0_indexOf_EQ f4906_0_indexOf_EQ f4906_0_indexOf_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
f2688_0_createList_LE f2688_0_createList_LE f2688_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
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
f4036_0_equals_Return f4036_0_equals_Return f4036_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
f529_0_createList_Load f529_0_createList_Load f529_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
f4565_0_indexOf_EQ f4565_0_indexOf_EQ f4565_0_indexOf_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
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 { f3921_0_indexOf_EQ, f4036_0_equals_Return, f4029_0_equals_Return }.

2.1.1 Transition Removal

We remove transitions 26, 27, 29, 28, 40, 41 using the following ranking functions, which are bounded by 0.

f3921_0_indexOf_EQ: −1 + x6 + x9
f4029_0_equals_Return: −1 + x7 + x9
f4036_0_equals_Return: −1 + x4 + x6

2.1.2 Transition Removal

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

f4029_0_equals_Return: 0⋅x3
f3921_0_indexOf_EQ: −1
f4036_0_equals_Return: 0⋅x3

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

Here we consider the SCC { f4022_0_equals_Return, f3920_0_indexOf_EQ, f4015_0_equals_Return }.

2.2.1 Transition Removal

We remove transitions 23, 24, 38, 39 using the following ranking functions, which are bounded by 0.

f3920_0_indexOf_EQ: 2⋅x6 + 2⋅x9 − 1
f4015_0_equals_Return: 2⋅x9 + 2⋅x7
f4022_0_equals_Return: 2⋅x4 + 2⋅x6

2.2.2 Transition Removal

We remove transitions 35, 25 using the following ranking functions, which are bounded by −1.

f3920_0_indexOf_EQ: −1
f4015_0_equals_Return: −1
f4022_0_equals_Return: −2⋅x3

2.2.3 Transition Removal

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

f3920_0_indexOf_EQ: x4x8
f4015_0_equals_Return: 0⋅x3 + x4x6

2.2.4 Transition Removal

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

f3920_0_indexOf_EQ: 0
f4015_0_equals_Return: −1 + 0⋅x3

2.2.5 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 { f3801_0_entry_GT }.

2.3.1 Transition Removal

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

f3801_0_entry_GT: x4 + x5

2.3.2 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 { f3555_0_entry_LE }.

2.4.1 Transition Removal

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

f3555_0_entry_LE: x4x5

2.4.2 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 { f4822_0_indexOf_EQ, f4904_0_indexOf_EQ, f4906_0_indexOf_EQ }.

2.5.1 Transition Removal

We remove transitions 58, 64, 65, 59, 60 using the following ranking functions, which are bounded by 0.

f4822_0_indexOf_EQ: 3⋅x7 + 3⋅x11 + 2⋅x10 − 1
f4904_0_indexOf_EQ: 2⋅x9 + 3⋅x11 + 3⋅x7
f4906_0_indexOf_EQ: 3⋅x10 + 3⋅x4 + 2⋅x6

2.5.2 Transition Removal

We remove transitions 68, 69, 61 using the following ranking functions, which are bounded by 0.

f4904_0_indexOf_EQ: 1 + 0⋅x3
f4822_0_indexOf_EQ: 0
f4906_0_indexOf_EQ: 1 − 2⋅x3

2.5.3 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 { f4821_0_indexOf_EQ, f4900_0_indexOf_EQ, f4902_0_indexOf_EQ }.

2.6.1 Transition Removal

We remove transitions 62, 63, 56 using the following ranking functions, which are bounded by 0.

f4821_0_indexOf_EQ: 3⋅x7 + 3⋅x12 + 2⋅x10 − 1
f4900_0_indexOf_EQ: 2⋅x9 + 3⋅x12 + 3⋅x7
f4902_0_indexOf_EQ: 3⋅x11 + 3⋅x4 + 2⋅x6

2.6.2 Transition Removal

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

f4821_0_indexOf_EQ: −3 + x7 + x10
f4900_0_indexOf_EQ: −3 + x7 + x9
f4902_0_indexOf_EQ: −3 + x4 + x6

2.6.3 Transition Removal

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

f4900_0_indexOf_EQ: 0⋅x3
f4821_0_indexOf_EQ: −1
f4902_0_indexOf_EQ: 0⋅x3

2.6.4 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 { f4566_0_indexOf_EQ }.

2.7.1 Transition Removal

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

f4566_0_indexOf_EQ: x5

2.7.2 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 { f4565_0_indexOf_EQ }.

2.8.1 Transition Removal

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

f4565_0_indexOf_EQ: x5

2.8.2 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 { f2688_0_createList_LE }.

2.9.1 Transition Removal

We remove transitions 72, 73 using the following ranking functions, which are bounded by 0.

f2688_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