MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: fcons(X,Z) -> cons(X,Z) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z)) from(X) -> cons(X,from(s(X))) quote(0()) -> 01() quote(s(X)) -> s1(quote(X)) quote(sel(X,Z)) -> sel1(X,Z) quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z)) quote1(first(X,Z)) -> first1(X,Z) quote1(nil()) -> nil1() sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) sel1(0(),cons(X,Z)) -> quote(X) sel1(s(X),cons(Y,Z)) -> sel1(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1} / {0/0,01/0,cons/2 ,cons1/2,nil/0,nil1/0,s/1,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {fcons,first,first1,from,quote,quote1,sel,sel1,unquote ,unquote1} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs fcons#(X,Z) -> c_1() first#(0(),Z) -> c_2() first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(0(),Z) -> c_4() first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(0()) -> c_7() quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) quote1#(nil()) -> c_12() sel#(0(),cons(X,Z)) -> c_13() sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(01()) -> c_17() unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_20() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: fcons#(X,Z) -> c_1() first#(0(),Z) -> c_2() first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(0(),Z) -> c_4() first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(0()) -> c_7() quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) quote1#(nil()) -> c_12() sel#(0(),cons(X,Z)) -> c_13() sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(01()) -> c_17() unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_20() - Weak TRS: fcons(X,Z) -> cons(X,Z) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z)) from(X) -> cons(X,from(s(X))) quote(0()) -> 01() quote(s(X)) -> s1(quote(X)) quote(sel(X,Z)) -> sel1(X,Z) quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z)) quote1(first(X,Z)) -> first1(X,Z) quote1(nil()) -> nil1() sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) sel1(0(),cons(X,Z)) -> quote(X) sel1(s(X),cons(Y,Z)) -> sel1(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1,fcons#/2,first#/2 ,first1#/2,from#/1,quote#/1,quote1#/1,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {0/0,01/0,cons/2,cons1/2 ,nil/0,nil1/0,s/1,s1/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/1,c_10/2,c_11/1,c_12/0,c_13/0 ,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/3,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {fcons#,first#,first1#,from#,quote#,quote1#,sel#,sel1# ,unquote#,unquote1#} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: fcons(X,Z) -> cons(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() fcons#(X,Z) -> c_1() first#(0(),Z) -> c_2() first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(0(),Z) -> c_4() first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(0()) -> c_7() quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) quote1#(nil()) -> c_12() sel#(0(),cons(X,Z)) -> c_13() sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(01()) -> c_17() unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_20() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: fcons#(X,Z) -> c_1() first#(0(),Z) -> c_2() first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(0(),Z) -> c_4() first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(0()) -> c_7() quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) quote1#(nil()) -> c_12() sel#(0(),cons(X,Z)) -> c_13() sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(01()) -> c_17() unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_20() - Weak TRS: fcons(X,Z) -> cons(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1,fcons#/2,first#/2 ,first1#/2,from#/1,quote#/1,quote1#/1,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {0/0,01/0,cons/2,cons1/2 ,nil/0,nil1/0,s/1,s1/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/1,c_10/2,c_11/1,c_12/0,c_13/0 ,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/3,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {fcons#,first#,first1#,from#,quote#,quote1#,sel#,sel1# ,unquote#,unquote1#} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,4,7,12,13,17,20} by application of Pre({1,2,4,7,12,13,17,20}) = {3,5,8,10,11,14,15,18,19}. Here rules are labelled as follows: 1: fcons#(X,Z) -> c_1() 2: first#(0(),Z) -> c_2() 3: first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) 4: first1#(0(),Z) -> c_4() 5: first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) 6: from#(X) -> c_6(from#(s(X))) 7: quote#(0()) -> c_7() 8: quote#(s(X)) -> c_8(quote#(X)) 9: quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) 10: quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) 11: quote1#(first(X,Z)) -> c_11(first1#(X,Z)) 12: quote1#(nil()) -> c_12() 13: sel#(0(),cons(X,Z)) -> c_13() 14: sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) 15: sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) 16: sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) 17: unquote#(01()) -> c_17() 18: unquote#(s1(X)) -> c_18(unquote#(X)) 19: unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) 20: unquote1#(nil1()) -> c_20() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) - Weak DPs: fcons#(X,Z) -> c_1() first#(0(),Z) -> c_2() first1#(0(),Z) -> c_4() quote#(0()) -> c_7() quote1#(nil()) -> c_12() sel#(0(),cons(X,Z)) -> c_13() unquote#(01()) -> c_17() unquote1#(nil1()) -> c_20() - Weak TRS: fcons(X,Z) -> cons(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1,fcons#/2,first#/2 ,first1#/2,from#/1,quote#/1,quote1#/1,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {0/0,01/0,cons/2,cons1/2 ,nil/0,nil1/0,s/1,s1/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/1,c_10/2,c_11/1,c_12/0,c_13/0 ,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/3,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {fcons#,first#,first1#,from#,quote#,quote1#,sel#,sel1# ,unquote#,unquote1#} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) -->_1 first#(0(),Z) -> c_2():14 -->_1 first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)):1 2:S:first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 -->_1 quote#(0()) -> c_7():16 -->_2 first1#(0(),Z) -> c_4():15 -->_2 first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)):2 3:S:from#(X) -> c_6(from#(s(X))) -->_1 from#(X) -> c_6(from#(s(X))):3 4:S:quote#(s(X)) -> c_8(quote#(X)) -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(0()) -> c_7():16 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 5:S:quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) -->_1 sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)):10 -->_1 sel1#(0(),cons(X,Z)) -> c_15(quote#(X)):9 6:S:quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) -->_2 quote1#(first(X,Z)) -> c_11(first1#(X,Z)):7 -->_2 quote1#(nil()) -> c_12():17 -->_1 quote#(0()) -> c_7():16 -->_2 quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)):6 -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 7:S:quote1#(first(X,Z)) -> c_11(first1#(X,Z)) -->_1 first1#(0(),Z) -> c_4():15 -->_1 first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)):2 8:S:sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) -->_1 sel#(0(),cons(X,Z)) -> c_13():18 -->_1 sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)):8 9:S:sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) -->_1 quote#(0()) -> c_7():16 -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 10:S:sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) -->_1 sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)):10 -->_1 sel1#(0(),cons(X,Z)) -> c_15(quote#(X)):9 11:S:unquote#(s1(X)) -> c_18(unquote#(X)) -->_1 unquote#(01()) -> c_17():19 -->_1 unquote#(s1(X)) -> c_18(unquote#(X)):11 12:S:unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) -->_3 unquote1#(nil1()) -> c_20():20 -->_2 unquote#(01()) -> c_17():19 -->_1 fcons#(X,Z) -> c_1():13 -->_3 unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)):12 -->_2 unquote#(s1(X)) -> c_18(unquote#(X)):11 13:W:fcons#(X,Z) -> c_1() 14:W:first#(0(),Z) -> c_2() 15:W:first1#(0(),Z) -> c_4() 16:W:quote#(0()) -> c_7() 17:W:quote1#(nil()) -> c_12() 18:W:sel#(0(),cons(X,Z)) -> c_13() 19:W:unquote#(01()) -> c_17() 20:W:unquote1#(nil1()) -> c_20() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: fcons#(X,Z) -> c_1() 20: unquote1#(nil1()) -> c_20() 19: unquote#(01()) -> c_17() 18: sel#(0(),cons(X,Z)) -> c_13() 17: quote1#(nil()) -> c_12() 15: first1#(0(),Z) -> c_4() 16: quote#(0()) -> c_7() 14: first#(0(),Z) -> c_2() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) - Weak TRS: fcons(X,Z) -> cons(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1,fcons#/2,first#/2 ,first1#/2,from#/1,quote#/1,quote1#/1,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {0/0,01/0,cons/2,cons1/2 ,nil/0,nil1/0,s/1,s1/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/1,c_10/2,c_11/1,c_12/0,c_13/0 ,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/3,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {fcons#,first#,first1#,from#,quote#,quote1#,sel#,sel1# ,unquote#,unquote1#} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) -->_1 first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)):1 2:S:first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 -->_2 first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)):2 3:S:from#(X) -> c_6(from#(s(X))) -->_1 from#(X) -> c_6(from#(s(X))):3 4:S:quote#(s(X)) -> c_8(quote#(X)) -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 5:S:quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) -->_1 sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)):10 -->_1 sel1#(0(),cons(X,Z)) -> c_15(quote#(X)):9 6:S:quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) -->_2 quote1#(first(X,Z)) -> c_11(first1#(X,Z)):7 -->_2 quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)):6 -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 7:S:quote1#(first(X,Z)) -> c_11(first1#(X,Z)) -->_1 first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)):2 8:S:sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) -->_1 sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)):8 9:S:sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) -->_1 quote#(sel(X,Z)) -> c_9(sel1#(X,Z)):5 -->_1 quote#(s(X)) -> c_8(quote#(X)):4 10:S:sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) -->_1 sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)):10 -->_1 sel1#(0(),cons(X,Z)) -> c_15(quote#(X)):9 11:S:unquote#(s1(X)) -> c_18(unquote#(X)) -->_1 unquote#(s1(X)) -> c_18(unquote#(X)):11 12:S:unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) -->_3 unquote1#(cons1(X,Z)) -> c_19(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)):12 -->_2 unquote#(s1(X)) -> c_18(unquote#(X)):11 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: unquote1#(cons1(X,Z)) -> c_19(unquote#(X),unquote1#(Z)) * Step 6: UsableRules MAYBE + Considered Problem: - Strict DPs: first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(unquote#(X),unquote1#(Z)) - Weak TRS: fcons(X,Z) -> cons(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1,fcons#/2,first#/2 ,first1#/2,from#/1,quote#/1,quote1#/1,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {0/0,01/0,cons/2,cons1/2 ,nil/0,nil1/0,s/1,s1/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/1,c_10/2,c_11/1,c_12/0,c_13/0 ,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/2,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {fcons#,first#,first1#,from#,quote#,quote1#,sel#,sel1# ,unquote#,unquote1#} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(unquote#(X),unquote1#(Z)) * Step 7: WeightGap MAYBE + Considered Problem: - Strict DPs: first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(s(X)) -> c_8(quote#(X)) quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(unquote#(X),unquote1#(Z)) - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1,fcons#/2,first#/2 ,first1#/2,from#/1,quote#/1,quote1#/1,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {0/0,01/0,cons/2,cons1/2 ,nil/0,nil1/0,s/1,s1/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/1,c_10/2,c_11/1,c_12/0,c_13/0 ,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/2,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {fcons#,first#,first1#,from#,quote#,quote1#,sel#,sel1# ,unquote#,unquote1#} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_5) = {1,2}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1,2}, uargs(c_11) = {1}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1}, uargs(c_18) = {1}, uargs(c_19) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(01) = [0] p(cons) = [0] p(cons1) = [0] p(fcons) = [0] p(first) = [1] x2 + [0] p(first1) = [1] x1 + [1] p(from) = [0] p(nil) = [0] p(nil1) = [0] p(quote) = [0] p(quote1) = [0] p(s) = [4] p(s1) = [0] p(sel) = [0] p(sel1) = [0] p(unquote) = [0] p(unquote1) = [0] p(fcons#) = [0] p(first#) = [4] p(first1#) = [0] p(from#) = [1] x1 + [0] p(quote#) = [7] p(quote1#) = [3] p(sel#) = [7] p(sel1#) = [4] p(unquote#) = [2] p(unquote1#) = [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [1] x1 + [1] x2 + [3] p(c_6) = [1] x1 + [4] p(c_7) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [2] p(c_10) = [1] x1 + [1] x2 + [5] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [0] p(c_17) = [0] p(c_18) = [1] x1 + [1] p(c_19) = [1] x1 + [1] x2 + [6] p(c_20) = [1] Following rules are strictly oriented: quote#(sel(X,Z)) = [7] > [6] = c_9(sel1#(X,Z)) quote1#(first(X,Z)) = [3] > [0] = c_11(first1#(X,Z)) Following rules are (at-least) weakly oriented: first#(s(X),cons(Y,Z)) = [4] >= [4] = c_3(first#(X,Z)) first1#(s(X),cons(Y,Z)) = [0] >= [10] = c_5(quote#(Y),first1#(X,Z)) from#(X) = [1] X + [0] >= [8] = c_6(from#(s(X))) quote#(s(X)) = [7] >= [7] = c_8(quote#(X)) quote1#(cons(X,Z)) = [3] >= [15] = c_10(quote#(X),quote1#(Z)) sel#(s(X),cons(Y,Z)) = [7] >= [7] = c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) = [4] >= [7] = c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) = [4] >= [4] = c_16(sel1#(X,Z)) unquote#(s1(X)) = [2] >= [3] = c_18(unquote#(X)) unquote1#(cons1(X,Z)) = [1] >= [9] = c_19(unquote#(X),unquote1#(Z)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: first#(s(X),cons(Y,Z)) -> c_3(first#(X,Z)) first1#(s(X),cons(Y,Z)) -> c_5(quote#(Y),first1#(X,Z)) from#(X) -> c_6(from#(s(X))) quote#(s(X)) -> c_8(quote#(X)) quote1#(cons(X,Z)) -> c_10(quote#(X),quote1#(Z)) sel#(s(X),cons(Y,Z)) -> c_14(sel#(X,Z)) sel1#(0(),cons(X,Z)) -> c_15(quote#(X)) sel1#(s(X),cons(Y,Z)) -> c_16(sel1#(X,Z)) unquote#(s1(X)) -> c_18(unquote#(X)) unquote1#(cons1(X,Z)) -> c_19(unquote#(X),unquote1#(Z)) - Weak DPs: quote#(sel(X,Z)) -> c_9(sel1#(X,Z)) quote1#(first(X,Z)) -> c_11(first1#(X,Z)) - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1,fcons#/2,first#/2 ,first1#/2,from#/1,quote#/1,quote1#/1,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {0/0,01/0,cons/2,cons1/2 ,nil/0,nil1/0,s/1,s1/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/1,c_10/2,c_11/1,c_12/0,c_13/0 ,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/2,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {fcons#,first#,first1#,from#,quote#,quote1#,sel#,sel1# ,unquote#,unquote1#} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE