D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
↳ QTRS
↳ DependencyPairsProof
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
D11(*2(x, y)) -> D11(x)
D11(minus1(x)) -> D11(x)
D11(*2(x, y)) -> D11(y)
D11(+2(x, y)) -> D11(x)
D11(+2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(x)
D11(ln1(x)) -> D11(x)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
D11(*2(x, y)) -> D11(x)
D11(minus1(x)) -> D11(x)
D11(*2(x, y)) -> D11(y)
D11(+2(x, y)) -> D11(x)
D11(+2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(x)
D11(ln1(x)) -> D11(x)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D11(*2(x, y)) -> D11(x)
D11(*2(x, y)) -> D11(y)
Used ordering: Polynomial interpretation [21]:
D11(minus1(x)) -> D11(x)
D11(+2(x, y)) -> D11(x)
D11(+2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(x)
D11(ln1(x)) -> D11(x)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
POL(*2(x1, x2)) = 1 + x1 + x2
POL(+2(x1, x2)) = x1 + x2
POL(-2(x1, x2)) = x1 + x2
POL(D11(x1)) = x1
POL(div2(x1, x2)) = x1 + x2
POL(ln1(x1)) = x1
POL(minus1(x1)) = x1
POL(pow2(x1, x2)) = x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D11(minus1(x)) -> D11(x)
D11(+2(x, y)) -> D11(x)
D11(+2(x, y)) -> D11(y)
D11(ln1(x)) -> D11(x)
D11(pow2(x, y)) -> D11(x)
D11(pow2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(y)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D11(minus1(x)) -> D11(x)
Used ordering: Polynomial interpretation [21]:
D11(+2(x, y)) -> D11(x)
D11(+2(x, y)) -> D11(y)
D11(ln1(x)) -> D11(x)
D11(pow2(x, y)) -> D11(x)
D11(pow2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(y)
POL(+2(x1, x2)) = x1 + x2
POL(-2(x1, x2)) = x1 + x2
POL(D11(x1)) = x1
POL(div2(x1, x2)) = x1 + x2
POL(ln1(x1)) = x1
POL(minus1(x1)) = 1 + x1
POL(pow2(x1, x2)) = x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D11(+2(x, y)) -> D11(x)
D11(+2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(x)
D11(ln1(x)) -> D11(x)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D11(+2(x, y)) -> D11(x)
D11(+2(x, y)) -> D11(y)
Used ordering: Polynomial interpretation [21]:
D11(pow2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(x)
D11(ln1(x)) -> D11(x)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
POL(+2(x1, x2)) = 1 + x1 + x2
POL(-2(x1, x2)) = x1 + x2
POL(D11(x1)) = x1
POL(div2(x1, x2)) = x1 + x2
POL(ln1(x1)) = x1
POL(pow2(x1, x2)) = x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D11(ln1(x)) -> D11(x)
D11(pow2(x, y)) -> D11(x)
D11(pow2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(y)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D11(ln1(x)) -> D11(x)
Used ordering: Polynomial interpretation [21]:
D11(pow2(x, y)) -> D11(x)
D11(pow2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(y)
POL(-2(x1, x2)) = x1 + x2
POL(D11(x1)) = x1
POL(div2(x1, x2)) = x1 + x2
POL(ln1(x1)) = 1 + x1
POL(pow2(x1, x2)) = x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D11(pow2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D11(pow2(x, y)) -> D11(y)
D11(pow2(x, y)) -> D11(x)
Used ordering: Polynomial interpretation [21]:
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
POL(-2(x1, x2)) = x1 + x2
POL(D11(x1)) = x1
POL(div2(x1, x2)) = x1 + x2
POL(pow2(x1, x2)) = 1 + x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D11(div2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
D11(div2(x, y)) -> D11(y)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D11(div2(x, y)) -> D11(x)
D11(div2(x, y)) -> D11(y)
Used ordering: Polynomial interpretation [21]:
D11(-2(x, y)) -> D11(x)
D11(-2(x, y)) -> D11(y)
POL(-2(x1, x2)) = x1 + x2
POL(D11(x1)) = x1
POL(div2(x1, x2)) = 1 + x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D11(-2(x, y)) -> D11(y)
D11(-2(x, y)) -> D11(x)
POL(-2(x1, x2)) = 1 + x1 + x2
POL(D11(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
D1(t) -> 1
D1(constant) -> 0
D1(+2(x, y)) -> +2(D1(x), D1(y))
D1(*2(x, y)) -> +2(*2(y, D1(x)), *2(x, D1(y)))
D1(-2(x, y)) -> -2(D1(x), D1(y))
D1(minus1(x)) -> minus1(D1(x))
D1(div2(x, y)) -> -2(div2(D1(x), y), div2(*2(x, D1(y)), pow2(y, 2)))
D1(ln1(x)) -> div2(D1(x), x)
D1(pow2(x, y)) -> +2(*2(*2(y, pow2(x, -2(y, 1))), D1(x)), *2(*2(pow2(x, y), ln1(x)), D1(y)))