# 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 ∧ − arg1P ≤ 0 ∧ arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ 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 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 1 1 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ − arg3P ≤ 0 ∧ arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ − arg5P ≤ 0 ∧ arg5P ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 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 2 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 20 − arg4 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ −1 + arg3 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ 1 + arg2 − arg3P ≤ 0 ∧ −1 − arg2 + arg3P ≤ 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 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 2 3 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + arg4 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ −1 + arg3 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ 1 + arg2 − arg3P ≤ 0 ∧ −1 − arg2 + arg3P ≤ 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 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + arg2 ≤ 0 ∧ 1 − x29 + x30 ≤ 0 ∧ −19 + arg4 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ − arg3P ≤ 0 ∧ arg3P ≤ 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 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 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 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + arg2 ≤ 0 ∧ 1 + x36 − x37 ≤ 0 ∧ −19 + arg4 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ − arg3P ≤ 0 ∧ arg3P ≤ 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 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 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 6 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + arg1 ≤ 0 ∧ −19 + arg2 ≤ 0 ∧ 20 − arg4 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ 1 − arg1P + arg1 ≤ 0 ∧ −1 + arg1P − arg1 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ 1 + arg2 − arg3P ≤ 0 ∧ −1 − arg2 + 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 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 2 7 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + arg4 ≤ 0 ∧ −19 + arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 + arg5 ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ −1 + arg3P ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 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 3 8 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 ∧ − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: TRUE 2: − arg3P ≤ 0 ∧ − arg3 ≤ 0 3: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

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

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 1 9 1: − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − 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 16 2: − x37 + x37 ≤ 0 ∧ x37 − x37 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − 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.

### 3 Transition Removal

We remove transitions 0, 8 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

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

1* 12 1: x37 + x37 ≤ 0x37x37 ≤ 0x36 + x36 ≤ 0x36x36 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x29 + x29 ≤ 0x29x29 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

1 10 1_var_snapshot: x37 + x37 ≤ 0x37x37 ≤ 0x36 + x36 ≤ 0x36x36 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x29 + x29 ≤ 0x29x29 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

2* 19 2: x37 + x37 ≤ 0x37x37 ≤ 0x36 + x36 ≤ 0x36x36 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x29 + x29 ≤ 0x29x29 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

2 17 2_var_snapshot: x37 + x37 ≤ 0x37x37 ≤ 0x36 + x36 ≤ 0x36x36 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x29 + x29 ≤ 0x29x29 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

### 8 SCC Decomposition

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

### 8.1 SCC Subproblem 1/1

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

### 8.1.1 Transition Removal

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

 1: 2 − 6⋅arg2 − 2⋅arg3 2: −8⋅arg2 − 4⋅arg3 1_var_snapshot: 1 − 6⋅arg2 − 2⋅arg3 1*: 3 − 6⋅arg2 − 2⋅arg3 2_var_snapshot: −8⋅arg2 − 4⋅arg3 2*: −8⋅arg2 − 4⋅arg3

### 8.1.2 Transition Removal

We remove transitions 10, 12, 2, 3 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

### 8.1.3 Transition Removal

We remove transitions 4, 5 using the following ranking functions, which are bounded by −77.

 1: 0 2: 1 − 3⋅arg4 − arg5 1_var_snapshot: 0 1*: 0 2_var_snapshot: −3⋅arg4 − arg5 2*: 2 − 3⋅arg4 − arg5

### 8.1.4 Transition Removal

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

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

### 8.1.5 Transition Removal

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

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

### 8.1.6 Splitting Cut-Point Transitions

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

### 8.1.6.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 9.

### 8.1.6.1.1 Splitting Cut-Point Transitions

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

### 8.1.6.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 16.

### 8.1.6.2.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0