LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155 using the following ranking functions, which are bounded by −140.

68: 0
67: 0
54: 0
47: 0
39: 0
34: 0
28: 0
21: 0
13: 0
3: 0
4: 0
56: 0
55: 0
53: 0
52: 0
51: 0
50: 0
49: 0
48: 0
46: 0
45: 0
44: 0
43: 0
42: 0
41: 0
40: 0
38: 0
37: 0
36: 0
35: 0
33: 0
32: 0
31: 0
30: 0
29: 0
27: 0
26: 0
25: 0
24: 0
23: 0
22: 0
20: 0
19: 0
18: 0
17: 0
16: 0
15: 0
14: 0
12: 0
11: 0
10: 0
9: 0
8: 0
7: 0
6: 0
5: 0
2: 0
0: 0
1: 0
66: 0
65: 0
64: 0
63: 0
62: 0
61: 0
60: 0
59: 0
57: 0
58: 0
68: −70
67: −71
54: −72
47: −73
39: −74
34: −75
28: −76
21: −77
13: −78
3: −79
4: −80
56: −81
55: −82
53: −83
52: −84
51: −85
50: −86
49: −87
48: −88
46: −89
45: −90
44: −91
43: −92
42: −93
41: −94
40: −95
38: −96
37: −97
36: −98
35: −99
33: −100
32: −101
31: −102
30: −103
29: −104
27: −105
26: −106
25: −107
24: −108
23: −109
22: −110
20: −111
19: −112
18: −113
17: −114
16: −115
15: −116
14: −117
12: −118
11: −119
10: −120
9: −121
8: −122
7: −123
6: −124
5: −125
2: −126
0: −127
1: −128
66: −129
65: −130
64: −131
63: −132
62: −133
61: −134
60: −135
59: −136
57: −137
58: −138

3 SCC Decomposition

There exist no SCC in the program graph.

Tool configuration

T2Cert