R
↳Dependency Pair Analysis
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
↳Remaining
FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
one new Dependency Pair is created:
FIRST(s(X), cons(Y, Z)) -> FIRST(X, Z)
FIRST(s(s(X'')), cons(Y, Z')) -> FIRST(s(X''), Z')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 3
↳Forward Instantiation Transformation
→DP Problem 2
↳Remaining
FIRST(s(s(X'')), cons(Y, Z')) -> FIRST(s(X''), Z')
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
one new Dependency Pair is created:
FIRST(s(s(X'')), cons(Y, Z')) -> FIRST(s(X''), Z')
FIRST(s(s(s(X''''))), cons(Y, Z'')) -> FIRST(s(s(X'''')), Z'')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 3
↳FwdInst
...
→DP Problem 4
↳Forward Instantiation Transformation
→DP Problem 2
↳Remaining
FIRST(s(s(s(X''''))), cons(Y, Z'')) -> FIRST(s(s(X'''')), Z'')
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
one new Dependency Pair is created:
FIRST(s(s(s(X''''))), cons(Y, Z'')) -> FIRST(s(s(X'''')), Z'')
FIRST(s(s(s(s(X'''''')))), cons(Y, Z''')) -> FIRST(s(s(s(X''''''))), Z''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 3
↳FwdInst
...
→DP Problem 5
↳Forward Instantiation Transformation
→DP Problem 2
↳Remaining
FIRST(s(s(s(s(X'''''')))), cons(Y, Z''')) -> FIRST(s(s(s(X''''''))), Z''')
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
one new Dependency Pair is created:
FIRST(s(s(s(s(X'''''')))), cons(Y, Z''')) -> FIRST(s(s(s(X''''''))), Z''')
FIRST(s(s(s(s(s(X''''''''))))), cons(Y, Z'''')) -> FIRST(s(s(s(s(X'''''''')))), Z'''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 3
↳FwdInst
...
→DP Problem 6
↳Forward Instantiation Transformation
→DP Problem 2
↳Remaining
FIRST(s(s(s(s(s(X''''''''))))), cons(Y, Z'''')) -> FIRST(s(s(s(s(X'''''''')))), Z'''')
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
one new Dependency Pair is created:
FIRST(s(s(s(s(s(X''''''''))))), cons(Y, Z'''')) -> FIRST(s(s(s(s(X'''''''')))), Z'''')
FIRST(s(s(s(s(s(s(X'''''''''')))))), cons(Y, Z''''')) -> FIRST(s(s(s(s(s(X''''''''''))))), Z''''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Remaining Obligation(s)
FIRST(s(s(s(s(s(s(X'''''''''')))))), cons(Y, Z''''')) -> FIRST(s(s(s(s(s(X''''''''''))))), Z''''')
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
FROM(X) -> FROM(s(X))
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Remaining Obligation(s)
FIRST(s(s(s(s(s(s(X'''''''''')))))), cons(Y, Z''''')) -> FIRST(s(s(s(s(s(X''''''''''))))), Z''''')
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))
FROM(X) -> FROM(s(X))
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
from(X) -> cons(X, from(s(X)))