YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
log(s(x0)) |
→ |
s(log(half(s(x0)))) |
|
half(0(x0)) |
→ |
0(s(s(half(x0)))) |
|
half(s(0(x0))) |
→ |
0(x0) |
|
half(s(s(x0))) |
→ |
s(half(p(s(s(x0))))) |
|
half(half(s(s(s(s(x0)))))) |
→ |
s(s(half(half(x0)))) |
|
p(s(s(s(x0)))) |
→ |
s(p(s(s(x0)))) |
|
s(s(p(s(x0)))) |
→ |
s(s(x0)) |
|
0(x0) |
→ |
x0 |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [p(x1)] |
= |
0 ·
x1 +
-∞
|
| [log(x1)] |
= |
0 ·
x1 +
-∞
|
| [0(x1)] |
= |
1 ·
x1 +
-∞
|
| [s(x1)] |
= |
0 ·
x1 +
-∞
|
| [half(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
log(s(x0)) |
→ |
s(log(half(s(x0)))) |
|
half(0(x0)) |
→ |
0(s(s(half(x0)))) |
|
half(s(0(x0))) |
→ |
0(x0) |
|
half(s(s(x0))) |
→ |
s(half(p(s(s(x0))))) |
|
half(half(s(s(s(s(x0)))))) |
→ |
s(s(half(half(x0)))) |
|
p(s(s(s(x0)))) |
→ |
s(p(s(s(x0)))) |
|
s(s(p(s(x0)))) |
→ |
s(s(x0)) |
remain.
1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
log#(s(x0)) |
→ |
half#(s(x0)) |
|
log#(s(x0)) |
→ |
log#(half(s(x0))) |
|
log#(s(x0)) |
→ |
s#(log(half(s(x0)))) |
|
half#(0(x0)) |
→ |
half#(x0) |
|
half#(0(x0)) |
→ |
s#(half(x0)) |
|
half#(0(x0)) |
→ |
s#(s(half(x0))) |
|
half#(s(s(x0))) |
→ |
p#(s(s(x0))) |
|
half#(s(s(x0))) |
→ |
half#(p(s(s(x0)))) |
|
half#(s(s(x0))) |
→ |
s#(half(p(s(s(x0))))) |
|
half#(half(s(s(s(s(x0)))))) |
→ |
half#(x0) |
|
half#(half(s(s(s(s(x0)))))) |
→ |
half#(half(x0)) |
|
half#(half(s(s(s(s(x0)))))) |
→ |
s#(half(half(x0))) |
|
half#(half(s(s(s(s(x0)))))) |
→ |
s#(s(half(half(x0)))) |
|
p#(s(s(s(x0)))) |
→ |
p#(s(s(x0))) |
|
p#(s(s(s(x0)))) |
→ |
s#(p(s(s(x0)))) |
|
s#(s(p(s(x0)))) |
→ |
s#(s(x0)) |
1.1.1 Dependency Graph Processor
The dependency pairs are split into 4
components.
-
The
1st
component contains the
pair
|
log#(s(x0)) |
→ |
log#(half(s(x0))) |
1.1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [p(x1)] |
= |
-7 ·
x1 + 4 |
| [0(x1)] |
= |
-∞
·
x1 + 0 |
| [log#(x1)] |
= |
0 ·
x1 + 4 |
| [s(x1)] |
= |
7 ·
x1 + 8 |
| [half(x1)] |
= |
-7 ·
x1 + 0 |
together with the usable
rules
|
s(s(p(s(x0)))) |
→ |
s(s(x0)) |
|
half(0(x0)) |
→ |
0(s(s(half(x0)))) |
|
half(s(0(x0))) |
→ |
0(x0) |
|
half(s(s(x0))) |
→ |
s(half(p(s(s(x0))))) |
|
half(half(s(s(s(s(x0)))))) |
→ |
s(s(half(half(x0)))) |
|
p(s(s(s(x0)))) |
→ |
s(p(s(s(x0)))) |
(w.r.t. the implicit argument filter of the reduction pair),
all pairs could be removed.
1.1.1.1.1 P is empty
There are no pairs anymore.
-
The
2nd
component contains the
pairs
|
half#(0(x0)) |
→ |
half#(x0) |
|
half#(half(s(s(s(s(x0)))))) |
→ |
half#(half(x0)) |
|
half#(half(s(s(s(s(x0)))))) |
→ |
half#(x0) |
|
half#(s(s(x0))) |
→ |
half#(p(s(s(x0)))) |
1.1.1.2 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [p(x1)] |
= |
0 ·
x1 +
-∞
|
| [0(x1)] |
= |
0 ·
x1 +
-∞
|
| [s(x1)] |
= |
0 ·
x1 +
-∞
|
| [half#(x1)] |
= |
4 ·
x1 + 0 |
| [half(x1)] |
= |
12 ·
x1 + 0 |
together with the usable
rules
|
half(0(x0)) |
→ |
0(s(s(half(x0)))) |
|
half(s(0(x0))) |
→ |
0(x0) |
|
half(s(s(x0))) |
→ |
s(half(p(s(s(x0))))) |
|
half(half(s(s(s(s(x0)))))) |
→ |
s(s(half(half(x0)))) |
|
s(s(p(s(x0)))) |
→ |
s(s(x0)) |
|
p(s(s(s(x0)))) |
→ |
s(p(s(s(x0)))) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
|
half#(0(x0)) |
→ |
half#(x0) |
|
half#(half(s(s(s(s(x0)))))) |
→ |
half#(half(x0)) |
|
half#(s(s(x0))) |
→ |
half#(p(s(s(x0)))) |
remain.
1.1.1.2.1 Dependency Graph Processor
The dependency pairs are split into 2
components.
-
The
3rd
component contains the
pair
|
p#(s(s(s(x0)))) |
→ |
p#(s(s(x0))) |
1.1.1.3 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [p(x1)] |
= |
1 ·
x1 + 4 |
| [p#(x1)] |
= |
0 ·
x1 + 0 |
| [s(x1)] |
= |
10 ·
x1 + 1 |
together with the usable
rule
|
s(s(p(s(x0)))) |
→ |
s(s(x0)) |
(w.r.t. the implicit argument filter of the reduction pair),
all pairs could be removed.
1.1.1.3.1 P is empty
There are no pairs anymore.
-
The
4th
component contains the
pair
|
s#(s(p(s(x0)))) |
→ |
s#(s(x0)) |
1.1.1.4 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the arctic semiring over the integers
| [p(x1)] |
= |
1 ·
x1 + 1 |
| [s(x1)] |
= |
0 ·
x1 +
-∞
|
| [s#(x1)] |
= |
0 ·
x1 +
-∞
|
together with the usable
rule
|
s(s(p(s(x0)))) |
→ |
s(s(x0)) |
(w.r.t. the implicit argument filter of the reduction pair),
all pairs could be removed.
1.1.1.4.1 P is empty
There are no pairs anymore.