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