# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 4
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ y_13_0 ≤ 0 ∧ rt_11_post − st_14_0 ≤ 0 ∧ − rt_11_post + st_14_0 ≤ 0 ∧ rt_11_0 − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_post ≤ 0 ∧ − y_13_post + y_13_post ≤ 0 ∧ y_13_post − y_13_post ≤ 0 ∧ − y_13_0 + y_13_0 ≤ 0 ∧ y_13_0 − y_13_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 0 1 2: 1 − y_13_0 ≤ 0 ∧ − y_13_post + y_13_post ≤ 0 ∧ y_13_post − y_13_post ≤ 0 ∧ − y_13_0 + y_13_0 ≤ 0 ∧ y_13_0 − y_13_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 2 2 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ x_15_0 ≤ 0 ∧ rt_11_post − st_14_0 ≤ 0 ∧ − rt_11_post + st_14_0 ≤ 0 ∧ rt_11_0 − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_post ≤ 0 ∧ − y_13_post + y_13_post ≤ 0 ∧ y_13_post − y_13_post ≤ 0 ∧ − y_13_0 + y_13_0 ≤ 0 ∧ y_13_0 − y_13_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 2 3 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − x_15_0 ≤ 0 ∧ − x_15_0 + x_15_post + y_13_0 ≤ 0 ∧ x_15_0 − x_15_post − y_13_0 ≤ 0 ∧ −1 − y_13_0 + y_13_post ≤ 0 ∧ 1 + y_13_0 − y_13_post ≤ 0 ∧ x_15_0 − x_15_post ≤ 0 ∧ − x_15_0 + x_15_post ≤ 0 ∧ y_13_0 − y_13_post ≤ 0 ∧ − y_13_0 + y_13_post ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 3 4 2: − y_13_post + y_13_post ≤ 0 ∧ y_13_post − y_13_post ≤ 0 ∧ − y_13_0 + y_13_0 ≤ 0 ∧ y_13_0 − y_13_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 4 5 0: − y_13_post + y_13_post ≤ 0 ∧ y_13_post − y_13_post ≤ 0 ∧ − y_13_0 + y_13_0 ≤ 0 ∧ y_13_0 − y_13_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 2 6 2: − y_13_post + y_13_post ≤ 0 ∧ y_13_post − y_13_post ≤ 0 ∧ − y_13_0 + y_13_0 ≤ 0 ∧ y_13_0 − y_13_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 2 Transition Removal

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

 4: 0 0: 0 2: 0 3: 0 1: 0 4: −5 0: −6 2: −7 3: −7 2_var_snapshot: −7 2*: −7 1: −11
Hints:
 7 lexWeak[ [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, 0, 0] ] 4 lexWeak[ [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] ] 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] ] 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] ] 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] ]

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

2* 9 2: y_13_post + y_13_post ≤ 0y_13_posty_13_post ≤ 0y_13_0 + y_13_0 ≤ 0y_13_0y_13_0 ≤ 0x_15_post + x_15_post ≤ 0x_15_postx_15_post ≤ 0x_15_0 + x_15_0 ≤ 0x_15_0x_15_0 ≤ 0st_14_0 + st_14_0 ≤ 0st_14_0st_14_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0

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

2 7 2_var_snapshot: y_13_post + y_13_post ≤ 0y_13_posty_13_post ≤ 0y_13_0 + y_13_0 ≤ 0y_13_0y_13_0 ≤ 0x_15_post + x_15_post ≤ 0x_15_postx_15_post ≤ 0x_15_0 + x_15_0 ≤ 0x_15_0x_15_0 ≤ 0st_14_0 + st_14_0 ≤ 0st_14_0st_14_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_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 { 2, 3, 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 6.

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

 7: __snapshot_2_y_13_post ≤ y_13_post ∧ y_13_post ≤ __snapshot_2_y_13_post 9: __snapshot_2_y_13_post ≤ __snapshot_2_y_13_post ∧ __snapshot_2_y_13_post ≤ __snapshot_2_y_13_post 3: __snapshot_2_y_13_post ≤ __snapshot_2_y_13_post ∧ __snapshot_2_y_13_post ≤ __snapshot_2_y_13_post 4: __snapshot_2_y_13_post ≤ __snapshot_2_y_13_post ∧ __snapshot_2_y_13_post ≤ __snapshot_2_y_13_post

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

 7: __snapshot_2_y_13_0 ≤ y_13_0 ∧ y_13_0 ≤ __snapshot_2_y_13_0 9: __snapshot_2_y_13_0 ≤ __snapshot_2_y_13_0 ∧ __snapshot_2_y_13_0 ≤ __snapshot_2_y_13_0 3: __snapshot_2_y_13_0 ≤ __snapshot_2_y_13_0 ∧ __snapshot_2_y_13_0 ≤ __snapshot_2_y_13_0 4: __snapshot_2_y_13_0 ≤ __snapshot_2_y_13_0 ∧ __snapshot_2_y_13_0 ≤ __snapshot_2_y_13_0

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

 7: __snapshot_2_x_15_post ≤ x_15_post ∧ x_15_post ≤ __snapshot_2_x_15_post 9: __snapshot_2_x_15_post ≤ __snapshot_2_x_15_post ∧ __snapshot_2_x_15_post ≤ __snapshot_2_x_15_post 3: __snapshot_2_x_15_post ≤ __snapshot_2_x_15_post ∧ __snapshot_2_x_15_post ≤ __snapshot_2_x_15_post 4: __snapshot_2_x_15_post ≤ __snapshot_2_x_15_post ∧ __snapshot_2_x_15_post ≤ __snapshot_2_x_15_post

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

 7: __snapshot_2_x_15_0 ≤ x_15_0 ∧ x_15_0 ≤ __snapshot_2_x_15_0 9: __snapshot_2_x_15_0 ≤ __snapshot_2_x_15_0 ∧ __snapshot_2_x_15_0 ≤ __snapshot_2_x_15_0 3: __snapshot_2_x_15_0 ≤ __snapshot_2_x_15_0 ∧ __snapshot_2_x_15_0 ≤ __snapshot_2_x_15_0 4: __snapshot_2_x_15_0 ≤ __snapshot_2_x_15_0 ∧ __snapshot_2_x_15_0 ≤ __snapshot_2_x_15_0

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

 7: __snapshot_2_st_14_0 ≤ st_14_0 ∧ st_14_0 ≤ __snapshot_2_st_14_0 9: __snapshot_2_st_14_0 ≤ __snapshot_2_st_14_0 ∧ __snapshot_2_st_14_0 ≤ __snapshot_2_st_14_0 3: __snapshot_2_st_14_0 ≤ __snapshot_2_st_14_0 ∧ __snapshot_2_st_14_0 ≤ __snapshot_2_st_14_0 4: __snapshot_2_st_14_0 ≤ __snapshot_2_st_14_0 ∧ __snapshot_2_st_14_0 ≤ __snapshot_2_st_14_0

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

 7: __snapshot_2_rt_11_post ≤ rt_11_post ∧ rt_11_post ≤ __snapshot_2_rt_11_post 9: __snapshot_2_rt_11_post ≤ __snapshot_2_rt_11_post ∧ __snapshot_2_rt_11_post ≤ __snapshot_2_rt_11_post 3: __snapshot_2_rt_11_post ≤ __snapshot_2_rt_11_post ∧ __snapshot_2_rt_11_post ≤ __snapshot_2_rt_11_post 4: __snapshot_2_rt_11_post ≤ __snapshot_2_rt_11_post ∧ __snapshot_2_rt_11_post ≤ __snapshot_2_rt_11_post

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

 7: __snapshot_2_rt_11_0 ≤ rt_11_0 ∧ rt_11_0 ≤ __snapshot_2_rt_11_0 9: __snapshot_2_rt_11_0 ≤ __snapshot_2_rt_11_0 ∧ __snapshot_2_rt_11_0 ≤ __snapshot_2_rt_11_0 3: __snapshot_2_rt_11_0 ≤ __snapshot_2_rt_11_0 ∧ __snapshot_2_rt_11_0 ≤ __snapshot_2_rt_11_0 4: __snapshot_2_rt_11_0 ≤ __snapshot_2_rt_11_0 ∧ __snapshot_2_rt_11_0 ≤ __snapshot_2_rt_11_0

The following invariants are asserted.

 0: TRUE 1: TRUE 2: 1 − y_13_0 ≤ 0 3: 1 − y_13_0 ≤ 0 4: TRUE 2: 1 − y_13_0 ≤ 0 ∨ 1 − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 ≤ 0 ∧ 1 − y_13_0 ≤ 0 3: 1 − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 ≤ 0 ∧ 1 − y_13_0 ≤ 0 2_var_snapshot: − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 + x_15_0 − y_13_0 ≤ 0 ∧ − y_13_0 ≤ 0 2*: 1 − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 ≤ 0 ∧ 1 − y_13_0 ≤ 0

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (4) TRUE 1 (0) TRUE 2 (1) TRUE 3 (2) 1 − y_13_0 ≤ 0 4 (1) TRUE 5 (3) 1 − y_13_0 ≤ 0 6 (2) 1 − y_13_0 ≤ 0 7 (2_var_snapshot) − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 + x_15_0 − y_13_0 ≤ 0 ∧ − y_13_0 ≤ 0 12 (2) 1 − y_13_0 ≤ 0 16 (3) 1 − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 ≤ 0 ∧ 1 − y_13_0 ≤ 0 17 (2*) 1 − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 ≤ 0 ∧ 1 − y_13_0 ≤ 0 18 (2) 1 − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 ≤ 0 ∧ 1 − y_13_0 ≤ 0 19 (2_var_snapshot) − __snapshot_2_x_15_0 + x_15_0 ≤ 0 ∧ 1 − __snapshot_2_x_15_0 + x_15_0 − y_13_0 ≤ 0 ∧ − y_13_0 ≤ 0
• initial node: 0
• cover edges:
2 → 4 Hint: auto
12 → 3 Hint: [1]
19 → 7 Hint: distribute conclusion [1, 0, 0] [0, 1, 0] [0, 0, 1]
• transition edges:
0 5 1 Hint: auto
1 0 2 Hint: auto
1 1 3 Hint: [1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
3 2 4 Hint: auto
3 3 5 Hint: [1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0]
3 6 6 Hint: [1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
5 4 12 Hint: [1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
6 7 7 Hint: distribute conclusion [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [1, 0, 0, 0, 1, 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 3 16 Hint: distribute conclusion [0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
16 4 17 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
17 9 18 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
18 7 19 Hint: distribute conclusion [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, 0, 0, 0, 0, 0, 0] [0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0] [0, 0, 1, 0, 0, 0, 1, 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.1.1.1.9 Transition Removal

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

 2: x_15_0 3: __snapshot_2_x_15_0 2_var_snapshot: __snapshot_2_x_15_0 2*: __snapshot_2_x_15_0
Hints:
7 distribute assertion
 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0] ] lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0] ]
9 lexStrict[ [1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 1, 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] ]
3 lexWeak[ [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, 0, 0, 0, 0, 0, 0, 0] ]
4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0] ]

### 5.1.1.1.10 Transition Removal

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

 2: −1 2_var_snapshot: −2 3: −3 2*: −4
Hints:
7 distribute assertion
 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, 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, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4 lexWeak[ [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.1.1.1.11 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0