YES We show the termination of the TRS R: 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 union(empty(),h) -> h union(edge(x,y,i),h) -> edge(x,y,union(i,h)) reach(x,y,empty(),h) -> false() reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h) if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h) if_reach_2(true(),x,y,edge(u,v,i),h) -> true() if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: eq#(s(x),s(y)) -> eq#(x,y) p2: union#(edge(x,y,i),h) -> union#(i,h) p3: reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) p4: reach#(x,y,edge(u,v,i),h) -> eq#(x,u) p5: if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) p6: if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq#(y,v) p7: if_reach_2#(false(),x,y,edge(u,v,i),h) -> or#(reach(x,y,i,h),reach(v,y,union(i,h),empty())) p8: if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) p9: if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) p10: if_reach_2#(false(),x,y,edge(u,v,i),h) -> union#(i,h) p11: if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(x)) -> false() r3: eq(s(x),|0|()) -> false() r4: eq(s(x),s(y)) -> eq(x,y) r5: or(true(),y) -> true() r6: or(false(),y) -> y r7: union(empty(),h) -> h r8: union(edge(x,y,i),h) -> edge(x,y,union(i,h)) r9: reach(x,y,empty(),h) -> false() r10: reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h) r11: if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h) r12: if_reach_2(true(),x,y,edge(u,v,i),h) -> true() r13: if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) r14: if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)) The estimated dependency graph contains the following SCCs: {p3, p5, p8, p9, p11} {p1} {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) p2: reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) p3: if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) p4: if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) p5: if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(x)) -> false() r3: eq(s(x),|0|()) -> false() r4: eq(s(x),s(y)) -> eq(x,y) r5: or(true(),y) -> true() r6: or(false(),y) -> y r7: union(empty(),h) -> h r8: union(edge(x,y,i),h) -> edge(x,y,union(i,h)) r9: reach(x,y,empty(),h) -> false() r10: reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h) r11: if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h) r12: if_reach_2(true(),x,y,edge(u,v,i),h) -> true() r13: if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) r14: if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)) The set of usable rules consists of r1, r2, r3, r4, r7, r8 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: if_reach_2#_A(x1,x2,x3,x4,x5) = max{44, x1 - 71} false_A = 46 edge_A(x1,x2,x3) = 32 reach#_A(x1,x2,x3,x4) = 44 union_A(x1,x2) = max{125, x1 + 11, x2 + 11} empty_A = 30 if_reach_1#_A(x1,x2,x3,x4,x5) = max{44, x4 + 11} eq_A(x1,x2) = 82 true_A = 44 |0|_A = 2 s_A(x1) = x1 + 4 if_reach_2#!_A(x1,x2,x3,x4,x5) = max{50, x1 - 32, x4 - 33} false!_A = 53 edge!_A(x1,x2,x3) = 40 reach#!_A(x1,x2,x3,x4) = 50 union!_A(x1,x2) = max{55, x1 - 1, x2 + 41} empty!_A = 54 if_reach_1#!_A(x1,x2,x3,x4,x5) = max{50, x1 - 32, x4 + 9} eq!_A(x1,x2) = 77 true!_A = 51 |0|!_A = 52 s!_A(x1) = x1 + 54 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: if_reach_2#_A(x1,x2,x3,x4,x5) = 0 false_A() = 2 edge_A(x1,x2,x3) = x1 + x2 + x3 + 12 reach#_A(x1,x2,x3,x4) = 0 union_A(x1,x2) = x1 + x2 + 1 empty_A() = 3 if_reach_1#_A(x1,x2,x3,x4,x5) = 0 eq_A(x1,x2) = x1 + x2 + 2 true_A() = 8 |0|_A() = 3 s_A(x1) = x1 + 1 if_reach_2#!_A(x1,x2,x3,x4,x5) = x4 + x5 false!_A() = 6 edge!_A(x1,x2,x3) = 0 reach#!_A(x1,x2,x3,x4) = x3 + x4 + 1 union!_A(x1,x2) = 1 empty!_A() = 7 if_reach_1#!_A(x1,x2,x3,x4,x5) = x4 + x5 + 1 eq!_A(x1,x2) = 10 true!_A() = 11 |0|!_A() = 12 s!_A(x1) = 7 partial status: pi(if_reach_2#) = [4] pi(false) = [] pi(edge) = [] pi(reach#) = [] pi(union) = [1, 2] pi(empty) = [] pi(if_reach_1#) = [] pi(eq) = [] pi(true) = [] pi(|0|) = [] pi(s) = [1] The following rules are removed: p1, p4, p5 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) p2: if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(x)) -> false() r3: eq(s(x),|0|()) -> false() r4: eq(s(x),s(y)) -> eq(x,y) r5: or(true(),y) -> true() r6: or(false(),y) -> y r7: union(empty(),h) -> h r8: union(edge(x,y,i),h) -> edge(x,y,union(i,h)) r9: reach(x,y,empty(),h) -> false() r10: reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h) r11: if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h) r12: if_reach_2(true(),x,y,edge(u,v,i),h) -> true() r13: if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) r14: if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) p2: if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(x)) -> false() r3: eq(s(x),|0|()) -> false() r4: eq(s(x),s(y)) -> eq(x,y) r5: or(true(),y) -> true() r6: or(false(),y) -> y r7: union(empty(),h) -> h r8: union(edge(x,y,i),h) -> edge(x,y,union(i,h)) r9: reach(x,y,empty(),h) -> false() r10: reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h) r11: if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h) r12: if_reach_2(true(),x,y,edge(u,v,i),h) -> true() r13: if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) r14: if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)) The set of usable rules consists of r1, r2, r3, r4 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: reach#_A(x1,x2,x3,x4) = 1 edge_A(x1,x2,x3) = max{x1 + 12, x2 - 2} if_reach_1#_A(x1,x2,x3,x4,x5) = max{1, x1 - 5} eq_A(x1,x2) = 6 false_A = 4 |0|_A = 0 true_A = 4 s_A(x1) = x1 reach#!_A(x1,x2,x3,x4) = max{8, x3 - 12, x4} edge!_A(x1,x2,x3) = max{43, x1 + 28, x2 + 12, x3 + 11} if_reach_1#!_A(x1,x2,x3,x4,x5) = max{7, x1 + 1, x5 - 1} eq!_A(x1,x2) = 47 false!_A = 9 |0|!_A = 50 true!_A = 49 s!_A(x1) = max{48, x1 + 8} 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: reach#_A(x1,x2,x3,x4) = 0 edge_A(x1,x2,x3) = x1 + x2 if_reach_1#_A(x1,x2,x3,x4,x5) = 0 eq_A(x1,x2) = x1 + x2 + 1 false_A() = 3 |0|_A() = 1 true_A() = 3 s_A(x1) = x1 + 3 reach#!_A(x1,x2,x3,x4) = x3 + x4 + 4 edge!_A(x1,x2,x3) = x1 + x2 + x3 + 7 if_reach_1#!_A(x1,x2,x3,x4,x5) = x1 + 2 eq!_A(x1,x2) = x2 + 3 false!_A() = 5 |0|!_A() = 6 true!_A() = 0 s!_A(x1) = x1 + 4 partial status: pi(reach#) = [3] pi(edge) = [3] pi(if_reach_1#) = [4] pi(eq) = [1, 2] pi(false) = [] pi(|0|) = [] pi(true) = [] pi(s) = [1] The following rules are removed: p1, p2 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: eq#(s(x),s(y)) -> eq#(x,y) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(x)) -> false() r3: eq(s(x),|0|()) -> false() r4: eq(s(x),s(y)) -> eq(x,y) r5: or(true(),y) -> true() r6: or(false(),y) -> y r7: union(empty(),h) -> h r8: union(edge(x,y,i),h) -> edge(x,y,union(i,h)) r9: reach(x,y,empty(),h) -> false() r10: reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h) r11: if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h) r12: if_reach_2(true(),x,y,edge(u,v,i),h) -> true() r13: if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) r14: if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)) The set of usable rules consists of (no rules) Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: eq#_A(x1,x2) = 0 s_A(x1) = max{0, x1 - 61} eq#!_A(x1,x2) = 24 s!_A(x1) = 23 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: eq#_A(x1,x2) = x1 + x2 s_A(x1) = x1 + 1 eq#!_A(x1,x2) = x2 + 5 s!_A(x1) = 6 partial status: pi(eq#) = [1] pi(s) = [1] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: union#(edge(x,y,i),h) -> union#(i,h) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(x)) -> false() r3: eq(s(x),|0|()) -> false() r4: eq(s(x),s(y)) -> eq(x,y) r5: or(true(),y) -> true() r6: or(false(),y) -> y r7: union(empty(),h) -> h r8: union(edge(x,y,i),h) -> edge(x,y,union(i,h)) r9: reach(x,y,empty(),h) -> false() r10: reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h) r11: if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h) r12: if_reach_2(true(),x,y,edge(u,v,i),h) -> true() r13: if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) r14: if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)) The set of usable rules consists of (no rules) Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: union#_A(x1,x2) = 0 edge_A(x1,x2,x3) = max{x1 + 8, x2 - 7, x3 - 7} union#!_A(x1,x2) = x2 + 52 edge!_A(x1,x2,x3) = max{x1 + 46, x3 + 50} 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: union#_A(x1,x2) = x1 edge_A(x1,x2,x3) = x1 + x2 + x3 + 6 union#!_A(x1,x2) = x1 + 9 edge!_A(x1,x2,x3) = x3 + 8 partial status: pi(union#) = [] pi(edge) = [] The following rules are removed: p1 Then no dependency pair remains.