LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 3

Transitions: (pre-variables and post-variables)

0	0	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg2P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg1P ≤ 0 ∧ arg1P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0
1	1	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − arg1P + arg3 ≤ 0 ∧ arg1P − arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg2 − arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ arg3 − arg4P ≤ 0 ∧ − arg3 + arg4P ≤ 0 ∧ arg3 − arg5P ≤ 0 ∧ − arg3 + arg5P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0
2	2	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ 1 − arg4P + arg4 ≤ 0 ∧ −1 + arg4P − arg4 ≤ 0 ∧ 1 + arg4 − arg5P ≤ 0 ∧ −1 − arg4 + arg5P ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	3	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ 1 − arg4P + arg4 ≤ 0 ∧ −1 + arg4P − arg4 ≤ 0 ∧ 1 + arg4 − arg5P ≤ 0 ∧ −1 − arg4 + arg5P ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	4	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ −1 − arg3P + arg3 ≤ 0 ∧ 1 + arg3P − arg3 ≤ 0 ∧ −1 − arg4P + arg4 ≤ 0 ∧ 1 + arg4P − arg4 ≤ 0 ∧ −1 + arg4 − arg5P ≤ 0 ∧ 1 − arg4 + arg5P ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	5	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ − arg5 ≤ 0 ∧ arg5 ≤ 0 ∧ 1 − arg1P + arg2 ≤ 0 ∧ −1 + arg1P − arg2 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0
3	6	0:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

1	7	1:	− arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	14	2:	− arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

and for every transition t, a duplicate t is considered.

2 Transition Removal

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

3:	0
0:	0
1:	0
2:	0
3:	−4
0:	−5
1:	−6
2:	−6
1_var_snapshot:	−6
1*:	−6
2_var_snapshot:	−6
2*:	−6

3 Location Addition

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

1* 10 1: − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

4 Location Addition

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

1 8 1_var_snapshot: − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

5 Location Addition

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

2* 17 2: − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

6 Location Addition

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

2 15 2_var_snapshot: − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

7 SCC Decomposition

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

7.1 SCC Subproblem 1/1

Here we consider the SCC { 1, 2, 1_var_snapshot, 1*, 2_var_snapshot, 2* }.

7.1.1 Transition Removal

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

1:	−2 + 4⋅arg2
2:	4⋅arg3 − arg4 − 3⋅arg5
1_var_snapshot:	−3 + 4⋅arg2
1*:	−1 + 4⋅arg2
2_var_snapshot:	4⋅arg3 − arg4 − 3⋅arg5
2*:	4⋅arg3 − arg4 − 3⋅arg5

7.1.2 Transition Removal

We remove transitions 8, 10, 3, 5 using the following ranking functions, which are bounded by −3.

1:	−2
2:	0
1_var_snapshot:	−3
1*:	−1
2_var_snapshot:	0
2*:	0

7.1.3 Splitting Cut-Point Transitions

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

7.1.3.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 7.

7.1.3.1.1 Splitting Cut-Point Transitions

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

7.1.3.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 14.

7.1.3.2.1 Fresh Variable Addition

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

8:	__snapshot_2_arg5P ≤ __snapshot_2_arg5P ∧ __snapshot_2_arg5P ≤ __snapshot_2_arg5P
15:	__snapshot_2_arg5P ≤ arg5P ∧ arg5P ≤ __snapshot_2_arg5P
17:	__snapshot_2_arg5P ≤ __snapshot_2_arg5P ∧ __snapshot_2_arg5P ≤ __snapshot_2_arg5P
2:	__snapshot_2_arg5P ≤ __snapshot_2_arg5P ∧ __snapshot_2_arg5P ≤ __snapshot_2_arg5P
4:	__snapshot_2_arg5P ≤ __snapshot_2_arg5P ∧ __snapshot_2_arg5P ≤ __snapshot_2_arg5P

7.1.3.2.2 Fresh Variable Addition

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

8:	__snapshot_2_arg5 ≤ __snapshot_2_arg5 ∧ __snapshot_2_arg5 ≤ __snapshot_2_arg5
15:	__snapshot_2_arg5 ≤ arg5 ∧ arg5 ≤ __snapshot_2_arg5
17:	__snapshot_2_arg5 ≤ __snapshot_2_arg5 ∧ __snapshot_2_arg5 ≤ __snapshot_2_arg5
2:	__snapshot_2_arg5 ≤ __snapshot_2_arg5 ∧ __snapshot_2_arg5 ≤ __snapshot_2_arg5
4:	__snapshot_2_arg5 ≤ __snapshot_2_arg5 ∧ __snapshot_2_arg5 ≤ __snapshot_2_arg5

7.1.3.2.3 Fresh Variable Addition

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

8:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P
15:	__snapshot_2_arg4P ≤ arg4P ∧ arg4P ≤ __snapshot_2_arg4P
17:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P
2:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P
4:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P

7.1.3.2.4 Fresh Variable Addition

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

8:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4
15:	__snapshot_2_arg4 ≤ arg4 ∧ arg4 ≤ __snapshot_2_arg4
17:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4
2:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4
4:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4

7.1.3.2.5 Fresh Variable Addition

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

8:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P
15:	__snapshot_2_arg3P ≤ arg3P ∧ arg3P ≤ __snapshot_2_arg3P
17:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P
2:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P
4:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P

7.1.3.2.6 Fresh Variable Addition

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

8:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3
15:	__snapshot_2_arg3 ≤ arg3 ∧ arg3 ≤ __snapshot_2_arg3
17:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3
2:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3
4:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3

7.1.3.2.7 Fresh Variable Addition

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

8:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P
15:	__snapshot_2_arg2P ≤ arg2P ∧ arg2P ≤ __snapshot_2_arg2P
17:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P
2:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P
4:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P

7.1.3.2.8 Fresh Variable Addition

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

8:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2
15:	__snapshot_2_arg2 ≤ arg2 ∧ arg2 ≤ __snapshot_2_arg2
17:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2
2:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2
4:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2

7.1.3.2.9 Fresh Variable Addition

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

8:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P
15:	__snapshot_2_arg1P ≤ arg1P ∧ arg1P ≤ __snapshot_2_arg1P
17:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P
2:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P
4:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P

7.1.3.2.10 Fresh Variable Addition

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

8:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1
15:	__snapshot_2_arg1 ≤ arg1 ∧ arg1 ≤ __snapshot_2_arg1
17:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1
2:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1
4:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1

7.1.3.2.11 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	TRUE
2:	1 − arg4 ≤ 0 ∨ 1 ≤ 0 ∨ − arg5 ≤ 0
3:	TRUE
1:	FALSE
2:	1 − arg4 ≤ 0 ∨ 1 − __snapshot_2_arg4 + arg4 ≤ 0 ∧ 1 − __snapshot_2_arg4 ≤ 0 ∧ − arg5 ≤ 0 ∨ − arg5 ≤ 0
1_var_snapshot:	1 ≤ 0
1*:	1 ≤ 0
2_var_snapshot:	− __snapshot_2_arg4 + arg4 ≤ 0 ∧ 1 − __snapshot_2_arg4 ≤ 0 ∧ 1 − arg4 ≤ 0 ∨ − __snapshot_2_arg4 + arg4 ≤ 0 ∧ − arg5 ≤ 0
2*:	1 ≤ 0 ∨ 1 − __snapshot_2_arg4 + arg4 ≤ 0 ∧ 1 − __snapshot_2_arg4 ≤ 0 ∧ − arg5 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(3)	TRUE
1	(0)	TRUE
2	(1)	TRUE
3	(2)	1 − arg4 ≤ 0
8	(2)	1 ≤ 0
9	(2)	1 ≤ 0
10	(2)	− arg5 ≤ 0
11	(1)	TRUE
12	(2)	1 − arg4 ≤ 0
13	(2_var_snapshot)	− __snapshot_2_arg4 + arg4 ≤ 0 ∧ 1 − __snapshot_2_arg4 ≤ 0 ∧ 1 − arg4 ≤ 0
18	(2*)	1 ≤ 0
19	(2*)	1 − __snapshot_2_arg4 + arg4 ≤ 0 ∧ 1 − __snapshot_2_arg4 ≤ 0 ∧ − arg5 ≤ 0
20	(2)	1 − __snapshot_2_arg4 + arg4 ≤ 0 ∧ 1 − __snapshot_2_arg4 ≤ 0 ∧ − arg5 ≤ 0
21	(2_var_snapshot)	− __snapshot_2_arg4 + arg4 ≤ 0 ∧ − arg5 ≤ 0
22	(2_var_snapshot)	− __snapshot_2_arg4 + arg4 ≤ 0 ∧ − arg5 ≤ 0
30	(2)	1 ≤ 0
31	(2)	1 ≤ 0
32	(2)	− arg5 ≤ 0
33	(1)	TRUE
34	(2)	− arg5 ≤ 0
35	(2_var_snapshot)	− __snapshot_2_arg4 + arg4 ≤ 0 ∧ − arg5 ≤ 0
38	(2*)	1 ≤ 0
39	(2*)	1 − __snapshot_2_arg4 + arg4 ≤ 0 ∧ 1 − __snapshot_2_arg4 ≤ 0 ∧ − arg5 ≤ 0

initial node: 0
cover edges:

11 → 2

21 → 22

32 → 10

33 → 2

35 → 22

39 → 19

transition edges:

0	6 1
1	0 2
2	1 3
3	2 8
3	3 9
3	4 10
3	5 11
3	14 12
10	2 30
10	3 31
10	4 32
10	5 33
10	14 34
12	15 13
13	2 18
13	4 19
19	17 20
20	15 21
20	15 22
22	2 38
22	4 39
34	15 35

7.1.3.2.12 Transition Removal

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

1:	__snapshot_2_arg4
2:	arg4
1_var_snapshot:	__snapshot_2_arg4
1*:	__snapshot_2_arg4
2_var_snapshot:	__snapshot_2_arg4
2*:	__snapshot_2_arg4

7.1.3.2.13 Transition Removal

We remove transition 15 using the following ranking functions, which are bounded by −8.

1:	−1
2:	−2
1_var_snapshot:	−3
1*:	−4
2_var_snapshot:	−5
2*:	−6

7.1.3.2.14 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0

11	→ 2
21	→ 22
32	→ 10
33	→ 2
35	→ 22
39	→ 19