R
↳Dependency Pair Analysis
TERMS(N) > SQR(N)
SQR(s(X)) > ADD(sqr(X), dbl(X))
SQR(s(X)) > SQR(X)
SQR(s(X)) > DBL(X)
DBL(s(X)) > DBL(X)
ADD(s(X), Y) > ADD(X, Y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
ADD(s(X), Y) > ADD(X, Y)
terms(N) > cons(recip(sqr(N)))
sqr(0) > 0
sqr(s(X)) > s(add(sqr(X), dbl(X)))
dbl(0) > 0
dbl(s(X)) > s(s(dbl(X)))
add(0, X) > X
add(s(X), Y) > s(add(X, Y))
first(0, X) > nil
first(s(X), cons(Y)) > cons(Y)
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳SizeChange Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
ADD(s(X), Y) > ADD(X, Y)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
DBL(s(X)) > DBL(X)
terms(N) > cons(recip(sqr(N)))
sqr(0) > 0
sqr(s(X)) > s(add(sqr(X), dbl(X)))
dbl(0) > 0
dbl(s(X)) > s(s(dbl(X)))
add(0, X) > X
add(s(X), Y) > s(add(X, Y))
first(0, X) > nil
first(s(X), cons(Y)) > cons(Y)
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 5
↳SizeChange Principle
→DP Problem 3
↳UsableRules
DBL(s(X)) > DBL(X)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
SQR(s(X)) > SQR(X)
terms(N) > cons(recip(sqr(N)))
sqr(0) > 0
sqr(s(X)) > s(add(sqr(X), dbl(X)))
dbl(0) > 0
dbl(s(X)) > s(s(dbl(X)))
add(0, X) > X
add(s(X), Y) > s(add(X, Y))
first(0, X) > nil
first(s(X), cons(Y)) > cons(Y)
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳SizeChange Principle
SQR(s(X)) > SQR(X)
none
innermost


trivial
s(x_{1}) > s(x_{1})