Input TRS: 1: dbl(0()) -> 0() 2: dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) 3: dbls(nil()) -> nil() 4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) 5: sel(0(),cons(X,Y)) -> activate(X) 6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) 7: indx(nil(),X) -> nil() 8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) 9: from(X) -> cons(activate(X),n__from(n__s(activate(X)))) 10: dbl1(0()) -> 01() 11: dbl1(s(X)) -> s1(s1(dbl1(activate(X)))) 12: sel1(0(),cons(X,Y)) -> activate(X) 13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z)) 14: quote(0()) -> 01() 15: quote(s(X)) -> s1(quote(activate(X))) 16: quote(dbl(X)) -> dbl1(X) 17: quote(sel(X,Y)) -> sel1(X,Y) 18: s(X) -> n__s(X) 19: dbl(X) -> n__dbl(X) 20: dbls(X) -> n__dbls(X) 21: sel(X1,X2) -> n__sel(X1,X2) 22: indx(X1,X2) -> n__indx(X1,X2) 23: from(X) -> n__from(X) 24: activate(n__s(X)) -> s(X) 25: activate(n__dbl(X)) -> dbl(X) 26: activate(n__dbls(X)) -> dbls(X) 27: activate(n__sel(X1,X2)) -> sel(X1,X2) 28: activate(n__indx(X1,X2)) -> indx(X1,X2) 29: activate(n__from(X)) -> from(X) 30: activate(X) -> X Number of strict rules: 30 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #dbl(s(X)) -> #s(n__s(n__dbl(activate(X)))) #2: #dbl(s(X)) -> #activate(X) #3: #activate(n__from(X)) -> #from(X) #4: #sel(s(X),cons(Y,Z)) -> #sel(activate(X),activate(Z)) #5: #sel(s(X),cons(Y,Z)) -> #activate(X) #6: #sel(s(X),cons(Y,Z)) -> #activate(Z) #7: #sel1(s(X),cons(Y,Z)) -> #sel1(activate(X),activate(Z)) #8: #sel1(s(X),cons(Y,Z)) -> #activate(X) #9: #sel1(s(X),cons(Y,Z)) -> #activate(Z) #10: #from(X) -> #activate(X) #11: #from(X) -> #activate(X) #12: #dbl1(s(X)) -> #dbl1(activate(X)) #13: #dbl1(s(X)) -> #activate(X) #14: #activate(n__s(X)) -> #s(X) #15: #sel1(0(),cons(X,Y)) -> #activate(X) #16: #activate(n__dbl(X)) -> #dbl(X) #17: #sel(0(),cons(X,Y)) -> #activate(X) #18: #activate(n__indx(X1,X2)) -> #indx(X1,X2) #19: #activate(n__sel(X1,X2)) -> #sel(X1,X2) #20: #quote(sel(X,Y)) -> #sel1(X,Y) #21: #activate(n__dbls(X)) -> #dbls(X) #22: #quote(dbl(X)) -> #dbl1(X) #23: #indx(cons(X,Y),Z) -> #activate(X) #24: #indx(cons(X,Y),Z) -> #activate(Z) #25: #indx(cons(X,Y),Z) -> #activate(Y) #26: #indx(cons(X,Y),Z) -> #activate(Z) #27: #quote(s(X)) -> #quote(activate(X)) #28: #quote(s(X)) -> #activate(X) #29: #dbls(cons(X,Y)) -> #activate(X) #30: #dbls(cons(X,Y)) -> #activate(Y) Number of SCCs: 4, DPs: 21, edges: 80 SCC { #12 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #dbl1(x1) weight: x1 status: [x1] precedence above: 01() weight: 0 status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: n__s dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: n__dbls sel nil n__sel cons activate(x1) weight: x1 status: x1 dbl(x1) weight: (/ 1 16) + x1 status: [x1] precedence above: s n__s n__dbl indx(x1,x2) weight: (/ 1 2) + x2 status: [x2] precedence above: n__indx sel nil n__sel cons n__indx(x1,x2) weight: (/ 1 2) + x2 status: [x2] precedence above: indx sel nil n__sel cons n__from(x1) weight: (/ 1 4) + x1 status: [] precedence above: s n__s sel from n__sel cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: x1 status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: dbls sel nil n__sel cons n__s(x1) weight: x1 status: [x1] precedence above: s n__dbl(x1) weight: (/ 1 16) + x1 status: [x1] precedence above: s dbl n__s 0() weight: (/ 1 16) status: [] precedence above: #sel(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x2,x1] precedence above: #indx(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: sel(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: n__sel from(x1) weight: (/ 1 4) + x1 status: [] precedence above: s n__from n__s sel n__sel cons #s(x1) weight: x1 status: [] precedence above: nil() weight: (/ 1 16) status: [] precedence above: dbl1(x1) weight: (/ 1 16) status: [] precedence above: #sel1(x1,x2) weight: (/ 1 16) + x1 status: [x1] precedence above: n__sel(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: sel #from(x1) weight: x1 status: [] precedence above: quote(x1) weight: (/ 1 16) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 3 16) + x1} status: [x1] precedence above: sel n__sel #quote(x1) weight: x1 status: [] precedence above: sel1(x1,x2) weight: (/ 1 16) + x1 status: [x1] precedence above: s1(x1) weight: x1 status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #12 Number of SCCs: 3, DPs: 20, edges: 79 SCC { #27 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #dbl1(x1) weight: x1 status: [x1] precedence above: 01() weight: 0 status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: activate n__s dbls(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: activate n__dbls sel nil n__sel cons activate(x1) weight: x1 status: [x1] precedence above: dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: s activate n__s n__dbl indx(x1,x2) weight: (/ 1 2) + x2 status: [x2] precedence above: activate n__indx sel nil n__sel cons n__indx(x1,x2) weight: (/ 1 2) + x2 status: [x2] precedence above: activate indx sel nil n__sel cons n__from(x1) weight: (/ 1 4) + x1 status: [] precedence above: s activate n__s sel from n__sel cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: x1 status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: dbls activate sel nil n__sel cons n__s(x1) weight: x1 status: [x1] precedence above: s activate n__dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: s activate dbl n__s 0() weight: (/ 1 16) status: [] precedence above: #sel(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x2,x1] precedence above: #indx(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: sel(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: activate n__sel from(x1) weight: (/ 1 4) + x1 status: [] precedence above: s activate n__from n__s sel n__sel cons #s(x1) weight: x1 status: [] precedence above: nil() weight: (/ 1 16) status: [] precedence above: dbl1(x1) weight: (/ 1 16) status: [] precedence above: #sel1(x1,x2) weight: (/ 1 16) + x1 status: [x1] precedence above: n__sel(x1,x2) weight: (/ 1 4) + x2 status: [] precedence above: activate sel #from(x1) weight: x1 status: [] precedence above: quote(x1) weight: (/ 1 16) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 3 16) + x1} status: [] precedence above: activate sel n__sel #quote(x1) weight: x1 status: [x1] precedence above: sel1(x1,x2) weight: (/ 1 16) + x1 status: [x1] precedence above: s1(x1) weight: x1 status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #27 Number of SCCs: 2, DPs: 19, edges: 78 SCC { #7 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #dbl1(x1) weight: 0 status: [] precedence above: 01() weight: 0 status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: activate n__s dbls(x1) weight: (/ 1 2) + x1 status: [x1] precedence above: activate n__dbls sel nil n__sel cons activate(x1) weight: x1 status: [x1] precedence above: dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s activate n__s n__dbl indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1,x2] precedence above: activate n__indx sel nil n__sel cons n__indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1,x2] precedence above: activate indx sel nil n__sel cons n__from(x1) weight: (/ 1 2) + x1 status: [] precedence above: from cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: x1 status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 2) + x1 status: [x1] precedence above: dbls activate sel nil n__sel cons n__s(x1) weight: x1 status: [x1] precedence above: s activate n__dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s activate dbl n__s 0() weight: (/ 1 8) status: [] precedence above: #sel(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x2,x1] precedence above: #indx(x1,x2) weight: (/ 1 8) + x2 status: [x2] precedence above: sel(x1,x2) weight: x2 status: [] precedence above: activate n__sel from(x1) weight: (/ 1 2) + x1 status: [] precedence above: n__from cons #s(x1) weight: x1 status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: (/ 1 8) status: [] precedence above: #sel1(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1] precedence above: activate n__sel(x1,x2) weight: x2 status: [] precedence above: activate sel #from(x1) weight: x1 status: [] precedence above: quote(x1) weight: (/ 1 8) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 3 8) + x1} status: [] precedence above: #quote(x1) weight: 0 status: [] precedence above: sel1(x1,x2) weight: (/ 1 8) + x1 status: [x1] precedence above: s1(x1) weight: x1 status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #7 Number of SCCs: 1, DPs: 18, edges: 77 SCC { #2..6 #10 #11 #16..19 #21 #23..26 #29 #30 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #dbl1(x1) weight: 0 01() weight: 0 s(x1) weight: x1 dbls(x1) weight: (/ 1 4) + x1 activate(x1) weight: x1 dbl(x1) weight: (/ 1 8) + x1 indx(x1,x2) weight: max{(/ 1 2) + x2, (/ 3 8) + x1} n__indx(x1,x2) weight: max{(/ 1 2) + x2, (/ 3 8) + x1} n__from(x1) weight: (/ 1 8) + x1 #dbl(x1) weight: (/ 1 16) + x1 #activate(x1) weight: x1 #dbls(x1) weight: (/ 1 16) + x1 n__dbls(x1) weight: (/ 1 4) + x1 n__s(x1) weight: x1 n__dbl(x1) weight: (/ 1 8) + x1 0() weight: (/ 1 16) #sel(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 16) + x1} #indx(x1,x2) weight: max{(/ 7 16) + x2, (/ 1 16) + x1} sel(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 16) + x1} from(x1) weight: (/ 1 8) + x1 #s(x1) weight: 0 nil() weight: (/ 9 16) dbl1(x1) weight: 0 #sel1(x1,x2) weight: 0 n__sel(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 16) + x1} #from(x1) weight: (/ 1 16) + x1 quote(x1) weight: 0 cons(x1,x2) weight: max{x2, (/ 1 8) + x1} #quote(x1) weight: 0 sel1(x1,x2) weight: 0 s1(x1) weight: 0 Usable rules: { 1..9 18..30 } Removed DPs: #2 #3 #5 #6 #10 #11 #16..19 #21 #23..26 #29 #30 Number of SCCs: 1, DPs: 1, edges: 1 SCC { #4 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. #dbl1(x1) weight: 0 status: [] precedence above: 01() weight: 0 status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: activate n__s dbls(x1) weight: (/ 1 2) + x1 status: [x1] precedence above: activate n__dbls sel nil n__sel cons activate(x1) weight: x1 status: [x1] precedence above: dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s activate n__s n__dbl indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1,x2] precedence above: activate n__indx sel nil n__sel cons n__indx(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1,x2] precedence above: activate indx sel nil n__sel cons n__from(x1) weight: (/ 1 2) + x1 status: [] precedence above: from cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: x1 status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 2) + x1 status: [x1] precedence above: dbls activate sel nil n__sel cons n__s(x1) weight: x1 status: [x1] precedence above: s activate n__dbl(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s activate dbl n__s 0() weight: (/ 1 8) status: [] precedence above: #sel(x1,x2) weight: x1 status: x1 #indx(x1,x2) weight: (/ 1 8) + x2 status: [x2] precedence above: sel(x1,x2) weight: x2 status: [] precedence above: activate n__sel from(x1) weight: (/ 1 2) + x1 status: [] precedence above: n__from cons #s(x1) weight: x1 status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: (/ 1 8) status: [] precedence above: #sel1(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1] precedence above: activate n__sel(x1,x2) weight: x2 status: [] precedence above: activate sel #from(x1) weight: x1 status: [] precedence above: quote(x1) weight: (/ 1 8) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 3 8) + x1} status: [] precedence above: #quote(x1) weight: 0 status: [] precedence above: sel1(x1,x2) weight: (/ 1 8) + x1 status: [x1] precedence above: s1(x1) weight: x1 status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #4 Number of SCCs: 0, DPs: 0, edges: 0 YES