LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f3763_0_lastIndexOf_EQ f3763_0_lastIndexOf_EQ f3763_0_lastIndexOf_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
f557_0_createList_Return f557_0_createList_Return f557_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
f3310_0_entry_LE f3310_0_entry_LE f3310_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
f3192_0_equals_Return f3192_0_equals_Return f3192_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
f3501_0_main_CheckCast f3501_0_main_CheckCast f3501_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
__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
f3701_0_lastIndexOf_EQ f3701_0_lastIndexOf_EQ f3701_0_lastIndexOf_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
f3702_0_lastIndexOf_EQ f3702_0_lastIndexOf_EQ f3702_0_lastIndexOf_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
f3078_0_lastIndexOf_EQ f3078_0_lastIndexOf_EQ f3078_0_lastIndexOf_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
f3947_0_lastIndexOf_EQ f3947_0_lastIndexOf_EQ f3947_0_lastIndexOf_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
f3171_0_equals_Return f3171_0_equals_Return f3171_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
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
f3185_0_equals_Return f3185_0_equals_Return f3185_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
f3946_0_lastIndexOf_EQ f3946_0_lastIndexOf_EQ f3946_0_lastIndexOf_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
f2433_0_createList_LE f2433_0_createList_LE f2433_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
f3178_0_equals_Return f3178_0_equals_Return f3178_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
f3933_0_lastIndexOf_EQ f3933_0_lastIndexOf_EQ f3933_0_lastIndexOf_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
f525_0_createList_Load f525_0_createList_Load f525_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
f2526_0_random_ArrayAccess f2526_0_random_ArrayAccess f2526_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
f3077_0_lastIndexOf_EQ f3077_0_lastIndexOf_EQ f3077_0_lastIndexOf_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
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
f3450_0_entry_GT f3450_0_entry_GT f3450_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
f4005_0_lastIndexOf_EQ f4005_0_lastIndexOf_EQ f4005_0_lastIndexOf_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
f4007_0_lastIndexOf_EQ f4007_0_lastIndexOf_EQ f4007_0_lastIndexOf_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 { f3450_0_entry_GT }.

2.1.1 Transition Removal

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

f3450_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 { f3310_0_entry_LE }.

2.2.1 Transition Removal

We remove transitions 23, 24, 25, 26, 27 using the following ranking functions, which are bounded by 0.

f3310_0_entry_LE: x5 + x4

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 { f3933_0_lastIndexOf_EQ, f4005_0_lastIndexOf_EQ, f4007_0_lastIndexOf_EQ }.

2.3.1 Transition Removal

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

f3933_0_lastIndexOf_EQ: 3⋅x6 + 3⋅x11 + 2⋅x10 − 1
f4005_0_lastIndexOf_EQ: 2⋅x9 + 3⋅x10 + 3⋅x7
f4007_0_lastIndexOf_EQ: 3⋅x7 + 3⋅x4 + 2⋅x6

2.3.2 Transition Removal

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

f3933_0_lastIndexOf_EQ: −3 + x6 + x10
f4005_0_lastIndexOf_EQ: −3 + 0⋅x3 + x7 + x9
f4007_0_lastIndexOf_EQ: −3 + x4 + x6

2.3.3 Transition Removal

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

f4005_0_lastIndexOf_EQ: 0⋅x3
f3933_0_lastIndexOf_EQ: −1
f4007_0_lastIndexOf_EQ: 0⋅x3

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 { f3763_0_lastIndexOf_EQ, f3947_0_lastIndexOf_EQ, f3946_0_lastIndexOf_EQ }.

2.4.1 Transition Removal

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

f3763_0_lastIndexOf_EQ: −2 + x7 + x9
f3946_0_lastIndexOf_EQ: −2 + x6 + x8
f3947_0_lastIndexOf_EQ: −1 − x3 + x4 + x6

2.4.2 Transition Removal

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

f3946_0_lastIndexOf_EQ: −2 + 0⋅x3 + x6 + x8
f3763_0_lastIndexOf_EQ: −2 + x7 + x9
f3947_0_lastIndexOf_EQ: −2 + 0⋅x3 + x4 + x6

2.4.3 Transition Removal

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

f3946_0_lastIndexOf_EQ: 0
f3763_0_lastIndexOf_EQ: −1
f3947_0_lastIndexOf_EQ: 0

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 { f3702_0_lastIndexOf_EQ }.

2.5.1 Transition Removal

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

f3702_0_lastIndexOf_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 { f3701_0_lastIndexOf_EQ }.

2.6.1 Transition Removal

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

f3701_0_lastIndexOf_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 { f3078_0_lastIndexOf_EQ, f3185_0_equals_Return, f3192_0_equals_Return }.

2.7.1 Transition Removal

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

f3078_0_lastIndexOf_EQ: 2⋅x6 + 2⋅x8 − 1
f3185_0_equals_Return: 2⋅x8 + 2⋅x6
f3192_0_equals_Return: 2⋅x4 + 2⋅x6

2.7.2 Transition Removal

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

f3078_0_lastIndexOf_EQ: −3 + x6 + x8
f3185_0_equals_Return: −3 + x6 + x8
f3192_0_equals_Return: −3 + x4 + x6

2.7.3 Transition Removal

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

f3185_0_equals_Return: 0
f3078_0_lastIndexOf_EQ: −1
f3192_0_equals_Return: 0

2.7.4 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 { f3171_0_equals_Return, f3178_0_equals_Return, f3077_0_lastIndexOf_EQ }.

2.8.1 Transition Removal

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

f3077_0_lastIndexOf_EQ: 2⋅x6 + 2⋅x8 − 1
f3171_0_equals_Return: 2⋅x8 + 2⋅x6
f3178_0_equals_Return: 2⋅x4 + 2⋅x6

2.8.2 Transition Removal

We remove transitions 7, 19, 9 using the following ranking functions, which are bounded by −1.

f3077_0_lastIndexOf_EQ: −1
f3171_0_equals_Return: x3 − 1
f3178_0_equals_Return: −2⋅x3

2.8.3 Transition Removal

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

f3077_0_lastIndexOf_EQ: −3⋅x4 + 3⋅x5 + 2
f3171_0_equals_Return: 3⋅x4 − 3⋅x5

2.8.4 Transition Removal

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

f3077_0_lastIndexOf_EQ: x3
f3171_0_equals_Return: 0

2.8.5 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 { f2433_0_createList_LE }.

2.9.1 Transition Removal

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

f2433_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