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(activate(X)) 26: activate(n__dbls(X)) -> dbls(activate(X)) 27: activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) 28: activate(n__indx(X1,X2)) -> indx(activate(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(activate(X)) #17: #activate(n__dbl(X)) -> #activate(X) #18: #sel(|0|(),cons(X,Y)) -> #activate(X) #19: #activate(n__indx(X1,X2)) -> #indx(activate(X1),X2) #20: #activate(n__indx(X1,X2)) -> #activate(X1) #21: #activate(n__sel(X1,X2)) -> #sel(activate(X1),activate(X2)) #22: #activate(n__sel(X1,X2)) -> #activate(X1) #23: #activate(n__sel(X1,X2)) -> #activate(X2) #24: #quote(sel(X,Y)) -> #sel1(X,Y) #25: #activate(n__dbls(X)) -> #dbls(activate(X)) #26: #activate(n__dbls(X)) -> #activate(X) #27: #quote(dbl(X)) -> #dbl1(X) #28: #indx(cons(X,Y),Z) -> #activate(X) #29: #indx(cons(X,Y),Z) -> #activate(Z) #30: #indx(cons(X,Y),Z) -> #activate(Y) #31: #indx(cons(X,Y),Z) -> #activate(Z) #32: #quote(s(X)) -> #quote(activate(X)) #33: #quote(s(X)) -> #activate(X) #34: #dbls(cons(X,Y)) -> #activate(X) #35: #dbls(cons(X,Y)) -> #activate(Y) Number of SCCs: 4, DPs: 26, edges: 190 SCC { #12 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. |0|() weight: (/ 1 8) status: [] precedence above: #dbl1(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: s(x1) weight: x1 status: [x1] precedence above: activate n__s dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: n__dbls cons activate(x1) weight: x1 status: x1 dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate n__s n__dbl indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate n__indx n__s sel nil n__sel cons n__indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate indx n__s sel nil n__sel cons n__from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__s from cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: (/ 1 8) status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: dbls cons n__s(x1) weight: x1 status: [x1] precedence above: s activate n__dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate dbl n__s #sel(x1,x2) weight: x1 status: [] precedence above: #indx(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1,x2] precedence above: sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s n__sel cons from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__from n__s cons #s(x1) weight: (/ 1 8) status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: x1 status: [] precedence above: #sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: n__sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s sel cons #from(x1) weight: (/ 1 8) status: [] precedence above: quote(x1) weight: (/ 1 8) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 1 4) + x1} status: [] precedence above: #quote(x1) weight: x1 status: [] precedence above: sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: |01|() weight: 0 status: [] precedence above: s1(x1) weight: (/ 1 8) status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #12 Number of SCCs: 3, DPs: 25, edges: 189 SCC { #32 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. |0|() weight: (/ 1 8) status: [] precedence above: #dbl1(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: s(x1) weight: x1 status: [x1] precedence above: activate n__s dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: n__dbls cons activate(x1) weight: x1 status: x1 dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate n__s n__dbl indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate n__indx n__s sel nil n__sel cons n__indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate indx n__s sel nil n__sel cons n__from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__s from cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: (/ 1 8) status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: dbls cons n__s(x1) weight: x1 status: [x1] precedence above: s activate n__dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate dbl n__s #sel(x1,x2) weight: x1 status: [] precedence above: #indx(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1,x2] precedence above: sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s n__sel cons from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__from n__s cons #s(x1) weight: (/ 1 8) status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: x1 status: [] precedence above: #sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: n__sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s sel cons #from(x1) weight: (/ 1 8) status: [] precedence above: quote(x1) weight: (/ 1 8) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 1 4) + x1} status: [] precedence above: #quote(x1) weight: x1 status: [x1] precedence above: sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: |01|() weight: 0 status: [] precedence above: s1(x1) weight: (/ 1 8) status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #32 Number of SCCs: 2, DPs: 24, edges: 188 SCC { #7 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. |0|() weight: (/ 1 8) status: [] precedence above: #dbl1(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: s(x1) weight: x1 status: [x1] precedence above: activate n__s #sel1 dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: activate n__dbls #sel1 cons activate(x1) weight: x1 status: x1 dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate n__s n__dbl #sel1 indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate n__indx n__s sel nil #sel1 n__sel cons n__indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate indx n__s sel nil #sel1 n__sel cons n__from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__s from #sel1 cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: (/ 1 8) status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: dbls activate #sel1 cons n__s(x1) weight: x1 status: [x1] precedence above: s activate #sel1 n__dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate dbl n__s #sel1 #sel(x1,x2) weight: x1 status: [] precedence above: #indx(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1,x2] precedence above: sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s #sel1 n__sel cons from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__from n__s #sel1 cons #s(x1) weight: (/ 1 8) status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: x1 status: [] precedence above: #sel1(x1,x2) weight: x1 status: [x1] precedence above: n__sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s sel #sel1 cons #from(x1) weight: (/ 1 8) status: [] precedence above: quote(x1) weight: (/ 1 8) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 1 4) + x1} status: [] precedence above: #quote(x1) weight: x1 status: [x1] precedence above: sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: |01|() weight: 0 status: [] precedence above: s1(x1) weight: (/ 1 8) status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #7 Number of SCCs: 1, DPs: 23, edges: 187 SCC { #2..6 #10 #11 #16..23 #25 #26 #28..31 #34 #35 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. |0|() weight: (/ 1 16) #dbl1(x1) 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{(/ 5 16) + x2, (/ 3 8) + x1} n__indx(x1,x2) weight: max{(/ 5 16) + 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 #sel(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} #indx(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 16) + x1} sel(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} from(x1) weight: (/ 1 8) + x1 #s(x1) weight: 0 nil() weight: (/ 3 8) dbl1(x1) weight: 0 #sel1(x1,x2) weight: 0 n__sel(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + 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 |01|() weight: 0 s1(x1) weight: 0 Usable rules: { 1..9 18..30 } Removed DPs: #2 #3 #5 #6 #10 #11 #16..20 #22 #23 #25 #26 #28..31 #34 #35 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. |0|() weight: (/ 1 8) status: [] precedence above: #dbl1(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: s(x1) weight: x1 status: [x1] precedence above: activate n__s #sel1 cons dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: activate n__dbls #sel1 cons activate(x1) weight: x1 status: x1 dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate n__s n__dbl #sel1 cons indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate n__indx n__s sel nil #sel1 n__sel cons n__indx(x1,x2) weight: (/ 3 4) + x2 status: [] precedence above: s activate indx n__s sel nil #sel1 n__sel cons n__from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__s from #sel1 cons #dbl(x1) weight: x1 status: [] precedence above: #activate(x1) weight: (/ 1 8) status: [] precedence above: #dbls(x1) weight: x1 status: [] precedence above: n__dbls(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: dbls activate #sel1 cons n__s(x1) weight: x1 status: [x1] precedence above: s activate #sel1 cons n__dbl(x1) weight: (/ 1 8) + x1 status: [x1] precedence above: |0| s activate dbl n__s #sel1 cons #sel(x1,x2) weight: x1 status: [x1] precedence above: cons #indx(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1,x2] precedence above: sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s #sel1 n__sel cons from(x1) weight: (/ 3 8) + x1 status: [x1] precedence above: s activate n__from n__s #sel1 cons #s(x1) weight: (/ 1 8) status: [] precedence above: nil() weight: (/ 1 8) status: [] precedence above: dbl1(x1) weight: x1 status: [] precedence above: #sel1(x1,x2) weight: x1 status: [x1] precedence above: n__sel(x1,x2) weight: (/ 3 8) + x2 status: [] precedence above: s activate n__s sel #sel1 cons #from(x1) weight: (/ 1 8) status: [] precedence above: quote(x1) weight: (/ 1 8) status: [] precedence above: cons(x1,x2) weight: max{x2, (/ 1 4) + x1} status: [] precedence above: #quote(x1) weight: x1 status: [x1] precedence above: sel1(x1,x2) weight: (/ 1 8) status: [] precedence above: |01|() weight: 0 status: [] precedence above: s1(x1) weight: (/ 1 8) status: [] precedence above: Usable rules: { 1..9 18..30 } Removed DPs: #4 Number of SCCs: 0, DPs: 0, edges: 0 YES