MAYBE Termination w.r.t. Q proof of ../tpdb/TRS/SchneiderKamp/trs/wiehe12.trs
Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

G(s(x), s(y)) → AND(f(s(x)), f(s(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
G(s(x), s(y)) → M(x, y)
P(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
F(s(x)) → H(x)
MINUS(s(x), s(y)) → MINUS(x, y)
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
G(s(x), s(y)) → IF(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
G(s(x), s(y)) → K(n(s(x), s(y)), s(s(0)))
G(s(x), s(y)) → N(x, y)
NOT(x) → IF(x, false, true)
H(s(x)) → F(x)
P(s(x), x) → IF(gt(x, x), id(x), id(x))
P(s(x), s(y)) → ID(x)
P(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
P(s(x), x) → ID(x)
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
N(s(x), s(y)) → N(x, y)
GT(s(x), s(y)) → GT(x, y)
M(s(x), s(y)) → M(x, y)
G(s(x), s(y)) → K(minus(m(x, y), n(x, y)), s(s(0)))
G(s(x), s(y)) → F(s(x))
G(s(x), s(y)) → F(s(y))
P(s(x), s(y)) → ID(y)
T(x) → P(x, x)
P(s(x), s(y)) → IF(gt(x, y), x, y)
G(s(x), s(y)) → MINUS(m(x, y), n(x, y))
P(id(x), s(y)) → GT(s(y), y)
G(s(x), s(y)) → N(s(x), s(y))
P(s(x), s(y)) → NOT(gt(x, y))
P(s(x), s(y)) → GT(x, y)
K(s(x), s(y)) → K(minus(x, y), s(y))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
P(s(x), x) → GT(x, x)
G(s(x), s(y)) → T(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0)))))
K(s(x), s(y)) → MINUS(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

G(s(x), s(y)) → AND(f(s(x)), f(s(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
G(s(x), s(y)) → M(x, y)
P(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
F(s(x)) → H(x)
MINUS(s(x), s(y)) → MINUS(x, y)
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
G(s(x), s(y)) → IF(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
G(s(x), s(y)) → K(n(s(x), s(y)), s(s(0)))
G(s(x), s(y)) → N(x, y)
NOT(x) → IF(x, false, true)
H(s(x)) → F(x)
P(s(x), x) → IF(gt(x, x), id(x), id(x))
P(s(x), s(y)) → ID(x)
P(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
P(s(x), x) → ID(x)
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
N(s(x), s(y)) → N(x, y)
GT(s(x), s(y)) → GT(x, y)
M(s(x), s(y)) → M(x, y)
G(s(x), s(y)) → K(minus(m(x, y), n(x, y)), s(s(0)))
G(s(x), s(y)) → F(s(x))
G(s(x), s(y)) → F(s(y))
P(s(x), s(y)) → ID(y)
T(x) → P(x, x)
P(s(x), s(y)) → IF(gt(x, y), x, y)
G(s(x), s(y)) → MINUS(m(x, y), n(x, y))
P(id(x), s(y)) → GT(s(y), y)
G(s(x), s(y)) → N(s(x), s(y))
P(s(x), s(y)) → NOT(gt(x, y))
P(s(x), s(y)) → GT(x, y)
K(s(x), s(y)) → K(minus(x, y), s(y))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
P(s(x), x) → GT(x, x)
G(s(x), s(y)) → T(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0)))))
K(s(x), s(y)) → MINUS(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 8 SCCs with 25 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(x), s(y)) → GT(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(x), s(y)) → GT(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(s(x)) → F(x)
F(s(x)) → H(x)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(s(x)) → F(x)
F(s(x)) → H(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS(s(x), s(y)) → MINUS(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS(s(x), s(y)) → MINUS(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

K(s(x), s(y)) → K(minus(x, y), s(y))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


K(s(x), s(y)) → K(minus(x, y), s(y))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
K(x1, x2)  =  K(x1, x2)
s(x1)  =  s(x1)
minus(x1, x2)  =  minus(x1)
0  =  0

Recursive path order with status [2].
Quasi-Precedence:
[K2, s1] > minus1
0 > minus1

Status:
minus1: multiset
K2: multiset
0: multiset
s1: [1]


The following usable rules [17] were oriented:

minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


K(s(x), s(y)) → K(minus(x, y), s(y))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(K(x1, x2)) = x1   
POL(minus(x1, x2)) = x1   
POL(s(x1)) = 1 + x1   

The following usable rules [17] were oriented:

minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
            ↳ QDPOrderProof
              ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

M(s(x), s(y)) → M(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

M(s(x), s(y)) → M(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

N(s(x), s(y)) → N(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

N(s(x), s(y)) → N(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( k(x1, x2) ) =
/0\
\0/
+
/10\
\01/
·x1+
/00\
\00/
·x2

M( minus(x1, x2) ) =
/0\
\0/
+
/10\
\01/
·x1+
/00\
\00/
·x2

M( s(x1) ) =
/1\
\0/
+
/11\
\11/
·x1

M( 0 ) =
/0\
\0/

M( n(x1, x2) ) =
/0\
\0/
+
/10\
\01/
·x1+
/00\
\00/
·x2

M( m(x1, x2) ) =
/0\
\0/
+
/10\
\01/
·x1+
/10\
\01/
·x2

Tuple symbols:
M( G(x1, x2) ) = 0+
[1,1]
·x1+
[1,0]
·x2


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

minus(s(x), s(y)) → minus(x, y)
m(x, 0) → x
k(0, s(y)) → 0
minus(x, 0) → x
n(x, 0) → 0
m(0, y) → y
m(s(x), s(y)) → s(m(x, y))
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
n(s(x), s(y)) → s(n(x, y))
n(0, y) → 0



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.