f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
↳ QTRS
↳ DependencyPairsProof
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
F(true, x, y) → PLUS(s(0), x)
DOUBLE(s(x)) → DOUBLE(x)
GT(s(u), s(v)) → GT(u, v)
F(true, x, y) → GT(y, s(s(0)))
F(true, x, y) → GT(x, y)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y) → DOUBLE(y)
F(true, x, y) → AND(gt(x, y), gt(y, s(s(0))))
F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(true, x, y) → PLUS(s(0), x)
DOUBLE(s(x)) → DOUBLE(x)
GT(s(u), s(v)) → GT(u, v)
F(true, x, y) → GT(y, s(s(0)))
F(true, x, y) → GT(x, y)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y) → DOUBLE(y)
F(true, x, y) → AND(gt(x, y), gt(y, s(s(0))))
F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
DOUBLE(s(x)) → DOUBLE(x)
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DOUBLE(s(x)) → DOUBLE(x)
The value of delta used in the strict ordering is 4.
POL(DOUBLE(x1)) = (4)x_1
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
PLUS(n, s(m)) → PLUS(n, m)
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(n, s(m)) → PLUS(n, m)
The value of delta used in the strict ordering is 4.
POL(PLUS(x1, x2)) = (4)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
GT(s(u), s(v)) → GT(u, v)
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GT(s(u), s(v)) → GT(u, v)
The value of delta used in the strict ordering is 12.
POL(s(x1)) = 4 + (2)x_1
POL(GT(x1, x2)) = (3)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))