MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #equal(@x,@y) -> #eq(@x,@y) #greater(@x,@y) -> #ckgt(#compare(@x,@y)) +(@x,@y) -> #add(@x,@y) firstline(@l) -> firstline#1(@l) firstline#1(::(@x,@xs)) -> ::(#abs(#0()),firstline(@xs)) firstline#1(nil()) -> nil() lcs(@l1,@l2) -> lcs#1(lcstable(@l1,@l2)) lcs#1(@m) -> lcs#2(@m) lcs#2(::(@l1,@_@2)) -> lcs#3(@l1) lcs#2(nil()) -> #abs(#0()) lcs#3(::(@len,@_@1)) -> @len lcs#3(nil()) -> #abs(#0()) lcstable(@l1,@l2) -> lcstable#1(@l1,@l2) lcstable#1(::(@x,@xs),@l2) -> lcstable#2(lcstable(@xs,@l2),@l2,@x) lcstable#1(nil(),@l2) -> ::(firstline(@l2),nil()) lcstable#2(@m,@l2,@x) -> lcstable#3(@m,@l2,@x) lcstable#3(::(@l,@ls),@l2,@x) -> ::(newline(@x,@l,@l2),::(@l,@ls)) lcstable#3(nil(),@l2,@x) -> nil() max(@a,@b) -> max#1(#greater(@a,@b),@a,@b) max#1(#false(),@a,@b) -> @b max#1(#true(),@a,@b) -> @a newline(@y,@lastline,@l) -> newline#1(@l,@lastline,@y) newline#1(::(@x,@xs),@lastline,@y) -> newline#2(@lastline,@x,@xs,@y) newline#1(nil(),@lastline,@y) -> nil() newline#2(::(@belowVal,@lastline'),@x,@xs,@y) -> newline#3(newline(@y,@lastline',@xs) ,@belowVal ,@lastline' ,@x ,@y) newline#2(nil(),@x,@xs,@y) -> nil() newline#3(@nl,@belowVal,@lastline',@x,@y) -> newline#4(right(@nl),@belowVal,@lastline',@nl,@x,@y) newline#4(@rightVal,@belowVal,@lastline',@nl,@x,@y) -> newline#5(right(@lastline') ,@belowVal ,@nl ,@rightVal ,@x ,@y) newline#5(@diagVal,@belowVal,@nl,@rightVal,@x,@y) -> newline#6(newline#7(#equal(@x,@y) ,@belowVal ,@diagVal ,@rightVal) ,@nl) newline#6(@elem,@nl) -> ::(@elem,@nl) newline#7(#false(),@belowVal,@diagVal,@rightVal) -> max(@belowVal,@rightVal) newline#7(#true(),@belowVal,@diagVal,@rightVal) -> +(@diagVal,#pos(#s(#0()))) right(@l) -> right#1(@l) right#1(::(@x,@xs)) -> @x right#1(nil()) -> #abs(#0()) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #ckgt(#EQ()) -> #false() #ckgt(#GT()) -> #true() #ckgt(#LT()) -> #false() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #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() #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) - Signature: {#abs/1,#add/2,#and/2,#ckgt/1,#compare/2,#eq/2,#equal/2,#greater/2,#pred/1,#succ/1,+/2,firstline/1 ,firstline#1/1,lcs/2,lcs#1/1,lcs#2/1,lcs#3/1,lcstable/2,lcstable#1/2,lcstable#2/3,lcstable#3/3,max/2,max#1/3 ,newline/3,newline#1/3,newline#2/4,newline#3/5,newline#4/6,newline#5/6,newline#6/2,newline#7/4,right/1 ,right#1/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs,#add,#and,#ckgt,#compare,#eq,#equal,#greater,#pred ,#succ,+,firstline,firstline#1,lcs,lcs#1,lcs#2,lcs#3,lcstable,lcstable#1,lcstable#2,lcstable#3,max,max#1 ,newline,newline#1,newline#2,newline#3,newline#4,newline#5,newline#6,newline#7,right ,right#1} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: Incompatible MAYBE