WORST_CASE(?,O(n^2)) * Step 1: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: a__add(X1,X2) -> add(X1,X2) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(add(X,Y)) a__from(X) -> cons(mark(X),from(s(X))) a__from(X) -> from(X) a__fst(X1,X2) -> fst(X1,X2) a__fst(0(),Z) -> nil() a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z)) a__len(X) -> len(X) a__len(cons(X,Z)) -> s(len(Z)) a__len(nil()) -> 0() mark(0()) -> 0() mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(from(X)) -> a__from(mark(X)) mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2)) mark(len(X)) -> a__len(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(X) - Signature: {a__add/2,a__from/1,a__fst/2,a__len/1,mark/1} / {0/0,add/2,cons/2,from/1,fst/2,len/1,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__add,a__from,a__fst,a__len,mark} and constructors {0 ,add,cons,from,fst,len,nil,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(6, 3) 0 :: [] -(0)-> A(9, 3) 0 :: [] -(0)-> A(13, 5) a__add :: [A(6, 3) x A(9, 3)] -(7)-> A(6, 3) a__from :: [A(9, 3)] -(8)-> A(6, 3) a__fst :: [A(6, 3) x A(9, 3)] -(7)-> A(6, 3) a__len :: [A(6, 3)] -(7)-> A(6, 3) add :: [A(9, 3) x A(12, 3)] -(9)-> A(9, 3) add :: [A(6, 3) x A(9, 3)] -(6)-> A(6, 3) add :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) cons :: [A(9, 3) x A(0, 0)] -(9)-> A(9, 3) cons :: [A(6, 3) x A(0, 0)] -(6)-> A(6, 3) from :: [A(12, 3)] -(9)-> A(9, 3) from :: [A(0, 0)] -(0)-> A(0, 0) from :: [A(9, 3)] -(6)-> A(6, 3) fst :: [A(9, 3) x A(12, 3)] -(9)-> A(9, 3) fst :: [A(6, 3) x A(9, 3)] -(6)-> A(6, 3) fst :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) len :: [A(9, 3)] -(9)-> A(9, 3) len :: [A(6, 3)] -(6)-> A(6, 3) len :: [A(0, 0)] -(0)-> A(0, 0) mark :: [A(9, 3)] -(1)-> A(6, 3) nil :: [] -(0)-> A(6, 3) nil :: [] -(0)-> A(9, 3) nil :: [] -(0)-> A(13, 5) s :: [A(0, 0)] -(3)-> A(6, 3) s :: [A(0, 0)] -(3)-> A(9, 3) s :: [A(0, 0)] -(4)-> A(12, 4) s :: [A(0, 0)] -(0)-> A(0, 0) s :: [A(0, 0)] -(9)-> A(10, 9) s :: [A(0, 0)] -(3)-> A(10, 3) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) 0 :: [] -(0)-> A_cf(3, 0) 0 :: [] -(0)-> A_cf(3, 2) a__add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__add :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) a__from :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) a__from :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) a__fst :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__fst :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) a__len :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) a__len :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) add :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(3, 0) x A_cf(0, 0)] -(3)-> A_cf(3, 0) from :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) from :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) fst :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) fst :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) len :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) len :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) mark :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) mark :: [A_cf(3, 0)] -(0)-> A_cf(3, 0) nil :: [] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(3, 0) nil :: [] -(0)-> A_cf(3, 2) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(3, 0) s :: [A_cf(0, 0)] -(2)-> A_cf(11, 2) s :: [A_cf(0, 0)] -(6)-> A_cf(4, 6) s :: [A_cf(0, 0)] -(0)-> A_cf(14, 0) s :: [A_cf(0, 0)] -(2)-> A_cf(10, 2) s :: [A_cf(0, 0)] -(1)-> A_cf(8, 1) s :: [A_cf(0, 0)] -(3)-> A_cf(12, 3) s :: [A_cf(0, 0)] -(0)-> A_cf(8, 0) s :: [A_cf(0, 0)] -(5)-> A_cf(4, 5) s :: [A_cf(0, 0)] -(0)-> A_cf(5, 0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) add_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0) add_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1) cons_A :: [A(1, 0) x A(0, 0)] -(1)-> A(1, 0) cons_A :: [A(0, 1) x A(0, 0)] -(0)-> A(0, 1) from_A :: [A(1, 0)] -(1)-> A(1, 0) from_A :: [A(1, 1)] -(0)-> A(0, 1) fst_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0) fst_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1) len_A :: [A(1, 0)] -(1)-> A(1, 0) len_A :: [A(0, 1)] -(0)-> A(0, 1) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) s_A :: [A(0, 0)] -(0)-> A(1, 0) s_A :: [A(0, 0)] -(1)-> A(0, 1) * Step 2: Open MAYBE - Strict TRS: a__add(X1,X2) -> add(X1,X2) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(add(X,Y)) a__from(X) -> cons(mark(X),from(s(X))) a__from(X) -> from(X) a__fst(X1,X2) -> fst(X1,X2) a__fst(0(),Z) -> nil() a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z)) a__len(X) -> len(X) a__len(cons(X,Z)) -> s(len(Z)) a__len(nil()) -> 0() mark(0()) -> 0() mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(from(X)) -> a__from(mark(X)) mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2)) mark(len(X)) -> a__len(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(X) - Signature: {a__add/2,a__from/1,a__fst/2,a__len/1,mark/1} / {0/0,add/2,cons/2,from/1,fst/2,len/1,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__add,a__from,a__fst,a__len,mark} and constructors {0 ,add,cons,from,fst,len,nil,s} Following problems could not be solved: - Strict TRS: a__add(X1,X2) -> add(X1,X2) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(add(X,Y)) a__from(X) -> cons(mark(X),from(s(X))) a__from(X) -> from(X) a__fst(X1,X2) -> fst(X1,X2) a__fst(0(),Z) -> nil() a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z)) a__len(X) -> len(X) a__len(cons(X,Z)) -> s(len(Z)) a__len(nil()) -> 0() mark(0()) -> 0() mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(from(X)) -> a__from(mark(X)) mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2)) mark(len(X)) -> a__len(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(X) - Signature: {a__add/2,a__from/1,a__fst/2,a__len/1,mark/1} / {0/0,add/2,cons/2,from/1,fst/2,len/1,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__add,a__from,a__fst,a__len,mark} and constructors {0 ,add,cons,from,fst,len,nil,s} WORST_CASE(?,O(n^2))