WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dfsAcc#3(Leaf(x8),x16) -> Cons(x8,x16) dfsAcc#3(Node(x6,x4),x2) -> dfsAcc#3(x4,dfsAcc#3(x6,x2)) main(x1) -> revApp#2(dfsAcc#3(x1,Nil()),Nil()) revApp#2(Cons(x6,x4),x2) -> revApp#2(x4,Cons(x6,x2)) revApp#2(Nil(),x16) -> x16 - Signature: {dfsAcc#3/2,main/1,revApp#2/2} / {Cons/2,Leaf/1,Nil/0,Node/2} - Obligation: innermost runtime complexity wrt. defined symbols {dfsAcc#3,main,revApp#2} and constructors {Cons,Leaf,Nil ,Node} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- Cons :: [A(0) x A(6)] -(6)-> A(6) Cons :: [A(0) x A(7)] -(7)-> A(7) Cons :: [A(0) x A(0)] -(0)-> A(0) Leaf :: [A(0)] -(14)-> A(14) Nil :: [] -(0)-> A(6) Nil :: [] -(0)-> A(8) Nil :: [] -(0)-> A(12) Node :: [A(14) x A(14)] -(14)-> A(14) dfsAcc#3 :: [A(14) x A(7)] -(0)-> A(7) main :: [A(14)] -(14)-> A(0) revApp#2 :: [A(6) x A(0)] -(10)-> A(0) Cost-free Signatures used: -------------------------- Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Leaf :: [A_cf(0)] -(0)-> A_cf(0) Nil :: [] -(0)-> A_cf(0) Node :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dfsAcc#3 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) revApp#2 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- Cons_A :: [A(0) x A(1)] -(1)-> A(1) Leaf_A :: [A(0)] -(1)-> A(1) Nil_A :: [] -(0)-> A(1) Node_A :: [A(1) x A(1)] -(1)-> A(1) * Step 2: Open MAYBE - Strict TRS: dfsAcc#3(Leaf(x8),x16) -> Cons(x8,x16) dfsAcc#3(Node(x6,x4),x2) -> dfsAcc#3(x4,dfsAcc#3(x6,x2)) main(x1) -> revApp#2(dfsAcc#3(x1,Nil()),Nil()) revApp#2(Cons(x6,x4),x2) -> revApp#2(x4,Cons(x6,x2)) revApp#2(Nil(),x16) -> x16 - Signature: {dfsAcc#3/2,main/1,revApp#2/2} / {Cons/2,Leaf/1,Nil/0,Node/2} - Obligation: innermost runtime complexity wrt. defined symbols {dfsAcc#3,main,revApp#2} and constructors {Cons,Leaf,Nil ,Node} Following problems could not be solved: - Strict TRS: dfsAcc#3(Leaf(x8),x16) -> Cons(x8,x16) dfsAcc#3(Node(x6,x4),x2) -> dfsAcc#3(x4,dfsAcc#3(x6,x2)) main(x1) -> revApp#2(dfsAcc#3(x1,Nil()),Nil()) revApp#2(Cons(x6,x4),x2) -> revApp#2(x4,Cons(x6,x2)) revApp#2(Nil(),x16) -> x16 - Signature: {dfsAcc#3/2,main/1,revApp#2/2} / {Cons/2,Leaf/1,Nil/0,Node/2} - Obligation: innermost runtime complexity wrt. defined symbols {dfsAcc#3,main,revApp#2} and constructors {Cons,Leaf,Nil ,Node} WORST_CASE(?,O(n^1))