LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 2

Transitions: (pre-variables and post-variables)

0	0	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg1P + arg2P − arg3P ≤ 0 ∧ − arg1P − arg2P + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0
1	1	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg1 + arg2 ≤ 0 ∧ −1 − arg1P + arg1 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ −1 + arg1 + arg2 − arg3P ≤ 0 ∧ 1 − arg1 − arg2 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
1	2	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg1 + arg2 − arg3P ≤ 0 ∧ 1 − arg1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
1	3	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ arg1 − arg2 ≤ 0 ∧ − arg1 + arg2 ≤ 0 ∧ −1 − arg1P + arg1 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ −1 + 2⋅arg1 − arg3P ≤ 0 ∧ 1 − 2⋅arg1 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0
2	4	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

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

− 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, 4 using the following ranking functions, which are bounded by −11.

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

3 Location Addition

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

1* 8 1: − 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 6 1_var_snapshot: − 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 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 { 1, 1_var_snapshot, 1* }.

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 5.

5.1.1.1.1 Fresh Variable Addition

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

6:	__snapshot_1_arg3P ≤ arg3P ∧ arg3P ≤ __snapshot_1_arg3P
8:	__snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P
1:	__snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P
2:	__snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P
3:	__snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P

5.1.1.1.2 Fresh Variable Addition

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

6:	__snapshot_1_arg3 ≤ arg3 ∧ arg3 ≤ __snapshot_1_arg3
8:	__snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3
1:	__snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3
2:	__snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3
3:	__snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3

5.1.1.1.3 Fresh Variable Addition

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

6:	__snapshot_1_arg2P ≤ arg2P ∧ arg2P ≤ __snapshot_1_arg2P
8:	__snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P
1:	__snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P
2:	__snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P
3:	__snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P

5.1.1.1.4 Fresh Variable Addition

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

6:	__snapshot_1_arg2 ≤ arg2 ∧ arg2 ≤ __snapshot_1_arg2
8:	__snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2
1:	__snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2
2:	__snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2
3:	__snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2

5.1.1.1.5 Fresh Variable Addition

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

6:	__snapshot_1_arg1P ≤ arg1P ∧ arg1P ≤ __snapshot_1_arg1P
8:	__snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P
1:	__snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P
2:	__snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P
3:	__snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P

5.1.1.1.6 Fresh Variable Addition

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

6:	__snapshot_1_arg1 ≤ arg1 ∧ arg1 ≤ __snapshot_1_arg1
8:	__snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1
1:	__snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1
2:	__snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1
3:	__snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1

5.1.1.1.7 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ −1 − 2⋅arg1 ≤ 0 ∨ −2 − 2⋅arg1 + arg3 ≤ 0 ∧ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0 ∨ 1 ≤ 0
2:	TRUE
1:	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ −1 − 2⋅arg1 ≤ 0 ∨ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ 1 − __snapshot_1_arg1 + __snapshot_1_arg2 + arg1 − arg2 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 ≤ 0 ∨ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0 ∨ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ arg1 − arg2 ≤ 0 ∨ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
1_var_snapshot:	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 − arg1 + arg2 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∨ − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0 ∨ − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0 ∨ − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0
1*:	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∨ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0 ∨ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ 1 − __snapshot_1_arg1 + __snapshot_1_arg2 + arg1 − arg2 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 ≤ 0 ∨ 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(2)	TRUE
1	(0)	TRUE
2	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ −1 − 2⋅arg1 ≤ 0
3	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ −1 − 2⋅arg1 ≤ 0
4	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ −1 − 2⋅arg1 ≤ 0
5	(1)	−2 − 2⋅arg1 + arg3 ≤ 0 ∧ −1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0
6	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ −1 − 2⋅arg1 ≤ 0
7	(1_var_snapshot)	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 − arg1 + arg2 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0
12	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
13	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0
14	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ 1 − __snapshot_1_arg1 + __snapshot_1_arg2 + arg1 − arg2 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 ≤ 0
15	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ 1 − __snapshot_1_arg1 + __snapshot_1_arg2 + arg1 − arg2 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 ≤ 0
16	(1_var_snapshot)	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0
17	(1_var_snapshot)	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∧ 1 + arg1 − arg2 ≤ 0
25	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0
26	(1_var_snapshot)	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0
27	(1_var_snapshot)	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0
51	(1)	1 ≤ 0
52	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ −1 − 2⋅arg1 ≤ 0
53	(1)	1 ≤ 0
54	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ arg1 − arg2 ≤ 0
55	(1_var_snapshot)	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0 ∧ arg1 − arg2 ≤ 0
58	(1*)	1 ≤ 0
59	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
60	(1*)	1 ≤ 0
61	(1*)	1 ≤ 0
62	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
63	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
64	(1)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
65	(1_var_snapshot)	− __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ −1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg3 ≤ 0 ∧ −2⋅__snapshot_1_arg1 + 2⋅__snapshot_1_arg2 + 2⋅arg1 − 2⋅arg2 ≤ 0
73	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
74	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0
75	(1*)	−1 − arg1 − arg2 + arg3 ≤ 0 ∧ 1 − __snapshot_1_arg1 − __snapshot_1_arg2 + arg1 + arg2 ≤ 0 ∧ − __snapshot_1_arg1 − __snapshot_1_arg2 ≤ 0

initial node: 0
cover edges:

3 → 2

4 → 2

16 → 17

26 → 27

52 → 2

55 → 27

59 → 12

62 → 12

63 → 12

73 → 12

74 → 12

75 → 12

transition edges:

0	4 1
1	0 2
2	1 3
2	2 4
2	3 5
2	5 6
5	1 51
5	2 52
5	3 53
5	5 54
6	6 7
7	1 12
7	2 13
7	3 14
12	8 64
13	8 25
14	8 15
15	6 16
15	6 17
17	1 58
17	2 59
17	3 60
25	6 26
25	6 27
27	1 61
27	2 62
27	3 63
54	6 55
64	6 65
65	1 73
65	2 74
65	3 75

5.1.1.1.8 Transition Removal

We remove transition 8 using the following lexicographic ranking functions, which are bounded by [−2, −2].

1:	[arg1 + arg2, 2⋅arg1 − 2⋅arg2]
1_var_snapshot:	[__snapshot_1_arg1 + __snapshot_1_arg2, 2⋅__snapshot_1_arg1 − 2⋅__snapshot_1_arg2]
1*:	[__snapshot_1_arg1 + __snapshot_1_arg2, 2⋅__snapshot_1_arg1 − 2⋅__snapshot_1_arg2]

5.1.1.1.9 Transition Removal

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

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

5.1.1.1.10 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0

3	→ 2
4	→ 2
16	→ 17
26	→ 27
52	→ 2
55	→ 27
59	→ 12
62	→ 12
63	→ 12
73	→ 12
74	→ 12
75	→ 12