R
↳Dependency Pair Analysis
H(z, e(x)) -> H(c(z), d(z, x))
H(z, e(x)) -> D(z, x)
D(z, g(x, y)) -> G(e(x), d(z, y))
D(z, g(x, y)) -> D(z, y)
D(c(z), g(g(x, y), 0)) -> G(d(c(z), g(x, y)), d(z, g(x, y)))
D(c(z), g(g(x, y), 0)) -> D(c(z), g(x, y))
D(c(z), g(g(x, y), 0)) -> D(z, g(x, y))
G(e(x), e(y)) -> G(x, y)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳Inst
G(e(x), e(y)) -> G(x, y)
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
G(e(x), e(y)) -> G(x, y)
G(x1, x2) -> G(x1, x2)
e(x1) -> e(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳Inst
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Inst
D(c(z), g(g(x, y), 0)) -> D(z, g(x, y))
D(c(z), g(g(x, y), 0)) -> D(c(z), g(x, y))
D(z, g(x, y)) -> D(z, y)
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
D(c(z), g(g(x, y), 0)) -> D(z, g(x, y))
D(c(z), g(g(x, y), 0)) -> D(c(z), g(x, y))
D(z, g(x, y)) -> D(z, y)
g(e(x), e(y)) -> e(g(x, y))
D(x1, x2) -> D(x1, x2)
c(x1) -> c(x1)
g(x1, x2) -> g(x1, x2)
e(x1) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Inst
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Instantiation Transformation
H(z, e(x)) -> H(c(z), d(z, x))
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
one new Dependency Pair is created:
H(z, e(x)) -> H(c(z), d(z, x))
H(c(z''), e(x')) -> H(c(c(z'')), d(c(z''), x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Inst
→DP Problem 6
↳Instantiation Transformation
H(c(z''), e(x')) -> H(c(c(z'')), d(c(z''), x'))
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
one new Dependency Pair is created:
H(c(z''), e(x')) -> H(c(c(z'')), d(c(z''), x'))
H(c(c(z'''')), e(x''')) -> H(c(c(c(z''''))), d(c(c(z'''')), x'''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Inst
→DP Problem 6
↳Inst
...
→DP Problem 7
↳Instantiation Transformation
H(c(c(z'''')), e(x''')) -> H(c(c(c(z''''))), d(c(c(z'''')), x'''))
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
one new Dependency Pair is created:
H(c(c(z'''')), e(x''')) -> H(c(c(c(z''''))), d(c(c(z'''')), x'''))
H(c(c(c(z''''''))), e(x'''')) -> H(c(c(c(c(z'''''')))), d(c(c(c(z''''''))), x''''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Inst
→DP Problem 6
↳Inst
...
→DP Problem 8
↳Instantiation Transformation
H(c(c(c(z''''''))), e(x'''')) -> H(c(c(c(c(z'''''')))), d(c(c(c(z''''''))), x''''))
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
one new Dependency Pair is created:
H(c(c(c(z''''''))), e(x'''')) -> H(c(c(c(c(z'''''')))), d(c(c(c(z''''''))), x''''))
H(c(c(c(c(z'''''''')))), e(x''''')) -> H(c(c(c(c(c(z''''''''))))), d(c(c(c(c(z'''''''')))), x'''''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Inst
→DP Problem 6
↳Inst
...
→DP Problem 9
↳Instantiation Transformation
H(c(c(c(c(z'''''''')))), e(x''''')) -> H(c(c(c(c(c(z''''''''))))), d(c(c(c(c(z'''''''')))), x'''''))
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))
one new Dependency Pair is created:
H(c(c(c(c(z'''''''')))), e(x''''')) -> H(c(c(c(c(c(z''''''''))))), d(c(c(c(c(z'''''''')))), x'''''))
H(c(c(c(c(c(z''''''''''))))), e(x'''''')) -> H(c(c(c(c(c(c(z'''''''''')))))), d(c(c(c(c(c(z''''''''''))))), x''''''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Inst
→DP Problem 6
↳Inst
...
→DP Problem 10
↳Remaining Obligation(s)
H(c(c(c(c(c(z''''''''''))))), e(x'''''')) -> H(c(c(c(c(c(c(z'''''''''')))))), d(c(c(c(c(c(z''''''''''))))), x''''''))
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))