WORST_CASE(?,O(n^2)) * Step 1: Sum WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: appendreverse(@toreverse,@sofar) -> appendreverse#1(@toreverse,@sofar) appendreverse#1(::(@a,@as),@sofar) -> appendreverse(@as,::(@a,@sofar)) appendreverse#1(nil(),@sofar) -> @sofar bfs(@queue,@futurequeue,@x) -> bfs#1(@queue,@futurequeue,@x) bfs#1(::(@t,@ts),@futurequeue,@x) -> bfs#3(@t,@futurequeue,@ts,@x) bfs#1(nil(),@futurequeue,@x) -> bfs#2(@futurequeue,@x) bfs#2(::(@t,@ts),@x) -> bfs(reverse(::(@t,@ts)),nil(),@x) bfs#2(nil(),@x) -> leaf() bfs#3(leaf(),@futurequeue,@ts,@x) -> bfs(@ts,@futurequeue,@x) bfs#3(node(@y,@t1,@t2),@futurequeue,@ts,@x) -> bfs#4(#equal(@x,@y),@futurequeue,@t1,@t2,@ts,@x,@y) bfs#4(#false(),@futurequeue,@t1,@t2,@ts,@x,@y) -> bfs(@ts,::(@t2,::(@t1,@futurequeue)),@x) bfs#4(#true(),@futurequeue,@t1,@t2,@ts,@x,@y) -> node(@y,@t1,@t2) bfs2(@t,@x) -> bfs2#1(dobfs(@t,@x),@x) bfs2#1(@t',@x) -> dobfs(@t',@x) dfs(@queue,@x) -> dfs#1(@queue,@x) dfs#1(::(@t,@ts),@x) -> dfs#2(@t,@t,@ts,@x) dfs#1(nil(),@x) -> leaf() dfs#2(leaf(),@t,@ts,@x) -> dfs(@ts,@x) dfs#2(node(@a,@t1,@t2),@t,@ts,@x) -> dfs#3(#equal(@a,@x),@t,@t1,@t2,@ts,@x) dfs#3(#false(),@t,@t1,@t2,@ts,@x) -> dfs(::(@t1,::(@t2,@ts)),@x) dfs#3(#true(),@t,@t1,@t2,@ts,@x) -> @t dobfs(@t,@x) -> bfs(::(@t,nil()),nil(),@x) dodfs(@t,@x) -> dfs(::(@t,nil()),@x) reverse(@xs) -> appendreverse(@xs,nil()) - 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),leaf()) -> #false() #eq(::(@x_1,@x_2),nil()) -> #false() #eq(::(@x_1,@x_2),node(@y_1,@y_2,@y_3)) -> #false() #eq(leaf(),::(@y_1,@y_2)) -> #false() #eq(leaf(),leaf()) -> #true() #eq(leaf(),nil()) -> #false() #eq(leaf(),node(@y_1,@y_2,@y_3)) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),leaf()) -> #false() #eq(nil(),nil()) -> #true() #eq(nil(),node(@y_1,@y_2,@y_3)) -> #false() #eq(node(@x_1,@x_2,@x_3),::(@y_1,@y_2)) -> #false() #eq(node(@x_1,@x_2,@x_3),leaf()) -> #false() #eq(node(@x_1,@x_2,@x_3),nil()) -> #false() #eq(node(@x_1,@x_2,@x_3),node(@y_1,@y_2,@y_3)) -> #and(#eq(@x_1,@y_1),#and(#eq(@x_2,@y_2),#eq(@x_3,@y_3))) #equal(@x,@y) -> #eq(@x,@y) - Signature: {#and/2,#eq/2,#equal/2,appendreverse/2,appendreverse#1/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,bfs2/2 ,bfs2#1/2,dfs/2,dfs#1/2,dfs#2/4,dfs#3/6,dobfs/2,dodfs/2,reverse/1} / {#0/0,#false/0,#neg/1,#pos/1,#s/1 ,#true/0,::/2,leaf/0,nil/0,node/3} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,appendreverse,appendreverse#1,bfs,bfs#1 ,bfs#2,bfs#3,bfs#4,bfs2,bfs2#1,dfs,dfs#1,dfs#2,dfs#3,dobfs,dodfs,reverse} and constructors {#0,#false,#neg ,#pos,#s,#true,::,leaf,nil,node} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: appendreverse(@toreverse,@sofar) -> appendreverse#1(@toreverse,@sofar) appendreverse#1(::(@a,@as),@sofar) -> appendreverse(@as,::(@a,@sofar)) appendreverse#1(nil(),@sofar) -> @sofar bfs(@queue,@futurequeue,@x) -> bfs#1(@queue,@futurequeue,@x) bfs#1(::(@t,@ts),@futurequeue,@x) -> bfs#3(@t,@futurequeue,@ts,@x) bfs#1(nil(),@futurequeue,@x) -> bfs#2(@futurequeue,@x) bfs#2(::(@t,@ts),@x) -> bfs(reverse(::(@t,@ts)),nil(),@x) bfs#2(nil(),@x) -> leaf() bfs#3(leaf(),@futurequeue,@ts,@x) -> bfs(@ts,@futurequeue,@x) bfs#3(node(@y,@t1,@t2),@futurequeue,@ts,@x) -> bfs#4(#equal(@x,@y),@futurequeue,@t1,@t2,@ts,@x,@y) bfs#4(#false(),@futurequeue,@t1,@t2,@ts,@x,@y) -> bfs(@ts,::(@t2,::(@t1,@futurequeue)),@x) bfs#4(#true(),@futurequeue,@t1,@t2,@ts,@x,@y) -> node(@y,@t1,@t2) bfs2(@t,@x) -> bfs2#1(dobfs(@t,@x),@x) bfs2#1(@t',@x) -> dobfs(@t',@x) dfs(@queue,@x) -> dfs#1(@queue,@x) dfs#1(::(@t,@ts),@x) -> dfs#2(@t,@t,@ts,@x) dfs#1(nil(),@x) -> leaf() dfs#2(leaf(),@t,@ts,@x) -> dfs(@ts,@x) dfs#2(node(@a,@t1,@t2),@t,@ts,@x) -> dfs#3(#equal(@a,@x),@t,@t1,@t2,@ts,@x) dfs#3(#false(),@t,@t1,@t2,@ts,@x) -> dfs(::(@t1,::(@t2,@ts)),@x) dfs#3(#true(),@t,@t1,@t2,@ts,@x) -> @t dobfs(@t,@x) -> bfs(::(@t,nil()),nil(),@x) dodfs(@t,@x) -> dfs(::(@t,nil()),@x) reverse(@xs) -> appendreverse(@xs,nil()) - 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),leaf()) -> #false() #eq(::(@x_1,@x_2),nil()) -> #false() #eq(::(@x_1,@x_2),node(@y_1,@y_2,@y_3)) -> #false() #eq(leaf(),::(@y_1,@y_2)) -> #false() #eq(leaf(),leaf()) -> #true() #eq(leaf(),nil()) -> #false() #eq(leaf(),node(@y_1,@y_2,@y_3)) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),leaf()) -> #false() #eq(nil(),nil()) -> #true() #eq(nil(),node(@y_1,@y_2,@y_3)) -> #false() #eq(node(@x_1,@x_2,@x_3),::(@y_1,@y_2)) -> #false() #eq(node(@x_1,@x_2,@x_3),leaf()) -> #false() #eq(node(@x_1,@x_2,@x_3),nil()) -> #false() #eq(node(@x_1,@x_2,@x_3),node(@y_1,@y_2,@y_3)) -> #and(#eq(@x_1,@y_1),#and(#eq(@x_2,@y_2),#eq(@x_3,@y_3))) #equal(@x,@y) -> #eq(@x,@y) - Signature: {#and/2,#eq/2,#equal/2,appendreverse/2,appendreverse#1/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,bfs2/2 ,bfs2#1/2,dfs/2,dfs#1/2,dfs#2/4,dfs#3/6,dobfs/2,dodfs/2,reverse/1} / {#0/0,#false/0,#neg/1,#pos/1,#s/1 ,#true/0,::/2,leaf/0,nil/0,node/3} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,appendreverse,appendreverse#1,bfs,bfs#1 ,bfs#2,bfs#3,bfs#4,bfs2,bfs2#1,dfs,dfs#1,dfs#2,dfs#3,dobfs,dodfs,reverse} and constructors {#0,#false,#neg ,#pos,#s,#true,::,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 5, araRuleShifting = Nothing} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0, 0) #and :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) #eq :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) #equal :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) #false :: [] -(0)-> "A"(0, 0) #false :: [] -(0)-> "A"(1, 0) #neg :: ["A"(0, 0)] -(0)-> "A"(0, 0) #pos :: ["A"(0, 0)] -(0)-> "A"(0, 0) #s :: ["A"(0, 0)] -(0)-> "A"(0, 0) #true :: [] -(0)-> "A"(0, 0) #true :: [] -(0)-> "A"(0, 1) :: :: ["A"(42, 0) x "A"(42, 14)] -(14)-> "A"(42, 14) :: :: ["A"(42, 0) x "A"(42, 7)] -(7)-> "A"(42, 7) :: :: ["A"(42, 0) x "A"(42, 20)] -(20)-> "A"(42, 20) :: :: ["A"(8, 0) x "A"(8, 4)] -(4)-> "A"(8, 4) :: :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) :: :: ["A"(42, 0) x "A"(42, 15)] -(15)-> "A"(42, 15) :: :: ["A"(8, 0) x "A"(8, 8)] -(8)-> "A"(8, 8) appendreverse :: ["A"(42, 14) x "A"(42, 7)] -(2)-> "A"(42, 7) appendreverse#1 :: ["A"(42, 14) x "A"(42, 7)] -(1)-> "A"(42, 7) bfs :: ["A"(42, 7) x "A"(42, 20) x "A"(0, 0)] -(3)-> "A"(42, 0) bfs#1 :: ["A"(42, 7) x "A"(42, 20) x "A"(0, 0)] -(2)-> "A"(42, 0) bfs#2 :: ["A"(42, 20) x "A"(0, 0)] -(1)-> "A"(42, 0) bfs#3 :: ["A"(42, 0) x "A"(42, 20) x "A"(42, 7) x "A"(0, 0)] -(8)-> "A"(42, 0) bfs#4 :: ["A"(0, 0) x "A"(42, 20) x "A"(42, 0) x "A"(42, 0) x "A"(42, 7) x "A"(0, 0) x "A"(0, 0)] -(44)-> "A"(42, 0) bfs2 :: ["A"(42, 0) x "A"(0, 0)] -(40)-> "A"(0, 0) bfs2#1 :: ["A"(42, 0) x "A"(0, 0)] -(20)-> "A"(0, 0) dfs :: ["A"(8, 4) x "A"(0, 0)] -(2)-> "A"(0, 0) dfs#1 :: ["A"(8, 4) x "A"(0, 0)] -(1)-> "A"(0, 0) dfs#2 :: ["A"(8, 0) x "A"(0, 0) x "A"(8, 4) x "A"(0, 0)] -(4)-> "A"(0, 0) dfs#3 :: ["A"(0, 0) x "A"(0, 0) x "A"(8, 0) x "A"(8, 0) x "A"(8, 4) x "A"(0, 0)] -(11)-> "A"(0, 0) dobfs :: ["A"(42, 0) x "A"(0, 0)] -(19)-> "A"(42, 0) dodfs :: ["A"(8, 0) x "A"(0, 0)] -(11)-> "A"(0, 0) leaf :: [] -(0)-> "A"(42, 0) leaf :: [] -(0)-> "A"(8, 0) leaf :: [] -(0)-> "A"(0, 0) leaf :: [] -(0)-> "A"(42, 1) nil :: [] -(0)-> "A"(42, 14) nil :: [] -(0)-> "A"(42, 7) nil :: [] -(0)-> "A"(42, 20) nil :: [] -(0)-> "A"(8, 4) nil :: [] -(0)-> "A"(0, 0) nil :: [] -(0)-> "A"(42, 15) nil :: [] -(0)-> "A"(8, 8) node :: ["A"(0, 0) x "A"(42, 0) x "A"(42, 0)] -(42)-> "A"(42, 0) node :: ["A"(0, 0) x "A"(8, 0) x "A"(8, 0)] -(8)-> "A"(8, 0) node :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) reverse :: ["A"(42, 14)] -(3)-> "A"(42, 7) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(1)-> "A"(1, 0) "#0_A" :: [] -(0)-> "A"(0, 1) "#false_A" :: [] -(0)-> "A"(1, 0) "#false_A" :: [] -(1)-> "A"(0, 1) "#neg_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "#neg_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "#pos_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "#pos_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1) "#s_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "#s_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1) "#true_A" :: [] -(1)-> "A"(1, 0) "#true_A" :: [] -(0)-> "A"(0, 1) "::_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "::_A" :: ["A"(0, 0) x "A"(0, 1)] -(1)-> "A"(0, 1) "leaf_A" :: [] -(0)-> "A"(1, 0) "leaf_A" :: [] -(0)-> "A"(0, 1) "nil_A" :: [] -(0)-> "A"(1, 0) "nil_A" :: [] -(0)-> "A"(0, 1) "node_A" :: ["A"(0, 0) x "A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "node_A" :: ["A"(0, 1) x "A"(1, 1) x "A"(1, 1)] -(1)-> "A"(0, 1) WORST_CASE(?,O(n^2))