by T2Cert
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 ∧ i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ − i_1 + tmp10_post ≤ 0 ∧ i_1 − tmp10_post ≤ 0 ∧ −1 − i_1 + i_2 ≤ 0 ∧ 1 + i_1 − i_2 ≤ 0 ∧ − i_2 + tmp___011_post ≤ 0 ∧ i_2 − tmp___011_post ≤ 0 ∧ −1 − i_2 + i_3 ≤ 0 ∧ 1 + i_2 − i_3 ≤ 0 ∧ − i_3 + tmp13_post ≤ 0 ∧ i_3 − tmp13_post ≤ 0 ∧ −1 − i_3 + i_4 ≤ 0 ∧ 1 + i_3 − i_4 ≤ 0 ∧ − i_4 + tmp___014_post ≤ 0 ∧ i_4 − tmp___014_post ≤ 0 ∧ −1 − i_4 + i_post ≤ 0 ∧ 1 + i_4 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ tmp10_0 − tmp10_post ≤ 0 ∧ − tmp10_0 + tmp10_post ≤ 0 ∧ tmp13_0 − tmp13_post ≤ 0 ∧ − tmp13_0 + tmp13_post ≤ 0 ∧ tmp___011_0 − tmp___011_post ≤ 0 ∧ − tmp___011_0 + tmp___011_post ≤ 0 ∧ tmp___014_0 − tmp___014_post ≤ 0 ∧ − tmp___014_0 + tmp___014_post ≤ 0 | |
2 | 1 | 0: | − tmp___014_post + tmp___014_post ≤ 0 ∧ tmp___014_post − tmp___014_post ≤ 0 ∧ − tmp___014_0 + tmp___014_0 ≤ 0 ∧ tmp___014_0 − tmp___014_0 ≤ 0 ∧ − tmp___011_post + tmp___011_post ≤ 0 ∧ tmp___011_post − tmp___011_post ≤ 0 ∧ − tmp___011_0 + tmp___011_0 ≤ 0 ∧ tmp___011_0 − tmp___011_0 ≤ 0 ∧ − tmp13_post + tmp13_post ≤ 0 ∧ tmp13_post − tmp13_post ≤ 0 ∧ − tmp13_0 + tmp13_0 ≤ 0 ∧ tmp13_0 − tmp13_0 ≤ 0 ∧ − tmp10_post + tmp10_post ≤ 0 ∧ tmp10_post − tmp10_post ≤ 0 ∧ − tmp10_0 + tmp10_0 ≤ 0 ∧ tmp10_0 − tmp10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_4 + i_4 ≤ 0 ∧ i_4 − i_4 ≤ 0 ∧ − i_3 + i_3 ≤ 0 ∧ i_3 − i_3 ≤ 0 ∧ − i_2 + i_2 ≤ 0 ∧ i_2 − i_2 ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 |
The following invariants are asserted.
0: | TRUE |
1: | tmp10_post ≤ 0 ∧ i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ tmp10_0 ≤ 0 |
2: | TRUE |
The invariants are proved as follows.
0 | (0) | TRUE | ||
1 | (1) | tmp10_post ≤ 0 ∧ i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ tmp10_0 ≤ 0 | ||
2 | (2) | TRUE |
0 | 0 1 | |
2 | 1 0 |
We remove transitions
, using the following ranking functions, which are bounded by −8.2: | 0 |
0: | 0 |
1: | 0 |
: | −4 |
: | −5 |
: | −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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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] ] |
There exist no SCC in the program graph.
T2Cert