LTS Termination Proof
by AProVE
Input
Integer Transition System
-
Initial Location:
l1
-
Transitions: (pre-variables and post-variables)
Proof
1 Switch to Cooperation Termination Proof
We consider the following cutpoint-transitions:
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)