R
↳Dependency Pair Analysis
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
AF(g(X), Y) -> MARK(X)
MARK(f(X1, X2)) -> AF(mark(X1), X2)
MARK(f(X1, X2)) -> MARK(X1)
MARK(g(X)) -> MARK(X)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
MARK(g(X)) -> MARK(X)
MARK(f(X1, X2)) -> MARK(X1)
MARK(f(X1, X2)) -> AF(mark(X1), X2)
AF(g(X), Y) -> MARK(X)
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
two new Dependency Pairs are created:
MARK(f(X1, X2)) -> AF(mark(X1), X2)
MARK(f(f(X1'', X2''), X2)) -> AF(af(mark(X1''), X2''), X2)
MARK(f(g(X'), X2)) -> AF(g(mark(X')), X2)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
MARK(f(g(X'), X2)) -> AF(g(mark(X')), X2)
AF(g(X), Y) -> MARK(X)
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
MARK(f(f(X1'', X2''), X2)) -> AF(af(mark(X1''), X2''), X2)
MARK(f(X1, X2)) -> MARK(X1)
MARK(g(X)) -> MARK(X)
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
three new Dependency Pairs are created:
MARK(f(f(X1'', X2''), X2)) -> AF(af(mark(X1''), X2''), X2)
MARK(f(f(X1''', X2'''), X2)) -> AF(f(mark(X1'''), X2'''), X2)
MARK(f(f(f(X1', X2'''), X2''), X2)) -> AF(af(af(mark(X1'), X2'''), X2''), X2)
MARK(f(f(g(X'), X2''), X2)) -> AF(af(g(mark(X')), X2''), X2)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Argument Filtering and Ordering
MARK(f(f(g(X'), X2''), X2)) -> AF(af(g(mark(X')), X2''), X2)
MARK(f(f(f(X1', X2'''), X2''), X2)) -> AF(af(af(mark(X1'), X2'''), X2''), X2)
MARK(g(X)) -> MARK(X)
MARK(f(X1, X2)) -> MARK(X1)
AF(g(X), Y) -> MARK(X)
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
MARK(f(g(X'), X2)) -> AF(g(mark(X')), X2)
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
MARK(g(X)) -> MARK(X)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
{mark, MARK, g}
AF(x1, x2) -> x1
g(x1) -> g(x1)
mark(x1) -> mark(x1)
MARK(x1) -> MARK(x1)
f(x1, x2) -> x1
af(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Argument Filtering and Ordering
MARK(f(f(g(X'), X2''), X2)) -> AF(af(g(mark(X')), X2''), X2)
MARK(f(f(f(X1', X2'''), X2''), X2)) -> AF(af(af(mark(X1'), X2'''), X2''), X2)
MARK(f(X1, X2)) -> MARK(X1)
AF(g(X), Y) -> MARK(X)
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
MARK(f(g(X'), X2)) -> AF(g(mark(X')), X2)
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
MARK(f(f(g(X'), X2''), X2)) -> AF(af(g(mark(X')), X2''), X2)
MARK(f(f(f(X1', X2'''), X2''), X2)) -> AF(af(af(mark(X1'), X2'''), X2''), X2)
MARK(f(X1, X2)) -> MARK(X1)
MARK(f(g(X'), X2)) -> AF(g(mark(X')), X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
{mark, f, MARK, af, g}
AF(x1, x2) -> x1
g(x1) -> g(x1)
mark(x1) -> mark(x1)
MARK(x1) -> MARK(x1)
f(x1, x2) -> f(x1)
af(x1, x2) -> af(x1)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Dependency Graph
AF(g(X), Y) -> MARK(X)
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Instantiation Transformation
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
one new Dependency Pair is created:
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
AF(g(X0), f(g(X''), Y'')) -> AF(mark(X0), f(g(X0), f(g(X''), Y'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Instantiation Transformation
AF(g(X0), f(g(X''), Y'')) -> AF(mark(X0), f(g(X0), f(g(X''), Y'')))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
one new Dependency Pair is created:
AF(g(X0), f(g(X''), Y'')) -> AF(mark(X0), f(g(X0), f(g(X''), Y'')))
AF(g(X0''), f(g(X''''), f(g(X'''''), Y''''))) -> AF(mark(X0''), f(g(X0''), f(g(X''''), f(g(X'''''), Y''''))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Argument Filtering and Ordering
AF(g(X0''), f(g(X''''), f(g(X'''''), Y''''))) -> AF(mark(X0''), f(g(X0''), f(g(X''''), f(g(X'''''), Y''''))))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
AF(g(X0''), f(g(X''''), f(g(X'''''), Y''''))) -> AF(mark(X0''), f(g(X0''), f(g(X''''), f(g(X'''''), Y''''))))
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
trivial
AF(x1, x2) -> AF(x1, x2)
g(x1) -> g(x1)
f(x1, x2) -> x1
mark(x1) -> x1
af(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Dependency Graph
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))