MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),x,y,lists) -> s2bin2(x,lists) if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists)) if2(false(),x,xs,ys) -> s2bin2(x,ys) if2(true(),x,xs,ys) -> xs log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() s2bin(x) -> s2bin1(x,0(),cons(nil(),nil())) s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists) s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys) s2bin2(x,nil()) -> bug_list_not() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2} / {0/0,1/0 ,bug_list_not/0,cons/2,double/1,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s,bin2ss,eq,half,if1,if2,log,lt,more,s2bin,s2bin1 ,s2bin2} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2s#(nil()) -> c_2() bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) bin2ss#(x,nil()) -> c_5() eq#(0(),0()) -> c_6() eq#(0(),s(y)) -> c_7() eq#(s(x),0()) -> c_8() eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(0()) -> c_10() half#(s(0())) -> c_11() half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) if2#(true(),x,xs,ys) -> c_16() log#(0()) -> c_17() log#(s(0())) -> c_18() log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(x,0()) -> c_20() lt#(0(),s(y)) -> c_21() lt#(s(x),s(y)) -> c_22(lt#(x,y)) more#(cons(xs,ys)) -> c_23() more#(nil()) -> c_24() s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) s2bin2#(x,nil()) -> c_28() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2s#(nil()) -> c_2() bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) bin2ss#(x,nil()) -> c_5() eq#(0(),0()) -> c_6() eq#(0(),s(y)) -> c_7() eq#(s(x),0()) -> c_8() eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(0()) -> c_10() half#(s(0())) -> c_11() half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) if2#(true(),x,xs,ys) -> c_16() log#(0()) -> c_17() log#(s(0())) -> c_18() log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(x,0()) -> c_20() lt#(0(),s(y)) -> c_21() lt#(s(x),s(y)) -> c_22(lt#(x,y)) more#(cons(xs,ys)) -> c_23() more#(nil()) -> c_24() s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) s2bin2#(x,nil()) -> c_28() - Weak TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),x,y,lists) -> s2bin2(x,lists) if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists)) if2(false(),x,xs,ys) -> s2bin2(x,ys) if2(true(),x,xs,ys) -> xs log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() s2bin(x) -> s2bin1(x,0(),cons(nil(),nil())) s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists) s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys) s2bin2(x,nil()) -> bug_list_not() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2,bin2s#/1,bin2ss#/2 ,eq#/2,half#/1,if1#/4,if2#/4,log#/1,lt#/2,more#/1,s2bin#/1,s2bin1#/3,s2bin2#/2} / {0/0,1/0,bug_list_not/0 ,cons/2,double/1,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/0,c_12/1,c_13/1,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/2,c_20/0,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1 ,c_26/3,c_27/3,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin# ,s2bin1#,s2bin2#} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2s#(nil()) -> c_2() bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) bin2ss#(x,nil()) -> c_5() eq#(0(),0()) -> c_6() eq#(0(),s(y)) -> c_7() eq#(s(x),0()) -> c_8() eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(0()) -> c_10() half#(s(0())) -> c_11() half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) if2#(true(),x,xs,ys) -> c_16() log#(0()) -> c_17() log#(s(0())) -> c_18() log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(x,0()) -> c_20() lt#(0(),s(y)) -> c_21() lt#(s(x),s(y)) -> c_22(lt#(x,y)) more#(cons(xs,ys)) -> c_23() more#(nil()) -> c_24() s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) s2bin2#(x,nil()) -> c_28() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2s#(nil()) -> c_2() bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) bin2ss#(x,nil()) -> c_5() eq#(0(),0()) -> c_6() eq#(0(),s(y)) -> c_7() eq#(s(x),0()) -> c_8() eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(0()) -> c_10() half#(s(0())) -> c_11() half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) if2#(true(),x,xs,ys) -> c_16() log#(0()) -> c_17() log#(s(0())) -> c_18() log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(x,0()) -> c_20() lt#(0(),s(y)) -> c_21() lt#(s(x),s(y)) -> c_22(lt#(x,y)) more#(cons(xs,ys)) -> c_23() more#(nil()) -> c_24() s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) s2bin2#(x,nil()) -> c_28() - Weak TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2,bin2s#/1,bin2ss#/2 ,eq#/2,half#/1,if1#/4,if2#/4,log#/1,lt#/2,more#/1,s2bin#/1,s2bin1#/3,s2bin2#/2} / {0/0,1/0,bug_list_not/0 ,cons/2,double/1,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/0,c_12/1,c_13/1,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/2,c_20/0,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1 ,c_26/3,c_27/3,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin# ,s2bin1#,s2bin2#} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,5,6,7,8,10,11,16,17,18,20,21,23,24,28} by application of Pre({2,5,6,7,8,10,11,16,17,18,20,21,23,24,28}) = {1,3,4,9,12,13,14,15,19,22,26,27}. Here rules are labelled as follows: 1: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) 2: bin2s#(nil()) -> c_2() 3: bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) 4: bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) 5: bin2ss#(x,nil()) -> c_5() 6: eq#(0(),0()) -> c_6() 7: eq#(0(),s(y)) -> c_7() 8: eq#(s(x),0()) -> c_8() 9: eq#(s(x),s(y)) -> c_9(eq#(x,y)) 10: half#(0()) -> c_10() 11: half#(s(0())) -> c_11() 12: half#(s(s(x))) -> c_12(half#(x)) 13: if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) 14: if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) 15: if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) 16: if2#(true(),x,xs,ys) -> c_16() 17: log#(0()) -> c_17() 18: log#(s(0())) -> c_18() 19: log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) 20: lt#(x,0()) -> c_20() 21: lt#(0(),s(y)) -> c_21() 22: lt#(s(x),s(y)) -> c_22(lt#(x,y)) 23: more#(cons(xs,ys)) -> c_23() 24: more#(nil()) -> c_24() 25: s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) 26: s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) 27: s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) 28: s2bin2#(x,nil()) -> c_28() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(s(x),s(y)) -> c_22(lt#(x,y)) s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) - Weak DPs: bin2s#(nil()) -> c_2() bin2ss#(x,nil()) -> c_5() eq#(0(),0()) -> c_6() eq#(0(),s(y)) -> c_7() eq#(s(x),0()) -> c_8() half#(0()) -> c_10() half#(s(0())) -> c_11() if2#(true(),x,xs,ys) -> c_16() log#(0()) -> c_17() log#(s(0())) -> c_18() lt#(x,0()) -> c_20() lt#(0(),s(y)) -> c_21() more#(cons(xs,ys)) -> c_23() more#(nil()) -> c_24() s2bin2#(x,nil()) -> c_28() - Weak TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2,bin2s#/1,bin2ss#/2 ,eq#/2,half#/1,if1#/4,if2#/4,log#/1,lt#/2,more#/1,s2bin#/1,s2bin1#/3,s2bin2#/2} / {0/0,1/0,bug_list_not/0 ,cons/2,double/1,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/0,c_12/1,c_13/1,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/2,c_20/0,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1 ,c_26/3,c_27/3,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin# ,s2bin1#,s2bin2#} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 -->_1 bin2ss#(x,nil()) -> c_5():15 2:S:bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,nil()) -> c_5():15 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 3:S:bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) -->_1 bin2ss#(x,nil()) -> c_5():15 -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 4:S:eq#(s(x),s(y)) -> c_9(eq#(x,y)) -->_1 eq#(s(x),0()) -> c_8():18 -->_1 eq#(0(),s(y)) -> c_7():17 -->_1 eq#(0(),0()) -> c_6():16 -->_1 eq#(s(x),s(y)) -> c_9(eq#(x,y)):4 5:S:half#(s(s(x))) -> c_12(half#(x)) -->_1 half#(s(0())) -> c_11():20 -->_1 half#(0()) -> c_10():19 -->_1 half#(s(s(x))) -> c_12(half#(x)):5 6:S:if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) -->_1 s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)):13 -->_1 s2bin2#(x,nil()) -> c_28():28 7:S:if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) -->_1 s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)):12 -->_2 more#(nil()) -> c_24():27 -->_2 more#(cons(xs,ys)) -> c_23():26 8:S:if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) -->_1 s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)):13 -->_1 s2bin2#(x,nil()) -> c_28():28 9:S:log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) -->_1 log#(s(0())) -> c_18():23 -->_1 log#(0()) -> c_17():22 -->_1 log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))):9 -->_2 half#(s(s(x))) -> c_12(half#(x)):5 10:S:lt#(s(x),s(y)) -> c_22(lt#(x,y)) -->_1 lt#(0(),s(y)) -> c_21():25 -->_1 lt#(x,0()) -> c_20():24 -->_1 lt#(s(x),s(y)) -> c_22(lt#(x,y)):10 11:S:s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) -->_1 s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)):12 12:S:s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) -->_2 lt#(0(),s(y)) -> c_21():25 -->_2 lt#(x,0()) -> c_20():24 -->_3 log#(s(0())) -> c_18():23 -->_3 log#(0()) -> c_17():22 -->_2 lt#(s(x),s(y)) -> c_22(lt#(x,y)):10 -->_3 log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))):9 -->_1 if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)):7 -->_1 if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)):6 13:S:s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) -->_1 if2#(true(),x,xs,ys) -> c_16():21 -->_2 eq#(s(x),0()) -> c_8():18 -->_2 eq#(0(),s(y)) -> c_7():17 -->_2 eq#(0(),0()) -> c_6():16 -->_3 bin2s#(nil()) -> c_2():14 -->_1 if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)):8 -->_2 eq#(s(x),s(y)) -> c_9(eq#(x,y)):4 -->_3 bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)):1 14:W:bin2s#(nil()) -> c_2() 15:W:bin2ss#(x,nil()) -> c_5() 16:W:eq#(0(),0()) -> c_6() 17:W:eq#(0(),s(y)) -> c_7() 18:W:eq#(s(x),0()) -> c_8() 19:W:half#(0()) -> c_10() 20:W:half#(s(0())) -> c_11() 21:W:if2#(true(),x,xs,ys) -> c_16() 22:W:log#(0()) -> c_17() 23:W:log#(s(0())) -> c_18() 24:W:lt#(x,0()) -> c_20() 25:W:lt#(0(),s(y)) -> c_21() 26:W:more#(cons(xs,ys)) -> c_23() 27:W:more#(nil()) -> c_24() 28:W:s2bin2#(x,nil()) -> c_28() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 26: more#(cons(xs,ys)) -> c_23() 27: more#(nil()) -> c_24() 22: log#(0()) -> c_17() 23: log#(s(0())) -> c_18() 24: lt#(x,0()) -> c_20() 25: lt#(0(),s(y)) -> c_21() 28: s2bin2#(x,nil()) -> c_28() 14: bin2s#(nil()) -> c_2() 21: if2#(true(),x,xs,ys) -> c_16() 19: half#(0()) -> c_10() 20: half#(s(0())) -> c_11() 16: eq#(0(),0()) -> c_6() 17: eq#(0(),s(y)) -> c_7() 18: eq#(s(x),0()) -> c_8() 15: bin2ss#(x,nil()) -> c_5() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(s(x),s(y)) -> c_22(lt#(x,y)) s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) - Weak TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2,bin2s#/1,bin2ss#/2 ,eq#/2,half#/1,if1#/4,if2#/4,log#/1,lt#/2,more#/1,s2bin#/1,s2bin1#/3,s2bin2#/2} / {0/0,1/0,bug_list_not/0 ,cons/2,double/1,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/0,c_12/1,c_13/1,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/2,c_20/0,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1 ,c_26/3,c_27/3,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin# ,s2bin1#,s2bin2#} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 2:S:bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 3:S:bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 4:S:eq#(s(x),s(y)) -> c_9(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_9(eq#(x,y)):4 5:S:half#(s(s(x))) -> c_12(half#(x)) -->_1 half#(s(s(x))) -> c_12(half#(x)):5 6:S:if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) -->_1 s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)):13 7:S:if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)) -->_1 s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)):12 8:S:if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) -->_1 s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)):13 9:S:log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) -->_1 log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))):9 -->_2 half#(s(s(x))) -> c_12(half#(x)):5 10:S:lt#(s(x),s(y)) -> c_22(lt#(x,y)) -->_1 lt#(s(x),s(y)) -> c_22(lt#(x,y)):10 11:S:s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) -->_1 s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)):12 12:S:s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) -->_2 lt#(s(x),s(y)) -> c_22(lt#(x,y)):10 -->_3 log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))):9 -->_1 if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists)),more#(lists)):7 -->_1 if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)):6 13:S:s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) -->_1 if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)):8 -->_2 eq#(s(x),s(y)) -> c_9(eq#(x,y)):4 -->_3 bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists))) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists))) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(s(x),s(y)) -> c_22(lt#(x,y)) s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) - Weak TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2,bin2s#/1,bin2ss#/2 ,eq#/2,half#/1,if1#/4,if2#/4,log#/1,lt#/2,more#/1,s2bin#/1,s2bin1#/3,s2bin2#/2} / {0/0,1/0,bug_list_not/0 ,cons/2,double/1,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/0,c_12/1,c_13/1,c_14/1,c_15/1,c_16/0,c_17/0,c_18/0,c_19/2,c_20/0,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1 ,c_26/3,c_27/3,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin# ,s2bin1#,s2bin2#} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 2:S:bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 3:S:bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) -->_1 bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)):3 -->_1 bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)):2 4:S:eq#(s(x),s(y)) -> c_9(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_9(eq#(x,y)):4 5:S:half#(s(s(x))) -> c_12(half#(x)) -->_1 half#(s(s(x))) -> c_12(half#(x)):5 6:S:if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) -->_1 s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)):13 7:S:if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists))) -->_1 s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)):12 8:S:if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) -->_1 s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)):13 9:S:log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) -->_1 log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))):9 -->_2 half#(s(s(x))) -> c_12(half#(x)):5 10:S:lt#(s(x),s(y)) -> c_22(lt#(x,y)) -->_1 lt#(s(x),s(y)) -> c_22(lt#(x,y)):10 11:S:s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))) -->_1 s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)):12 12:S:s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) -->_2 lt#(s(x),s(y)) -> c_22(lt#(x,y)):10 -->_3 log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))):9 -->_1 if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists))):7 -->_1 if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)):6 13:S:s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) -->_1 if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)):8 -->_2 eq#(s(x),s(y)) -> c_9(eq#(x,y)):4 -->_3 bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)):1 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(11,s2bin#(x) -> c_25(s2bin1#(x,0(),cons(nil(),nil()))))] * Step 7: NaturalMI MAYBE + Considered Problem: - Strict DPs: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(s(s(x))) -> c_12(half#(x)) if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists))) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(s(x),s(y)) -> c_22(lt#(x,y)) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) - Weak TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2,bin2s#/1,bin2ss#/2 ,eq#/2,half#/1,if1#/4,if2#/4,log#/1,lt#/2,more#/1,s2bin#/1,s2bin1#/3,s2bin2#/2} / {0/0,1/0,bug_list_not/0 ,cons/2,double/1,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/0,c_12/1,c_13/1,c_14/1,c_15/1,c_16/0,c_17/0,c_18/0,c_19/2,c_20/0,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1 ,c_26/3,c_27/3,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin# ,s2bin1#,s2bin2#} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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_1) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_9) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_19) = {1,2}, uargs(c_22) = {1}, uargs(c_26) = {1,2,3}, uargs(c_27) = {1,2,3} Following symbols are considered usable: {eq,lt,more,bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin#,s2bin1#,s2bin2#} TcT has computed the following interpretation: p(0) = [4] p(1) = [4] p(bin2s) = [2] p(bin2ss) = [1] x2 + [0] p(bug_list_not) = [0] p(cons) = [0] p(double) = [0] p(eq) = [1] p(false) = [1] p(half) = [1] x1 + [0] p(if1) = [4] x4 + [0] p(if2) = [4] x1 + [1] x3 + [0] p(log) = [0] p(lt) = [1] p(more) = [0] p(nil) = [0] p(s) = [0] p(s2bin) = [1] x1 + [0] p(s2bin1) = [4] x2 + [1] x3 + [0] p(s2bin2) = [1] x1 + [2] p(true) = [1] p(bin2s#) = [0] p(bin2ss#) = [0] p(eq#) = [0] p(half#) = [0] p(if1#) = [6] x1 + [6] x2 + [0] p(if2#) = [4] x1 + [0] p(log#) = [0] p(lt#) = [0] p(more#) = [1] x1 + [4] p(s2bin#) = [2] p(s2bin1#) = [6] x1 + [4] x3 + [6] p(s2bin2#) = [4] p(c_1) = [4] x1 + [0] p(c_2) = [1] p(c_3) = [2] x1 + [0] p(c_4) = [4] x1 + [0] p(c_5) = [1] p(c_6) = [0] p(c_7) = [2] p(c_8) = [0] p(c_9) = [4] x1 + [0] p(c_10) = [0] p(c_11) = [1] p(c_12) = [4] x1 + [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] p(c_17) = [0] p(c_18) = [1] p(c_19) = [1] x1 + [2] x2 + [0] p(c_20) = [4] p(c_21) = [1] p(c_22) = [4] x1 + [0] p(c_23) = [1] p(c_24) = [0] p(c_25) = [0] p(c_26) = [1] x1 + [4] x2 + [4] x3 + [0] p(c_27) = [1] x1 + [4] x2 + [2] x3 + [0] p(c_28) = [1] Following rules are strictly oriented: if1#(false(),x,y,lists) = [6] x + [6] > [4] = c_13(s2bin2#(x,lists)) Following rules are (at-least) weakly oriented: bin2s#(cons(x,xs)) = [0] >= [0] = c_1(bin2ss#(x,xs)) bin2ss#(x,cons(0(),xs)) = [0] >= [0] = c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) = [0] >= [0] = c_4(bin2ss#(s(double(x)),xs)) eq#(s(x),s(y)) = [0] >= [0] = c_9(eq#(x,y)) half#(s(s(x))) = [0] >= [0] = c_12(half#(x)) if1#(true(),x,y,lists) = [6] x + [6] >= [6] x + [6] = c_14(s2bin1#(x,s(y),more(lists))) if2#(false(),x,xs,ys) = [4] >= [4] = c_15(s2bin2#(x,ys)) log#(s(s(x))) = [0] >= [0] = c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(s(x),s(y)) = [0] >= [0] = c_22(lt#(x,y)) s2bin1#(x,y,lists) = [4] lists + [6] x + [6] >= [6] x + [6] = c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) = [4] >= [4] = c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) eq(0(),0()) = [1] >= [1] = true() eq(0(),s(y)) = [1] >= [1] = false() eq(s(x),0()) = [1] >= [1] = false() eq(s(x),s(y)) = [1] >= [1] = eq(x,y) lt(x,0()) = [1] >= [1] = false() lt(0(),s(y)) = [1] >= [1] = true() lt(s(x),s(y)) = [1] >= [1] = lt(x,y) more(cons(xs,ys)) = [0] >= [0] = cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) = [0] >= [0] = nil() * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: bin2s#(cons(x,xs)) -> c_1(bin2ss#(x,xs)) bin2ss#(x,cons(0(),xs)) -> c_3(bin2ss#(double(x),xs)) bin2ss#(x,cons(1(),xs)) -> c_4(bin2ss#(s(double(x)),xs)) eq#(s(x),s(y)) -> c_9(eq#(x,y)) half#(s(s(x))) -> c_12(half#(x)) if1#(true(),x,y,lists) -> c_14(s2bin1#(x,s(y),more(lists))) if2#(false(),x,xs,ys) -> c_15(s2bin2#(x,ys)) log#(s(s(x))) -> c_19(log#(half(s(s(x)))),half#(s(s(x)))) lt#(s(x),s(y)) -> c_22(lt#(x,y)) s2bin1#(x,y,lists) -> c_26(if1#(lt(y,log(x)),x,y,lists),lt#(y,log(x)),log#(x)) s2bin2#(x,cons(xs,ys)) -> c_27(if2#(eq(x,bin2s(xs)),x,xs,ys),eq#(x,bin2s(xs)),bin2s#(xs)) - Weak DPs: if1#(false(),x,y,lists) -> c_13(s2bin2#(x,lists)) - Weak TRS: bin2s(cons(x,xs)) -> bin2ss(x,xs) bin2s(nil()) -> 0() bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs) bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs) bin2ss(x,nil()) -> x eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) log(0()) -> 0() log(s(0())) -> 0() log(s(s(x))) -> s(log(half(s(s(x))))) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys))) more(nil()) -> nil() - Signature: {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2,bin2s#/1,bin2ss#/2 ,eq#/2,half#/1,if1#/4,if2#/4,log#/1,lt#/2,more#/1,s2bin#/1,s2bin1#/3,s2bin2#/2} / {0/0,1/0,bug_list_not/0 ,cons/2,double/1,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/0,c_12/1,c_13/1,c_14/1,c_15/1,c_16/0,c_17/0,c_18/0,c_19/2,c_20/0,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1 ,c_26/3,c_27/3,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {bin2s#,bin2ss#,eq#,half#,if1#,if2#,log#,lt#,more#,s2bin# ,s2bin1#,s2bin2#} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE