R
↳Dependency Pair Analysis
TERMS(N) -> SQR(N)
TERMS(N) -> TERMS(s(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)
FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
ADD(s(X), Y) -> ADD(X, Y)
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
ADD(s(X), Y) -> ADD(X, Y)
ADD(s(s(X'')), Y'') -> ADD(s(X''), Y'')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 6
↳Forward Instantiation Transformation
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
ADD(s(s(X'')), Y'') -> ADD(s(X''), Y'')
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
ADD(s(s(X'')), Y'') -> ADD(s(X''), Y'')
ADD(s(s(s(X''''))), Y'''') -> ADD(s(s(X'''')), Y'''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 6
↳FwdInst
...
→DP Problem 7
↳Argument Filtering and Ordering
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
ADD(s(s(s(X''''))), Y'''') -> ADD(s(s(X'''')), Y'''')
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
ADD(s(s(s(X''''))), Y'''') -> ADD(s(s(X'''')), Y'''')
POL(s(x1)) = 1 + x1 POL(ADD(x1, x2)) = 1 + x1 + x2
ADD(x1, x2) -> ADD(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 6
↳FwdInst
...
→DP Problem 8
↳Dependency Graph
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Forward Instantiation Transformation
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
DBL(s(X)) -> DBL(X)
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
DBL(s(X)) -> DBL(X)
DBL(s(s(X''))) -> DBL(s(X''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 9
↳Forward Instantiation Transformation
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
DBL(s(s(X''))) -> DBL(s(X''))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
DBL(s(s(X''))) -> DBL(s(X''))
DBL(s(s(s(X'''')))) -> DBL(s(s(X'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 9
↳FwdInst
...
→DP Problem 10
↳Argument Filtering and Ordering
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
DBL(s(s(s(X'''')))) -> DBL(s(s(X'''')))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
DBL(s(s(s(X'''')))) -> DBL(s(s(X'''')))
POL(s(x1)) = 1 + x1 POL(DBL(x1)) = 1 + x1
DBL(x1) -> DBL(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 9
↳FwdInst
...
→DP Problem 11
↳Dependency Graph
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Forward Instantiation Transformation
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
FIRST(s(s(X'')), cons(Y, cons(Y'', Z''))) -> FIRST(s(X''), cons(Y'', Z''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 12
↳Forward Instantiation Transformation
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
FIRST(s(s(X'')), cons(Y, cons(Y'', Z''))) -> FIRST(s(X''), cons(Y'', Z''))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
FIRST(s(s(X'')), cons(Y, cons(Y'', Z''))) -> FIRST(s(X''), cons(Y'', Z''))
FIRST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FIRST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 12
↳FwdInst
...
→DP Problem 13
↳Argument Filtering and Ordering
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
FIRST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FIRST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
FIRST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FIRST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
POL(cons(x1, x2)) = x1 + x2 POL(FIRST(x1, x2)) = 1 + x1 + x2 POL(s(x1)) = 1 + x1
FIRST(x1, x2) -> FIRST(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 12
↳FwdInst
...
→DP Problem 14
↳Dependency Graph
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳Forward Instantiation Transformation
→DP Problem 5
↳Inst
SQR(s(X)) -> SQR(X)
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
SQR(s(X)) -> SQR(X)
SQR(s(s(X''))) -> SQR(s(X''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 15
↳Forward Instantiation Transformation
→DP Problem 5
↳Inst
SQR(s(s(X''))) -> SQR(s(X''))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
SQR(s(s(X''))) -> SQR(s(X''))
SQR(s(s(s(X'''')))) -> SQR(s(s(X'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 15
↳FwdInst
...
→DP Problem 16
↳Argument Filtering and Ordering
→DP Problem 5
↳Inst
SQR(s(s(s(X'''')))) -> SQR(s(s(X'''')))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
SQR(s(s(s(X'''')))) -> SQR(s(s(X'''')))
POL(s(x1)) = 1 + x1 POL(SQR(x1)) = 1 + x1
SQR(x1) -> SQR(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 15
↳FwdInst
...
→DP Problem 17
↳Dependency Graph
→DP Problem 5
↳Inst
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Instantiation Transformation
TERMS(N) -> TERMS(s(N))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
TERMS(N) -> TERMS(s(N))
TERMS(s(N'')) -> TERMS(s(s(N'')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
→DP Problem 18
↳Instantiation Transformation
TERMS(s(N'')) -> TERMS(s(s(N'')))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
TERMS(s(N'')) -> TERMS(s(s(N'')))
TERMS(s(s(N''''))) -> TERMS(s(s(s(N''''))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
→DP Problem 18
↳Inst
...
→DP Problem 19
↳Instantiation Transformation
TERMS(s(s(N''''))) -> TERMS(s(s(s(N''''))))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
TERMS(s(s(N''''))) -> TERMS(s(s(s(N''''))))
TERMS(s(s(s(N'''''')))) -> TERMS(s(s(s(s(N'''''')))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
→DP Problem 18
↳Inst
...
→DP Problem 20
↳Instantiation Transformation
TERMS(s(s(s(N'''''')))) -> TERMS(s(s(s(s(N'''''')))))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
TERMS(s(s(s(N'''''')))) -> TERMS(s(s(s(s(N'''''')))))
TERMS(s(s(s(s(N''''''''))))) -> TERMS(s(s(s(s(s(N''''''''))))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
→DP Problem 18
↳Inst
...
→DP Problem 21
↳Instantiation Transformation
TERMS(s(s(s(s(N''''''''))))) -> TERMS(s(s(s(s(s(N''''''''))))))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost
one new Dependency Pair is created:
TERMS(s(s(s(s(N''''''''))))) -> TERMS(s(s(s(s(s(N''''''''))))))
TERMS(s(s(s(s(s(N'''''''''')))))) -> TERMS(s(s(s(s(s(s(N'''''''''')))))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳FwdInst
→DP Problem 4
↳FwdInst
→DP Problem 5
↳Inst
→DP Problem 18
↳Inst
...
→DP Problem 22
↳Remaining Obligation(s)
TERMS(s(s(s(s(s(N'''''''''')))))) -> TERMS(s(s(s(s(s(s(N'''''''''')))))))
terms(N) -> cons(recip(sqr(N)), terms(s(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, Z)) -> cons(Y, first(X, Z))
innermost