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
↳Polynomial 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))))
POL(g(x1)) = 1 + x1 POL(a(x1, x2)) = 0 POL(f(x1)) = 0 POL(F(x1)) = x1
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))))