YES We show the termination of the relative TRS R/S: R: le(|0|(),y) -> true() le(s(x),|0|()) -> false() le(s(x),s(y)) -> le(x,y) minus(|0|(),y) -> |0|() minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) if_minus(true(),s(x),y) -> |0|() if_minus(false(),s(x),y) -> s(minus(x,y)) gcd(|0|(),y) -> y gcd(s(x),|0|()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) S: rand(x) -> x rand(x) -> rand(s(x)) -- SCC decomposition. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: le#(s(x),s(y)) -> le#(x,y) p2: minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y) p3: minus#(s(x),y) -> le#(s(x),y) p4: if_minus#(false(),s(x),y) -> minus#(x,y) p5: gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) p6: gcd#(s(x),s(y)) -> le#(y,x) p7: if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) p8: if_gcd#(true(),s(x),s(y)) -> minus#(x,y) p9: if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) p10: if_gcd#(false(),s(x),s(y)) -> minus#(y,x) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The estimated dependency graph contains the following SCCs: {p5, p7, p9} {p2, p4} {p1} -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) p2: gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) p3: if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14 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_gcd#_A(x1,x2,x3) = ((0,1),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 false_A() = (1,2) s_A(x1) = ((1,1),(0,0)) x1 gcd#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,0) minus_A(x1,x2) = ((1,0),(0,0)) x1 le_A(x1,x2) = ((1,0),(0,0)) x1 + (2,2) true_A() = (2,2) |0|_A() = (0,0) if_minus_A(x1,x2,x3) = ((1,0),(0,0)) x2 gcd_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (3,2) if_gcd_A(x1,x2,x3) = ((0,1),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (1,2) rand_A(x1) = ((1,1),(0,1)) x1 + (1,0) precedence: if_gcd# = false = s = gcd# = minus = le = true = |0| = if_minus = gcd = if_gcd = rand partial status: pi(if_gcd#) = [] pi(false) = [] pi(s) = [] pi(gcd#) = [] pi(minus) = [] pi(le) = [] pi(true) = [] pi(|0|) = [] pi(if_minus) = [] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: if_gcd#_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 false_A() = (3,16) s_A(x1) = ((0,1),(1,0)) x1 + (0,12) gcd#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,0) minus_A(x1,x2) = x1 + (5,5) le_A(x1,x2) = ((0,0),(1,1)) x1 + (2,1) true_A() = (1,4) |0|_A() = (4,17) if_minus_A(x1,x2,x3) = x2 + (5,5) gcd_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (2,17) if_gcd_A(x1,x2,x3) = ((1,1),(0,0)) x2 + ((1,1),(0,0)) x3 + (1,17) rand_A(x1) = (0,0) precedence: gcd > false > minus = if_minus > if_gcd# = s = gcd# = |0| = if_gcd > le > true > rand partial status: pi(if_gcd#) = [] pi(false) = [] pi(s) = [] pi(gcd#) = [] pi(minus) = [1] pi(le) = [] pi(true) = [] pi(|0|) = [] pi(if_minus) = [] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) p2: gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) p2: gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14 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_gcd#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (1,5) false_A() = (0,3) s_A(x1) = ((1,0),(0,0)) x1 gcd#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,5) minus_A(x1,x2) = ((1,0),(0,0)) x1 + (0,5) le_A(x1,x2) = ((0,0),(1,0)) x1 + (0,6) |0|_A() = (0,2) true_A() = (0,1) if_minus_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (0,2) gcd_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,1),(0,1)) x2 + (1,4) if_gcd_A(x1,x2,x3) = ((1,1),(0,0)) x2 + ((1,1),(0,0)) x3 + (1,4) rand_A(x1) = x1 + (1,1) precedence: if_gcd# = false = s = gcd# = minus = le = |0| = true = if_minus = gcd = if_gcd = rand partial status: pi(if_gcd#) = [] pi(false) = [] pi(s) = [] pi(gcd#) = [] pi(minus) = [] pi(le) = [] pi(|0|) = [] pi(true) = [] pi(if_minus) = [] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: if_gcd#_A(x1,x2,x3) = ((0,1),(0,0)) x1 + x2 + ((0,1),(0,1)) x3 + (1,3) false_A() = (6,2) s_A(x1) = ((1,0),(1,0)) x1 + (5,0) gcd#_A(x1,x2) = ((1,0),(1,0)) x1 + ((0,1),(0,1)) x2 + (4,3) minus_A(x1,x2) = x1 + (0,14) le_A(x1,x2) = (7,2) |0|_A() = (1,1) true_A() = (2,2) if_minus_A(x1,x2,x3) = ((0,0),(1,1)) x1 + ((0,1),(1,0)) x2 + (5,0) gcd_A(x1,x2) = (0,1) if_gcd_A(x1,x2,x3) = (0,1) rand_A(x1) = (1,0) precedence: minus = if_minus > |0| > true > if_gcd# = s = gcd# = gcd = if_gcd = rand > le > false partial status: pi(if_gcd#) = [] pi(false) = [] pi(s) = [] pi(gcd#) = [] pi(minus) = [1] pi(le) = [] pi(|0|) = [] pi(true) = [] pi(if_minus) = [] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The estimated dependency graph contains the following SCCs: (no SCCs) -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: if_minus#(false(),s(x),y) -> minus#(x,y) p2: minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: if_minus#_A(x1,x2,x3) = max{x1 + 7, x2 + 14, x3 + 15} false_A = 1 s_A(x1) = x1 minus#_A(x1,x2) = max{x1 + 14, x2 + 15} le_A(x1,x2) = max{x1 + 6, x2 + 5} |0|_A = 0 true_A = 3 minus_A(x1,x2) = max{x1, x2 - 1} if_minus_A(x1,x2,x3) = max{x1 - 6, x2, x3 - 1} gcd_A(x1,x2) = max{x1 + 7, x2 + 7} if_gcd_A(x1,x2,x3) = max{x1 + 1, x2 + 7, x3 + 7} rand_A(x1) = max{2, x1 + 1} precedence: le = gcd = if_gcd > true > false = minus = if_minus > if_minus# = minus# > s = |0| = rand partial status: pi(if_minus#) = [2, 3] pi(false) = [] pi(s) = [1] pi(minus#) = [1, 2] pi(le) = [2] pi(|0|) = [] pi(true) = [] pi(minus) = [1] pi(if_minus) = [2] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: if_minus#_A(x1,x2,x3) = max{x2, x3 + 34} false_A = 16 s_A(x1) = x1 + 15 minus#_A(x1,x2) = max{x1, x2 + 34} le_A(x1,x2) = max{40, x2 + 33} |0|_A = 0 true_A = 0 minus_A(x1,x2) = x1 if_minus_A(x1,x2,x3) = max{11, x2} gcd_A(x1,x2) = 13 if_gcd_A(x1,x2,x3) = 13 rand_A(x1) = 9 precedence: if_minus# = false = minus# = le = rand > |0| > minus > if_minus > true > s = gcd = if_gcd partial status: pi(if_minus#) = [2] pi(false) = [] pi(s) = [] pi(minus#) = [1, 2] pi(le) = [] pi(|0|) = [] pi(true) = [] pi(minus) = [] pi(if_minus) = [2] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: if_minus#(false(),s(x),y) -> minus#(x,y) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The estimated dependency graph contains the following SCCs: (no SCCs) -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: le#(s(x),s(y)) -> le#(x,y) and R consists of: r1: le(|0|(),y) -> true() r2: le(s(x),|0|()) -> false() r3: le(s(x),s(y)) -> le(x,y) r4: minus(|0|(),y) -> |0|() r5: minus(s(x),y) -> if_minus(le(s(x),y),s(x),y) r6: if_minus(true(),s(x),y) -> |0|() r7: if_minus(false(),s(x),y) -> s(minus(x,y)) r8: gcd(|0|(),y) -> y r9: gcd(s(x),|0|()) -> s(x) r10: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) r11: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) r12: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: le#_A(x1,x2) = max{x1 + 14, x2 + 1} s_A(x1) = max{12, x1} le_A(x1,x2) = max{9, x2 + 7} |0|_A = 8 true_A = 8 false_A = 14 minus_A(x1,x2) = max{x1, x2} if_minus_A(x1,x2,x3) = max{1, x1 - 10, x2, x3} gcd_A(x1,x2) = max{10, x1 + 6, x2 + 6} if_gcd_A(x1,x2,x3) = max{11, x1 - 1, x2 + 6, x3 + 6} rand_A(x1) = max{26, x1 + 13} precedence: le# > le > true > |0| = minus = if_minus > gcd = if_gcd > s = false = rand partial status: pi(le#) = [1, 2] pi(s) = [1] pi(le) = [2] pi(|0|) = [] pi(true) = [] pi(false) = [] pi(minus) = [1] pi(if_minus) = [2] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: le#_A(x1,x2) = max{6, x1} s_A(x1) = 3 le_A(x1,x2) = x2 + 23 |0|_A = 4 true_A = 5 false_A = 5 minus_A(x1,x2) = max{9, x1} if_minus_A(x1,x2,x3) = x2 + 2 gcd_A(x1,x2) = 7 if_gcd_A(x1,x2,x3) = 7 rand_A(x1) = 1 precedence: le# = s = le = |0| = true = false = minus = if_minus = gcd = if_gcd = rand partial status: pi(le#) = [1] pi(s) = [] pi(le) = [] pi(|0|) = [] pi(true) = [] pi(false) = [] pi(minus) = [1] pi(if_minus) = [2] pi(gcd) = [] pi(if_gcd) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.