MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalPI {shape = Mixed 3, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: Incompatible MAYBE