LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: −2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0
1: −2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0
2: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 0−10 + x_promoted_1_0 ≤ 010 − x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0−1 + a15_post ≤ 0−2 + b16_post ≤ 0−10 + c17_post ≤ 0−1 + a15_0 ≤ 0
3: −2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0
4: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 0−10 + x_promoted_1_0 ≤ 010 − x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0
5: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 0−10 + x_promoted_1_0 ≤ 010 − x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0
6: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 0−10 + x_promoted_1_0 ≤ 010 − x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0−1 + a15_post ≤ 0−2 + b16_post ≤ 0−10 + c17_post ≤ 0−1 + a15_0 ≤ 0−10 + c17_0 ≤ 0
7: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 0−10 + x_promoted_1_0 ≤ 010 − x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0−1 + a15_post ≤ 0−2 + b16_post ≤ 0−10 + c17_post ≤ 0−1 + a15_0 ≤ 0−2 + b16_0 ≤ 0−10 + c17_0 ≤ 0
8: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 010 − x_promoted_1_0 ≤ 0−1 + x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0−1 + a10_post ≤ 0−2 + b11_post ≤ 0−1 + c12_post ≤ 0−1 + a10_0 ≤ 0b11_0 ≤ 0−1 + c12_0 ≤ 0
9: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 010 − x_promoted_1_0 ≤ 0−1 + x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0−1 + a10_post ≤ 0−2 + b11_post ≤ 0−1 + c12_post ≤ 0−1 + a10_0 ≤ 0
10: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 010 − x_promoted_1_0 ≤ 0−1 + x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0−1 + a10_post ≤ 0−2 + b11_post ≤ 0−1 + c12_post ≤ 0−1 + a10_0 ≤ 0−2 + b11_0 ≤ 0−1 + c12_0 ≤ 0
11: −10 + x_promoted_1_post ≤ 010 − x_promoted_1_post ≤ 0−2 + y_promoted_2_post ≤ 02 − y_promoted_2_post ≤ 0−1 + z_post ≤ 01 − z_post ≤ 010 − x_promoted_1_0 ≤ 0−1 + x_promoted_1_0 ≤ 0−2 + y_promoted_2_0 ≤ 02 − y_promoted_2_0 ≤ 0−1 + z_0 ≤ 01 − z_0 ≤ 0−1 + a10_post ≤ 0−2 + b11_post ≤ 0−1 + c12_post ≤ 0−1 + a10_0 ≤ 0−2 + b11_0 ≤ 0−1 + c12_0 ≤ 0
12: TRUE
13: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 using the following ranking functions, which are bounded by −30.

13: 0
12: 0
4: 0
5: 0
7: 0
6: 0
2: 0
11: 0
8: 0
10: 0
9: 0
3: 0
0: 0
1: 0
13: −15
12: −16
4: −17
5: −18
7: −19
6: −20
2: −21
11: −22
8: −23
10: −24
9: −25
3: −26
0: −27
1: −28

4 SCC Decomposition

There exist no SCC in the program graph.

Tool configuration

T2Cert