LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: 1 − arg1P ≤ 0 ∧ 6 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 6 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0 ∧ 1 − x217 ≤ 0 ∧ 1 − x218 ≤ 0
1: 1 − arg1P ≤ 0 ∧ 6 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 6 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0 ∧ 1 − x217 ≤ 0 ∧ 1 − x218 ≤ 0
2: 1 − arg1P ≤ 0 ∧ 8 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ arg7P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 8 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ arg7 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0
3: 1 − arg1P ≤ 0 ∧ 8 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ arg7P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 8 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ arg7 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0
4: 1 − arg1P ≤ 0 ∧ 10 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 5 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 10 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 5 − arg5 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0
5: 1 − arg1P ≤ 0 ∧ 10 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 5 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 10 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 5 − arg5 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0
6: − arg1P ≤ 0 ∧ 8 − arg2P ≤ 0 ∧ −1 + arg5P ≤ 0 ∧ 1 − arg5P ≤ 0 ∧ arg6P ≤ 0 ∧ − arg6P ≤ 0 ∧ arg7P ≤ 0 ∧ − arg7P ≤ 0 ∧ − arg1 ≤ 0 ∧ 8 − arg2 ≤ 0 ∧ −1 + arg5 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ arg6 ≤ 0 ∧ − arg6 ≤ 0 ∧ arg7 ≤ 0 ∧ − arg7 ≤ 0
7: − arg1P ≤ 0 ∧ 10 − arg2P ≤ 0 ∧ arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ arg4P ≤ 0 ∧ − arg4P ≤ 0 ∧ arg8P ≤ 0 ∧ − arg8P ≤ 0 ∧ arg9P ≤ 0 ∧ − arg9P ≤ 0 ∧ arg10P ≤ 0 ∧ − arg10P ≤ 0 ∧ −1 + arg19P ≤ 0 ∧ arg22P ≤ 0 ∧ arg23P ≤ 0 ∧ − arg1 ≤ 0 ∧ 10 − arg2 ≤ 0 ∧ arg3 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg4 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg8 ≤ 0 ∧ − arg8 ≤ 0 ∧ arg9 ≤ 0 ∧ − arg9 ≤ 0 ∧ arg10 ≤ 0 ∧ − arg10 ≤ 0 ∧ −1 + arg19 ≤ 0 ∧ arg22 ≤ 0 ∧ arg23 ≤ 0
8: TRUE
9: 8 − arg1P ≤ 0 ∧ 3 − arg2P ≤ 0 ∧ 8 − arg1 ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0
11: 8 − arg1P ≤ 0 ∧ 5 − arg2P ≤ 0 ∧ arg3P ≤ 0 ∧ 8 − arg1 ≤ 0 ∧ 5 − arg2 ≤ 0 ∧ arg3 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0
12: 5 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ 5 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − x137 ≤ 0 ∧ − x138 ≤ 0 ∧ − x139 ≤ 0 ∧ 1 − x217 ≤ 0 ∧ 1 − x218 ≤ 0
13: 1 − arg1P ≤ 0 ∧ arg12P ≤ 0 ∧ − arg12P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg12 ≤ 0 ∧ − arg12 ≤ 0
14: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
13 18 13: − x436 + x436 ≤ 0 ∧ x436 − x436 ≤ 0 ∧ − x401 + x401 ≤ 0 ∧ x401 − x401 ≤ 0 ∧ − x400 + x400 ≤ 0 ∧ x400 − x400 ≤ 0 ∧ − x359 + x359 ≤ 0 ∧ x359 − x359 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x201 + x201 ≤ 0 ∧ x201 − x201 ≤ 0 ∧ − x200 + x200 ≤ 0 ∧ x200 − x200 ≤ 0 ∧ − x199 + x199 ≤ 0 ∧ x199 − x199 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x167 + x167 ≤ 0 ∧ x167 − x167 ≤ 0 ∧ − x166 + x166 ≤ 0 ∧ x166 − x166 ≤ 0 ∧ − x165 + x165 ≤ 0 ∧ x165 − x165 ≤ 0 ∧ − x139 + x139 ≤ 0 ∧ x139 − x139 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − x137 + x137 ≤ 0 ∧ x137 − x137 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 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 ∧ − arg32P + arg32P ≤ 0 ∧ arg32P − arg32P ≤ 0 ∧ − arg32 + arg32 ≤ 0 ∧ arg32 − arg32 ≤ 0 ∧ − arg31P + arg31P ≤ 0 ∧ arg31P − arg31P ≤ 0 ∧ − arg31 + arg31 ≤ 0 ∧ arg31 − arg31 ≤ 0 ∧ − arg30P + arg30P ≤ 0 ∧ arg30P − arg30P ≤ 0 ∧ − arg30 + arg30 ≤ 0 ∧ arg30 − arg30 ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 12, 13, 14, 17 using the following ranking functions, which are bounded by −33.

14: 0
8: 0
9: 0
11: 0
2: 0
3: 0
4: 0
5: 0
12: 0
0: 0
1: 0
6: 0
7: 0
13: 0
14: −15
8: −16
9: −17
11: −18
2: −19
3: −20
4: −21
5: −22
12: −23
0: −24
1: −25
6: −26
7: −27
13: −28
13_var_snapshot: −28
13*: −28

4 Location Addition

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

13* 21 13: − x436 + x436 ≤ 0 ∧ x436 − x436 ≤ 0 ∧ − x401 + x401 ≤ 0 ∧ x401 − x401 ≤ 0 ∧ − x400 + x400 ≤ 0 ∧ x400 − x400 ≤ 0 ∧ − x359 + x359 ≤ 0 ∧ x359 − x359 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x201 + x201 ≤ 0 ∧ x201 − x201 ≤ 0 ∧ − x200 + x200 ≤ 0 ∧ x200 − x200 ≤ 0 ∧ − x199 + x199 ≤ 0 ∧ x199 − x199 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x167 + x167 ≤ 0 ∧ x167 − x167 ≤ 0 ∧ − x166 + x166 ≤ 0 ∧ x166 − x166 ≤ 0 ∧ − x165 + x165 ≤ 0 ∧ x165 − x165 ≤ 0 ∧ − x139 + x139 ≤ 0 ∧ x139 − x139 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − x137 + x137 ≤ 0 ∧ x137 − x137 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 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 ∧ − arg32P + arg32P ≤ 0 ∧ arg32P − arg32P ≤ 0 ∧ − arg32 + arg32 ≤ 0 ∧ arg32 − arg32 ≤ 0 ∧ − arg31P + arg31P ≤ 0 ∧ arg31P − arg31P ≤ 0 ∧ − arg31 + arg31 ≤ 0 ∧ arg31 − arg31 ≤ 0 ∧ − arg30P + arg30P ≤ 0 ∧ arg30P − arg30P ≤ 0 ∧ − arg30 + arg30 ≤ 0 ∧ arg30 − arg30 ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 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.

13 19 13_var_snapshot: − x436 + x436 ≤ 0 ∧ x436 − x436 ≤ 0 ∧ − x401 + x401 ≤ 0 ∧ x401 − x401 ≤ 0 ∧ − x400 + x400 ≤ 0 ∧ x400 − x400 ≤ 0 ∧ − x359 + x359 ≤ 0 ∧ x359 − x359 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x201 + x201 ≤ 0 ∧ x201 − x201 ≤ 0 ∧ − x200 + x200 ≤ 0 ∧ x200 − x200 ≤ 0 ∧ − x199 + x199 ≤ 0 ∧ x199 − x199 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x167 + x167 ≤ 0 ∧ x167 − x167 ≤ 0 ∧ − x166 + x166 ≤ 0 ∧ x166 − x166 ≤ 0 ∧ − x165 + x165 ≤ 0 ∧ x165 − x165 ≤ 0 ∧ − x139 + x139 ≤ 0 ∧ x139 − x139 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − x137 + x137 ≤ 0 ∧ x137 − x137 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 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 ∧ − arg32P + arg32P ≤ 0 ∧ arg32P − arg32P ≤ 0 ∧ − arg32 + arg32 ≤ 0 ∧ arg32 − arg32 ≤ 0 ∧ − arg31P + arg31P ≤ 0 ∧ arg31P − arg31P ≤ 0 ∧ − arg31 + arg31 ≤ 0 ∧ arg31 − arg31 ≤ 0 ∧ − arg30P + arg30P ≤ 0 ∧ arg30P − arg30P ≤ 0 ∧ − arg30 + arg30 ≤ 0 ∧ arg30 − arg30 ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 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 { 13, 13_var_snapshot, 13* }.

6.1.1 Transition Removal

We remove transitions 19, 21, 15, 16 using the following ranking functions, which are bounded by −1.

13: 1
13_var_snapshot: 0
13*: 2

6.1.2 Splitting Cut-Point Transitions

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

6.1.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 18.

6.1.2.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert