Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

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

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

EQ(s(x), s(y)) → EQ(x, y)
SIZE(edge(x, y, i)) → SIZE(i)
LE(s(x), s(y)) → LE(x, y)
REACHABLE(x, y, i) → REACH(x, y, 0, i, i)
REACH(x, y, c, i, j) → IF1(eq(x, y), x, y, c, i, j)
REACH(x, y, c, i, j) → EQ(x, y)
IF1(false, x, y, c, i, j) → IF2(le(c, size(j)), x, y, c, i, j)
IF1(false, x, y, c, i, j) → LE(c, size(j))
IF1(false, x, y, c, i, j) → SIZE(j)
IF2(true, x, y, c, edge(u, v, i), j) → OR(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → AND(eq(x, u), reach(v, y, s(c), j, j))
IF2(true, x, y, c, edge(u, v, i), j) → EQ(x, u)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

(11) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

• LE(s(x), s(y)) → LE(x, y)
  The graph contains the following edges 1 > 1, 2 > 2

(13) TRUE

(14) Obligation:

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

SIZE(edge(x, y, i)) → SIZE(i)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

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

SIZE(edge(x, y, i)) → SIZE(i)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

(18) Obligation:

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

SIZE(edge(x, y, i)) → SIZE(i)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

• SIZE(edge(x, y, i)) → SIZE(i)
  The graph contains the following edges 1 > 1

(20) TRUE

(21) Obligation:

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

EQ(s(x), s(y)) → EQ(x, y)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(22) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

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

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(24) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

(25) Obligation:

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

EQ(s(x), s(y)) → EQ(x, y)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

• EQ(s(x), s(y)) → EQ(x, y)
  The graph contains the following edges 1 > 1, 2 > 2

(27) TRUE

(28) Obligation:

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

REACH(x, y, c, i, j) → IF1(eq(x, y), x, y, c, i, j)
IF1(false, x, y, c, i, j) → IF2(le(c, size(j)), x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) Obligation:

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

REACH(x, y, c, i, j) → IF1(eq(x, y), x, y, c, i, j)
IF1(false, x, y, c, i, j) → IF2(le(c, size(j)), x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

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

(31) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

or(true, x0)
or(false, x0)
and(true, x0)
and(false, x0)
reachable(x0, x1, x2)
reach(x0, x1, x2, x3, x4)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, empty, x3)
if2(true, x0, x1, x2, edge(x3, x4, x5), x6)

(32) Obligation:

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

REACH(x, y, c, i, j) → IF1(eq(x, y), x, y, c, i, j)
IF1(false, x, y, c, i, j) → IF2(le(c, size(j)), x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(33) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule REACH(x, y, c, i, j) → IF1(eq(x, y), x, y, c, i, j) we obtained the following new rules [LPAR04]:

REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)

(34) Obligation:

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

IF1(false, x, y, c, i, j) → IF2(le(c, size(j)), x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)
REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(35) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule REACH(x, y, c, i, j) → IF1(eq(x, y), x, y, c, i, j) we obtained the following new rules [LPAR04]:

REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)

(36) Obligation:

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

IF1(false, x, y, c, i, j) → IF2(le(c, size(j)), x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)
REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(37) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF1(false, x, y, c, i, j) → IF2(le(c, size(j)), x, y, c, i, j) we obtained the following new rules [LPAR04]:

IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3)

(38) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)
REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)
IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(39) NonInfProof (EQUIVALENT transformation)

The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j) the following chains were created:

• We consider the chain IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j), IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j) which results in the following constraint:
  

  (1)    (IF2(true, x0, x1, x2, x5, x6)=IF2(true, x7, x8, x9, edge(x10, x11, x12), x13) ⇒ IF2(true, x0, x1, x2, edge(x3, x4, x5), x6)≥IF2(true, x0, x1, x2, x5, x6))

  
  
  We simplified constraint (1) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (2)    (IF2(true, x0, x1, x2, edge(x3, x4, edge(x10, x11, x12)), x6)≥IF2(true, x0, x1, x2, edge(x10, x11, x12), x6))

  
  
  
• We consider the chain IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j), IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j) which results in the following constraint:
  

  (3)    (IF2(true, x14, x15, x16, x19, x20)=IF2(true, x21, x22, x23, edge(x24, x25, x26), x27) ⇒ IF2(true, x14, x15, x16, edge(x17, x18, x19), x20)≥IF2(true, x14, x15, x16, x19, x20))

  
  
  We simplified constraint (3) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (4)    (IF2(true, x14, x15, x16, edge(x17, x18, edge(x24, x25, x26)), x20)≥IF2(true, x14, x15, x16, edge(x24, x25, x26), x20))

  
  
  

For Pair IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j) the following chains were created:

• We consider the chain IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j), REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6) which results in the following constraint:
  

  (5)    (REACH(x60, x57, s(x58), x62, x62)=REACH(x63, x64, s(x65), x66, x66) ⇒ IF2(true, x56, x57, x58, edge(x59, x60, x61), x62)≥REACH(x60, x57, s(x58), x62, x62))

  
  
  We simplified constraint (5) using rules (I), (II), (IV) which results in the following new constraint:
  

  (6)    (IF2(true, x56, x57, x58, edge(x59, x60, x61), x62)≥REACH(x60, x57, s(x58), x62, x62))

  
  
  

For Pair REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6) the following chains were created:

• We consider the chain REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6), IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3) which results in the following constraint:
  

  (7)    (IF1(eq(x86, x87), x86, x87, s(x88), x89, x89)=IF1(false, x90, x91, s(x92), x93, x93) ⇒ REACH(x86, x87, s(x88), x89, x89)≥IF1(eq(x86, x87), x86, x87, s(x88), x89, x89))

  
  
  We simplified constraint (7) using rules (I), (II), (IV) which results in the following new constraint:
  

  (8)    (eq(x86, x87)=false ⇒ REACH(x86, x87, s(x88), x89, x89)≥IF1(eq(x86, x87), x86, x87, s(x88), x89, x89))

  
  
  We simplified constraint (8) using rule (V) (with possible (I) afterwards) using induction on eq(x86, x87)=false which results in the following new constraints:
  

  (9)    (false=false ⇒ REACH(0, s(x124), s(x88), x89, x89)≥IF1(eq(0, s(x124)), 0, s(x124), s(x88), x89, x89))

  
  

  (10)    (false=false ⇒ REACH(s(x125), 0, s(x88), x89, x89)≥IF1(eq(s(x125), 0), s(x125), 0, s(x88), x89, x89))

  
  

  (11)    (eq(x127, x126)=false∧(∀x128,x129:eq(x127, x126)=false ⇒ REACH(x127, x126, s(x128), x129, x129)≥IF1(eq(x127, x126), x127, x126, s(x128), x129, x129)) ⇒ REACH(s(x127), s(x126), s(x88), x89, x89)≥IF1(eq(s(x127), s(x126)), s(x127), s(x126), s(x88), x89, x89))

  
  
  We simplified constraint (9) using rules (I), (II) which results in the following new constraint:
  

  (12)    (REACH(0, s(x124), s(x88), x89, x89)≥IF1(eq(0, s(x124)), 0, s(x124), s(x88), x89, x89))

  
  
  We simplified constraint (10) using rules (I), (II) which results in the following new constraint:
  

  (13)    (REACH(s(x125), 0, s(x88), x89, x89)≥IF1(eq(s(x125), 0), s(x125), 0, s(x88), x89, x89))

  
  
  We simplified constraint (11) using rule (VI) where we applied the induction hypothesis (∀x128,x129:eq(x127, x126)=false ⇒ REACH(x127, x126, s(x128), x129, x129)≥IF1(eq(x127, x126), x127, x126, s(x128), x129, x129)) with σ = [x129 / x89, x128 / x88] which results in the following new constraint:
  

  (14)    (REACH(x127, x126, s(x88), x89, x89)≥IF1(eq(x127, x126), x127, x126, s(x88), x89, x89) ⇒ REACH(s(x127), s(x126), s(x88), x89, x89)≥IF1(eq(s(x127), s(x126)), s(x127), s(x126), s(x88), x89, x89))

  
  
  

For Pair IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3) the following chains were created:

• We consider the chain IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3), IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j) which results in the following constraint:
  

  (15)    (IF2(le(s(x96), size(x97)), x94, x95, s(x96), x97, x97)=IF2(true, x98, x99, x100, edge(x101, x102, x103), x104) ⇒ IF1(false, x94, x95, s(x96), x97, x97)≥IF2(le(s(x96), size(x97)), x94, x95, s(x96), x97, x97))

  
  
  We simplified constraint (15) using rules (I), (II), (III), (IV), (VII) which results in the following new constraint:
  

  (16)    (s(x96)=x130∧edge(x101, x102, x103)=x132∧size(x132)=x131∧le(x130, x131)=true ⇒ IF1(false, x94, x95, s(x96), edge(x101, x102, x103), edge(x101, x102, x103))≥IF2(le(s(x96), size(edge(x101, x102, x103))), x94, x95, s(x96), edge(x101, x102, x103), edge(x101, x102, x103)))

  
  
  We simplified constraint (16) using rule (V) (with possible (I) afterwards) using induction on le(x130, x131)=true which results in the following new constraints:
  

  (17)    (true=true∧s(x96)=0∧edge(x101, x102, x103)=x132∧size(x132)=x133 ⇒ IF1(false, x94, x95, s(x96), edge(x101, x102, x103), edge(x101, x102, x103))≥IF2(le(s(x96), size(edge(x101, x102, x103))), x94, x95, s(x96), edge(x101, x102, x103), edge(x101, x102, x103)))

  
  

  (18)    (le(x136, x135)=true∧s(x96)=s(x136)∧edge(x101, x102, x103)=x132∧size(x132)=s(x135)∧(∀x137,x138,x139,x140,x141,x142,x143:le(x136, x135)=true∧s(x137)=x136∧edge(x138, x139, x140)=x141∧size(x141)=x135 ⇒ IF1(false, x142, x143, s(x137), edge(x138, x139, x140), edge(x138, x139, x140))≥IF2(le(s(x137), size(edge(x138, x139, x140))), x142, x143, s(x137), edge(x138, x139, x140), edge(x138, x139, x140))) ⇒ IF1(false, x94, x95, s(x96), edge(x101, x102, x103), edge(x101, x102, x103))≥IF2(le(s(x96), size(edge(x101, x102, x103))), x94, x95, s(x96), edge(x101, x102, x103), edge(x101, x102, x103)))

  
  
  We solved constraint (17) using rules (I), (II).We simplified constraint (18) using rules (I), (II), (III) which results in the following new constraint:
  

  (19)    (le(x136, x135)=true∧edge(x101, x102, x103)=x132∧size(x132)=s(x135)∧(∀x137,x138,x139,x140,x141,x142,x143:le(x136, x135)=true∧s(x137)=x136∧edge(x138, x139, x140)=x141∧size(x141)=x135 ⇒ IF1(false, x142, x143, s(x137), edge(x138, x139, x140), edge(x138, x139, x140))≥IF2(le(s(x137), size(edge(x138, x139, x140))), x142, x143, s(x137), edge(x138, x139, x140), edge(x138, x139, x140))) ⇒ IF1(false, x94, x95, s(x136), edge(x101, x102, x103), edge(x101, x102, x103))≥IF2(le(s(x136), size(edge(x101, x102, x103))), x94, x95, s(x136), edge(x101, x102, x103), edge(x101, x102, x103)))

  
  
  We simplified constraint (19) using rule (V) (with possible (I) afterwards) using induction on size(x132)=s(x135) which results in the following new constraint:
  

  (20)    (s(size(x144))=s(x135)∧le(x136, x135)=true∧edge(x101, x102, x103)=edge(x146, x145, x144)∧(∀x137,x138,x139,x140,x141,x142,x143:le(x136, x135)=true∧s(x137)=x136∧edge(x138, x139, x140)=x141∧size(x141)=x135 ⇒ IF1(false, x142, x143, s(x137), edge(x138, x139, x140), edge(x138, x139, x140))≥IF2(le(s(x137), size(edge(x138, x139, x140))), x142, x143, s(x137), edge(x138, x139, x140), edge(x138, x139, x140)))∧(∀x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160:size(x144)=s(x147)∧le(x148, x147)=true∧edge(x149, x150, x151)=x144∧(∀x152,x153,x154,x155,x156,x157,x158:le(x148, x147)=true∧s(x152)=x148∧edge(x153, x154, x155)=x156∧size(x156)=x147 ⇒ IF1(false, x157, x158, s(x152), edge(x153, x154, x155), edge(x153, x154, x155))≥IF2(le(s(x152), size(edge(x153, x154, x155))), x157, x158, s(x152), edge(x153, x154, x155), edge(x153, x154, x155))) ⇒ IF1(false, x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151))≥IF2(le(s(x148), size(edge(x149, x150, x151))), x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151))) ⇒ IF1(false, x94, x95, s(x136), edge(x101, x102, x103), edge(x101, x102, x103))≥IF2(le(s(x136), size(edge(x101, x102, x103))), x94, x95, s(x136), edge(x101, x102, x103), edge(x101, x102, x103)))

  
  
  We simplified constraint (20) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (21)    (size(x144)=x135∧le(x136, x135)=true∧(∀x147,x148,x149,x150,x151,x159,x160:size(x144)=s(x147)∧le(x148, x147)=true∧edge(x149, x150, x151)=x144 ⇒ IF1(false, x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151))≥IF2(le(s(x148), size(edge(x149, x150, x151))), x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151))) ⇒ IF1(false, x94, x95, s(x136), edge(x101, x102, x144), edge(x101, x102, x144))≥IF2(le(s(x136), size(edge(x101, x102, x144))), x94, x95, s(x136), edge(x101, x102, x144), edge(x101, x102, x144)))

  
  
  We simplified constraint (21) using rule (V) (with possible (I) afterwards) using induction on le(x136, x135)=true which results in the following new constraints:
  

  (22)    (true=true∧size(x144)=x161∧(∀x147,x148,x149,x150,x151,x159,x160:size(x144)=s(x147)∧le(x148, x147)=true∧edge(x149, x150, x151)=x144 ⇒ IF1(false, x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151))≥IF2(le(s(x148), size(edge(x149, x150, x151))), x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151))) ⇒ IF1(false, x94, x95, s(0), edge(x101, x102, x144), edge(x101, x102, x144))≥IF2(le(s(0), size(edge(x101, x102, x144))), x94, x95, s(0), edge(x101, x102, x144), edge(x101, x102, x144)))

  
  

  (23)    (le(x164, x163)=true∧size(x144)=s(x163)∧(∀x147,x148,x149,x150,x151,x159,x160:size(x144)=s(x147)∧le(x148, x147)=true∧edge(x149, x150, x151)=x144 ⇒ IF1(false, x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151))≥IF2(le(s(x148), size(edge(x149, x150, x151))), x159, x160, s(x148), edge(x149, x150, x151), edge(x149, x150, x151)))∧(∀x165,x166,x167,x168,x169,x170,x171,x172,x173,x174,x175,x176:le(x164, x163)=true∧size(x165)=x163∧(∀x166,x167,x168,x169,x170,x171,x172:size(x165)=s(x166)∧le(x167, x166)=true∧edge(x168, x169, x170)=x165 ⇒ IF1(false, x171, x172, s(x167), edge(x168, x169, x170), edge(x168, x169, x170))≥IF2(le(s(x167), size(edge(x168, x169, x170))), x171, x172, s(x167), edge(x168, x169, x170), edge(x168, x169, x170))) ⇒ IF1(false, x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))≥IF2(le(s(x164), size(edge(x175, x176, x165))), x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))) ⇒ IF1(false, x94, x95, s(s(x164)), edge(x101, x102, x144), edge(x101, x102, x144))≥IF2(le(s(s(x164)), size(edge(x101, x102, x144))), x94, x95, s(s(x164)), edge(x101, x102, x144), edge(x101, x102, x144)))

  
  
  We simplified constraint (22) using rules (I), (II), (IV) which results in the following new constraint:
  

  (24)    (IF1(false, x94, x95, s(0), edge(x101, x102, x144), edge(x101, x102, x144))≥IF2(le(s(0), size(edge(x101, x102, x144))), x94, x95, s(0), edge(x101, x102, x144), edge(x101, x102, x144)))

  
  
  We simplified constraint (23) using rule (IV) which results in the following new constraint:
  

  (25)    (le(x164, x163)=true∧size(x144)=s(x163)∧(∀x165,x173,x174,x175,x176:le(x164, x163)=true∧size(x165)=x163 ⇒ IF1(false, x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))≥IF2(le(s(x164), size(edge(x175, x176, x165))), x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))) ⇒ IF1(false, x94, x95, s(s(x164)), edge(x101, x102, x144), edge(x101, x102, x144))≥IF2(le(s(s(x164)), size(edge(x101, x102, x144))), x94, x95, s(s(x164)), edge(x101, x102, x144), edge(x101, x102, x144)))

  
  
  We simplified constraint (25) using rule (V) (with possible (I) afterwards) using induction on size(x144)=s(x163) which results in the following new constraint:
  

  (26)    (s(size(x177))=s(x163)∧le(x164, x163)=true∧(∀x165,x173,x174,x175,x176:le(x164, x163)=true∧size(x165)=x163 ⇒ IF1(false, x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))≥IF2(le(s(x164), size(edge(x175, x176, x165))), x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165)))∧(∀x180,x181,x182,x183,x184,x185,x186,x187,x188,x189,x190:size(x177)=s(x180)∧le(x181, x180)=true∧(∀x182,x183,x184,x185,x186:le(x181, x180)=true∧size(x182)=x180 ⇒ IF1(false, x183, x184, s(x181), edge(x185, x186, x182), edge(x185, x186, x182))≥IF2(le(s(x181), size(edge(x185, x186, x182))), x183, x184, s(x181), edge(x185, x186, x182), edge(x185, x186, x182))) ⇒ IF1(false, x187, x188, s(s(x181)), edge(x189, x190, x177), edge(x189, x190, x177))≥IF2(le(s(s(x181)), size(edge(x189, x190, x177))), x187, x188, s(s(x181)), edge(x189, x190, x177), edge(x189, x190, x177))) ⇒ IF1(false, x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177)))≥IF2(le(s(s(x164)), size(edge(x101, x102, edge(x179, x178, x177)))), x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177))))

  
  
  We simplified constraint (26) using rules (I), (II) which results in the following new constraint:
  

  (27)    (size(x177)=x163∧le(x164, x163)=true∧(∀x165,x173,x174,x175,x176:le(x164, x163)=true∧size(x165)=x163 ⇒ IF1(false, x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))≥IF2(le(s(x164), size(edge(x175, x176, x165))), x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165)))∧(∀x180,x181,x182,x183,x184,x185,x186,x187,x188,x189,x190:size(x177)=s(x180)∧le(x181, x180)=true∧(∀x182,x183,x184,x185,x186:le(x181, x180)=true∧size(x182)=x180 ⇒ IF1(false, x183, x184, s(x181), edge(x185, x186, x182), edge(x185, x186, x182))≥IF2(le(s(x181), size(edge(x185, x186, x182))), x183, x184, s(x181), edge(x185, x186, x182), edge(x185, x186, x182))) ⇒ IF1(false, x187, x188, s(s(x181)), edge(x189, x190, x177), edge(x189, x190, x177))≥IF2(le(s(s(x181)), size(edge(x189, x190, x177))), x187, x188, s(s(x181)), edge(x189, x190, x177), edge(x189, x190, x177))) ⇒ IF1(false, x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177)))≥IF2(le(s(s(x164)), size(edge(x101, x102, edge(x179, x178, x177)))), x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177))))

  
  
  We simplified constraint (27) using rule (VI) where we applied the induction hypothesis (∀x165,x173,x174,x175,x176:le(x164, x163)=true∧size(x165)=x163 ⇒ IF1(false, x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))≥IF2(le(s(x164), size(edge(x175, x176, x165))), x173, x174, s(x164), edge(x175, x176, x165), edge(x175, x176, x165))) with σ = [x165 / x177, x173 / x94, x176 / x102, x174 / x95, x175 / x101] which results in the following new constraint:
  

  (28)    (IF1(false, x94, x95, s(x164), edge(x101, x102, x177), edge(x101, x102, x177))≥IF2(le(s(x164), size(edge(x101, x102, x177))), x94, x95, s(x164), edge(x101, x102, x177), edge(x101, x102, x177))∧(∀x180,x181,x182,x183,x184,x185,x186,x187,x188,x189,x190:size(x177)=s(x180)∧le(x181, x180)=true∧(∀x182,x183,x184,x185,x186:le(x181, x180)=true∧size(x182)=x180 ⇒ IF1(false, x183, x184, s(x181), edge(x185, x186, x182), edge(x185, x186, x182))≥IF2(le(s(x181), size(edge(x185, x186, x182))), x183, x184, s(x181), edge(x185, x186, x182), edge(x185, x186, x182))) ⇒ IF1(false, x187, x188, s(s(x181)), edge(x189, x190, x177), edge(x189, x190, x177))≥IF2(le(s(s(x181)), size(edge(x189, x190, x177))), x187, x188, s(s(x181)), edge(x189, x190, x177), edge(x189, x190, x177))) ⇒ IF1(false, x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177)))≥IF2(le(s(s(x164)), size(edge(x101, x102, edge(x179, x178, x177)))), x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177))))

  
  
  We simplified constraint (28) using rule (IV) which results in the following new constraint:
  

  (29)    (IF1(false, x94, x95, s(x164), edge(x101, x102, x177), edge(x101, x102, x177))≥IF2(le(s(x164), size(edge(x101, x102, x177))), x94, x95, s(x164), edge(x101, x102, x177), edge(x101, x102, x177)) ⇒ IF1(false, x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177)))≥IF2(le(s(s(x164)), size(edge(x101, x102, edge(x179, x178, x177)))), x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177))))

  
  
  
• We consider the chain IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3), IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j) which results in the following constraint:
  

  (30)    (IF2(le(s(x107), size(x108)), x105, x106, s(x107), x108, x108)=IF2(true, x109, x110, x111, edge(x112, x113, x114), x115) ⇒ IF1(false, x105, x106, s(x107), x108, x108)≥IF2(le(s(x107), size(x108)), x105, x106, s(x107), x108, x108))

  
  
  We simplified constraint (30) using rules (I), (II), (III), (IV), (VII) which results in the following new constraint:
  

  (31)    (s(x107)=x191∧edge(x112, x113, x114)=x193∧size(x193)=x192∧le(x191, x192)=true ⇒ IF1(false, x105, x106, s(x107), edge(x112, x113, x114), edge(x112, x113, x114))≥IF2(le(s(x107), size(edge(x112, x113, x114))), x105, x106, s(x107), edge(x112, x113, x114), edge(x112, x113, x114)))

  
  
  We simplified constraint (31) using rule (V) (with possible (I) afterwards) using induction on le(x191, x192)=true which results in the following new constraints:
  

  (32)    (true=true∧s(x107)=0∧edge(x112, x113, x114)=x193∧size(x193)=x194 ⇒ IF1(false, x105, x106, s(x107), edge(x112, x113, x114), edge(x112, x113, x114))≥IF2(le(s(x107), size(edge(x112, x113, x114))), x105, x106, s(x107), edge(x112, x113, x114), edge(x112, x113, x114)))

  
  

  (33)    (le(x197, x196)=true∧s(x107)=s(x197)∧edge(x112, x113, x114)=x193∧size(x193)=s(x196)∧(∀x198,x199,x200,x201,x202,x203,x204:le(x197, x196)=true∧s(x198)=x197∧edge(x199, x200, x201)=x202∧size(x202)=x196 ⇒ IF1(false, x203, x204, s(x198), edge(x199, x200, x201), edge(x199, x200, x201))≥IF2(le(s(x198), size(edge(x199, x200, x201))), x203, x204, s(x198), edge(x199, x200, x201), edge(x199, x200, x201))) ⇒ IF1(false, x105, x106, s(x107), edge(x112, x113, x114), edge(x112, x113, x114))≥IF2(le(s(x107), size(edge(x112, x113, x114))), x105, x106, s(x107), edge(x112, x113, x114), edge(x112, x113, x114)))

  
  
  We solved constraint (32) using rules (I), (II).We simplified constraint (33) using rules (I), (II), (III) which results in the following new constraint:
  

  (34)    (le(x197, x196)=true∧edge(x112, x113, x114)=x193∧size(x193)=s(x196)∧(∀x198,x199,x200,x201,x202,x203,x204:le(x197, x196)=true∧s(x198)=x197∧edge(x199, x200, x201)=x202∧size(x202)=x196 ⇒ IF1(false, x203, x204, s(x198), edge(x199, x200, x201), edge(x199, x200, x201))≥IF2(le(s(x198), size(edge(x199, x200, x201))), x203, x204, s(x198), edge(x199, x200, x201), edge(x199, x200, x201))) ⇒ IF1(false, x105, x106, s(x197), edge(x112, x113, x114), edge(x112, x113, x114))≥IF2(le(s(x197), size(edge(x112, x113, x114))), x105, x106, s(x197), edge(x112, x113, x114), edge(x112, x113, x114)))

  
  
  We simplified constraint (34) using rule (V) (with possible (I) afterwards) using induction on size(x193)=s(x196) which results in the following new constraint:
  

  (35)    (s(size(x205))=s(x196)∧le(x197, x196)=true∧edge(x112, x113, x114)=edge(x207, x206, x205)∧(∀x198,x199,x200,x201,x202,x203,x204:le(x197, x196)=true∧s(x198)=x197∧edge(x199, x200, x201)=x202∧size(x202)=x196 ⇒ IF1(false, x203, x204, s(x198), edge(x199, x200, x201), edge(x199, x200, x201))≥IF2(le(s(x198), size(edge(x199, x200, x201))), x203, x204, s(x198), edge(x199, x200, x201), edge(x199, x200, x201)))∧(∀x208,x209,x210,x211,x212,x213,x214,x215,x216,x217,x218,x219,x220,x221:size(x205)=s(x208)∧le(x209, x208)=true∧edge(x210, x211, x212)=x205∧(∀x213,x214,x215,x216,x217,x218,x219:le(x209, x208)=true∧s(x213)=x209∧edge(x214, x215, x216)=x217∧size(x217)=x208 ⇒ IF1(false, x218, x219, s(x213), edge(x214, x215, x216), edge(x214, x215, x216))≥IF2(le(s(x213), size(edge(x214, x215, x216))), x218, x219, s(x213), edge(x214, x215, x216), edge(x214, x215, x216))) ⇒ IF1(false, x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212))≥IF2(le(s(x209), size(edge(x210, x211, x212))), x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212))) ⇒ IF1(false, x105, x106, s(x197), edge(x112, x113, x114), edge(x112, x113, x114))≥IF2(le(s(x197), size(edge(x112, x113, x114))), x105, x106, s(x197), edge(x112, x113, x114), edge(x112, x113, x114)))

  
  
  We simplified constraint (35) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (36)    (size(x205)=x196∧le(x197, x196)=true∧(∀x208,x209,x210,x211,x212,x220,x221:size(x205)=s(x208)∧le(x209, x208)=true∧edge(x210, x211, x212)=x205 ⇒ IF1(false, x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212))≥IF2(le(s(x209), size(edge(x210, x211, x212))), x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212))) ⇒ IF1(false, x105, x106, s(x197), edge(x112, x113, x205), edge(x112, x113, x205))≥IF2(le(s(x197), size(edge(x112, x113, x205))), x105, x106, s(x197), edge(x112, x113, x205), edge(x112, x113, x205)))

  
  
  We simplified constraint (36) using rule (V) (with possible (I) afterwards) using induction on le(x197, x196)=true which results in the following new constraints:
  

  (37)    (true=true∧size(x205)=x222∧(∀x208,x209,x210,x211,x212,x220,x221:size(x205)=s(x208)∧le(x209, x208)=true∧edge(x210, x211, x212)=x205 ⇒ IF1(false, x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212))≥IF2(le(s(x209), size(edge(x210, x211, x212))), x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212))) ⇒ IF1(false, x105, x106, s(0), edge(x112, x113, x205), edge(x112, x113, x205))≥IF2(le(s(0), size(edge(x112, x113, x205))), x105, x106, s(0), edge(x112, x113, x205), edge(x112, x113, x205)))

  
  

  (38)    (le(x225, x224)=true∧size(x205)=s(x224)∧(∀x208,x209,x210,x211,x212,x220,x221:size(x205)=s(x208)∧le(x209, x208)=true∧edge(x210, x211, x212)=x205 ⇒ IF1(false, x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212))≥IF2(le(s(x209), size(edge(x210, x211, x212))), x220, x221, s(x209), edge(x210, x211, x212), edge(x210, x211, x212)))∧(∀x226,x227,x228,x229,x230,x231,x232,x233,x234,x235,x236,x237:le(x225, x224)=true∧size(x226)=x224∧(∀x227,x228,x229,x230,x231,x232,x233:size(x226)=s(x227)∧le(x228, x227)=true∧edge(x229, x230, x231)=x226 ⇒ IF1(false, x232, x233, s(x228), edge(x229, x230, x231), edge(x229, x230, x231))≥IF2(le(s(x228), size(edge(x229, x230, x231))), x232, x233, s(x228), edge(x229, x230, x231), edge(x229, x230, x231))) ⇒ IF1(false, x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))≥IF2(le(s(x225), size(edge(x236, x237, x226))), x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))) ⇒ IF1(false, x105, x106, s(s(x225)), edge(x112, x113, x205), edge(x112, x113, x205))≥IF2(le(s(s(x225)), size(edge(x112, x113, x205))), x105, x106, s(s(x225)), edge(x112, x113, x205), edge(x112, x113, x205)))

  
  
  We simplified constraint (37) using rules (I), (II), (IV) which results in the following new constraint:
  

  (39)    (IF1(false, x105, x106, s(0), edge(x112, x113, x205), edge(x112, x113, x205))≥IF2(le(s(0), size(edge(x112, x113, x205))), x105, x106, s(0), edge(x112, x113, x205), edge(x112, x113, x205)))

  
  
  We simplified constraint (38) using rule (IV) which results in the following new constraint:
  

  (40)    (le(x225, x224)=true∧size(x205)=s(x224)∧(∀x226,x234,x235,x236,x237:le(x225, x224)=true∧size(x226)=x224 ⇒ IF1(false, x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))≥IF2(le(s(x225), size(edge(x236, x237, x226))), x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))) ⇒ IF1(false, x105, x106, s(s(x225)), edge(x112, x113, x205), edge(x112, x113, x205))≥IF2(le(s(s(x225)), size(edge(x112, x113, x205))), x105, x106, s(s(x225)), edge(x112, x113, x205), edge(x112, x113, x205)))

  
  
  We simplified constraint (40) using rule (V) (with possible (I) afterwards) using induction on size(x205)=s(x224) which results in the following new constraint:
  

  (41)    (s(size(x238))=s(x224)∧le(x225, x224)=true∧(∀x226,x234,x235,x236,x237:le(x225, x224)=true∧size(x226)=x224 ⇒ IF1(false, x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))≥IF2(le(s(x225), size(edge(x236, x237, x226))), x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226)))∧(∀x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251:size(x238)=s(x241)∧le(x242, x241)=true∧(∀x243,x244,x245,x246,x247:le(x242, x241)=true∧size(x243)=x241 ⇒ IF1(false, x244, x245, s(x242), edge(x246, x247, x243), edge(x246, x247, x243))≥IF2(le(s(x242), size(edge(x246, x247, x243))), x244, x245, s(x242), edge(x246, x247, x243), edge(x246, x247, x243))) ⇒ IF1(false, x248, x249, s(s(x242)), edge(x250, x251, x238), edge(x250, x251, x238))≥IF2(le(s(s(x242)), size(edge(x250, x251, x238))), x248, x249, s(s(x242)), edge(x250, x251, x238), edge(x250, x251, x238))) ⇒ IF1(false, x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238)))≥IF2(le(s(s(x225)), size(edge(x112, x113, edge(x240, x239, x238)))), x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238))))

  
  
  We simplified constraint (41) using rules (I), (II) which results in the following new constraint:
  

  (42)    (size(x238)=x224∧le(x225, x224)=true∧(∀x226,x234,x235,x236,x237:le(x225, x224)=true∧size(x226)=x224 ⇒ IF1(false, x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))≥IF2(le(s(x225), size(edge(x236, x237, x226))), x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226)))∧(∀x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251:size(x238)=s(x241)∧le(x242, x241)=true∧(∀x243,x244,x245,x246,x247:le(x242, x241)=true∧size(x243)=x241 ⇒ IF1(false, x244, x245, s(x242), edge(x246, x247, x243), edge(x246, x247, x243))≥IF2(le(s(x242), size(edge(x246, x247, x243))), x244, x245, s(x242), edge(x246, x247, x243), edge(x246, x247, x243))) ⇒ IF1(false, x248, x249, s(s(x242)), edge(x250, x251, x238), edge(x250, x251, x238))≥IF2(le(s(s(x242)), size(edge(x250, x251, x238))), x248, x249, s(s(x242)), edge(x250, x251, x238), edge(x250, x251, x238))) ⇒ IF1(false, x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238)))≥IF2(le(s(s(x225)), size(edge(x112, x113, edge(x240, x239, x238)))), x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238))))

  
  
  We simplified constraint (42) using rule (VI) where we applied the induction hypothesis (∀x226,x234,x235,x236,x237:le(x225, x224)=true∧size(x226)=x224 ⇒ IF1(false, x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))≥IF2(le(s(x225), size(edge(x236, x237, x226))), x234, x235, s(x225), edge(x236, x237, x226), edge(x236, x237, x226))) with σ = [x226 / x238, x234 / x105, x235 / x106, x236 / x112, x237 / x113] which results in the following new constraint:
  

  (43)    (IF1(false, x105, x106, s(x225), edge(x112, x113, x238), edge(x112, x113, x238))≥IF2(le(s(x225), size(edge(x112, x113, x238))), x105, x106, s(x225), edge(x112, x113, x238), edge(x112, x113, x238))∧(∀x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251:size(x238)=s(x241)∧le(x242, x241)=true∧(∀x243,x244,x245,x246,x247:le(x242, x241)=true∧size(x243)=x241 ⇒ IF1(false, x244, x245, s(x242), edge(x246, x247, x243), edge(x246, x247, x243))≥IF2(le(s(x242), size(edge(x246, x247, x243))), x244, x245, s(x242), edge(x246, x247, x243), edge(x246, x247, x243))) ⇒ IF1(false, x248, x249, s(s(x242)), edge(x250, x251, x238), edge(x250, x251, x238))≥IF2(le(s(s(x242)), size(edge(x250, x251, x238))), x248, x249, s(s(x242)), edge(x250, x251, x238), edge(x250, x251, x238))) ⇒ IF1(false, x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238)))≥IF2(le(s(s(x225)), size(edge(x112, x113, edge(x240, x239, x238)))), x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238))))

  
  
  We simplified constraint (43) using rule (IV) which results in the following new constraint:
  

  (44)    (IF1(false, x105, x106, s(x225), edge(x112, x113, x238), edge(x112, x113, x238))≥IF2(le(s(x225), size(edge(x112, x113, x238))), x105, x106, s(x225), edge(x112, x113, x238), edge(x112, x113, x238)) ⇒ IF1(false, x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238)))≥IF2(le(s(s(x225)), size(edge(x112, x113, edge(x240, x239, x238)))), x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238))))

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
  
  • (IF2(true, x0, x1, x2, edge(x3, x4, edge(x10, x11, x12)), x6)≥IF2(true, x0, x1, x2, edge(x10, x11, x12), x6))
    
  • (IF2(true, x14, x15, x16, edge(x17, x18, edge(x24, x25, x26)), x20)≥IF2(true, x14, x15, x16, edge(x24, x25, x26), x20))
    
  
  
• IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)
  
  • (IF2(true, x56, x57, x58, edge(x59, x60, x61), x62)≥REACH(x60, x57, s(x58), x62, x62))
    
  
  
• REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)
  
  • (REACH(0, s(x124), s(x88), x89, x89)≥IF1(eq(0, s(x124)), 0, s(x124), s(x88), x89, x89))
    
  • (REACH(s(x125), 0, s(x88), x89, x89)≥IF1(eq(s(x125), 0), s(x125), 0, s(x88), x89, x89))
    
  • (REACH(x127, x126, s(x88), x89, x89)≥IF1(eq(x127, x126), x127, x126, s(x88), x89, x89) ⇒ REACH(s(x127), s(x126), s(x88), x89, x89)≥IF1(eq(s(x127), s(x126)), s(x127), s(x126), s(x88), x89, x89))
    
  
  
• IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3)
  
  • (IF1(false, x94, x95, s(0), edge(x101, x102, x144), edge(x101, x102, x144))≥IF2(le(s(0), size(edge(x101, x102, x144))), x94, x95, s(0), edge(x101, x102, x144), edge(x101, x102, x144)))
    
  • (IF1(false, x94, x95, s(x164), edge(x101, x102, x177), edge(x101, x102, x177))≥IF2(le(s(x164), size(edge(x101, x102, x177))), x94, x95, s(x164), edge(x101, x102, x177), edge(x101, x102, x177)) ⇒ IF1(false, x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177)))≥IF2(le(s(s(x164)), size(edge(x101, x102, edge(x179, x178, x177)))), x94, x95, s(s(x164)), edge(x101, x102, edge(x179, x178, x177)), edge(x101, x102, edge(x179, x178, x177))))
    
  • (IF1(false, x105, x106, s(0), edge(x112, x113, x205), edge(x112, x113, x205))≥IF2(le(s(0), size(edge(x112, x113, x205))), x105, x106, s(0), edge(x112, x113, x205), edge(x112, x113, x205)))
    
  • (IF1(false, x105, x106, s(x225), edge(x112, x113, x238), edge(x112, x113, x238))≥IF2(le(s(x225), size(edge(x112, x113, x238))), x105, x106, s(x225), edge(x112, x113, x238), edge(x112, x113, x238)) ⇒ IF1(false, x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238)))≥IF2(le(s(s(x225)), size(edge(x112, x113, edge(x240, x239, x238)))), x105, x106, s(s(x225)), edge(x112, x113, edge(x240, x239, x238)), edge(x112, x113, edge(x240, x239, x238))))
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(IF1(x₁, x₂, x₃, x₄, x₅, x₆)) = -1 - x₁ + x₃ - x₄ + x₆   
POL(IF2(x₁, x₂, x₃, x₄, x₅, x₆)) = -1 + x₃ - x₄ + x₆   
POL(REACH(x₁, x₂, x₃, x₄, x₅)) = -1 + x₂ - x₃ + x₄   
POL(c) = -2   
POL(edge(x₁, x₂, x₃)) = 1 + x₃   
POL(empty) = 0   
POL(eq(x₁, x₂)) = 0   
POL(false) = 0   
POL(le(x₁, x₂)) = x₂   
POL(s(x₁)) = 1 + x₁   
POL(size(x₁)) = 1   
POL(true) = 1   

The following pairs are in P_>:

IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)

The following pairs are in P_bound:

IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3)

The following rules are usable:

false → eq(0, s(x))
true → eq(0, 0)
eq(x, y) → eq(s(x), s(y))
false → eq(s(x), 0)

(40) Complex Obligation (AND)

(41) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)
IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(42) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(43) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(44) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(45) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(46) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

(47) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)

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

(48) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

• IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 5, 6 >= 6

(49) TRUE

(50) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
IF2(true, x, y, c, edge(u, v, i), j) → REACH(v, y, s(c), j, j)
REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(51) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(52) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)

The TRS R consists of the following rules:

size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(53) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(54) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(55) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
size(empty)
size(edge(x0, x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

(56) Obligation:

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

IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)

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

(57) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

• IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 5, 6 >= 6

(58) TRUE