# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 8
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − j_0 + x1_post ≤ 0 ∧ j_0 − x1_post ≤ 0 ∧ −1 − j_0 + y2_post ≤ 0 ∧ 1 + j_0 − y2_post ≤ 0 ∧ tmp3_0 − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ y2_0 − y2_post ≤ 0 ∧ − y2_0 + y2_post ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 0 1 1: − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 2 2 3: 4 − j_0 ≤ 0 ∧ − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 2 3 0: −3 + j_0 ≤ 0 ∧ − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 4 4 5: − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 6 5 2: − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 3 6 4: − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 3 7 4: − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 1 8 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 7 9 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ j_post ≤ 0 ∧ − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 8 10 7: − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: TRUE 2: TRUE 3: 4 − j_0 ≤ 0 4: 4 − j_0 ≤ 0 5: 4 − j_0 ≤ 0 6: TRUE 7: TRUE 8: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) TRUE 2 (2) TRUE 3 (3) 4 − j_0 ≤ 0 4 (4) 4 − j_0 ≤ 0 5 (5) 4 − j_0 ≤ 0 6 (6) TRUE 7 (7) TRUE 8 (8) TRUE
• initial node: 8
• cover edges:
• transition edges:  0 0 1 0 1 1 1 8 6 2 2 3 2 3 0 3 6 4 3 7 4 4 4 5 6 5 2 7 9 6 8 10 7

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 6 11 6: − y2_post + y2_post ≤ 0 ∧ y2_post − y2_post ≤ 0 ∧ − y2_0 + y2_0 ≤ 0 ∧ y2_0 − y2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 2, 4, 6, 7, 9, 10 using the following ranking functions, which are bounded by −17.

 8: 0 7: 0 0: 0 1: 0 2: 0 6: 0 3: 0 4: 0 5: 0 8: −7 7: −8 0: −9 1: −9 2: −9 6: −9 6_var_snapshot: −9 6*: −9 3: −10 4: −11 5: −12
Hints:
 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 2 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 4 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

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

6* 14 6: y2_post + y2_post ≤ 0y2_posty2_post ≤ 0y2_0 + y2_0 ≤ 0y2_0y2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0tmp3_post + tmp3_post ≤ 0tmp3_posttmp3_post ≤ 0tmp3_0 + tmp3_0 ≤ 0tmp3_0tmp3_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

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

6 12 6_var_snapshot: y2_post + y2_post ≤ 0y2_posty2_post ≤ 0y2_0 + y2_0 ≤ 0y2_0y2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0tmp3_post + tmp3_post ≤ 0tmp3_posttmp3_post ≤ 0tmp3_0 + tmp3_0 ≤ 0tmp3_0tmp3_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

### 6 SCC Decomposition

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

### 6.1 SCC Subproblem 1/1

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

### 6.1.1 Transition Removal

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

 0: 1 − 6⋅j_0 1: −6⋅j_0 2: 2 − 6⋅j_0 6: 4 − 6⋅j_0 6_var_snapshot: 3 − 6⋅j_0 6*: 5 − 6⋅j_0
Hints:
 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6] ] 14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6] ] 3 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6] , [6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6] ] 8 lexWeak[ [0, 0, 0, 6, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 6.1.2 Transition Removal

We remove transitions 12, 14, 0, 1, 5, 8 using the following ranking functions, which are bounded by −4.

 0: 1 1: 0 2: −4 6: −2 6_var_snapshot: −3 6*: −1
Hints:
 12 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 14 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 0 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 1 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 6.1.3 Splitting Cut-Point Transitions

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

### 6.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 11.

### 6.1.3.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0