LTS Termination Proof
by
AProVE
Input
Integer Transition System
Initial Location:
l0
,
l2
Transitions: (
pre-variables
and
post-variables
)
l0
1
l1
:
x1
=
_Result_4HAT0
∧
x1
=
_Result_4HATpost
∧
_Result_4HAT1
=
_Result_4HAT1
∧
_Result_4HATpost
=
_Result_4HATpost
l2
2
l0
:
x1
=
_x
∧
x1
=
_x1
∧
_x
=
_x1
Proof
1 Switch to Cooperation Termination Proof
We consider the following cutpoint-transitions:
l0
l0
l0
:
x1
=
x1
l2
l2
l2
:
x1
=
x1
and for every transition
t
, a duplicate
t
is considered.
2 SCC Decomposition
There exist no SCC in the program graph.
Tool configuration
AProVE
version: AProVE Commit ID: unknown
strategy: Statistics for single proof: 100.00 % (2 real / 0 unknown / 0 assumptions / 2 total proof steps)