YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
thrice(0(x0)) |
→ |
p(s(p(p(p(s(s(s(0(p(s(p(s(x0))))))))))))) |
|
thrice(s(x0)) |
→ |
p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x0)))))))))))))))))) |
|
half(0(x0)) |
→ |
p(p(s(s(p(s(0(p(s(s(s(s(x0)))))))))))) |
|
half(s(x0)) |
→ |
p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x0))))))))))))))))) |
|
half(s(s(x0))) |
→ |
p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x0)))))))))))))))) |
|
sixtimes(0(x0)) |
→ |
p(s(p(s(0(s(s(s(s(s(p(s(p(s(x0)))))))))))))) |
|
sixtimes(s(x0)) |
→ |
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x0))))))))))))))))))))))))) |
|
p(p(s(x0))) |
→ |
p(x0) |
|
p(s(x0)) |
→ |
x0 |
|
p(0(x0)) |
→ |
0(s(s(s(s(x0))))) |
|
0(x0) |
→ |
x0 |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [sixtimes(x1)] |
= |
0 ·
x1 +
-∞
|
| [thrice(x1)] |
= |
2 ·
x1 +
-∞
|
| [p(x1)] |
= |
0 ·
x1 +
-∞
|
| [half(x1)] |
= |
1 ·
x1 +
-∞
|
| [0(x1)] |
= |
0 ·
x1 +
-∞
|
| [s(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
half(s(x0)) |
→ |
p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x0))))))))))))))))) |
|
half(s(s(x0))) |
→ |
p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x0)))))))))))))))) |
|
sixtimes(0(x0)) |
→ |
p(s(p(s(0(s(s(s(s(s(p(s(p(s(x0)))))))))))))) |
|
sixtimes(s(x0)) |
→ |
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x0))))))))))))))))))))))))) |
|
p(p(s(x0))) |
→ |
p(x0) |
|
p(s(x0)) |
→ |
x0 |
|
p(0(x0)) |
→ |
0(s(s(s(s(x0))))) |
|
0(x0) |
→ |
x0 |
remain.
1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [sixtimes(x1)] |
= |
4 ·
x1 +
-∞
|
| [p(x1)] |
= |
0 ·
x1 +
-∞
|
| [half(x1)] |
= |
1 ·
x1 +
-∞
|
| [0(x1)] |
= |
1 ·
x1 +
-∞
|
| [s(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
half(s(x0)) |
→ |
p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x0))))))))))))))))) |
|
half(s(s(x0))) |
→ |
p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x0)))))))))))))))) |
|
sixtimes(s(x0)) |
→ |
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x0))))))))))))))))))))))))) |
|
p(p(s(x0))) |
→ |
p(x0) |
|
p(s(x0)) |
→ |
x0 |
|
p(0(x0)) |
→ |
0(s(s(s(s(x0))))) |
remain.
1.1.1 Bounds
The given TRS is
match-bounded by 1.
This is shown by the following automaton.
-
final states:
{46, 2, 45, 21, 19, 1}
-
transitions:
| 33 |
→ |
54 |
| 33 |
→ |
35 |
| 10 |
→ |
64 |
| 10 |
→ |
12 |
| 41 |
→ |
49 |
| 3 |
→ |
74 |
| 3 |
→ |
25 |
| 3 |
→ |
57 |
| 57 |
→ |
25 |
| 9 |
→ |
65 |
| 5 |
→ |
62 |
| 5 |
→ |
7 |
| 65 |
→ |
13 |
| 55 |
→ |
36 |
| 31 |
→ |
33 |
| 49 |
→ |
21 |
| 1 |
→ |
71 |
| 1 |
→ |
65 |
| 1 |
→ |
9 |
| 71 |
→ |
17 |
| 13 |
→ |
1 |
| 13 |
→ |
17 |
| 13 |
→ |
71 |
| 26 |
→ |
28 |
| 21 |
→ |
29 |
| 22 |
→ |
56 |
| 22 |
→ |
24 |
| 75 |
→ |
26 |
| 2 |
→ |
4 |
| 2 |
→ |
75 |
| 2 |
→ |
45 |
| 4 |
→ |
63 |
| 16 |
→ |
19 |
| 14 |
→ |
70 |
| 14 |
→ |
16 |
| 63 |
→ |
8 |
| 30 |
→ |
36 |
| 30 |
→ |
55 |
| 42 |
→ |
48 |
| 42 |
→ |
44 |
| 46 |
→ |
45 |
| 17 |
→ |
1 |
| 19 |
→ |
71 |
|
half0(8) |
→ |
9 |
|
sixtimes0(28) |
→ |
29 |
|
s0(33) |
→ |
34 |
|
s0(23) |
→ |
47 |
|
s0(26) |
→ |
27 |
|
s0(42) |
→ |
43 |
|
s0(41) |
→ |
42 |
|
s0(14) |
→ |
15 |
|
s0(30) |
→ |
31 |
|
s0(37) |
→ |
38 |
|
s0(38) |
→ |
39 |
|
s0(36) |
→ |
37 |
|
s0(29) |
→ |
30 |
|
s0(3) |
→ |
22 |
|
s0(40) |
→ |
41 |
|
s0(9) |
→ |
10 |
|
s0(13) |
→ |
14 |
|
s0(31) |
→ |
32 |
|
s0(5) |
→ |
6 |
|
s0(17) |
→ |
18 |
|
s0(10) |
→ |
11 |
|
s0(2) |
→ |
3 |
|
s0(4) |
→ |
5 |
|
s0(39) |
→ |
40 |
|
s0(16) |
→ |
20 |
|
s0(22) |
→ |
23 |
|
00(47) |
→ |
46 |
|
p1(64) |
→ |
65 |
|
p1(70) |
→ |
71 |
|
p1(48) |
→ |
49 |
|
p1(54) |
→ |
55 |
|
p1(62) |
→ |
63 |
|
p1(74) |
→ |
75 |
|
p1(56) |
→ |
57 |
|
f60
|
→ |
2 |
|
p0(2) |
→ |
45 |
|
p0(18) |
→ |
1 |
|
p0(24) |
→ |
25 |
|
p0(25) |
→ |
26 |
|
p0(43) |
→ |
44 |
|
p0(3) |
→ |
4 |
|
p0(11) |
→ |
12 |
|
p0(6) |
→ |
7 |
|
p0(23) |
→ |
24 |
|
p0(32) |
→ |
33 |
|
p0(7) |
→ |
8 |
|
p0(15) |
→ |
16 |
|
p0(27) |
→ |
28 |
|
p0(35) |
→ |
36 |
|
p0(20) |
→ |
19 |
|
p0(12) |
→ |
13 |
|
p0(34) |
→ |
35 |
|
p0(44) |
→ |
21 |
|
p0(16) |
→ |
17 |