0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
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))
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)
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)
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(e(x), e(y)) → G(x, y)
h > [e1, d2]
0 > [e1, d2]
G1: [1]
e1: [1]
h: multiset
d2: [2,1]
0: multiset
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))
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(c(z), g(x, y))
D(z, g(x, y)) → D(z, y)
D(c(z), g(g(x, y), 0)) → D(z, 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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D(c(z), g(g(x, y), 0)) → D(z, g(x, y))
g > 0 > c1 > d2
h > c1 > d2
c1: [1]
g: multiset
0: multiset
h: []
d2: multiset
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(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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D(c(z), g(g(x, y), 0)) → D(c(z), g(x, y))
D(z, g(x, y)) → D(z, y)
[0, d2] > [D2, g2] > e1
h1 > e1
D2: [1,2]
g2: multiset
0: multiset
h1: [1]
e1: multiset
d2: [1,2]
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))
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))
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))