Term Rewriting System R:
[x, y, z]
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

Termination of R to be shown.

R
Dependency Pair Analysis

R contains the following Dependency Pairs:

F(x, g(y)) -> F(h(x), i(x, y))
F(x, g(y)) -> I(x, y)
I(x, j(y, z)) -> J(g(y), i(x, z))
I(x, j(y, z)) -> I(x, z)
I(h(x), j(j(y, z), 0)) -> J(i(h(x), j(y, z)), i(x, j(y, z)))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
J(g(x), g(y)) -> J(x, y)

Furthermore, R contains three SCCs.

R
DPs
→DP Problem 1
Polynomial Ordering
→DP Problem 2
Polo
→DP Problem 3
Remaining

Dependency Pair:

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

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(i(x1, x2)) =  1 POL(0) =  0 POL(g(x1)) =  1 + x1 POL(h(x1)) =  0 POL(j(x1, x2)) =  x2 POL(J(x1, x2)) =  x1 POL(f(x1, x2)) =  0

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 4
Dependency Graph
→DP Problem 2
Polo
→DP Problem 3
Remaining

Dependency Pair:

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polynomial Ordering
→DP Problem 3
Remaining

Dependency Pairs:

I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(x, j(y, z)) -> I(x, z)

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

The following dependency pair can be strictly oriented:

I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))

Additionally, the following rules can be oriented:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(I(x1, x2)) =  x1 POL(i(x1, x2)) =  0 POL(0) =  0 POL(g(x1)) =  0 POL(h(x1)) =  1 + x1 POL(j(x1, x2)) =  0 POL(f(x1, x2)) =  0

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 5
Polynomial Ordering
→DP Problem 3
Remaining

Dependency Pairs:

I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(x, j(y, z)) -> I(x, z)

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

The following dependency pair can be strictly oriented:

I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))

Additionally, the following rules can be oriented:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(I(x1, x2)) =  x1 + x2 POL(i(x1, x2)) =  0 POL(0) =  1 POL(g(x1)) =  0 POL(h(x1)) =  0 POL(j(x1, x2)) =  x1 + x2 POL(f(x1, x2)) =  1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Remaining Obligation(s)

The following remains to be proven:
• Dependency Pair:

I(x, j(y, z)) -> I(x, z)

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

• Dependency Pair:

F(x, g(y)) -> F(h(x), i(x, y))

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Remaining Obligation(s)

The following remains to be proven:
• Dependency Pair:

I(x, j(y, z)) -> I(x, z)

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

• Dependency Pair:

F(x, g(y)) -> F(h(x), i(x, y))

Rules:

f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

Termination of R could not be shown.
Duration:
0:00 minutes