LTS Termination Proof

Input

Integer Transition System

Initial Location: l4, l3, l0, l2

Transitions: (pre-variables and post-variables)

l0	1	l1:		x1 = _iHAT0 ∧ x2 = _jHAT0 ∧ x3 = _tmp1HAT0 ∧ x4 = _tmp2HAT0 ∧ x5 = _tmp3HAT0 ∧ x1 = _iHATpost ∧ x2 = _jHATpost ∧ x3 = _tmp1HATpost ∧ x4 = _tmp2HATpost ∧ x5 = _tmp3HATpost ∧ _tmp3HAT0 = _tmp3HATpost ∧ _tmp2HAT0 = _tmp2HATpost ∧ _tmp1HAT0 = _tmp1HATpost ∧ _jHAT0 = _jHATpost ∧ _iHAT0 = _iHATpost
l2	2	l0:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x1 = _x5 ∧ x2 = _x6 ∧ x3 = _x7 ∧ x4 = _x8 ∧ x5 = _x9 ∧ _x4 = _x9 ∧ _x3 = _x8 ∧ _x2 = _x7 ∧ _x1 = _x6 ∧ _x = _x5
l3	3	l2:		x1 = _x10 ∧ x2 = _x11 ∧ x3 = _x12 ∧ x4 = _x13 ∧ x5 = _x14 ∧ x1 = _x15 ∧ x2 = _x16 ∧ x3 = _x17 ∧ x4 = _x18 ∧ x5 = _x19 ∧ _x19 = _x19 ∧ _x18 = _x18 ∧ _x17 = _x17 ∧ _x16 = 1 ∧ _x15 = 0
l4	4	l3:		x1 = _x20 ∧ x2 = _x21 ∧ x3 = _x22 ∧ x4 = _x23 ∧ x5 = _x24 ∧ x1 = _x25 ∧ x2 = _x26 ∧ x3 = _x27 ∧ x4 = _x28 ∧ x5 = _x29 ∧ _x24 = _x29 ∧ _x23 = _x28 ∧ _x22 = _x27 ∧ _x21 = _x26 ∧ _x20 = _x25

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

l4	l4	l4:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5
l3	l3	l3:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5
l0	l0	l0:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5
l2	l2	l2:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5

and for every transition t, a duplicate t is considered.

2 SCC Decomposition

There exist no SCC in the program graph.

Tool configuration

version: AProVE Commit ID: unknown
strategy: Statistics for single proof: 100.00 % (2 real / 0 unknown / 0 assumptions / 2 total proof steps)