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