R
↳Dependency Pair Analysis
+'(X, s(Y)) > +'(X, Y)
DOUBLE(X) > +'(X, X)
F(0, s(0), X) > F(X, double(X), X)
F(0, s(0), X) > DOUBLE(X)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
+'(X, s(Y)) > +'(X, Y)
+(X, 0) > X
+(X, s(Y)) > s(+(X, Y))
double(X) > +(X, X)
f(0, s(0), X) > f(X, double(X), X)
g(X, Y) > X
g(X, Y) > Y
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳SizeChange Principle
→DP Problem 2
↳UsableRules
+'(X, s(Y)) > +'(X, Y)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
F(0, s(0), X) > F(X, double(X), X)
+(X, 0) > X
+(X, s(Y)) > s(+(X, Y))
double(X) > +(X, X)
f(0, s(0), X) > f(X, double(X), X)
g(X, Y) > X
g(X, Y) > Y
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rewriting Transformation
F(0, s(0), X) > F(X, double(X), X)
+(X, 0) > X
+(X, s(Y)) > s(+(X, Y))
double(X) > +(X, X)
innermost
one new Dependency Pair is created:
F(0, s(0), X) > F(X, double(X), X)
F(0, s(0), X) > F(X, +(X, X), X)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 5
↳Narrowing Transformation
F(0, s(0), X) > F(X, +(X, X), X)
+(X, 0) > X
+(X, s(Y)) > s(+(X, Y))
double(X) > +(X, X)
innermost
two new Dependency Pairs are created:
F(0, s(0), X) > F(X, +(X, X), X)
F(0, s(0), 0) > F(0, 0, 0)
F(0, s(0), s(Y')) > F(s(Y'), s(+(s(Y'), Y')), s(Y'))