Input TRS: 1: a__dbl(0()) -> 0() 2: a__dbl(s(X)) -> s(s(dbl(X))) 3: a__dbls(nil()) -> nil() 4: a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) 5: a__sel(0(),cons(X,Y)) -> mark(X) 6: a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) 7: a__indx(nil(),X) -> nil() 8: a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) 9: a__from(X) -> cons(X,from(s(X))) 10: a__dbl1(0()) -> 01() 11: a__dbl1(s(X)) -> s1(s1(a__dbl1(mark(X)))) 12: a__sel1(0(),cons(X,Y)) -> mark(X) 13: a__sel1(s(X),cons(Y,Z)) -> a__sel1(mark(X),mark(Z)) 14: a__quote(0()) -> 01() 15: a__quote(s(X)) -> s1(a__quote(mark(X))) 16: a__quote(dbl(X)) -> a__dbl1(mark(X)) 17: a__quote(sel(X,Y)) -> a__sel1(mark(X),mark(Y)) 18: mark(dbl(X)) -> a__dbl(mark(X)) 19: mark(dbls(X)) -> a__dbls(mark(X)) 20: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) 21: mark(indx(X1,X2)) -> a__indx(mark(X1),X2) 22: mark(from(X)) -> a__from(X) 23: mark(dbl1(X)) -> a__dbl1(mark(X)) 24: mark(sel1(X1,X2)) -> a__sel1(mark(X1),mark(X2)) 25: mark(quote(X)) -> a__quote(mark(X)) 26: mark(0()) -> 0() 27: mark(s(X)) -> s(X) 28: mark(nil()) -> nil() 29: mark(cons(X1,X2)) -> cons(X1,X2) 30: mark(01()) -> 01() 31: mark(s1(X)) -> s1(mark(X)) 32: a__dbl(X) -> dbl(X) 33: a__dbls(X) -> dbls(X) 34: a__sel(X1,X2) -> sel(X1,X2) 35: a__indx(X1,X2) -> indx(X1,X2) 36: a__from(X) -> from(X) 37: a__dbl1(X) -> dbl1(X) 38: a__sel1(X1,X2) -> sel1(X1,X2) 39: a__quote(X) -> quote(X) Number of strict rules: 39 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #a__sel(s(X),cons(Y,Z)) -> #a__sel(mark(X),mark(Z)) #2: #a__sel(s(X),cons(Y,Z)) -> #mark(X) #3: #a__sel(s(X),cons(Y,Z)) -> #mark(Z) #4: #a__sel1(s(X),cons(Y,Z)) -> #a__sel1(mark(X),mark(Z)) #5: #a__sel1(s(X),cons(Y,Z)) -> #mark(X) #6: #a__sel1(s(X),cons(Y,Z)) -> #mark(Z) #7: #a__dbl1(s(X)) -> #a__dbl1(mark(X)) #8: #a__dbl1(s(X)) -> #mark(X) #9: #mark(sel1(X1,X2)) -> #a__sel1(mark(X1),mark(X2)) #10: #mark(sel1(X1,X2)) -> #mark(X1) #11: #mark(sel1(X1,X2)) -> #mark(X2) #12: #mark(dbl1(X)) -> #a__dbl1(mark(X)) #13: #mark(dbl1(X)) -> #mark(X) #14: #a__sel1(0(),cons(X,Y)) -> #mark(X) #15: #mark(s1(X)) -> #mark(X) #16: #mark(quote(X)) -> #a__quote(mark(X)) #17: #mark(quote(X)) -> #mark(X) #18: #mark(sel(X1,X2)) -> #a__sel(mark(X1),mark(X2)) #19: #mark(sel(X1,X2)) -> #mark(X1) #20: #mark(sel(X1,X2)) -> #mark(X2) #21: #a__sel(0(),cons(X,Y)) -> #mark(X) #22: #mark(from(X)) -> #a__from(X) #23: #a__quote(sel(X,Y)) -> #a__sel1(mark(X),mark(Y)) #24: #a__quote(sel(X,Y)) -> #mark(X) #25: #a__quote(sel(X,Y)) -> #mark(Y) #26: #mark(dbls(X)) -> #a__dbls(mark(X)) #27: #mark(dbls(X)) -> #mark(X) #28: #mark(indx(X1,X2)) -> #a__indx(mark(X1),X2) #29: #mark(indx(X1,X2)) -> #mark(X1) #30: #a__quote(dbl(X)) -> #a__dbl1(mark(X)) #31: #a__quote(dbl(X)) -> #mark(X) #32: #a__quote(s(X)) -> #a__quote(mark(X)) #33: #a__quote(s(X)) -> #mark(X) #34: #mark(dbl(X)) -> #a__dbl(mark(X)) #35: #mark(dbl(X)) -> #mark(X) Number of SCCs: 1, DPs: 31, edges: 334 SCC { #1..21 #23..25 #27 #29..33 #35 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__quote(x1) weight: x1 a__dbl1(x1) weight: (/ 1 4) + x1 01() weight: (/ 1 8) s(x1) weight: x1 #a__from(x1) weight: 0 dbls(x1) weight: (/ 1 4) + x1 a__indx(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 4) + x1} a__from(x1) weight: (/ 1 8) + x1 #a__indx(x1,x2) weight: 0 dbl(x1) weight: (/ 1 4) + x1 indx(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 4) + x1} #a__dbl1(x1) weight: (/ 1 8) + x1 a__dbl(x1) weight: (/ 1 4) + x1 a__sel1(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 8) + x1} #a__dbls(x1) weight: 0 #mark(x1) weight: x1 0() weight: (/ 1 8) a__quote(x1) weight: (/ 1 4) + x1 sel(x1,x2) weight: max{x2, (/ 1 4) + x1} from(x1) weight: (/ 1 8) + x1 #a__sel1(x1,x2) weight: max{x2, x1} nil() weight: (/ 1 4) dbl1(x1) weight: (/ 1 4) + x1 #a__dbl(x1) weight: 0 #a__sel(x1,x2) weight: max{x2, (/ 1 8) + x1} mark(x1) weight: x1 a__sel(x1,x2) weight: max{x2, (/ 1 4) + x1} a__dbls(x1) weight: (/ 1 4) + x1 quote(x1) weight: (/ 1 4) + x1 cons(x1,x2) weight: max{x2, x1} sel1(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 8) + x1} s1(x1) weight: x1 Usable rules: { 1..39 } Removed DPs: #2 #8..13 #16 #17 #19 #24 #27 #29..31 #35 Number of SCCs: 4, DPs: 9, edges: 21 SCC { #7 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #a__quote(x1) weight: (/ 1 8) status: [] precedence above: a__dbl1(x1) weight: (/ 3 8) status: [] precedence above: 01 dbl1 01() weight: (/ 1 4) status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: mark #a__from(x1) weight: x1 status: [] precedence above: dbls(x1) weight: (/ 1 2) + x1 status: [] precedence above: a__sel1 sel mark a__sel a__dbls cons sel1 a__indx(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: indx a__sel1 sel nil a__sel cons sel1 a__from(x1) weight: (/ 1 4) + x1 status: [] precedence above: a__sel1 sel from a__sel cons sel1 #a__indx(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x2,x1] precedence above: dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s a__dbl mark indx(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: a__indx a__sel1 sel nil a__sel cons sel1 #a__dbl1(x1) weight: x1 status: [x1] precedence above: a__dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s dbl mark a__sel1(x1,x2) weight: x2 status: [] precedence above: sel1 #a__dbls(x1) weight: x1 status: [] precedence above: #mark(x1) weight: (/ 1 8) status: [] precedence above: 0() weight: (/ 1 8) status: [] precedence above: a__quote(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: a__dbl1 01 dbl1 quote s1 sel(x1,x2) weight: x2 status: [] precedence above: a__sel1 a__sel sel1 from(x1) weight: (/ 1 4) + x1 status: [] precedence above: a__from a__sel1 sel a__sel cons sel1 #a__sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: (/ 3 8) status: [] precedence above: a__dbl1 01 #a__dbl(x1) weight: x1 status: [] precedence above: #a__sel(x1,x2) weight: (/ 1 8) + x1 status: [x1] precedence above: mark(x1) weight: x1 status: x1 a__sel(x1,x2) weight: x2 status: [] precedence above: a__sel1 sel sel1 a__dbls(x1) weight: (/ 1 2) + x1 status: [] precedence above: dbls a__sel1 sel mark a__sel cons sel1 quote(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: a__dbl1 01 a__quote dbl1 s1 cons(x1,x2) weight: max{x2, (/ 1 8) + x1} status: [] precedence above: a__sel1 sel a__sel sel1 sel1(x1,x2) weight: x2 status: [] precedence above: a__sel1 s1(x1) weight: (/ 1 8) status: [] precedence above: Usable rules: { 1..39 } Removed DPs: #7 Number of SCCs: 3, DPs: 8, edges: 20 SCC { #32 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #a__quote(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: a__dbl1(x1) weight: (/ 3 8) status: [] precedence above: 01 dbl1 01() weight: (/ 1 4) status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: s1 #a__from(x1) weight: x1 status: [] precedence above: dbls(x1) weight: (/ 1 2) + x1 status: [] precedence above: a__sel1 sel a__sel a__dbls cons sel1 a__indx(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: indx a__sel1 sel nil a__sel cons sel1 a__from(x1) weight: (/ 1 4) + x1 status: [] precedence above: a__sel1 sel from a__sel cons sel1 #a__indx(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x2,x1] precedence above: dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s a__dbl s1 indx(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: a__indx a__sel1 sel nil a__sel cons sel1 #a__dbl1(x1) weight: x1 status: [x1] precedence above: a__dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s dbl s1 a__sel1(x1,x2) weight: x2 status: [] precedence above: sel1 #a__dbls(x1) weight: x1 status: [] precedence above: #mark(x1) weight: (/ 1 8) status: [] precedence above: 0() weight: (/ 1 8) status: [] precedence above: a__quote(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: a__dbl1 01 dbl1 quote s1 sel(x1,x2) weight: x2 status: [] precedence above: a__sel1 a__sel sel1 from(x1) weight: (/ 1 4) + x1 status: [] precedence above: a__from a__sel1 sel a__sel cons sel1 #a__sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: (/ 3 8) status: [] precedence above: a__dbl1 01 #a__dbl(x1) weight: x1 status: [] precedence above: #a__sel(x1,x2) weight: (/ 1 8) + x1 status: [x1] precedence above: mark(x1) weight: x1 status: x1 a__sel(x1,x2) weight: x2 status: [] precedence above: a__sel1 sel sel1 a__dbls(x1) weight: (/ 1 2) + x1 status: [] precedence above: dbls a__sel1 sel a__sel cons sel1 quote(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: a__dbl1 01 a__quote dbl1 s1 cons(x1,x2) weight: max{x2, (/ 1 8) + x1} status: [] precedence above: a__sel1 sel a__sel sel1 sel1(x1,x2) weight: x2 status: [] precedence above: a__sel1 s1(x1) weight: (/ 1 8) status: [] precedence above: Usable rules: { 1..39 } Removed DPs: #32 Number of SCCs: 2, DPs: 7, edges: 19 SCC { #4 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #a__quote(x1) weight: (/ 1 16) status: [] precedence above: a__dbl1(x1) weight: (/ 3 16) status: [] precedence above: s dbl1 01() weight: (/ 1 8) status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: a__dbl1 dbl1 #a__from(x1) weight: x1 status: [] precedence above: dbls(x1) weight: (/ 1 8) + x1 status: [] precedence above: a__dbl1 s dbl a__dbl dbl1 mark a__dbls cons a__indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1] precedence above: indx a__sel1 sel nil mark a__sel cons sel1 a__from(x1) weight: (/ 1 4) + x1 status: [] precedence above: from mark cons #a__indx(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x2,x1] precedence above: dbl(x1) weight: (/ 1 16) + x1 status: [x1] precedence above: a__dbl1 s a__dbl dbl1 indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1] precedence above: a__indx a__sel1 sel nil mark a__sel cons sel1 #a__dbl1(x1) weight: 0 status: [] precedence above: a__dbl(x1) weight: (/ 1 16) + x1 status: [x1] precedence above: a__dbl1 s dbl dbl1 a__sel1(x1,x2) weight: (/ 5 16) + x2 status: [] precedence above: sel1 #a__dbls(x1) weight: x1 status: [] precedence above: #mark(x1) weight: (/ 1 16) status: [] precedence above: 0() weight: (/ 1 16) status: [] precedence above: a__quote(x1) weight: (/ 3 16) + x1 status: [x1] precedence above: a__dbl1 01 s a__sel1 dbl1 quote sel1 s1 sel(x1,x2) weight: (/ 1 4) + x2 + x1 status: [x1,x2] precedence above: a__sel1 a__sel sel1 from(x1) weight: (/ 1 4) + x1 status: [] precedence above: a__from mark cons #a__sel1(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x1,x2] precedence above: nil() weight: 0 status: [] precedence above: dbl1(x1) weight: (/ 3 16) status: [] precedence above: a__dbl1 s #a__dbl(x1) weight: x1 status: [] precedence above: #a__sel(x1,x2) weight: (/ 1 16) + x1 status: [x1] precedence above: mark(x1) weight: x1 status: x1 a__sel(x1,x2) weight: (/ 1 4) + x2 + x1 status: [x1,x2] precedence above: a__sel1 sel sel1 a__dbls(x1) weight: (/ 1 8) + x1 status: [] precedence above: a__dbl1 s dbls dbl a__dbl dbl1 mark cons quote(x1) weight: (/ 3 16) + x1 status: [x1] precedence above: a__dbl1 01 s a__sel1 a__quote dbl1 sel1 s1 cons(x1,x2) weight: max{x2, (/ 3 16) + x1} status: [] precedence above: mark sel1(x1,x2) weight: (/ 5 16) + x2 status: [] precedence above: a__sel1 s1(x1) weight: (/ 1 16) status: [] precedence above: Usable rules: { 1..39 } Removed DPs: #4 Number of SCCs: 1, DPs: 6, edges: 18 SCC { #1 #3 #15 #18 #20 #21 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__quote(x1) weight: 0 a__dbl1(x1) weight: (/ 1 8) 01() weight: (/ 1 8) s(x1) weight: x1 #a__from(x1) weight: 0 dbls(x1) weight: (/ 5 4) a__indx(x1,x2) weight: max{(/ 9 8) + x2, (/ 9 8) + x1} a__from(x1) weight: (/ 3 8) + x1 #a__indx(x1,x2) weight: 0 dbl(x1) weight: (/ 1 8) indx(x1,x2) weight: max{(/ 9 8) + x2, (/ 9 8) + x1} #a__dbl1(x1) weight: (/ 1 8) a__dbl(x1) weight: (/ 1 8) a__sel1(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 8) + x1} #a__dbls(x1) weight: 0 #mark(x1) weight: x1 0() weight: (/ 1 8) a__quote(x1) weight: (/ 1 8) + x1 sel(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 4) + x1} from(x1) weight: (/ 3 8) + x1 #a__sel1(x1,x2) weight: 0 nil() weight: (/ 5 4) dbl1(x1) weight: (/ 1 8) #a__dbl(x1) weight: 0 #a__sel(x1,x2) weight: max{(/ 1 8) + x2, (/ 3 8) + x1} mark(x1) weight: x1 a__sel(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 4) + x1} a__dbls(x1) weight: (/ 5 4) quote(x1) weight: (/ 1 8) + x1 cons(x1,x2) weight: max{x2, (/ 3 8) + x1} sel1(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 8) + x1} s1(x1) weight: x1 Usable rules: { 1..39 } Removed DPs: #3 #18 #20 #21 Number of SCCs: 2, DPs: 2, edges: 2 SCC { #15 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #a__quote(x1) weight: (/ 1 8) a__dbl1(x1) weight: (/ 1 8) + x1 01() weight: 0 s(x1) weight: (/ 1 2) #a__from(x1) weight: 0 dbls(x1) weight: (/ 1 8) + x1 a__indx(x1,x2) weight: (/ 3 8) a__from(x1) weight: (/ 3 8) #a__indx(x1,x2) weight: 0 dbl(x1) weight: (/ 1 8) + x1 indx(x1,x2) weight: (/ 1 8) + x1 #a__dbl1(x1) weight: 0 a__dbl(x1) weight: (/ 3 8) a__sel1(x1,x2) weight: (/ 1 4) + x2 #a__dbls(x1) weight: 0 #mark(x1) weight: (/ 1 8) + x1 0() weight: 0 a__quote(x1) weight: (/ 1 8) sel(x1,x2) weight: (/ 1 8) + x1 from(x1) weight: (/ 1 8) #a__sel1(x1,x2) weight: (/ 1 8) nil() weight: 0 dbl1(x1) weight: (/ 1 4) + x1 #a__dbl(x1) weight: 0 #a__sel(x1,x2) weight: 0 mark(x1) weight: (/ 1 8) + x1 a__sel(x1,x2) weight: (/ 3 8) a__dbls(x1) weight: 0 quote(x1) weight: (/ 1 4) cons(x1,x2) weight: (/ 1 2) sel1(x1,x2) weight: (/ 1 8) + x1 + x2 s1(x1) weight: (/ 1 4) + x1 Usable rules: { } Removed DPs: #15 Number of SCCs: 1, DPs: 1, edges: 1 SCC { #1 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #a__quote(x1) weight: (/ 1 16) status: [] precedence above: a__dbl1(x1) weight: (/ 3 16) status: [] precedence above: s dbl1 01() weight: (/ 1 8) status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: a__dbl1 dbl1 #a__from(x1) weight: x1 status: [] precedence above: dbls(x1) weight: (/ 1 8) + x1 status: [] precedence above: a__dbl1 s dbl a__dbl dbl1 mark a__dbls cons a__indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1] precedence above: indx a__sel1 sel nil mark a__sel cons sel1 a__from(x1) weight: (/ 1 4) + x1 status: [] precedence above: from mark cons #a__indx(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x2,x1] precedence above: dbl(x1) weight: (/ 1 16) + x1 status: [x1] precedence above: a__dbl1 s a__dbl dbl1 indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1] precedence above: a__indx a__sel1 sel nil mark a__sel cons sel1 #a__dbl1(x1) weight: 0 status: [] precedence above: a__dbl(x1) weight: (/ 1 16) + x1 status: [x1] precedence above: a__dbl1 s dbl dbl1 a__sel1(x1,x2) weight: (/ 5 16) + x2 status: [] precedence above: sel1 #a__dbls(x1) weight: x1 status: [] precedence above: #mark(x1) weight: (/ 1 16) status: [] precedence above: 0() weight: (/ 1 16) status: [] precedence above: a__quote(x1) weight: (/ 3 16) + x1 status: [x1] precedence above: a__dbl1 01 s a__sel1 dbl1 quote sel1 s1 sel(x1,x2) weight: (/ 1 4) + x2 + x1 status: [x1,x2] precedence above: a__sel1 a__sel sel1 from(x1) weight: (/ 1 4) + x1 status: [] precedence above: a__from mark cons #a__sel1(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x1,x2] precedence above: nil() weight: 0 status: [] precedence above: dbl1(x1) weight: (/ 3 16) status: [] precedence above: a__dbl1 s #a__dbl(x1) weight: x1 status: [] precedence above: #a__sel(x1,x2) weight: (/ 1 16) + x1 status: [x1] precedence above: mark mark(x1) weight: x1 status: x1 a__sel(x1,x2) weight: (/ 1 4) + x2 + x1 status: [x1,x2] precedence above: a__sel1 sel sel1 a__dbls(x1) weight: (/ 1 8) + x1 status: [] precedence above: a__dbl1 s dbls dbl a__dbl dbl1 mark cons quote(x1) weight: (/ 3 16) + x1 status: [x1] precedence above: a__dbl1 01 s a__sel1 a__quote dbl1 sel1 s1 cons(x1,x2) weight: max{x2, (/ 3 16) + x1} status: [] precedence above: mark sel1(x1,x2) weight: (/ 5 16) + x2 status: [] precedence above: a__sel1 s1(x1) weight: (/ 1 16) status: [] precedence above: Usable rules: { 1..39 } Removed DPs: #1 Number of SCCs: 0, DPs: 0, edges: 0 YES