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 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!): 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() = 4 edge_A(x1,x2,x3) = x1 + x3 + 7 reach#_A(x1,x2,x3,x4) = 0 union_A(x1,x2) = x1 + x2 + 1 empty_A() = 1 if_reach_1#_A(x1,x2,x3,x4,x5) = 0 eq_A(x1,x2) = x1 + x2 + 1 true_A() = 6 if_reach_2#!_A(x1,x2,x3,x4,x5) = x4 + x5 + 2 false!_A() = 12 edge!_A(x1,x2,x3) = 11 reach#!_A(x1,x2,x3,x4) = x3 + x4 + 6 union!_A(x1,x2) = 8 empty!_A() = 13 if_reach_1#!_A(x1,x2,x3,x4,x5) = x4 + x5 + 6 eq!_A(x1,x2) = 14 true!_A() = 10 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: if_reach_2#_A(x1,x2,x3,x4,x5) = max{x2 + 1, x3 + 11, x4 - 1, x5 - 1} false_A = 38 edge_A(x1,x2,x3) = max{x1 + 2, x2 + 10, x3} reach#_A(x1,x2,x3,x4) = max{x1 + 1, x2 + 11, x3 - 1, x4 - 1} union_A(x1,x2) = max{12, x1, x2} empty_A = 0 if_reach_1#_A(x1,x2,x3,x4,x5) = max{x2 + 1, x3 + 11, x4 - 1, x5 - 1} eq_A(x1,x2) = x2 + 35 true_A = 36 if_reach_2#!_A(x1,x2,x3,x4,x5) = max{x2 + 41, x3 + 42, x4 + 38} false!_A = 22 edge!_A(x1,x2,x3) = max{28, x2 + 26} reach#!_A(x1,x2,x3,x4) = max{x1 + 34, x2 + 29, x3 + 29} union!_A(x1,x2) = 0 empty!_A = 23 if_reach_1#!_A(x1,x2,x3,x4,x5) = max{39, x2 + 34, x3 + 29, x4 + 29} eq!_A(x1,x2) = max{73, x1 + 34, x2 + 2} true!_A = 27 partial status: pi(if_reach_2#) = [] pi(false) = [] pi(edge) = [] pi(reach#) = [] pi(union) = [1, 2] pi(empty) = [] pi(if_reach_1#) = [] pi(eq) = [1, 2] pi(true) = [] 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!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: reach#_A(x1,x2,x3,x4) = x3 + x4 edge_A(x1,x2,x3) = x1 + x3 + 8 if_reach_1#_A(x1,x2,x3,x4,x5) = x4 + x5 eq_A(x1,x2) = 10 false_A() = 10 |0|_A() = 1 true_A() = 10 s_A(x1) = x1 reach#!_A(x1,x2,x3,x4) = x3 + 17 edge!_A(x1,x2,x3) = 19 if_reach_1#!_A(x1,x2,x3,x4,x5) = x1 + x4 eq!_A(x1,x2) = x2 + 24 false!_A() = 0 |0|!_A() = 22 true!_A() = 21 s!_A(x1) = x1 + 25 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: reach#_A(x1,x2,x3,x4) = max{0, x1 - 8, x2 - 8, x3 - 40, x4 - 40} edge_A(x1,x2,x3) = max{x1 + 38, x2 - 52, x3} if_reach_1#_A(x1,x2,x3,x4,x5) = max{0, x1 - 36, x2 - 8, x3 - 8, x4 - 40, x5 - 40} eq_A(x1,x2) = max{35, x1 - 77, x2 - 77} false_A = 2 |0|_A = 0 true_A = 3 s_A(x1) = x1 + 76 reach#!_A(x1,x2,x3,x4) = max{x1 - 77, x2 + 1} edge!_A(x1,x2,x3) = 0 if_reach_1#!_A(x1,x2,x3,x4,x5) = max{x1, x2 + 2, x3 + 2, x4 + 24} eq!_A(x1,x2) = max{23, x1 - 1, x2 - 34} false!_A = 41 |0|!_A = 42 true!_A = 24 s!_A(x1) = max{42, x1 - 35} partial status: pi(reach#) = [] pi(edge) = [] pi(if_reach_1#) = [] pi(eq) = [] pi(false) = [] pi(|0|) = [] pi(true) = [] pi(s) = [] 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!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: eq#_A(x1,x2) = x1 + x2 s_A(x1) = x1 + 2 eq#!_A(x1,x2) = x1 s!_A(x1) = 4 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: eq#_A(x1,x2) = 0 s_A(x1) = max{0, x1 - 5} eq#!_A(x1,x2) = max{0, x1 - 59} s!_A(x1) = max{6, x1 - 59} 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!): 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 + 1 union#!_A(x1,x2) = x1 + 7 edge!_A(x1,x2,x3) = x1 + x2 + x3 + 6 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: union#_A(x1,x2) = 0 edge_A(x1,x2,x3) = max{10, x1 - 56, x2 - 17, x3 - 71} union#!_A(x1,x2) = max{7, x1 - 11, x2 - 1} edge!_A(x1,x2,x3) = max{11, x1 + 8, x3 + 4} partial status: pi(union#) = [2] pi(edge) = [] The following rules are removed: p1 Then no dependency pair remains.