Term Rewriting System R:
[x, y, h, i, u, v]
app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, x)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(or, true), y) -> true
app(app(or, false), y) -> y
app(app(union, empty), h) -> h
app(app(union, app(app(app(edge, x), y), i)), h) -> app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) -> false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(ifreach2, true), x), y), app(app(app(edge, u), v), i)), h) -> true
app(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))

Termination of R to be shown. 



   R
     ↳Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost. 


   R
     ↳OC
       →TRS2
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

APP(app(eq, app(s, x)), app(s, y)) -> APP(app(eq, x), y)
APP(app(eq, app(s, x)), app(s, y)) -> APP(eq, x)
APP(app(union, app(app(app(edge, x), y), i)), h) -> APP(app(app(edge, x), y), app(app(union, i), h))
APP(app(union, app(app(app(edge, x), y), i)), h) -> APP(app(union, i), h)
APP(app(union, app(app(app(edge, x), y), i)), h) -> APP(union, i)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i))
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(ifreach1, app(app(eq, x), u)), x), y)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(app(ifreach1, app(app(eq, x), u)), x)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(ifreach1, app(app(eq, x), u))
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(app(eq, x), u)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(eq, x)
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i))
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(ifreach2, app(app(eq, y), v)), x), y)
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(ifreach2, app(app(eq, y), v)), x)
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(ifreach2, app(app(eq, y), v))
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(eq, y), v)
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(eq, y)
APP(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
APP(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(reach, x), y), i)
APP(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(reach, x), y)
APP(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(reach, x)
APP(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(edge, u), v), h)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(or, app(app(app(app(reach, x), y), i), h))
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, x), y), i), h)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(reach, x), y), i)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(reach, x), y)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(reach, x)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, v), y), app(app(union, i), h)), empty)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(reach, v), y), app(app(union, i), h))
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(reach, v), y)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(reach, v)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(union, i), h)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(union, i)

Furthermore, R contains three SCCs. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Usable Rules (Innermost)
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules


Dependency Pair:

APP(app(eq, app(s, x)), app(s, y)) -> APP(app(eq, x), y)


Rules:


app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, x)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(or, true), y) -> true
app(app(or, false), y) -> y
app(app(union, empty), h) -> h
app(app(union, app(app(app(edge, x), y), i)), h) -> app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) -> false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(ifreach2, true), x), y), app(app(app(edge, u), v), i)), h) -> true
app(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))


Strategy:

innermost




As we are in the innermost case, we can delete all 14 non-usable-rules.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
             ...
               →DP Problem 4
                 ↳A-Transformation
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules


Dependency Pair:

APP(app(eq, app(s, x)), app(s, y)) -> APP(app(eq, x), y)


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
             ...
               →DP Problem 5
                 ↳Size-Change Principle
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules


Dependency Pair:

EQ(s(x), s(y)) -> EQ(x, y)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. EQ(s(x), s(y)) -> EQ(x, y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳Usable Rules (Innermost)
           →DP Problem 3
             ↳UsableRules


Dependency Pair:

APP(app(union, app(app(app(edge, x), y), i)), h) -> APP(app(union, i), h)


Rules:


app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, x)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(or, true), y) -> true
app(app(or, false), y) -> y
app(app(union, empty), h) -> h
app(app(union, app(app(app(edge, x), y), i)), h) -> app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) -> false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(ifreach2, true), x), y), app(app(app(edge, u), v), i)), h) -> true
app(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))


Strategy:

innermost




As we are in the innermost case, we can delete all 14 non-usable-rules.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
             ...
               →DP Problem 6
                 ↳A-Transformation
           →DP Problem 3
             ↳UsableRules


Dependency Pair:

APP(app(union, app(app(app(edge, x), y), i)), h) -> APP(app(union, i), h)


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
             ...
               →DP Problem 7
                 ↳Size-Change Principle
           →DP Problem 3
             ↳UsableRules


Dependency Pair:

UNION(edge(x, y, i), h) -> UNION(i, h)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. UNION(edge(x, y, i), h) -> UNION(i, h)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
edge(x1, x2, x3) -> edge(x1, x2, x3)

We obtain no new DP problems. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳Usable Rules (Innermost)


Dependency Pairs:

APP(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, v), y), app(app(union, i), h)), empty)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, x), y), i), h)
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)


Rules:


app(app(eq, 0), 0) -> true
app(app(eq, 0), app(s, x)) -> false
app(app(eq, app(s, x)), 0) -> false
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)
app(app(or, true), y) -> true
app(app(or, false), y) -> y
app(app(union, empty), h) -> h
app(app(union, app(app(app(edge, x), y), i)), h) -> app(app(app(edge, x), y), app(app(union, i), h))
app(app(app(app(reach, x), y), empty), h) -> false
app(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
app(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
app(app(app(app(app(ifreach2, true), x), y), app(app(app(edge, u), v), i)), h) -> true
app(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> app(app(or, app(app(app(app(reach, x), y), i), h)), app(app(app(app(reach, v), y), app(app(union, i), h)), empty))


Strategy:

innermost




As we are in the innermost case, we can delete all 8 non-usable-rules.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules
             ...
               →DP Problem 8
                 ↳A-Transformation


Dependency Pairs:

APP(app(app(app(app(ifreach1, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, x), y), i), app(app(app(edge, u), v), h))
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, v), y), app(app(union, i), h)), empty)
APP(app(app(app(app(ifreach2, false), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(reach, x), y), i), h)
APP(app(app(app(app(ifreach1, true), x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(app(ifreach2, app(app(eq, y), v)), x), y), app(app(app(edge, u), v), i)), h)
APP(app(app(app(reach, x), y), app(app(app(edge, u), v), i)), h) -> APP(app(app(app(app(ifreach1, app(app(eq, x), u)), x), y), app(app(app(edge, u), v), i)), h)


Rules:


app(app(union, empty), h) -> h
app(app(union, app(app(app(edge, x), y), i)), h) -> app(app(app(edge, x), y), app(app(union, i), h))
app(app(eq, app(s, x)), 0) -> false
app(app(eq, 0), app(s, x)) -> false
app(app(eq, 0), 0) -> true
app(app(eq, app(s, x)), app(s, y)) -> app(app(eq, x), y)


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules
             ...
               →DP Problem 9
                 ↳Negative Polynomial Order


Dependency Pairs:

IFREACH1(false, x, y, edge(u, v, i), h) -> REACH(x, y, i, edge(u, v, h))
IFREACH2(false, x, y, edge(u, v, i), h) -> REACH(v, y, union(i, h), empty)
IFREACH2(false, x, y, edge(u, v, i), h) -> REACH(x, y, i, h)
IFREACH1(true, x, y, edge(u, v, i), h) -> IFREACH2(eq(y, v), x, y, edge(u, v, i), h)
REACH(x, y, edge(u, v, i), h) -> IFREACH1(eq(x, u), x, y, edge(u, v, i), h)


Rules:


union(empty, h) -> h
union(edge(x, y, i), h) -> edge(x, y, union(i, h))
eq(s(x), 0) -> false
eq(0, s(x)) -> false
eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)


Strategy:

innermost




The following Dependency Pairs can be strictly oriented using the given order.

IFREACH2(false, x, y, edge(u, v, i), h) -> REACH(v, y, union(i, h), empty)
IFREACH2(false, x, y, edge(u, v, i), h) -> REACH(x, y, i, h)


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

union(empty, h) -> h
union(edge(x, y, i), h) -> edge(x, y, union(i, h))
eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)
eq(s(x), 0) -> false
eq(0, s(x)) -> false


Used ordering:
Polynomial Order with Interpretation:

POL( IFREACH2(x1, ..., x5) ) = x4 + x5

POL( edge(x1, ..., x3) ) = x3 + 1

POL( REACH(x1, ..., x4) ) = x3 + x4

POL( union(x1, x2) ) = x1 + x2

POL( empty ) = 0

POL( IFREACH1(x1, ..., x5) ) = x4 + x5

POL( eq(x1, x2) ) = 0

POL( true ) = 0

POL( false ) = 0


This results in one new DP problem. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules
             ...
               →DP Problem 10
                 ↳Dependency Graph


Dependency Pairs:

IFREACH1(false, x, y, edge(u, v, i), h) -> REACH(x, y, i, edge(u, v, h))
IFREACH1(true, x, y, edge(u, v, i), h) -> IFREACH2(eq(y, v), x, y, edge(u, v, i), h)
REACH(x, y, edge(u, v, i), h) -> IFREACH1(eq(x, u), x, y, edge(u, v, i), h)


Rules:


union(empty, h) -> h
union(edge(x, y, i), h) -> edge(x, y, union(i, h))
eq(s(x), 0) -> false
eq(0, s(x)) -> false
eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)


Strategy:

innermost




Using the Dependency Graph the DP problem was split into 1 DP problems.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules
             ...
               →DP Problem 11
                 ↳Usable Rules (Innermost)


Dependency Pairs:

REACH(x, y, edge(u, v, i), h) -> IFREACH1(eq(x, u), x, y, edge(u, v, i), h)
IFREACH1(false, x, y, edge(u, v, i), h) -> REACH(x, y, i, edge(u, v, h))


Rules:


union(empty, h) -> h
union(edge(x, y, i), h) -> edge(x, y, union(i, h))
eq(s(x), 0) -> false
eq(0, s(x)) -> false
eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)


Strategy:

innermost




As we are in the innermost case, we can delete all 2 non-usable-rules.


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
           →DP Problem 3
             ↳UsableRules
             ...
               →DP Problem 12
                 ↳Size-Change Principle


Dependency Pairs:

REACH(x, y, edge(u, v, i), h) -> IFREACH1(eq(x, u), x, y, edge(u, v, i), h)
IFREACH1(false, x, y, edge(u, v, i), h) -> REACH(x, y, i, edge(u, v, h))


Rules:


eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)
eq(s(x), 0) -> false
eq(0, s(x)) -> false


Strategy:

innermost




We number the DPs as follows:
  1. REACH(x, y, edge(u, v, i), h) -> IFREACH1(eq(x, u), x, y, edge(u, v, i), h)
  2. IFREACH1(false, x, y, edge(u, v, i), h) -> REACH(x, y, i, edge(u, v, h))
and get the following Size-Change Graph(s):
{1} , {1}
1=2
2=3
3=4
4=5
{2} , {2}
2=1
3=2
4>3

which lead(s) to this/these maximal multigraph(s):
{2} , {1}
2=2
3=3
4>4
{1} , {2}
1=1
2=2
3>3

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
edge(x1, x2, x3) -> edge(x1, x2, x3)

We obtain no new DP problems.

Termination of R successfully shown.
Duration:
0:08 minutes