Term Rewriting System R:
[x, y]
f(0) -> true
f(1) -> false
f(s(x)) -> f(x)
if(true, s(x), s(y)) -> s(x)
if(false, s(x), s(y)) -> s(y)
g(x, c(y)) -> c(g(x, y))
g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(s(x)) -> F(x)
G(x, c(y)) -> G(x, y)
G(x, c(y)) -> G(x, if(f(x), c(g(s(x), y)), c(y)))
G(x, c(y)) -> IF(f(x), c(g(s(x), y)), c(y))
G(x, c(y)) -> F(x)
G(x, c(y)) -> G(s(x), y)
Furthermore, R contains two SCCs.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
→DP Problem 2
↳SCP
Dependency Pair:
F(s(x)) -> F(x)
Rules:
f(0) -> true
f(1) -> false
f(s(x)) -> f(x)
if(true, s(x), s(y)) -> s(x)
if(false, s(x), s(y)) -> s(y)
g(x, c(y)) -> c(g(x, y))
g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
We number the DPs as follows:
- F(s(x)) -> F(x)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s(x1) -> s(x1)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Size-Change Principle
Dependency Pairs:
G(x, c(y)) -> G(s(x), y)
G(x, c(y)) -> G(x, y)
Rules:
f(0) -> true
f(1) -> false
f(s(x)) -> f(x)
if(true, s(x), s(y)) -> s(x)
if(false, s(x), s(y)) -> s(y)
g(x, c(y)) -> c(g(x, y))
g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
We number the DPs as follows:
- G(x, c(y)) -> G(s(x), y)
- G(x, c(y)) -> G(x, y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
c(x1) -> c(x1)
s(x1) -> s(x1)
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes