LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

1: 1 − arg1P ≤ 0arg2P ≤ 01 − arg1 ≤ 0arg2 ≤ 0
2: TRUE
3: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
5: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
6: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 01 − arg4 ≤ 0
7: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
8: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
9: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
10: TRUE
11: arg1P ≤ 0arg2P ≤ 0arg1 ≤ 0arg2 ≤ 0
12: arg1P ≤ 0arg2P ≤ 0arg1 ≤ 0arg2 ≤ 0
13: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
3 34 3: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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
10 41 10: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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
11 48 11: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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
12 55 12: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 1, 2, 16, 17, 18, 20, 21, 23, 25, 26, 27, 28, 29, 31, 33 using the following ranking functions, which are bounded by −25.

13: 0
2: 0
1: 0
3: 0
5: 0
6: 0
7: 0
8: 0
9: 0
12: 0
11: 0
10: 0
13: −8
2: −9
1: −10
3: −11
5: −11
6: −11
7: −11
8: −11
9: −11
3_var_snapshot: −11
3*: −11
12: −12
12_var_snapshot: −12
12*: −12
11: −17
11_var_snapshot: −17
11*: −17
10: −20
10_var_snapshot: −20
10*: −20
Hints:
35 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
42 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
49 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
56 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, 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, 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, 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, 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 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, 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, 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 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, 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, 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 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, 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, 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 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, 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, 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 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, 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, 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 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, 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, 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] ]
11 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, 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, 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] ]
12 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, 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, 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] ]
13 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, 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, 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 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, 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, 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] ]
15 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, 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, 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] ]
19 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22 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, 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, 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] ]
24 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, 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, 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] ]
30 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
32 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
16 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, 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, 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, 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] ]
17 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, 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, 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, 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] ]
18 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, 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, 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, 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] ]
20 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, 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, 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, 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] ]
21 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, 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, 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, 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] ]
23 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, 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, 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, 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, 0, 0] ]
25 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, 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, 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, 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, 0, 0, 0, 0, 0, 0] ]
26 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, 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, 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, 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] ]
27 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, 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, 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, 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] ]
28 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, 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, 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, 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] ]
29 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, 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, 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, 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] ]
31 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, 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, 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, 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] ]
33 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, 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, 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, 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 Location Addition

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

3* 37 3: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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

5 Location Addition

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

3 35 3_var_snapshot: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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

6 Location Addition

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

10* 44 10: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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

7 Location Addition

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

10 42 10_var_snapshot: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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 Location Addition

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

11* 51 11: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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

9 Location Addition

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

11 49 11_var_snapshot: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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

10 Location Addition

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

12* 58 12: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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

11 Location Addition

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

12 56 12_var_snapshot: x86 + x86 ≤ 0x86x86 ≤ 0x85 + x85 ≤ 0x85x85 ≤ 0x78 + x78 ≤ 0x78x78 ≤ 0x77 + x77 ≤ 0x77x77 ≤ 0x76 + x76 ≤ 0x76x76 ≤ 0x75 + x75 ≤ 0x75x75 ≤ 0x68 + x68 ≤ 0x68x68 ≤ 0x67 + x67 ≤ 0x67x67 ≤ 0x248 + x248 ≤ 0x248x248 ≤ 0x247 + x247 ≤ 0x247x247 ≤ 0x240 + x240 ≤ 0x240x240 ≤ 0x239 + x239 ≤ 0x239x239 ≤ 0x238 + x238 ≤ 0x238x238 ≤ 0x237 + x237 ≤ 0x237x237 ≤ 0x232 + x232 ≤ 0x232x232 ≤ 0x231 + x231 ≤ 0x231x231 ≤ 0x224 + x224 ≤ 0x224x224 ≤ 0x223 + x223 ≤ 0x223x223 ≤ 0x222 + x222 ≤ 0x222x222 ≤ 0x221 + x221 ≤ 0x221x221 ≤ 0x216 + x216 ≤ 0x216x216 ≤ 0x215 + x215 ≤ 0x215x215 ≤ 0x214 + x214 ≤ 0x214x214 ≤ 0x213 + x213 ≤ 0x213x213 ≤ 0x206 + x206 ≤ 0x206x206 ≤ 0x205 + x205 ≤ 0x205x205 ≤ 0x204 + x204 ≤ 0x204x204 ≤ 0x203 + x203 ≤ 0x203x203 ≤ 0x195 + x195 ≤ 0x195x195 ≤ 0x194 + x194 ≤ 0x194x194 ≤ 0x193 + x193 ≤ 0x193x193 ≤ 0x192 + x192 ≤ 0x192x192 ≤ 0x191 + x191 ≤ 0x191x191 ≤ 0x186 + x186 ≤ 0x186x186 ≤ 0x185 + x185 ≤ 0x185x185 ≤ 0x184 + x184 ≤ 0x184x184 ≤ 0x183 + x183 ≤ 0x183x183 ≤ 0x175 + x175 ≤ 0x175x175 ≤ 0x174 + x174 ≤ 0x174x174 ≤ 0x173 + x173 ≤ 0x173x173 ≤ 0x172 + x172 ≤ 0x172x172 ≤ 0x171 + x171 ≤ 0x171x171 ≤ 0x153 + x153 ≤ 0x153x153 ≤ 0x152 + x152 ≤ 0x152x152 ≤ 0x146 + x146 ≤ 0x146x146 ≤ 0x145 + x145 ≤ 0x145x145 ≤ 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

12 SCC Decomposition

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

12.1 SCC Subproblem 1/4

Here we consider the SCC { 12, 12_var_snapshot, 12* }.

12.1.1 Transition Removal

We remove transitions 56, 58, 32 using the following ranking functions, which are bounded by −1.

12: 1 + 3⋅arg2
12_var_snapshot: 3⋅arg2
12*: 2 + 3⋅arg2
Hints:
56 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, 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, 0, 0, 0, 0, 0] , [0, 0, 0, 3, 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, 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] ]
58 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, 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, 0, 0, 0, 0, 0] , [0, 0, 0, 3, 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, 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] ]
32 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 3, 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, 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, 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, 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] ]

12.1.2 Splitting Cut-Point Transitions

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

12.1.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 55.

12.1.2.1.1 Splitting Cut-Point Transitions

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

12.2 SCC Subproblem 2/4

Here we consider the SCC { 11, 11_var_snapshot, 11* }.

12.2.1 Transition Removal

We remove transitions 49, 51, 30 using the following ranking functions, which are bounded by −1.

11: 1 + 3⋅arg2
11_var_snapshot: 3⋅arg2
11*: 2 + 3⋅arg2
Hints:
49 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, 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, 0, 0, 0, 0, 0] , [0, 0, 0, 3, 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, 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] ]
51 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, 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, 0, 0, 0, 0, 0] , [0, 0, 0, 3, 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, 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] ]
30 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 3, 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, 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, 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, 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] ]

12.2.2 Splitting Cut-Point Transitions

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

12.2.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 48.

12.2.2.1.1 Splitting Cut-Point Transitions

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

12.3 SCC Subproblem 3/4

Here we consider the SCC { 3, 5, 6, 7, 8, 9, 3_var_snapshot, 3* }.

12.3.1 Transition Removal

We remove transitions 37, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 22, 24 using the following ranking functions, which are bounded by −4.

3: 2 + 8⋅arg1 + 8⋅arg2 + 8⋅arg3
5: 8⋅arg1 + 8⋅arg2 + 8⋅arg3
6: −1 + 8⋅arg1 + 8⋅arg2 + 8⋅arg3
7: −2 + 8⋅arg1 + 8⋅arg2 + 8⋅arg3
8: −3 + 8⋅arg1 + 8⋅arg2 + 8⋅arg3
9: 4 + 8⋅arg1 + 8⋅arg2 + 8⋅arg3
3_var_snapshot: 1 + 8⋅arg1 + 8⋅arg2 + 8⋅arg3
3*: 3 + 8⋅arg1 + 8⋅arg2 + 8⋅arg3
Hints:
35 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, 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, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 8, 0, 0, 0, 8, 0] ]
37 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, 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, 8, 0, 0, 0, 8, 0, 0, 0, 8, 0] , [0, 0, 0, 8, 8, 8, 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, 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] ]
4 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8, 8, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8, 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, 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] ]
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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 8, 0, 0, 0, 8, 0] , [0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 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, 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] ]
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, 8, 8, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 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, 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] ]
7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 8, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 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, 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] ]
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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 8, 0, 0, 0, 8, 0] , [0, 0, 0, 8, 8, 8, 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, 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] ]
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, 8, 8, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 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, 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, 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] ]
10 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8, 8, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8, 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, 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] ]
11 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 8, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 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, 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] ]
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, 8, 8, 8, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 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, 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] ]
13 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, 8, 8, 8, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 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, 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, 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] ]
14 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 8, 8, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8, 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, 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] ]
15 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 8, 8, 0, 0, 0, 0, 0, 0, 8, 0, 8, 0, 8, 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, 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, 8, 8, 8, 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, 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] ]
22 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, 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, 8, 0, 0, 0, 8, 0, 0, 0, 8, 0] , [0, 0, 0, 8, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 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, 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] ]
24 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, 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, 8, 0, 0, 0, 8, 0, 0, 0, 8, 0] , [0, 0, 0, 8, 8, 8, 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, 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] ]

12.3.2 Transition Removal

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

3: 0
5: 0
6: 0
7: 0
8: 0
9: 0
3_var_snapshot: −1
3*: 0
Hints:
35 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, 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, 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, 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] ]

12.3.3 Splitting Cut-Point Transitions

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

12.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 34.

12.3.3.1.1 Splitting Cut-Point Transitions

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

12.4 SCC Subproblem 4/4

Here we consider the SCC { 10, 10_var_snapshot, 10* }.

12.4.1 Splitting Cut-Point Transitions

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

12.4.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 41.

12.4.1.1.1 Fresh Variable Addition

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

42: __snapshot_10_x86x86x86__snapshot_10_x86
44: __snapshot_10_x86__snapshot_10_x86__snapshot_10_x86__snapshot_10_x86
19: __snapshot_10_x86__snapshot_10_x86__snapshot_10_x86__snapshot_10_x86

12.4.1.1.2 Fresh Variable Addition

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

42: __snapshot_10_x85x85x85__snapshot_10_x85
44: __snapshot_10_x85__snapshot_10_x85__snapshot_10_x85__snapshot_10_x85
19: __snapshot_10_x85__snapshot_10_x85__snapshot_10_x85__snapshot_10_x85

12.4.1.1.3 Fresh Variable Addition

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

42: __snapshot_10_x78x78x78__snapshot_10_x78
44: __snapshot_10_x78__snapshot_10_x78__snapshot_10_x78__snapshot_10_x78
19: __snapshot_10_x78__snapshot_10_x78__snapshot_10_x78__snapshot_10_x78

12.4.1.1.4 Fresh Variable Addition

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

42: __snapshot_10_x77x77x77__snapshot_10_x77
44: __snapshot_10_x77__snapshot_10_x77__snapshot_10_x77__snapshot_10_x77
19: __snapshot_10_x77__snapshot_10_x77__snapshot_10_x77__snapshot_10_x77

12.4.1.1.5 Fresh Variable Addition

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

42: __snapshot_10_x76x76x76__snapshot_10_x76
44: __snapshot_10_x76__snapshot_10_x76__snapshot_10_x76__snapshot_10_x76
19: __snapshot_10_x76__snapshot_10_x76__snapshot_10_x76__snapshot_10_x76

12.4.1.1.6 Fresh Variable Addition

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

42: __snapshot_10_x75x75x75__snapshot_10_x75
44: __snapshot_10_x75__snapshot_10_x75__snapshot_10_x75__snapshot_10_x75
19: __snapshot_10_x75__snapshot_10_x75__snapshot_10_x75__snapshot_10_x75

12.4.1.1.7 Fresh Variable Addition

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

42: __snapshot_10_x68x68x68__snapshot_10_x68
44: __snapshot_10_x68__snapshot_10_x68__snapshot_10_x68__snapshot_10_x68
19: __snapshot_10_x68__snapshot_10_x68__snapshot_10_x68__snapshot_10_x68

12.4.1.1.8 Fresh Variable Addition

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

42: __snapshot_10_x67x67x67__snapshot_10_x67
44: __snapshot_10_x67__snapshot_10_x67__snapshot_10_x67__snapshot_10_x67
19: __snapshot_10_x67__snapshot_10_x67__snapshot_10_x67__snapshot_10_x67

12.4.1.1.9 Fresh Variable Addition

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

42: __snapshot_10_x248x248x248__snapshot_10_x248
44: __snapshot_10_x248__snapshot_10_x248__snapshot_10_x248__snapshot_10_x248
19: __snapshot_10_x248__snapshot_10_x248__snapshot_10_x248__snapshot_10_x248

12.4.1.1.10 Fresh Variable Addition

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

42: __snapshot_10_x247x247x247__snapshot_10_x247
44: __snapshot_10_x247__snapshot_10_x247__snapshot_10_x247__snapshot_10_x247
19: __snapshot_10_x247__snapshot_10_x247__snapshot_10_x247__snapshot_10_x247

12.4.1.1.11 Fresh Variable Addition

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

42: __snapshot_10_x240x240x240__snapshot_10_x240
44: __snapshot_10_x240__snapshot_10_x240__snapshot_10_x240__snapshot_10_x240
19: __snapshot_10_x240__snapshot_10_x240__snapshot_10_x240__snapshot_10_x240

12.4.1.1.12 Fresh Variable Addition

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

42: __snapshot_10_x239x239x239__snapshot_10_x239
44: __snapshot_10_x239__snapshot_10_x239__snapshot_10_x239__snapshot_10_x239
19: __snapshot_10_x239__snapshot_10_x239__snapshot_10_x239__snapshot_10_x239

12.4.1.1.13 Fresh Variable Addition

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

42: __snapshot_10_x238x238x238__snapshot_10_x238
44: __snapshot_10_x238__snapshot_10_x238__snapshot_10_x238__snapshot_10_x238
19: __snapshot_10_x238__snapshot_10_x238__snapshot_10_x238__snapshot_10_x238

12.4.1.1.14 Fresh Variable Addition

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

42: __snapshot_10_x237x237x237__snapshot_10_x237
44: __snapshot_10_x237__snapshot_10_x237__snapshot_10_x237__snapshot_10_x237
19: __snapshot_10_x237__snapshot_10_x237__snapshot_10_x237__snapshot_10_x237

12.4.1.1.15 Fresh Variable Addition

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

42: __snapshot_10_x232x232x232__snapshot_10_x232
44: __snapshot_10_x232__snapshot_10_x232__snapshot_10_x232__snapshot_10_x232
19: __snapshot_10_x232__snapshot_10_x232__snapshot_10_x232__snapshot_10_x232

12.4.1.1.16 Fresh Variable Addition

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

42: __snapshot_10_x231x231x231__snapshot_10_x231
44: __snapshot_10_x231__snapshot_10_x231__snapshot_10_x231__snapshot_10_x231
19: __snapshot_10_x231__snapshot_10_x231__snapshot_10_x231__snapshot_10_x231

12.4.1.1.17 Fresh Variable Addition

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

42: __snapshot_10_x224x224x224__snapshot_10_x224
44: __snapshot_10_x224__snapshot_10_x224__snapshot_10_x224__snapshot_10_x224
19: __snapshot_10_x224__snapshot_10_x224__snapshot_10_x224__snapshot_10_x224

12.4.1.1.18 Fresh Variable Addition

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

42: __snapshot_10_x223x223x223__snapshot_10_x223
44: __snapshot_10_x223__snapshot_10_x223__snapshot_10_x223__snapshot_10_x223
19: __snapshot_10_x223__snapshot_10_x223__snapshot_10_x223__snapshot_10_x223

12.4.1.1.19 Fresh Variable Addition

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

42: __snapshot_10_x222x222x222__snapshot_10_x222
44: __snapshot_10_x222__snapshot_10_x222__snapshot_10_x222__snapshot_10_x222
19: __snapshot_10_x222__snapshot_10_x222__snapshot_10_x222__snapshot_10_x222

12.4.1.1.20 Fresh Variable Addition

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

42: __snapshot_10_x221x221x221__snapshot_10_x221
44: __snapshot_10_x221__snapshot_10_x221__snapshot_10_x221__snapshot_10_x221
19: __snapshot_10_x221__snapshot_10_x221__snapshot_10_x221__snapshot_10_x221

12.4.1.1.21 Fresh Variable Addition

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

42: __snapshot_10_x216x216x216__snapshot_10_x216
44: __snapshot_10_x216__snapshot_10_x216__snapshot_10_x216__snapshot_10_x216
19: __snapshot_10_x216__snapshot_10_x216__snapshot_10_x216__snapshot_10_x216

12.4.1.1.22 Fresh Variable Addition

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

42: __snapshot_10_x215x215x215__snapshot_10_x215
44: __snapshot_10_x215__snapshot_10_x215__snapshot_10_x215__snapshot_10_x215
19: __snapshot_10_x215__snapshot_10_x215__snapshot_10_x215__snapshot_10_x215

12.4.1.1.23 Fresh Variable Addition

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

42: __snapshot_10_x214x214x214__snapshot_10_x214
44: __snapshot_10_x214__snapshot_10_x214__snapshot_10_x214__snapshot_10_x214
19: __snapshot_10_x214__snapshot_10_x214__snapshot_10_x214__snapshot_10_x214

12.4.1.1.24 Fresh Variable Addition

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

42: __snapshot_10_x213x213x213__snapshot_10_x213
44: __snapshot_10_x213__snapshot_10_x213__snapshot_10_x213__snapshot_10_x213
19: __snapshot_10_x213__snapshot_10_x213__snapshot_10_x213__snapshot_10_x213

12.4.1.1.25 Fresh Variable Addition

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

42: __snapshot_10_x206x206x206__snapshot_10_x206
44: __snapshot_10_x206__snapshot_10_x206__snapshot_10_x206__snapshot_10_x206
19: __snapshot_10_x206__snapshot_10_x206__snapshot_10_x206__snapshot_10_x206

12.4.1.1.26 Fresh Variable Addition

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

42: __snapshot_10_x205x205x205__snapshot_10_x205
44: __snapshot_10_x205__snapshot_10_x205__snapshot_10_x205__snapshot_10_x205
19: __snapshot_10_x205__snapshot_10_x205__snapshot_10_x205__snapshot_10_x205

12.4.1.1.27 Fresh Variable Addition

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

42: __snapshot_10_x204x204x204__snapshot_10_x204
44: __snapshot_10_x204__snapshot_10_x204__snapshot_10_x204__snapshot_10_x204
19: __snapshot_10_x204__snapshot_10_x204__snapshot_10_x204__snapshot_10_x204

12.4.1.1.28 Fresh Variable Addition

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

42: __snapshot_10_x203x203x203__snapshot_10_x203
44: __snapshot_10_x203__snapshot_10_x203__snapshot_10_x203__snapshot_10_x203
19: __snapshot_10_x203__snapshot_10_x203__snapshot_10_x203__snapshot_10_x203

12.4.1.1.29 Fresh Variable Addition

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

42: __snapshot_10_x195x195x195__snapshot_10_x195
44: __snapshot_10_x195__snapshot_10_x195__snapshot_10_x195__snapshot_10_x195
19: __snapshot_10_x195__snapshot_10_x195__snapshot_10_x195__snapshot_10_x195

12.4.1.1.30 Fresh Variable Addition

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

42: __snapshot_10_x194x194x194__snapshot_10_x194
44: __snapshot_10_x194__snapshot_10_x194__snapshot_10_x194__snapshot_10_x194
19: __snapshot_10_x194__snapshot_10_x194__snapshot_10_x194__snapshot_10_x194

12.4.1.1.31 Fresh Variable Addition

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

42: __snapshot_10_x193x193x193__snapshot_10_x193
44: __snapshot_10_x193__snapshot_10_x193__snapshot_10_x193__snapshot_10_x193
19: __snapshot_10_x193__snapshot_10_x193__snapshot_10_x193__snapshot_10_x193

12.4.1.1.32 Fresh Variable Addition

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

42: __snapshot_10_x192x192x192__snapshot_10_x192
44: __snapshot_10_x192__snapshot_10_x192__snapshot_10_x192__snapshot_10_x192
19: __snapshot_10_x192__snapshot_10_x192__snapshot_10_x192__snapshot_10_x192

12.4.1.1.33 Fresh Variable Addition

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

42: __snapshot_10_x191x191x191__snapshot_10_x191
44: __snapshot_10_x191__snapshot_10_x191__snapshot_10_x191__snapshot_10_x191
19: __snapshot_10_x191__snapshot_10_x191__snapshot_10_x191__snapshot_10_x191

12.4.1.1.34 Fresh Variable Addition

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

42: __snapshot_10_x186x186x186__snapshot_10_x186
44: __snapshot_10_x186__snapshot_10_x186__snapshot_10_x186__snapshot_10_x186
19: __snapshot_10_x186__snapshot_10_x186__snapshot_10_x186__snapshot_10_x186

12.4.1.1.35 Fresh Variable Addition

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

42: __snapshot_10_x185x185x185__snapshot_10_x185
44: __snapshot_10_x185__snapshot_10_x185__snapshot_10_x185__snapshot_10_x185
19: __snapshot_10_x185__snapshot_10_x185__snapshot_10_x185__snapshot_10_x185

12.4.1.1.36 Fresh Variable Addition

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

42: __snapshot_10_x184x184x184__snapshot_10_x184
44: __snapshot_10_x184__snapshot_10_x184__snapshot_10_x184__snapshot_10_x184
19: __snapshot_10_x184__snapshot_10_x184__snapshot_10_x184__snapshot_10_x184

12.4.1.1.37 Fresh Variable Addition

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

42: __snapshot_10_x183x183x183__snapshot_10_x183
44: __snapshot_10_x183__snapshot_10_x183__snapshot_10_x183__snapshot_10_x183
19: __snapshot_10_x183__snapshot_10_x183__snapshot_10_x183__snapshot_10_x183

12.4.1.1.38 Fresh Variable Addition

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

42: __snapshot_10_x175x175x175__snapshot_10_x175
44: __snapshot_10_x175__snapshot_10_x175__snapshot_10_x175__snapshot_10_x175
19: __snapshot_10_x175__snapshot_10_x175__snapshot_10_x175__snapshot_10_x175

12.4.1.1.39 Fresh Variable Addition

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

42: __snapshot_10_x174x174x174__snapshot_10_x174
44: __snapshot_10_x174__snapshot_10_x174__snapshot_10_x174__snapshot_10_x174
19: __snapshot_10_x174__snapshot_10_x174__snapshot_10_x174__snapshot_10_x174

12.4.1.1.40 Fresh Variable Addition

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

42: __snapshot_10_x173x173x173__snapshot_10_x173
44: __snapshot_10_x173__snapshot_10_x173__snapshot_10_x173__snapshot_10_x173
19: __snapshot_10_x173__snapshot_10_x173__snapshot_10_x173__snapshot_10_x173

12.4.1.1.41 Fresh Variable Addition

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

42: __snapshot_10_x172x172x172__snapshot_10_x172
44: __snapshot_10_x172__snapshot_10_x172__snapshot_10_x172__snapshot_10_x172
19: __snapshot_10_x172__snapshot_10_x172__snapshot_10_x172__snapshot_10_x172

12.4.1.1.42 Fresh Variable Addition

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

42: __snapshot_10_x171x171x171__snapshot_10_x171
44: __snapshot_10_x171__snapshot_10_x171__snapshot_10_x171__snapshot_10_x171
19: __snapshot_10_x171__snapshot_10_x171__snapshot_10_x171__snapshot_10_x171

12.4.1.1.43 Fresh Variable Addition

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

42: __snapshot_10_x153x153x153__snapshot_10_x153
44: __snapshot_10_x153__snapshot_10_x153__snapshot_10_x153__snapshot_10_x153
19: __snapshot_10_x153__snapshot_10_x153__snapshot_10_x153__snapshot_10_x153

12.4.1.1.44 Fresh Variable Addition

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

42: __snapshot_10_x152x152x152__snapshot_10_x152
44: __snapshot_10_x152__snapshot_10_x152__snapshot_10_x152__snapshot_10_x152
19: __snapshot_10_x152__snapshot_10_x152__snapshot_10_x152__snapshot_10_x152

12.4.1.1.45 Fresh Variable Addition

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

42: __snapshot_10_x146x146x146__snapshot_10_x146
44: __snapshot_10_x146__snapshot_10_x146__snapshot_10_x146__snapshot_10_x146
19: __snapshot_10_x146__snapshot_10_x146__snapshot_10_x146__snapshot_10_x146

12.4.1.1.46 Fresh Variable Addition

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

42: __snapshot_10_x145x145x145__snapshot_10_x145
44: __snapshot_10_x145__snapshot_10_x145__snapshot_10_x145__snapshot_10_x145
19: __snapshot_10_x145__snapshot_10_x145__snapshot_10_x145__snapshot_10_x145

12.4.1.1.47 Fresh Variable Addition

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

42: __snapshot_10_arg4Parg4Parg4P__snapshot_10_arg4P
44: __snapshot_10_arg4P__snapshot_10_arg4P__snapshot_10_arg4P__snapshot_10_arg4P
19: __snapshot_10_arg4P__snapshot_10_arg4P__snapshot_10_arg4P__snapshot_10_arg4P

12.4.1.1.48 Fresh Variable Addition

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

42: __snapshot_10_arg4arg4arg4__snapshot_10_arg4
44: __snapshot_10_arg4__snapshot_10_arg4__snapshot_10_arg4__snapshot_10_arg4
19: __snapshot_10_arg4__snapshot_10_arg4__snapshot_10_arg4__snapshot_10_arg4

12.4.1.1.49 Fresh Variable Addition

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

42: __snapshot_10_arg3Parg3Parg3P__snapshot_10_arg3P
44: __snapshot_10_arg3P__snapshot_10_arg3P__snapshot_10_arg3P__snapshot_10_arg3P
19: __snapshot_10_arg3P__snapshot_10_arg3P__snapshot_10_arg3P__snapshot_10_arg3P

12.4.1.1.50 Fresh Variable Addition

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

42: __snapshot_10_arg3arg3arg3__snapshot_10_arg3
44: __snapshot_10_arg3__snapshot_10_arg3__snapshot_10_arg3__snapshot_10_arg3
19: __snapshot_10_arg3__snapshot_10_arg3__snapshot_10_arg3__snapshot_10_arg3

12.4.1.1.51 Fresh Variable Addition

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

42: __snapshot_10_arg2Parg2Parg2P__snapshot_10_arg2P
44: __snapshot_10_arg2P__snapshot_10_arg2P__snapshot_10_arg2P__snapshot_10_arg2P
19: __snapshot_10_arg2P__snapshot_10_arg2P__snapshot_10_arg2P__snapshot_10_arg2P

12.4.1.1.52 Fresh Variable Addition

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

42: __snapshot_10_arg2arg2arg2__snapshot_10_arg2
44: __snapshot_10_arg2__snapshot_10_arg2__snapshot_10_arg2__snapshot_10_arg2
19: __snapshot_10_arg2__snapshot_10_arg2__snapshot_10_arg2__snapshot_10_arg2

12.4.1.1.53 Fresh Variable Addition

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

42: __snapshot_10_arg1Parg1Parg1P__snapshot_10_arg1P
44: __snapshot_10_arg1P__snapshot_10_arg1P__snapshot_10_arg1P__snapshot_10_arg1P
19: __snapshot_10_arg1P__snapshot_10_arg1P__snapshot_10_arg1P__snapshot_10_arg1P

12.4.1.1.54 Fresh Variable Addition

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

42: __snapshot_10_arg1arg1arg1__snapshot_10_arg1
44: __snapshot_10_arg1__snapshot_10_arg1__snapshot_10_arg1__snapshot_10_arg1
19: __snapshot_10_arg1__snapshot_10_arg1__snapshot_10_arg1__snapshot_10_arg1

12.4.1.1.55 Invariant Updates

The following invariants are asserted.

1: −7 + arg3arg4 ≤ 0−1 − arg4 ≤ 01 − arg1P ≤ 0arg2P ≤ 01 − arg1 ≤ 0arg2 ≤ 0
2: arg2arg2P ≤ 0
3: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
5: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
6: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 01 − arg4 ≤ 0
7: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
8: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
9: arg1P ≤ 0arg2P ≤ 0arg3P ≤ 0arg1 ≤ 0arg2 ≤ 0arg3 ≤ 0
10: −1 − arg1 + arg2 ≤ 01 + arg1arg2P ≤ 0arg2P ≤ 0
11: arg1P ≤ 0arg2P ≤ 0arg1 ≤ 0arg2 ≤ 0
12: arg1P ≤ 0arg2P ≤ 0arg1 ≤ 0arg2 ≤ 0
13: TRUE
10: −1 − arg1 + arg2 ≤ 01 + arg1arg2P ≤ 0arg2P ≤ 0−1 − arg1 + arg2 ≤ 01 − __snapshot_10_arg2P + arg2P ≤ 01 + arg1arg2P ≤ 0__snapshot_10_arg2P ≤ 0arg2P ≤ 0
10_var_snapshot: 1 − __snapshot_10_arg2P + arg1 ≤ 0−1 − arg1 + arg2 ≤ 0__snapshot_10_arg2P ≤ 0
10*: −1 − arg1 + arg2 ≤ 01 − __snapshot_10_arg2P + arg2P ≤ 01 + arg1arg2P ≤ 0__snapshot_10_arg2P ≤ 0arg2P ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

12.4.1.1.56 Transition Removal

We remove transition 44 using the following ranking functions, which are bounded by −2.

10: arg2P
10_var_snapshot: __snapshot_10_arg2P
10*: __snapshot_10_arg2P
Hints:
42 distribute assertion
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, 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, 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, 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, 0, 0, 0, 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, 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, 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, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0] ]
44 lexStrict[ [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, 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, 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, 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, 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, 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, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
19 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, 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, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0] ]

12.4.1.1.57 Transition Removal

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

10: −1
10_var_snapshot: −2
10*: −3
Hints:
42 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0] ]
19 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, 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, 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, 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, 0, 0] ]

12.4.1.1.58 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert