R
↳Dependency Pair Analysis
APP(g, app(g, x)) -> APP(g, app(h, app(g, x)))
APP(g, app(g, x)) -> APP(h, app(g, x))
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(f, app(h, x))
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, x)) -> APP(h, app(g, x))
APP(g, app(g, x)) -> APP(g, app(h, app(g, x)))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
two new Dependency Pairs are created:
APP(g, app(g, x)) -> APP(g, app(h, app(g, x)))
APP(g, app(g, app(h, app(g, x'')))) -> APP(g, app(h, app(g, x'')))
APP(g, app(g, app(g, x''))) -> APP(g, app(h, app(g, app(h, app(g, x'')))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
APP(g, app(g, app(g, x''))) -> APP(g, app(h, app(g, app(h, app(g, x'')))))
APP(g, app(g, app(h, app(g, x'')))) -> APP(g, app(h, app(g, x'')))
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, x)) -> APP(h, app(g, x))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
two new Dependency Pairs are created:
APP(g, app(g, x)) -> APP(h, app(g, x))
APP(g, app(g, app(h, app(g, x'')))) -> APP(h, app(g, x''))
APP(g, app(g, app(g, x''))) -> APP(h, app(g, app(h, app(g, x''))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Narrowing Transformation
APP(g, app(g, app(g, x''))) -> APP(h, app(g, app(h, app(g, x''))))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, app(h, app(g, x'')))) -> APP(h, app(g, x''))
APP(g, app(g, app(h, app(g, x'')))) -> APP(g, app(h, app(g, x'')))
APP(g, app(g, app(g, x''))) -> APP(g, app(h, app(g, app(h, app(g, x'')))))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
two new Dependency Pairs are created:
APP(g, app(g, app(h, app(g, x'')))) -> APP(g, app(h, app(g, x'')))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(g, app(h, app(g, x')))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(g, app(h, app(g, x')))
APP(g, app(g, app(h, app(g, x'')))) -> APP(h, app(g, x''))
APP(g, app(g, app(g, x''))) -> APP(g, app(h, app(g, app(h, app(g, x'')))))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, app(g, x''))) -> APP(h, app(g, app(h, app(g, x''))))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
three new Dependency Pairs are created:
APP(g, app(g, app(g, x''))) -> APP(g, app(h, app(g, app(h, app(g, x'')))))
APP(g, app(g, app(g, x'''))) -> APP(g, app(h, app(g, x''')))
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(g, app(g, x')))) -> APP(g, app(h, app(g, app(h, app(g, app(h, app(g, x')))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
APP(g, app(g, app(g, app(g, x')))) -> APP(g, app(h, app(g, app(h, app(g, app(h, app(g, x')))))))
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(g, x'''))) -> APP(g, app(h, app(g, x''')))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(g, app(h, app(g, x')))
APP(g, app(g, app(g, x''))) -> APP(h, app(g, app(h, app(g, x''))))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, app(h, app(g, x'')))) -> APP(h, app(g, x''))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
two new Dependency Pairs are created:
APP(g, app(g, app(h, app(g, x'')))) -> APP(h, app(g, x''))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(h, app(g, x'))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(h, app(g, app(h, app(g, x'))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(h, app(g, app(h, app(g, x'))))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(h, app(g, x'))
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(g, x'''))) -> APP(g, app(h, app(g, x''')))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(g, app(h, app(g, x')))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, app(g, x''))) -> APP(h, app(g, app(h, app(g, x''))))
APP(g, app(g, app(g, app(g, x')))) -> APP(g, app(h, app(g, app(h, app(g, app(h, app(g, x')))))))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
three new Dependency Pairs are created:
APP(g, app(g, app(g, x''))) -> APP(h, app(g, app(h, app(g, x''))))
APP(g, app(g, app(g, x'''))) -> APP(h, app(g, x'''))
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(h, app(g, app(h, app(g, x'))))
APP(g, app(g, app(g, app(g, x')))) -> APP(h, app(g, app(h, app(g, app(h, app(g, x'))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Forward Instantiation Transformation
APP(g, app(g, app(g, app(g, x')))) -> APP(h, app(g, app(h, app(g, app(h, app(g, x'))))))
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(h, app(g, app(h, app(g, x'))))
APP(g, app(g, app(g, x'''))) -> APP(h, app(g, x'''))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(h, app(g, x'))
APP(g, app(g, app(g, app(g, x')))) -> APP(g, app(h, app(g, app(h, app(g, app(h, app(g, x')))))))
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(g, x'''))) -> APP(g, app(h, app(g, x''')))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(g, app(h, app(g, x')))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(h, app(g, app(h, app(g, x'))))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
no new Dependency Pairs are created.
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Argument Filtering and Ordering
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
h > f
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 10
↳Dependency Graph
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Argument Filtering and Ordering
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(g, x'''))) -> APP(g, app(h, app(g, x''')))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(g, app(h, app(g, x')))
APP(g, app(g, app(g, app(g, x')))) -> APP(g, app(h, app(g, app(h, app(g, app(h, app(g, x')))))))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
APP(g, app(g, app(g, app(h, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(g, x'''))) -> APP(g, app(h, app(g, x''')))
APP(g, app(g, app(h, app(g, app(g, x'))))) -> APP(g, app(h, app(g, app(h, app(g, x')))))
APP(g, app(g, app(h, app(g, app(h, app(g, x')))))) -> APP(g, app(h, app(g, x')))
APP(g, app(g, app(g, app(g, x')))) -> APP(g, app(h, app(g, app(h, app(g, app(h, app(g, x')))))))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
g > h
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> x1