MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: del(x,cons(y,xs)) -> if(eq(x,y),x,y,xs) del(x,nil()) -> nil() double(0()) -> 0() double(s(x)) -> s(s(double(x))) doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs)))) doublelist(nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) first(cons(x,xs)) -> x first(nil()) -> 0() if(false(),x,y,xs) -> cons(y,del(x,xs)) if(true(),x,y,xs) -> xs - Signature: {del/2,double/1,doublelist/1,eq/2,first/1,if/4} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {del,double,doublelist,eq,first,if} and constructors {0 ,cons,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) del#(x,nil()) -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) doublelist#(nil()) -> c_6() eq#(0(),0()) -> c_7() eq#(0(),s(y)) -> c_8() eq#(s(x),0()) -> c_9() eq#(s(x),s(y)) -> c_10(eq#(x,y)) first#(cons(x,xs)) -> c_11() first#(nil()) -> c_12() if#(false(),x,y,xs) -> c_13(del#(x,xs)) if#(true(),x,y,xs) -> c_14() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) del#(x,nil()) -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) doublelist#(nil()) -> c_6() eq#(0(),0()) -> c_7() eq#(0(),s(y)) -> c_8() eq#(s(x),0()) -> c_9() eq#(s(x),s(y)) -> c_10(eq#(x,y)) first#(cons(x,xs)) -> c_11() first#(nil()) -> c_12() if#(false(),x,y,xs) -> c_13(del#(x,xs)) if#(true(),x,y,xs) -> c_14() - Weak TRS: del(x,cons(y,xs)) -> if(eq(x,y),x,y,xs) del(x,nil()) -> nil() double(0()) -> 0() double(s(x)) -> s(s(double(x))) doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs)))) doublelist(nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) first(cons(x,xs)) -> x first(nil()) -> 0() if(false(),x,y,xs) -> cons(y,del(x,xs)) if(true(),x,y,xs) -> xs - Signature: {del/2,double/1,doublelist/1,eq/2,first/1,if/4,del#/2,double#/1,doublelist#/1,eq#/2,first#/1,if#/4} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/4,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0 ,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {del#,double#,doublelist#,eq#,first# ,if#} and constructors {0,cons,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: del(x,cons(y,xs)) -> if(eq(x,y),x,y,xs) del(x,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) first(cons(x,xs)) -> x if(false(),x,y,xs) -> cons(y,del(x,xs)) if(true(),x,y,xs) -> xs del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) del#(x,nil()) -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) doublelist#(nil()) -> c_6() eq#(0(),0()) -> c_7() eq#(0(),s(y)) -> c_8() eq#(s(x),0()) -> c_9() eq#(s(x),s(y)) -> c_10(eq#(x,y)) first#(cons(x,xs)) -> c_11() first#(nil()) -> c_12() if#(false(),x,y,xs) -> c_13(del#(x,xs)) if#(true(),x,y,xs) -> c_14() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) del#(x,nil()) -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) doublelist#(nil()) -> c_6() eq#(0(),0()) -> c_7() eq#(0(),s(y)) -> c_8() eq#(s(x),0()) -> c_9() eq#(s(x),s(y)) -> c_10(eq#(x,y)) first#(cons(x,xs)) -> c_11() first#(nil()) -> c_12() if#(false(),x,y,xs) -> c_13(del#(x,xs)) if#(true(),x,y,xs) -> c_14() - Weak TRS: del(x,cons(y,xs)) -> if(eq(x,y),x,y,xs) del(x,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) first(cons(x,xs)) -> x if(false(),x,y,xs) -> cons(y,del(x,xs)) if(true(),x,y,xs) -> xs - Signature: {del/2,double/1,doublelist/1,eq/2,first/1,if/4,del#/2,double#/1,doublelist#/1,eq#/2,first#/1,if#/4} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/4,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0 ,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {del#,double#,doublelist#,eq#,first# ,if#} and constructors {0,cons,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,6,7,8,9,11,12,14} by application of Pre({2,3,6,7,8,9,11,12,14}) = {1,4,5,10,13}. Here rules are labelled as follows: 1: del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) 2: del#(x,nil()) -> c_2() 3: double#(0()) -> c_3() 4: double#(s(x)) -> c_4(double#(x)) 5: doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) 6: doublelist#(nil()) -> c_6() 7: eq#(0(),0()) -> c_7() 8: eq#(0(),s(y)) -> c_8() 9: eq#(s(x),0()) -> c_9() 10: eq#(s(x),s(y)) -> c_10(eq#(x,y)) 11: first#(cons(x,xs)) -> c_11() 12: first#(nil()) -> c_12() 13: if#(false(),x,y,xs) -> c_13(del#(x,xs)) 14: if#(true(),x,y,xs) -> c_14() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) double#(s(x)) -> c_4(double#(x)) doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) eq#(s(x),s(y)) -> c_10(eq#(x,y)) if#(false(),x,y,xs) -> c_13(del#(x,xs)) - Weak DPs: del#(x,nil()) -> c_2() double#(0()) -> c_3() doublelist#(nil()) -> c_6() eq#(0(),0()) -> c_7() eq#(0(),s(y)) -> c_8() eq#(s(x),0()) -> c_9() first#(cons(x,xs)) -> c_11() first#(nil()) -> c_12() if#(true(),x,y,xs) -> c_14() - Weak TRS: del(x,cons(y,xs)) -> if(eq(x,y),x,y,xs) del(x,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) first(cons(x,xs)) -> x if(false(),x,y,xs) -> cons(y,del(x,xs)) if(true(),x,y,xs) -> xs - Signature: {del/2,double/1,doublelist/1,eq/2,first/1,if/4,del#/2,double#/1,doublelist#/1,eq#/2,first#/1,if#/4} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/4,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0 ,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {del#,double#,doublelist#,eq#,first# ,if#} and constructors {0,cons,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) -->_1 if#(false(),x,y,xs) -> c_13(del#(x,xs)):5 -->_2 eq#(s(x),s(y)) -> c_10(eq#(x,y)):4 -->_1 if#(true(),x,y,xs) -> c_14():14 -->_2 eq#(s(x),0()) -> c_9():11 -->_2 eq#(0(),s(y)) -> c_8():10 -->_2 eq#(0(),0()) -> c_7():9 2:S:double#(s(x)) -> c_4(double#(x)) -->_1 double#(0()) -> c_3():7 -->_1 double#(s(x)) -> c_4(double#(x)):2 3:S:doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) -->_4 first#(cons(x,xs)) -> c_11():12 -->_2 doublelist#(nil()) -> c_6():8 -->_1 double#(0()) -> c_3():7 -->_2 doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))):3 -->_1 double#(s(x)) -> c_4(double#(x)):2 -->_3 del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)):1 4:S:eq#(s(x),s(y)) -> c_10(eq#(x,y)) -->_1 eq#(s(x),0()) -> c_9():11 -->_1 eq#(0(),s(y)) -> c_8():10 -->_1 eq#(0(),0()) -> c_7():9 -->_1 eq#(s(x),s(y)) -> c_10(eq#(x,y)):4 5:S:if#(false(),x,y,xs) -> c_13(del#(x,xs)) -->_1 del#(x,nil()) -> c_2():6 -->_1 del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)):1 6:W:del#(x,nil()) -> c_2() 7:W:double#(0()) -> c_3() 8:W:doublelist#(nil()) -> c_6() 9:W:eq#(0(),0()) -> c_7() 10:W:eq#(0(),s(y)) -> c_8() 11:W:eq#(s(x),0()) -> c_9() 12:W:first#(cons(x,xs)) -> c_11() 13:W:first#(nil()) -> c_12() 14:W:if#(true(),x,y,xs) -> c_14() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: first#(nil()) -> c_12() 8: doublelist#(nil()) -> c_6() 12: first#(cons(x,xs)) -> c_11() 7: double#(0()) -> c_3() 14: if#(true(),x,y,xs) -> c_14() 9: eq#(0(),0()) -> c_7() 10: eq#(0(),s(y)) -> c_8() 11: eq#(s(x),0()) -> c_9() 6: del#(x,nil()) -> c_2() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) double#(s(x)) -> c_4(double#(x)) doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) eq#(s(x),s(y)) -> c_10(eq#(x,y)) if#(false(),x,y,xs) -> c_13(del#(x,xs)) - Weak TRS: del(x,cons(y,xs)) -> if(eq(x,y),x,y,xs) del(x,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) first(cons(x,xs)) -> x if(false(),x,y,xs) -> cons(y,del(x,xs)) if(true(),x,y,xs) -> xs - Signature: {del/2,double/1,doublelist/1,eq/2,first/1,if/4,del#/2,double#/1,doublelist#/1,eq#/2,first#/1,if#/4} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/4,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0 ,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {del#,double#,doublelist#,eq#,first# ,if#} and constructors {0,cons,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) -->_1 if#(false(),x,y,xs) -> c_13(del#(x,xs)):5 -->_2 eq#(s(x),s(y)) -> c_10(eq#(x,y)):4 2:S:double#(s(x)) -> c_4(double#(x)) -->_1 double#(s(x)) -> c_4(double#(x)):2 3:S:doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))) -->_2 doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs)) ,first#(cons(x,xs))):3 -->_1 double#(s(x)) -> c_4(double#(x)):2 -->_3 del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)):1 4:S:eq#(s(x),s(y)) -> c_10(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_10(eq#(x,y)):4 5:S:if#(false(),x,y,xs) -> c_13(del#(x,xs)) -->_1 del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs))) * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: del#(x,cons(y,xs)) -> c_1(if#(eq(x,y),x,y,xs),eq#(x,y)) double#(s(x)) -> c_4(double#(x)) doublelist#(cons(x,xs)) -> c_5(double#(x) ,doublelist#(del(first(cons(x,xs)),cons(x,xs))) ,del#(first(cons(x,xs)),cons(x,xs))) eq#(s(x),s(y)) -> c_10(eq#(x,y)) if#(false(),x,y,xs) -> c_13(del#(x,xs)) - Weak TRS: del(x,cons(y,xs)) -> if(eq(x,y),x,y,xs) del(x,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) first(cons(x,xs)) -> x if(false(),x,y,xs) -> cons(y,del(x,xs)) if(true(),x,y,xs) -> xs - Signature: {del/2,double/1,doublelist/1,eq/2,first/1,if/4,del#/2,double#/1,doublelist#/1,eq#/2,first#/1,if#/4} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/3,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0 ,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {del#,double#,doublelist#,eq#,first# ,if#} and constructors {0,cons,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE