R
↳Dependency Pair Analysis
F(x) -> F(g(x))
R
↳DPs
→DP Problem 1
↳Instantiation Transformation
F(x) -> F(g(x))
f(x) -> f(g(x))
one new Dependency Pair is created:
F(x) -> F(g(x))
F(g(x'')) -> F(g(g(x'')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Instantiation Transformation
F(g(x'')) -> F(g(g(x'')))
f(x) -> f(g(x))
one new Dependency Pair is created:
F(g(x'')) -> F(g(g(x'')))
F(g(g(x''''))) -> F(g(g(g(x''''))))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 3
↳Instantiation Transformation
F(g(g(x''''))) -> F(g(g(g(x''''))))
f(x) -> f(g(x))
one new Dependency Pair is created:
F(g(g(x''''))) -> F(g(g(g(x''''))))
F(g(g(g(x'''''')))) -> F(g(g(g(g(x'''''')))))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 4
↳Instantiation Transformation
F(g(g(g(x'''''')))) -> F(g(g(g(g(x'''''')))))
f(x) -> f(g(x))
one new Dependency Pair is created:
F(g(g(g(x'''''')))) -> F(g(g(g(g(x'''''')))))
F(g(g(g(g(x''''''''))))) -> F(g(g(g(g(g(x''''''''))))))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 5
↳Instantiation Transformation
F(g(g(g(g(x''''''''))))) -> F(g(g(g(g(g(x''''''''))))))
f(x) -> f(g(x))
one new Dependency Pair is created:
F(g(g(g(g(x''''''''))))) -> F(g(g(g(g(g(x''''''''))))))
F(g(g(g(g(g(x'''''''''')))))) -> F(g(g(g(g(g(g(x'''''''''')))))))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 6
↳Remaining Obligation(s)
F(g(g(g(g(g(x'''''''''')))))) -> F(g(g(g(g(g(g(x'''''''''')))))))
f(x) -> f(g(x))