R
↳Dependency Pair Analysis
FST(s(X), cons(Y, Z)) -> FST(X, Z)
FROM(X) -> FROM(s(X))
ADD(s(X), Y) -> ADD(X, Y)
LEN(cons(X, Z)) -> LEN(Z)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
→DP Problem 2
↳Inst
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FST(s(X), cons(Y, Z)) -> FST(X, Z)
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
one new Dependency Pair is created:
FST(s(X), cons(Y, Z)) -> FST(X, Z)
FST(s(s(X'')), cons(Y, cons(Y'', Z''))) -> FST(s(X''), cons(Y'', Z''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 5
↳Forward Instantiation Transformation
→DP Problem 2
↳Inst
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FST(s(s(X'')), cons(Y, cons(Y'', Z''))) -> FST(s(X''), cons(Y'', Z''))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
one new Dependency Pair is created:
FST(s(s(X'')), cons(Y, cons(Y'', Z''))) -> FST(s(X''), cons(Y'', Z''))
FST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 5
↳FwdInst
...
→DP Problem 6
↳Argument Filtering and Ordering
→DP Problem 2
↳Inst
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
FST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
POL(FST(x1, x2)) = 1 + x1 + x2 POL(cons(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
FST(x1, x2) -> FST(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 5
↳FwdInst
...
→DP Problem 7
↳Dependency Graph
→DP Problem 2
↳Inst
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Instantiation Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FROM(X) -> FROM(s(X))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
one new Dependency Pair is created:
FROM(X) -> FROM(s(X))
FROM(s(X'')) -> FROM(s(s(X'')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Inst
→DP Problem 8
↳Instantiation Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FROM(s(X'')) -> FROM(s(s(X'')))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
one new Dependency Pair is created:
FROM(s(X'')) -> FROM(s(s(X'')))
FROM(s(s(X''''))) -> FROM(s(s(s(X''''))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Inst
→DP Problem 8
↳Inst
...
→DP Problem 9
↳Instantiation Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FROM(s(s(X''''))) -> FROM(s(s(s(X''''))))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
one new Dependency Pair is created:
FROM(s(s(X''''))) -> FROM(s(s(s(X''''))))
FROM(s(s(s(X'''''')))) -> FROM(s(s(s(s(X'''''')))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Inst
→DP Problem 8
↳Inst
...
→DP Problem 10
↳Instantiation Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FROM(s(s(s(X'''''')))) -> FROM(s(s(s(s(X'''''')))))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
one new Dependency Pair is created:
FROM(s(s(s(X'''''')))) -> FROM(s(s(s(s(X'''''')))))
FROM(s(s(s(s(X''''''''))))) -> FROM(s(s(s(s(s(X''''''''))))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Inst
→DP Problem 8
↳Inst
...
→DP Problem 11
↳Instantiation Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
FROM(s(s(s(s(X''''''''))))) -> FROM(s(s(s(s(s(X''''''''))))))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
one new Dependency Pair is created:
FROM(s(s(s(s(X''''''''))))) -> FROM(s(s(s(s(s(X''''''''))))))
FROM(s(s(s(s(s(X'''''''''')))))) -> FROM(s(s(s(s(s(s(X'''''''''')))))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Inst
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
FROM(s(s(s(s(s(X'''''''''')))))) -> FROM(s(s(s(s(s(s(X'''''''''')))))))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
ADD(s(X), Y) -> ADD(X, Y)
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
LEN(cons(X, Z)) -> LEN(Z)
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Inst
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
FROM(s(s(s(s(s(X'''''''''')))))) -> FROM(s(s(s(s(s(s(X'''''''''')))))))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
ADD(s(X), Y) -> ADD(X, Y)
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
LEN(cons(X, Z)) -> LEN(Z)
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Inst
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
FROM(s(s(s(s(s(X'''''''''')))))) -> FROM(s(s(s(s(s(s(X'''''''''')))))))
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
ADD(s(X), Y) -> ADD(X, Y)
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost
LEN(cons(X, Z)) -> LEN(Z)
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, fst(X, Z))
from(X) -> cons(X, from(s(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
len(nil) -> 0
len(cons(X, Z)) -> s(len(Z))
innermost