R
↳Dependency Pair Analysis
F(g(x), y) -> F(x, y)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
F(g(x), y) -> F(x, y)
f(x, x) -> a
f(g(x), y) -> f(x, y)
one new Dependency Pair is created:
F(g(x), y) -> F(x, y)
F(g(g(x'')), y'') -> F(g(x''), y'')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Forward Instantiation Transformation
F(g(g(x'')), y'') -> F(g(x''), y'')
f(x, x) -> a
f(g(x), y) -> f(x, y)
one new Dependency Pair is created:
F(g(g(x'')), y'') -> F(g(x''), y'')
F(g(g(g(x''''))), y'''') -> F(g(g(x'''')), y'''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 3
↳Argument Filtering and Ordering
F(g(g(g(x''''))), y'''') -> F(g(g(x'''')), y'''')
f(x, x) -> a
f(g(x), y) -> f(x, y)
F(g(g(g(x''''))), y'''') -> F(g(g(x'''')), y'''')
f(x, x) -> a
f(g(x), y) -> f(x, y)
f > a
F(x1, x2) -> F(x1, x2)
g(x1) -> g(x1)
f(x1, x2) -> f(x1, x2)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 4
↳Dependency Graph
f(x, x) -> a
f(g(x), y) -> f(x, y)