0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Instantiation (⇔)
↳34 QDP
↳35 Instantiation (⇔)
↳36 QDP
↳37 Instantiation (⇔)
↳38 QDP
↳39 NonInfProof (⇔)
↳40 QDP
↳41 DependencyGraphProof (⇔)
↳42 QDP
↳43 UsableRulesProof (⇔)
↳44 QDP
↳45 QReductionProof (⇔)
↳46 QDP
↳47 QDPSizeChangeProof (⇔)
↳48 TRUE
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)))
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)))
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)
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)
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)))
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)
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)
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)))
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)
LE(s(x), s(y)) → LE(x, y)
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)
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)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
SIZE(edge(x, y, i)) → SIZE(i)
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)))
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)
SIZE(edge(x, y, i)) → SIZE(i)
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)
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)
SIZE(edge(x, y, i)) → SIZE(i)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x), s(y)) → EQ(x, y)
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)))
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)
EQ(s(x), s(y)) → EQ(x, y)
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)
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)
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
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)
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)))
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)
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)
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)
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)
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)
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)
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)
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))
REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)
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)
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)
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))
REACH(z4, z1, s(z2), z6, z6) → IF1(eq(z4, z1), z4, z1, s(z2), z6, z6)
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)
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)
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))
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)
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)
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)
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))
(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))
(2) (IF2(true, x0, x1, x2, edge(x3, x4, edge(x10, x11, x12)), x6)≥IF2(true, x0, x1, x2, edge(x10, x11, x12), x6))
(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))
(4) (IF2(true, x14, x15, x16, edge(x17, x18, edge(x24, x25, x26)), x20)≥IF2(true, x14, x15, x16, edge(x24, x25, x26), x20))
(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))
(6) (IF2(true, x56, x57, x58, edge(x59, x60, x61), x62)≥REACH(x60, x57, s(x58), x62, x62))
(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))
(8) (eq(x86, x87)=false ⇒ REACH(x86, x87, s(x88), x89, x89)≥IF1(eq(x86, x87), x86, x87, s(x88), x89, x89))
(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))
(12) (REACH(0, s(x124), s(x88), x89, x89)≥IF1(eq(0, s(x124)), 0, s(x124), s(x88), x89, x89))
(13) (REACH(s(x125), 0, s(x88), x89, x89)≥IF1(eq(s(x125), 0), s(x125), 0, s(x88), x89, x89))
(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))
(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))
(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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(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))))
(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))))
(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))))
(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))))
(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))
(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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(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))))
(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))))
(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))))
(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))))
POL(0) = 0
POL(IF1(x1, x2, x3, x4, x5, x6)) = -x1 + x3 - x4 + x5
POL(IF2(x1, x2, x3, x4, x5, x6)) = -1 + x3 - x4 + x6
POL(REACH(x1, x2, x3, x4, x5)) = x2 - x3 + x4
POL(c) = -1
POL(edge(x1, x2, x3)) = 1 + x3
POL(empty) = 0
POL(eq(x1, x2)) = 0
POL(false) = 0
POL(le(x1, x2)) = x2
POL(s(x1)) = 1 + x1
POL(size(x1)) = x1
POL(true) = 1
The following pairs are in Pbound:
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:
IF1(false, z0, z1, s(z2), z3, z3) → IF2(le(s(z2), size(z3)), z0, z1, s(z2), z3, z3)
false → eq(0, s(x))
true → eq(0, 0)
eq(x, y) → eq(s(x), s(y))
false → eq(s(x), 0)
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)
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)
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))
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
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)
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))
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
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))
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))
IF2(true, x, y, c, edge(u, v, i), j) → IF2(true, x, y, c, i, j)
From the DPs we obtained the following set of size-change graphs: