Input TRS: 1: le(0(),y) -> true() 2: le(s(x),0()) -> false() 3: le(s(x),s(y)) -> le(x,y) 4: app(nil(),y) -> y 5: app(add(n,x),y) -> add(n,app(x,y)) 6: low(n,nil()) -> nil() 7: low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x)) 8: if_low(true(),n,add(m,x)) -> add(m,low(n,x)) 9: if_low(false(),n,add(m,x)) -> low(n,x) 10: high(n,nil()) -> nil() 11: high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x)) 12: if_high(true(),n,add(m,x)) -> high(n,x) 13: if_high(false(),n,add(m,x)) -> add(m,high(n,x)) 14: head(add(n,x)) -> n 15: tail(add(n,x)) -> x 16: isempty(nil()) -> true() 17: isempty(add(n,x)) -> false() 18: quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) 19: if_qs(true(),x,n,y) -> nil() 20: if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y))) Number of strict rules: 20 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #if_high(false(),n,add(m,x)) -> #high(n,x) #2: #if_low(false(),n,add(m,x)) -> #low(n,x) #3: #high(n,add(m,x)) -> #if_high(le(m,n),n,add(m,x)) #4: #high(n,add(m,x)) -> #le(m,n) #5: #if_high(true(),n,add(m,x)) -> #high(n,x) #6: #if_qs(false(),x,n,y) -> #app(quicksort(x),add(n,quicksort(y))) #7: #if_qs(false(),x,n,y) -> #quicksort(x) #8: #if_qs(false(),x,n,y) -> #quicksort(y) #9: #low(n,add(m,x)) -> #if_low(le(m,n),n,add(m,x)) #10: #low(n,add(m,x)) -> #le(m,n) #11: #app(add(n,x),y) -> #app(x,y) #12: #le(s(x),s(y)) -> #le(x,y) #13: #if_low(true(),n,add(m,x)) -> #low(n,x) #14: #quicksort(x) -> #if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) #15: #quicksort(x) -> #isempty(x) #16: #quicksort(x) -> #low(head(x),tail(x)) #17: #quicksort(x) -> #head(x) #18: #quicksort(x) -> #tail(x) #19: #quicksort(x) -> #head(x) #20: #quicksort(x) -> #high(head(x),tail(x)) #21: #quicksort(x) -> #head(x) #22: #quicksort(x) -> #tail(x) Number of SCCs: 5, DPs: 11, edges: 14 SCC { #12 } Removing DPs: Order(PosReal,>,Sum)... succeeded. isempty(x1) weight: 0 le(x1,x2) weight: 0 s(x1) weight: (/ 1 2) + x1 #le(x1,x2) weight: x2 if_high(x1,x2,x3) weight: 0 #if_qs(x1,x2,x3,x4) weight: 0 if_qs(x1,x2,x3,x4) weight: 0 #isempty(x1) weight: 0 #quicksort(x1) weight: 0 #high(x1,x2) weight: 0 false() weight: 0 #head(x1) weight: 0 #if_high(x1,x2,x3) weight: 0 quicksort(x1) weight: 0 true() weight: 0 tail(x1) weight: 0 0() weight: 0 high(x1,x2) weight: 0 nil() weight: 0 #tail(x1) weight: 0 #app(x1,x2) weight: 0 low(x1,x2) weight: 0 head(x1) weight: 0 add(x1,x2) weight: 0 if_low(x1,x2,x3) weight: 0 #if_low(x1,x2,x3) weight: 0 #low(x1,x2) weight: 0 app(x1,x2) weight: 0 Usable rules: { } Removed DPs: #12 Number of SCCs: 4, DPs: 10, edges: 13 SCC { #11 } Removing DPs: Order(PosReal,>,Sum)... succeeded. isempty(x1) weight: 0 le(x1,x2) weight: 0 s(x1) weight: (/ 1 2) #le(x1,x2) weight: 0 if_high(x1,x2,x3) weight: 0 #if_qs(x1,x2,x3,x4) weight: 0 if_qs(x1,x2,x3,x4) weight: 0 #isempty(x1) weight: 0 #quicksort(x1) weight: 0 #high(x1,x2) weight: 0 false() weight: 0 #head(x1) weight: 0 #if_high(x1,x2,x3) weight: 0 quicksort(x1) weight: 0 true() weight: 0 tail(x1) weight: 0 0() weight: 0 high(x1,x2) weight: 0 nil() weight: 0 #tail(x1) weight: 0 #app(x1,x2) weight: x1 low(x1,x2) weight: 0 head(x1) weight: 0 add(x1,x2) weight: (/ 1 2) + x2 if_low(x1,x2,x3) weight: 0 #if_low(x1,x2,x3) weight: 0 #low(x1,x2) weight: 0 app(x1,x2) weight: 0 Usable rules: { } Removed DPs: #11 Number of SCCs: 3, DPs: 9, edges: 12 SCC { #1 #3 #5 } Removing DPs: Order(PosReal,>,Sum)... succeeded. isempty(x1) weight: 0 le(x1,x2) weight: (/ 1 4) + x1 s(x1) weight: (/ 1 4) + x1 #le(x1,x2) weight: 0 if_high(x1,x2,x3) weight: 0 #if_qs(x1,x2,x3,x4) weight: 0 if_qs(x1,x2,x3,x4) weight: 0 #isempty(x1) weight: 0 #quicksort(x1) weight: 0 #high(x1,x2) weight: (/ 1 4) + x2 false() weight: 0 #head(x1) weight: 0 #if_high(x1,x2,x3) weight: x3 quicksort(x1) weight: 0 true() weight: 0 tail(x1) weight: 0 0() weight: 0 high(x1,x2) weight: 0 nil() weight: 0 #tail(x1) weight: 0 #app(x1,x2) weight: 0 low(x1,x2) weight: 0 head(x1) weight: 0 add(x1,x2) weight: (/ 1 2) + x1 + x2 if_low(x1,x2,x3) weight: 0 #if_low(x1,x2,x3) weight: 0 #low(x1,x2) weight: 0 app(x1,x2) weight: 0 Usable rules: { } Removed DPs: #1 #3 #5 Number of SCCs: 2, DPs: 6, edges: 8 SCC { #2 #9 #13 } Removing DPs: Order(PosReal,>,Sum)... succeeded. isempty(x1) weight: 0 le(x1,x2) weight: (/ 1 4) + x1 s(x1) weight: (/ 1 4) #le(x1,x2) weight: 0 if_high(x1,x2,x3) weight: 0 #if_qs(x1,x2,x3,x4) weight: 0 if_qs(x1,x2,x3,x4) weight: 0 #isempty(x1) weight: 0 #quicksort(x1) weight: 0 #high(x1,x2) weight: (/ 1 4) false() weight: 0 #head(x1) weight: 0 #if_high(x1,x2,x3) weight: 0 quicksort(x1) weight: 0 true() weight: 0 tail(x1) weight: 0 0() weight: 0 high(x1,x2) weight: 0 nil() weight: 0 #tail(x1) weight: 0 #app(x1,x2) weight: 0 low(x1,x2) weight: 0 head(x1) weight: 0 add(x1,x2) weight: (/ 1 2) + x1 + x2 if_low(x1,x2,x3) weight: 0 #if_low(x1,x2,x3) weight: x3 #low(x1,x2) weight: (/ 1 4) + x2 app(x1,x2) weight: 0 Usable rules: { } Removed DPs: #2 #9 #13 Number of SCCs: 1, DPs: 3, edges: 4 SCC { #7 #8 #14 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded. isempty(x1) weight: max{0, (- (/ 3 8)) + x1} le(x1,x2) weight: max{0, (/ 1 8) + x1, (- (/ 1 8)) + x2} s(x1) weight: max{0, x1} #le(x1,x2) weight: 0 if_high(x1,x2,x3) weight: max{0, x3} #if_qs(x1,x2,x3,x4) weight: max{0, (- (/ 1 8)) + x1, (- (/ 1 4)) + x2, (- (/ 1 4)) + x4} if_qs(x1,x2,x3,x4) weight: 0 #isempty(x1) weight: 0 #quicksort(x1) weight: max{0, (- (/ 3 8)) + x1} #high(x1,x2) weight: 0 false() weight: (/ 1 4) #head(x1) weight: 0 #if_high(x1,x2,x3) weight: 0 quicksort(x1) weight: 0 true() weight: 0 tail(x1) weight: max{0, (- (/ 5 8)) + x1} 0() weight: (/ 1 4) high(x1,x2) weight: max{0, x2} nil() weight: (/ 1 8) #tail(x1) weight: 0 #app(x1,x2) weight: 0 low(x1,x2) weight: max{0, (/ 1 8) + x2} head(x1) weight: (max (- (/ 1 4)) 0) add(x1,x2) weight: max{0, (/ 5 8) + x2} if_low(x1,x2,x3) weight: max{0, (/ 1 8) + x3} #if_low(x1,x2,x3) weight: 0 #low(x1,x2) weight: 0 app(x1,x2) weight: 0 Usable rules: { 6..13 15..17 } Removed DPs: #7 #8 Number of SCCs: 0, DPs: 0, edges: 0 YES