h(

d(

d(

d(c(

g(e(

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)

Furthermore,

R

↳DPs

→DP Problem 1

↳Argument Filtering and Ordering

→DP Problem 2

↳AFS

→DP Problem 3

↳Remaining

**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 dependency pair can be strictly oriented:

G(e(x), e(y)) -> G(x,y)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

resulting in one new DP problem.

Used Argument Filtering System:

G(x,_{1}x) -> G(_{2}x,_{1}x)_{2}

e(x) -> e(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 4

↳Dependency Graph

→DP Problem 2

↳AFS

→DP Problem 3

↳Remaining

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))

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳Argument Filtering and Ordering

→DP Problem 3

↳Remaining

**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 dependency pairs can be strictly oriented:

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)

The following usable rule using the Ce-refinement can be oriented:

g(e(x), e(y)) -> e(g(x,y))

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

g > e

resulting in one new DP problem.

Used Argument Filtering System:

D(x,_{1}x) -> D(_{2}x,_{1}x)_{2}

c(x) -> c(_{1}x)_{1}

g(x,_{1}x) -> g(_{2}x,_{1}x)_{2}

e(x) -> e(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 5

↳Dependency Graph

→DP Problem 3

↳Remaining

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))

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

**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))

Duration:

0:00 minutes