LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

1: 1 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg2 ≤ 0
2: TRUE
3: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
5: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
6: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0
7: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
8: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
9: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
10: TRUE
11: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0
12: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
10 41 10: − x86 + x86 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
11 48 11: − x86 + x86 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
12 55 12: − x86 + x86 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 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

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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 ≤ 0 ∧ x86 − x86 ≤ 0 ∧ − x85 + x85 ≤ 0 ∧ x85 − x85 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x240 + x240 ≤ 0 ∧ x240 − x240 ≤ 0 ∧ − x239 + x239 ≤ 0 ∧ x239 − x239 ≤ 0 ∧ − x238 + x238 ≤ 0 ∧ x238 − x238 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x232 + x232 ≤ 0 ∧ x232 − x232 ≤ 0 ∧ − x231 + x231 ≤ 0 ∧ x231 − x231 ≤ 0 ∧ − x224 + x224 ≤ 0 ∧ x224 − x224 ≤ 0 ∧ − x223 + x223 ≤ 0 ∧ x223 − x223 ≤ 0 ∧ − x222 + x222 ≤ 0 ∧ x222 − x222 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x213 + x213 ≤ 0 ∧ x213 − x213 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x195 + x195 ≤ 0 ∧ x195 − x195 ≤ 0 ∧ − x194 + x194 ≤ 0 ∧ x194 − x194 ≤ 0 ∧ − x193 + x193 ≤ 0 ∧ x193 − x193 ≤ 0 ∧ − x192 + x192 ≤ 0 ∧ x192 − x192 ≤ 0 ∧ − x191 + x191 ≤ 0 ∧ x191 − x191 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x175 + x175 ≤ 0 ∧ x175 − x175 ≤ 0 ∧ − x174 + x174 ≤ 0 ∧ x174 − x174 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x171 + x171 ≤ 0 ∧ x171 − x171 ≤ 0 ∧ − x153 + x153 ≤ 0 ∧ x153 − x153 ≤ 0 ∧ − x152 + x152 ≤ 0 ∧ x152 − x152 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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

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

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

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

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_x86 ≤ x86 ∧ x86 ≤ __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_x85 ≤ x85 ∧ x85 ≤ __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_x78 ≤ x78 ∧ x78 ≤ __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_x77 ≤ x77 ∧ x77 ≤ __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_x76 ≤ x76 ∧ x76 ≤ __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_x75 ≤ x75 ∧ x75 ≤ __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_x68 ≤ x68 ∧ x68 ≤ __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_x67 ≤ x67 ∧ x67 ≤ __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_x248 ≤ x248 ∧ x248 ≤ __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_x247 ≤ x247 ∧ x247 ≤ __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_x240 ≤ x240 ∧ x240 ≤ __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_x239 ≤ x239 ∧ x239 ≤ __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_x238 ≤ x238 ∧ x238 ≤ __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_x237 ≤ x237 ∧ x237 ≤ __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_x232 ≤ x232 ∧ x232 ≤ __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_x231 ≤ x231 ∧ x231 ≤ __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_x224 ≤ x224 ∧ x224 ≤ __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_x223 ≤ x223 ∧ x223 ≤ __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_x222 ≤ x222 ∧ x222 ≤ __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_x221 ≤ x221 ∧ x221 ≤ __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_x216 ≤ x216 ∧ x216 ≤ __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_x215 ≤ x215 ∧ x215 ≤ __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_x214 ≤ x214 ∧ x214 ≤ __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_x213 ≤ x213 ∧ x213 ≤ __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_x206 ≤ x206 ∧ x206 ≤ __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_x205 ≤ x205 ∧ x205 ≤ __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_x204 ≤ x204 ∧ x204 ≤ __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_x203 ≤ x203 ∧ x203 ≤ __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_x195 ≤ x195 ∧ x195 ≤ __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_x194 ≤ x194 ∧ x194 ≤ __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_x193 ≤ x193 ∧ x193 ≤ __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_x192 ≤ x192 ∧ x192 ≤ __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_x191 ≤ x191 ∧ x191 ≤ __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_x186 ≤ x186 ∧ x186 ≤ __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_x185 ≤ x185 ∧ x185 ≤ __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_x184 ≤ x184 ∧ x184 ≤ __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_x183 ≤ x183 ∧ x183 ≤ __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_x175 ≤ x175 ∧ x175 ≤ __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_x174 ≤ x174 ∧ x174 ≤ __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_x173 ≤ x173 ∧ x173 ≤ __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_x172 ≤ x172 ∧ x172 ≤ __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_x171 ≤ x171 ∧ x171 ≤ __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_x153 ≤ x153 ∧ x153 ≤ __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_x152 ≤ x152 ∧ x152 ≤ __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_x146 ≤ x146 ∧ x146 ≤ __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_x145 ≤ x145 ∧ x145 ≤ __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_arg4P ≤ arg4P ∧ arg4P ≤ __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_arg4 ≤ arg4 ∧ arg4 ≤ __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_arg3P ≤ arg3P ∧ arg3P ≤ __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_arg3 ≤ arg3 ∧ arg3 ≤ __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_arg2P ≤ arg2P ∧ arg2P ≤ __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_arg2 ≤ arg2 ∧ arg2 ≤ __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_arg1P ≤ arg1P ∧ arg1P ≤ __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_arg1 ≤ arg1 ∧ arg1 ≤ __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 + arg3 − arg4 ≤ 0 ∧ −1 − arg4 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg2 ≤ 0
2: arg2 − arg2P ≤ 0
3: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
5: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
6: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0
7: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
8: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
9: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0
10: −1 − arg1 + arg2 ≤ 0 ∧ 1 + arg1 − arg2P ≤ 0 ∧ − arg2P ≤ 0
11: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0
12: − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0
13: TRUE
10: −1 − arg1 + arg2 ≤ 0 ∧ 1 + arg1 − arg2P ≤ 0 ∧ − arg2P ≤ 0 ∨ −1 − arg1 + arg2 ≤ 0 ∧ 1 − __snapshot_10_arg2P + arg2P ≤ 0 ∧ 1 + arg1 − arg2P ≤ 0 ∧ − __snapshot_10_arg2P ≤ 0 ∧ − arg2P ≤ 0
10_var_snapshot: 1 − __snapshot_10_arg2P + arg1 ≤ 0 ∧ −1 − arg1 + arg2 ≤ 0 ∧ − __snapshot_10_arg2P ≤ 0
10*: −1 − arg1 + arg2 ≤ 0 ∧ 1 − __snapshot_10_arg2P + arg2P ≤ 0 ∧ 1 + arg1 − arg2P ≤ 0 ∧ − __snapshot_10_arg2P ≤ 0 ∧ − arg2P ≤ 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

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

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