Termination proof
1: switching to dependency pairs
The following set of initial dependency pairs has been identified.
|
div#(
X
,
e
)
|
→ |
i#(
X
)
|
|
i#(
div(
X
,
Y
)
)
|
→ |
div#(
Y
,
X
)
|
|
div#(
div(
X
,
Y
)
,
Z
)
|
→ |
div#(
Y
,
div(
i(
X
)
,
Z
)
)
|
|
div#(
div(
X
,
Y
)
,
Z
)
|
→ |
div#(
i(
X
)
,
Z
)
|
|
div#(
div(
X
,
Y
)
,
Z
)
|
→ |
i#(
X
)
|
1.1: reduction pair processor
Using the following reduction pair
Linear polynomial
interpretation over
the naturals
|
[e]
|
= |
1
|
|
[i
(x1)
]
|
= |
x1
|
|
[i#
(x1)
]
|
= |
x1
+
3
|
|
[div#
(x1, x2)
]
|
= |
x1 + x2
+
2
|
|
[div
(x1, x2)
]
|
= |
x1 + x2
+
2
|
|
[f(x1, ..., xn)]
|
= |
x1 + ... + xn + 1
|
for all other symbols f of arity n
|
one remains with the following pair(s).
|
div#(
X
,
e
)
|
→ |
i#(
X
)
|
|
div#(
div(
X
,
Y
)
,
Z
)
|
→ |
div#(
Y
,
div(
i(
X
)
,
Z
)
)
|
1.1.1: dependency graph processor
The dependency pairs are split into 1 component(s).