Consider the TRS R consisting of the rewrite rules

1: eq(0,0) -> true
2: eq(0,s(x)) -> false
3: eq(s(x),0) -> false
4: eq(s(x),s(y)) -> eq(x,y)
5: or(true,y) -> true
6: or(false,y) -> y
7: union(empty,h) -> h
8: union(edge(x,y,i),h) -> edge(x,y,union(i,h))
9: reach(x,y,empty,h) -> false
10: reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
11: if_reach_1(true,x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
12: if_reach_2(true,x,y,edge(u,v,i),h) -> true
13: if_reach_2(false,x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty))
14: if_reach_1(false,x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))

There are 11 dependency pairs:

15: EQ(s(x),s(y)) -> EQ(x,y)
16: UNION(edge(x,y,i),h) -> UNION(i,h)
17: REACH(x,y,edge(u,v,i),h) -> IF_REACH_1(eq(x,u),x,y,edge(u,v,i),h)
18: REACH(x,y,edge(u,v,i),h) -> EQ(x,u)
19: IF_REACH_1(true,x,y,edge(u,v,i),h) -> IF_REACH_2(eq(y,v),x,y,edge(u,v,i),h)
20: IF_REACH_1(true,x,y,edge(u,v,i),h) -> EQ(y,v)
21: IF_REACH_2(false,x,y,edge(u,v,i),h) -> OR(reach(x,y,i,h),reach(v,y,union(i,h),empty))
22: IF_REACH_2(false,x,y,edge(u,v,i),h) -> REACH(x,y,i,h)
23: IF_REACH_2(false,x,y,edge(u,v,i),h) -> REACH(v,y,union(i,h),empty)
24: IF_REACH_2(false,x,y,edge(u,v,i),h) -> UNION(i,h)
25: IF_REACH_1(false,x,y,edge(u,v,i),h) -> REACH(x,y,i,edge(u,v,h))

The approximated dependency graph contains 3 SCCs:
{15},
{16}
and {17,19,22,23,25}.

- Consider the SCC {15}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [EQ](x,y) = x + y + 1,
rule 15
is strictly decreasing.

- Consider the SCC {16}.
There are no usable rules.
By taking the polynomial interpretation
[UNION](x,y) = x + y + 1
and [edge](x,y,z) = x + y + z + 1,
rule 16
is strictly decreasing.

- Consider the SCC {17,19,22,23,25}.
The usable rules are {1-4,7,8}.
By taking the polynomial interpretation
[0] = [empty] = [false] = [true] = 1,
[s](x) = x + 1,
[union](x,y) = x + y,
[eq](x,y) = x + y + 1,
[edge](x,y,z) = x + y + z + 1,
[REACH](x,y,z,w) = x + y + z + w + 1
and [IF_REACH_1](x,y,z,w,v) = [IF_REACH_2](x,y,z,w,v) = y + z + w + v + 1,
the rules in {8,17,19,23,25}
are weakly decreasing and
the rules in {1-4,7,22}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {17,19,23,25}.
By taking the polynomial interpretation
[empty] = 0,
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[union](x,y) = x + y,
[eq](x,y) = x + y + 1,
[edge](x,y,z) = x + y + z + 1,
[REACH](x,y,z,w) = x + y + z + w + 1
and [IF_REACH_1](x,y,z,w,v) = [IF_REACH_2](x,y,z,w,v) = y + z + w + v + 1,
the rules in {7,8,17,19,25}
are weakly decreasing and
the rules in {1-4,23}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {17,25}.
The usable rules are {1-4}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[eq](x,y) = x + y + 1,
[edge](x,y,z) = [REACH](x,y,z,w) = x + y + z + 1
and [IF_REACH_1](x,y,z,w,v) = y + z + w + 1,
rule 17
is weakly decreasing and
the rules in {1-4,25}
are strictly decreasing.



Hence the TRS is terminating.