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