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: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: if_reach_2#_A(x1,x2,x3,x4,x5) = ((1,1),(1,1)) x2 + x4 + x5 + (9,5) false_A() = (9,4) edge_A(x1,x2,x3) = ((1,1),(1,0)) x1 + ((1,1),(1,1)) x2 + x3 + (3,2) reach#_A(x1,x2,x3,x4) = ((1,1),(1,1)) x1 + x3 + x4 + (10,5) union_A(x1,x2) = x1 + x2 + (0,1) empty_A() = (1,1) if_reach_1#_A(x1,x2,x3,x4,x5) = ((1,1),(1,1)) x2 + x4 + x5 + (10,5) eq_A(x1,x2) = x2 + (4,3) true_A() = (13,2) |0|_A() = (14,1) s_A(x1) = x1 + (5,3) precedence: reach# = if_reach_1# > empty > eq = true = s > false > |0| > union > if_reach_2# = edge partial status: pi(if_reach_2#) = [4] pi(false) = [] pi(edge) = [2, 3] pi(reach#) = [1] pi(union) = [1, 2] pi(empty) = [] pi(if_reach_1#) = [2] pi(eq) = [2] pi(true) = [] pi(|0|) = [] pi(s) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: if_reach_2#_A(x1,x2,x3,x4,x5) = ((0,0),(0,1)) x4 + (2,1) false_A() = (4,1) edge_A(x1,x2,x3) = ((0,0),(1,1)) x2 + ((0,0),(0,1)) x3 + (6,2) reach#_A(x1,x2,x3,x4) = (0,0) union_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,4) empty_A() = (1,3) if_reach_1#_A(x1,x2,x3,x4,x5) = (0,0) eq_A(x1,x2) = (5,1) true_A() = (5,1) |0|_A() = (6,1) s_A(x1) = (6,1) precedence: empty > false > eq = true = |0| = s > union > edge > if_reach_2# > reach# = if_reach_1# partial status: pi(if_reach_2#) = [] pi(false) = [] pi(edge) = [] pi(reach#) = [] pi(union) = [] pi(empty) = [] pi(if_reach_1#) = [] pi(eq) = [] pi(true) = [] pi(|0|) = [] pi(s) = [] The next rules are strictly ordered: p1, p4, p5 We remove them from the problem. -- 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: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: reach#_A(x1,x2,x3,x4) = max{x1 + 11, x2 + 11, x3 + 5, x4 + 4} edge_A(x1,x2,x3) = max{x1 + 6, x2, x3} if_reach_1#_A(x1,x2,x3,x4,x5) = max{x1 + 1, x2 + 11, x3 + 11, x4 + 5, x5 + 4} eq_A(x1,x2) = max{2, x1 - 14, x2 - 12} false_A = 10 |0|_A = 23 true_A = 8 s_A(x1) = max{25, x1 + 11} precedence: reach# = edge = if_reach_1# = eq = false = |0| = true = s partial status: pi(reach#) = [1, 2, 3, 4] pi(edge) = [1, 2, 3] pi(if_reach_1#) = [2, 3, 4, 5] pi(eq) = [] pi(false) = [] pi(|0|) = [] pi(true) = [] pi(s) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: reach#_A(x1,x2,x3,x4) = max{x1 + 10, x2 + 6, x3 - 2, x4 + 6} edge_A(x1,x2,x3) = max{12, x1 + 1, x2 + 1, x3 + 6} if_reach_1#_A(x1,x2,x3,x4,x5) = max{5, x4 - 9, x5 + 1} eq_A(x1,x2) = 11 false_A = 12 |0|_A = 0 true_A = 12 s_A(x1) = x1 + 13 precedence: reach# = if_reach_1# = eq = false = |0| = true = s > edge partial status: pi(reach#) = [] pi(edge) = [] pi(if_reach_1#) = [5] pi(eq) = [] pi(false) = [] pi(|0|) = [] pi(true) = [] pi(s) = [1] The next rules are strictly ordered: p2 We remove them from the problem. -- 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) 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: (no SCCs) -- 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: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: eq#_A(x1,x2) = max{2, x1 - 1, x2 + 1} s_A(x1) = max{1, x1} precedence: eq# = s partial status: pi(eq#) = [2] pi(s) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: eq#_A(x1,x2) = 0 s_A(x1) = max{2, x1} precedence: eq# = s partial status: pi(eq#) = [] pi(s) = [1] The next rules are strictly ordered: p1 We remove them from the problem. 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: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: union#_A(x1,x2) = max{x1 + 1, x2} edge_A(x1,x2,x3) = x3 precedence: union# = edge partial status: pi(union#) = [1, 2] pi(edge) = [3] 2. weighted path order base order: max/plus interpretations on natural numbers: union#_A(x1,x2) = max{x1 - 1, x2 + 1} edge_A(x1,x2,x3) = x3 precedence: union# = edge partial status: pi(union#) = [] pi(edge) = [3] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.