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