LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f4561_0_remove_EQ f4561_0_remove_EQ f4561_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
f554_0_createList_Return f554_0_createList_Return f554_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
f3399_0_equals_Return f3399_0_equals_Return f3399_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
f4150_0_remove_EQ f4150_0_remove_EQ f4150_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
f4563_0_remove_EQ f4563_0_remove_EQ f4563_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
f3634_0_remove_FieldAccess f3634_0_remove_FieldAccess f3634_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
f4562_0_remove_EQ f4562_0_remove_EQ f4562_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
__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
f2780_0_random_ArrayAccess f2780_0_random_ArrayAccess f2780_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
f3315_0_remove_EQ f3315_0_remove_EQ f3315_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
f3316_0_remove_EQ f3316_0_remove_EQ f3316_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
f3633_0_remove_FieldAccess f3633_0_remove_FieldAccess f3633_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
f3636_0_remove_FieldAccess f3636_0_remove_FieldAccess f3636_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
f3413_0_equals_Return f3413_0_equals_Return f3413_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
f4218_0_remove_EQ f4218_0_remove_EQ f4218_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
f2664_0_createList_LE f2664_0_createList_LE f2664_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
f4384_0_remove_FieldAccess f4384_0_remove_FieldAccess f4384_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
f4382_0_remove_FieldAccess f4382_0_remove_FieldAccess f4382_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
f4380_0_remove_FieldAccess f4380_0_remove_FieldAccess f4380_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
f3406_0_equals_Return f3406_0_equals_Return f3406_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
f3635_0_remove_FieldAccess f3635_0_remove_FieldAccess f3635_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
f4386_0_remove_FieldAccess f4386_0_remove_FieldAccess f4386_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
f3930_0_main_CheckCast f3930_0_main_CheckCast f3930_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
f3420_0_equals_Return f3420_0_equals_Return f3420_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
f4465_0_remove_FieldAccess f4465_0_remove_FieldAccess f4465_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
f3832_0_entry_GT f3832_0_entry_GT f3832_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
f522_0_createList_Load f522_0_createList_Load f522_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
f4149_0_remove_EQ f4149_0_remove_EQ f4149_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
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
f3589_0_entry_LE f3589_0_entry_LE f3589_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
f4564_0_remove_EQ f4564_0_remove_EQ f4564_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
f4219_0_remove_EQ f4219_0_remove_EQ f4219_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
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 { f3832_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.

f3832_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 { f3589_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.

f3589_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 { f4563_0_remove_EQ, f4564_0_remove_EQ, f4219_0_remove_EQ }.

2.3.1 Transition Removal

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

f4219_0_remove_EQ: 2⋅x7 + 3⋅x10 + 2⋅x9 − 1
f4563_0_remove_EQ: 3⋅x11 + 2⋅x7 + 2⋅x9
f4564_0_remove_EQ: 3⋅x10 + 2⋅x5 + 2⋅x7

2.3.2 Transition Removal

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

f4219_0_remove_EQ: −3 + x7 + x9
f4563_0_remove_EQ: −2 + 0⋅x4 + x7 + x9
f4564_0_remove_EQ: −3 + x5 + x7

2.3.3 Transition Removal

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

f4563_0_remove_EQ: −4 + 0⋅x4 + x7 + x8 + x9
f4219_0_remove_EQ: −4 + x7 + x8 + x9
f4564_0_remove_EQ: −4 + 0⋅x4 + x5 + x6 + x7

2.3.4 Transition Removal

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

f4563_0_remove_EQ: 0⋅x4
f4219_0_remove_EQ: −1
f4564_0_remove_EQ: 0⋅x4

2.3.5 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 { f4218_0_remove_EQ, f4561_0_remove_EQ, f4562_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.

f4218_0_remove_EQ: −2 + x7 + x9
f4561_0_remove_EQ: −2 + x7 + x9
f4562_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.

f4561_0_remove_EQ: −2 + 0⋅x4 + x7 + x9
f4218_0_remove_EQ: −2 + x7 + x9
f4562_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.

f4561_0_remove_EQ: 0⋅x4
f4218_0_remove_EQ: −1
f4562_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 { f4150_0_remove_EQ }.

2.5.1 Transition Removal

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

f4150_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 { f4149_0_remove_EQ }.

2.6.1 Transition Removal

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

f4149_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 { f3316_0_remove_EQ, f3420_0_equals_Return, f3413_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.

f3316_0_remove_EQ: −1 + x6 + x8
f3413_0_equals_Return: −1 + x7 + x9
f3420_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.

f3413_0_equals_Return: x1
f3316_0_remove_EQ: 0
f3420_0_equals_Return: 1

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 { f3315_0_remove_EQ, f3399_0_equals_Return, f3406_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.

f3315_0_remove_EQ: −1 + x6 + x8
f3399_0_equals_Return: −1 + x7 + x9
f3406_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.

f3399_0_equals_Return: 0⋅x4
f3315_0_remove_EQ: −1
f3406_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 { f2664_0_createList_LE }.

2.9.1 Transition Removal

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

f2664_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