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
↳Forward Instantiation Transformation
F(g(g(g(x''''))), y'''') -> F(g(g(x'''')), y'''')
f(x, x) -> a
f(g(x), y) -> f(x, y)
one new Dependency Pair is created:
F(g(g(g(x''''))), y'''') -> F(g(g(x'''')), y'''')
F(g(g(g(g(x'''''')))), y'''''') -> F(g(g(g(x''''''))), y'''''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 4
↳Forward Instantiation Transformation
F(g(g(g(g(x'''''')))), y'''''') -> F(g(g(g(x''''''))), y'''''')
f(x, x) -> a
f(g(x), y) -> f(x, y)
one new Dependency Pair is created:
F(g(g(g(g(x'''''')))), y'''''') -> F(g(g(g(x''''''))), y'''''')
F(g(g(g(g(g(x''''''''))))), y'''''''') -> F(g(g(g(g(x'''''''')))), y'''''''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 5
↳Forward Instantiation Transformation
F(g(g(g(g(g(x''''''''))))), y'''''''') -> F(g(g(g(g(x'''''''')))), y'''''''')
f(x, x) -> a
f(g(x), y) -> f(x, y)
one new Dependency Pair is created:
F(g(g(g(g(g(x''''''''))))), y'''''''') -> F(g(g(g(g(x'''''''')))), y'''''''')
F(g(g(g(g(g(g(x'''''''''')))))), y'''''''''') -> F(g(g(g(g(g(x''''''''''))))), y'''''''''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 6
↳Remaining Obligation(s)
F(g(g(g(g(g(g(x'''''''''')))))), y'''''''''') -> F(g(g(g(g(g(x''''''''''))))), y'''''''''')
f(x, x) -> a
f(g(x), y) -> f(x, y)