R
↳Dependency Pair Analysis
F(s(s(x))) -> F(f(s(x)))
F(s(s(x))) -> F(s(x))
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
F(s(s(x))) -> F(s(x))
F(s(s(x))) -> F(f(s(x)))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
two new Dependency Pairs are created:
F(s(s(x))) -> F(f(s(x)))
F(s(s(0))) -> F(s(0))
F(s(s(s(x'')))) -> F(f(f(s(x''))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
F(s(s(s(x'')))) -> F(f(f(s(x''))))
F(s(s(x))) -> F(s(x))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
two new Dependency Pairs are created:
F(s(s(s(x'')))) -> F(f(f(s(x''))))
F(s(s(s(0)))) -> F(f(s(0)))
F(s(s(s(s(x'))))) -> F(f(f(f(s(x')))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Narrowing Transformation
F(s(s(s(s(x'))))) -> F(f(f(f(s(x')))))
F(s(s(s(0)))) -> F(f(s(0)))
F(s(s(x))) -> F(s(x))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
one new Dependency Pair is created:
F(s(s(s(0)))) -> F(f(s(0)))
F(s(s(s(0)))) -> F(s(0))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
F(s(s(x))) -> F(s(x))
F(s(s(s(s(x'))))) -> F(f(f(f(s(x')))))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
two new Dependency Pairs are created:
F(s(s(s(s(x'))))) -> F(f(f(f(s(x')))))
F(s(s(s(s(0))))) -> F(f(f(s(0))))
F(s(s(s(s(s(x'')))))) -> F(f(f(f(f(s(x''))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
F(s(s(s(s(s(x'')))))) -> F(f(f(f(f(s(x''))))))
F(s(s(s(s(0))))) -> F(f(f(s(0))))
F(s(s(x))) -> F(s(x))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
one new Dependency Pair is created:
F(s(s(s(s(0))))) -> F(f(f(s(0))))
F(s(s(s(s(0))))) -> F(f(s(0)))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
F(s(s(s(s(0))))) -> F(f(s(0)))
F(s(s(x))) -> F(s(x))
F(s(s(s(s(s(x'')))))) -> F(f(f(f(f(s(x''))))))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
two new Dependency Pairs are created:
F(s(s(s(s(s(x'')))))) -> F(f(f(f(f(s(x''))))))
F(s(s(s(s(s(0)))))) -> F(f(f(f(s(0)))))
F(s(s(s(s(s(s(x'))))))) -> F(f(f(f(f(f(s(x')))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
F(s(s(s(s(s(s(x'))))))) -> F(f(f(f(f(f(s(x')))))))
F(s(s(s(s(s(0)))))) -> F(f(f(f(s(0)))))
F(s(s(x))) -> F(s(x))
F(s(s(s(s(0))))) -> F(f(s(0)))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
one new Dependency Pair is created:
F(s(s(s(s(0))))) -> F(f(s(0)))
F(s(s(s(s(0))))) -> F(s(0))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
F(s(s(s(s(s(0)))))) -> F(f(f(f(s(0)))))
F(s(s(x))) -> F(s(x))
F(s(s(s(s(s(s(x'))))))) -> F(f(f(f(f(f(s(x')))))))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
one new Dependency Pair is created:
F(s(s(s(s(s(0)))))) -> F(f(f(f(s(0)))))
F(s(s(s(s(s(0)))))) -> F(f(f(s(0))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Narrowing Transformation
F(s(s(s(s(s(0)))))) -> F(f(f(s(0))))
F(s(s(s(s(s(s(x'))))))) -> F(f(f(f(f(f(s(x')))))))
F(s(s(x))) -> F(s(x))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))
two new Dependency Pairs are created:
F(s(s(s(s(s(s(x'))))))) -> F(f(f(f(f(f(s(x')))))))
F(s(s(s(s(s(s(0))))))) -> F(f(f(f(f(s(0))))))
F(s(s(s(s(s(s(s(x'')))))))) -> F(f(f(f(f(f(f(s(x''))))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 10
↳Remaining Obligation(s)
F(s(s(s(s(s(s(s(x'')))))))) -> F(f(f(f(f(f(f(s(x''))))))))
F(s(s(s(s(s(s(0))))))) -> F(f(f(f(f(s(0))))))
F(s(s(x))) -> F(s(x))
F(s(s(s(s(s(0)))))) -> F(f(f(s(0))))
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x)))