R
↳Dependency Pair Analysis
ADD(s(X), Y) -> ADD(X, Y)
FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
FROM(X) -> FROM(s(X))
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Inst
ADD(s(X), Y) -> ADD(X, Y)
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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 4
↳Forward Instantiation Transformation
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Inst
ADD(s(s(X'')), Y'') -> ADD(s(X''), Y'')
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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 4
↳FwdInst
...
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Inst
ADD(s(s(s(X''''))), Y'''') -> ADD(s(s(X'''')), Y'''')
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
innermost
ADD(s(s(s(X''''))), Y'''') -> ADD(s(s(X'''')), Y'''')
ADD(x1, x2) -> ADD(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Inst
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Forward Instantiation Transformation
→DP Problem 3
↳Inst
FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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 7
↳Forward Instantiation Transformation
→DP Problem 3
↳Inst
FIRST(s(s(X'')), cons(Y, cons(Y'', Z''))) -> FIRST(s(X''), cons(Y'', Z''))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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 7
↳FwdInst
...
→DP Problem 8
↳Argument Filtering and Ordering
→DP Problem 3
↳Inst
FIRST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FIRST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
innermost
FIRST(s(s(s(X''''))), cons(Y, cons(Y''0, cons(Y'''', Z'''')))) -> FIRST(s(s(X'''')), cons(Y''0, cons(Y'''', Z'''')))
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 7
↳FwdInst
...
→DP Problem 9
↳Dependency Graph
→DP Problem 3
↳Inst
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Instantiation Transformation
FROM(X) -> FROM(s(X))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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
↳FwdInst
→DP Problem 3
↳Inst
→DP Problem 10
↳Instantiation Transformation
FROM(s(X'')) -> FROM(s(s(X'')))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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
↳FwdInst
→DP Problem 3
↳Inst
→DP Problem 10
↳Inst
...
→DP Problem 11
↳Instantiation Transformation
FROM(s(s(X''''))) -> FROM(s(s(s(X''''))))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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
↳FwdInst
→DP Problem 3
↳Inst
→DP Problem 10
↳Inst
...
→DP Problem 12
↳Instantiation Transformation
FROM(s(s(s(X'''''')))) -> FROM(s(s(s(s(X'''''')))))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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
↳FwdInst
→DP Problem 3
↳Inst
→DP Problem 10
↳Inst
...
→DP Problem 13
↳Instantiation Transformation
FROM(s(s(s(s(X''''''''))))) -> FROM(s(s(s(s(s(X''''''''))))))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
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
↳FwdInst
→DP Problem 3
↳Inst
→DP Problem 10
↳Inst
...
→DP Problem 14
↳Remaining Obligation(s)
FROM(s(s(s(s(s(X'''''''''')))))) -> FROM(s(s(s(s(s(s(X'''''''''')))))))
and(true, X) -> X
and(false, Y) -> false
if(true, X, Y) -> X
if(false, X, Y) -> Y
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))
from(X) -> cons(X, from(s(X)))
innermost