LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 31 2: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 5, 8, 11, 12, 14, 15, 16, 17, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30 using the following ranking functions, which are bounded by −17.

11: 0
10: 0
0: 0
2: 0
3: 0
4: 0
6: 0
7: 0
9: 0
5: 0
8: 0
1: 0
11: −7
10: −8
0: −9
2: −9
3: −9
4: −9
6: −9
7: −9
9: −9
2_var_snapshot: −9
2*: −9
5: −10
8: −11
1: −12

3 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2* 34 2: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2 32 2_var_snapshot: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

5 SCC Decomposition

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

5.1 SCC Subproblem 1/1

Here we consider the SCC { 0, 2, 3, 4, 6, 7, 9, 2_var_snapshot, 2* }.

5.1.1 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

5.1.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 31.

5.1.1.1.1 Fresh Variable Addition

The new variable __snapshot_2_x1_post is introduced. The transition formulas are extended as follows:

32: __snapshot_2_x1_postx1_postx1_post__snapshot_2_x1_post
34: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
1: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
2: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
3: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
4: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
6: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
7: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
9: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
10: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
13: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
18: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post
19: __snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post__snapshot_2_x1_post

5.1.1.1.2 Fresh Variable Addition

The new variable __snapshot_2_x1_0 is introduced. The transition formulas are extended as follows:

32: __snapshot_2_x1_0x1_0x1_0__snapshot_2_x1_0
34: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
1: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
2: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
3: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
4: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
6: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
7: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
9: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
10: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
13: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
18: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0
19: __snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0__snapshot_2_x1_0

5.1.1.1.3 Fresh Variable Addition

The new variable __snapshot_2_x0_post is introduced. The transition formulas are extended as follows:

32: __snapshot_2_x0_postx0_postx0_post__snapshot_2_x0_post
34: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
1: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
2: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
3: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
4: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
6: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
7: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
9: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
10: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
13: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
18: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post
19: __snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post__snapshot_2_x0_post

5.1.1.1.4 Fresh Variable Addition

The new variable __snapshot_2_x0_0 is introduced. The transition formulas are extended as follows:

32: __snapshot_2_x0_0x0_0x0_0__snapshot_2_x0_0
34: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
1: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
2: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
3: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
4: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
6: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
7: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
9: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
10: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
13: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
18: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0
19: __snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0__snapshot_2_x0_0

5.1.1.1.5 Fresh Variable Addition

The new variable __snapshot_2_oldX4_post is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX4_postoldX4_postoldX4_post__snapshot_2_oldX4_post
34: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
1: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
2: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
3: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
4: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
6: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
7: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
9: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
10: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
13: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
18: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post
19: __snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post__snapshot_2_oldX4_post

5.1.1.1.6 Fresh Variable Addition

The new variable __snapshot_2_oldX4_0 is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX4_0oldX4_0oldX4_0__snapshot_2_oldX4_0
34: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
1: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
2: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
3: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
4: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
6: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
7: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
9: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
10: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
13: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
18: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0
19: __snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0__snapshot_2_oldX4_0

5.1.1.1.7 Fresh Variable Addition

The new variable __snapshot_2_oldX3_post is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX3_postoldX3_postoldX3_post__snapshot_2_oldX3_post
34: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
1: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
2: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
3: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
4: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
6: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
7: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
9: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
10: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
13: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
18: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post
19: __snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post__snapshot_2_oldX3_post

5.1.1.1.8 Fresh Variable Addition

The new variable __snapshot_2_oldX3_0 is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX3_0oldX3_0oldX3_0__snapshot_2_oldX3_0
34: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
1: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
2: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
3: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
4: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
6: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
7: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
9: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
10: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
13: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
18: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0
19: __snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0__snapshot_2_oldX3_0

5.1.1.1.9 Fresh Variable Addition

The new variable __snapshot_2_oldX2_post is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX2_postoldX2_postoldX2_post__snapshot_2_oldX2_post
34: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
1: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
2: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
3: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
4: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
6: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
7: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
9: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
10: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
13: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
18: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post
19: __snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post__snapshot_2_oldX2_post

5.1.1.1.10 Fresh Variable Addition

The new variable __snapshot_2_oldX2_0 is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX2_0oldX2_0oldX2_0__snapshot_2_oldX2_0
34: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
1: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
2: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
3: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
4: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
6: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
7: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
9: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
10: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
13: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
18: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0
19: __snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0__snapshot_2_oldX2_0

5.1.1.1.11 Fresh Variable Addition

The new variable __snapshot_2_oldX1_post is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX1_postoldX1_postoldX1_post__snapshot_2_oldX1_post
34: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
1: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
2: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
3: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
4: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
6: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
7: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
9: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
10: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
13: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
18: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post
19: __snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post__snapshot_2_oldX1_post

5.1.1.1.12 Fresh Variable Addition

The new variable __snapshot_2_oldX1_0 is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX1_0oldX1_0oldX1_0__snapshot_2_oldX1_0
34: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
1: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
2: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
3: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
4: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
6: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
7: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
9: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
10: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
13: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
18: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0
19: __snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0__snapshot_2_oldX1_0

5.1.1.1.13 Fresh Variable Addition

The new variable __snapshot_2_oldX0_post is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX0_postoldX0_postoldX0_post__snapshot_2_oldX0_post
34: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
1: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
2: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
3: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
4: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
6: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
7: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
9: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
10: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
13: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
18: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post
19: __snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post__snapshot_2_oldX0_post

5.1.1.1.14 Fresh Variable Addition

The new variable __snapshot_2_oldX0_0 is introduced. The transition formulas are extended as follows:

32: __snapshot_2_oldX0_0oldX0_0oldX0_0__snapshot_2_oldX0_0
34: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
1: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
2: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
3: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
4: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
6: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
7: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
9: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
10: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
13: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
18: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0
19: __snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0__snapshot_2_oldX0_0

5.1.1.1.15 Invariant Updates

The following invariants are asserted.

0: TRUE
1: TRUE
2: TRUE
3: TRUE
4: TRUE
5: TRUE
6: TRUE
7: TRUE
8: TRUE
9: TRUE
10: TRUE
11: TRUE
0: __snapshot_2_x1_0 + x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 0
2: TRUE ∨ 1 − __snapshot_2_x1_0 + x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 0
3: __snapshot_2_x1_0 + x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 0
4: 1 − 2⋅__snapshot_2_x1_0 + x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 0
6: __snapshot_2_x1_0 + x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 01 ≤ 0
7: __snapshot_2_x1_0 + x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 01 − x1_0 ≤ 0
9: __snapshot_2_x1_0 + x1_0 ≤ 0
2_var_snapshot: __snapshot_2_x1_0 + x1_0 ≤ 0
2*: 1 − __snapshot_2_x1_0 + x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 01 − 2⋅__snapshot_2_x1_0 + 2⋅x1_0 ≤ 01 − __snapshot_2_x1_0 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

5.1.1.1.16 Transition Removal

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

0: __snapshot_2_x1_0
2: x1_0
3: __snapshot_2_x1_0
4: __snapshot_2_x1_0
6: __snapshot_2_x1_0
7: __snapshot_2_x1_0
9: __snapshot_2_x1_0
2_var_snapshot: __snapshot_2_x1_0
2*: __snapshot_2_x1_0

5.1.1.1.17 Transition Removal

We remove transition 32 using the following ranking functions, which are bounded by −11.

2: −1
2_var_snapshot: −2
9: −3
7: −4
6: −5
3: −6
4: −7
0: −8
2*: −9

5.1.1.1.18 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert