LTS Termination Proof
by T2Cert
Input
Integer Transition System

Initial Location:
2

Transitions: (prevariables and postvariables)
Proof
1 Switch to Cooperation Termination Proof
We consider the following cutpointtransitions:
and for every transition t,
a duplicate t is considered.
2 Transition Removal
We remove transitions 0, 1
using the following ranking functions, which are bounded by
−8.
2:

0 
0:

0 
1:

0 
2:

−4 
0:

−5 
1:

−6 
Hints:
0 
lexStrict[auto, auto]

1 
lexStrict[auto, auto]

3 SCC Decomposition
There exist no SCC in the program graph.
Tool configuration
T2Cert