WORST_CASE(?,O(n^2)) * Step 1: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: a__div(X1,X2) -> div(X1,X2) a__div(0(),s(Y)) -> 0() a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__geq(X,0()) -> true() a__geq(X1,X2) -> geq(X1,X2) a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) a__minus(X1,X2) -> minus(X1,X2) a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) mark(0()) -> 0() mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(false()) -> false() mark(geq(X1,X2)) -> a__geq(X1,X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(s(X)) -> s(mark(X)) mark(true()) -> true() - Signature: {a__div/2,a__geq/2,a__if/3,a__minus/2,mark/1} / {0/0,div/2,false/0,geq/2,if/3,minus/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__div,a__geq,a__if,a__minus,mark} and constructors {0 ,div,false,geq,if,minus,s,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(13, 1) 0 :: [] -(0)-> A(0, 0) 0 :: [] -(0)-> A(1, 0) 0 :: [] -(0)-> A(2, 0) 0 :: [] -(0)-> A(3, 11) 0 :: [] -(0)-> A(5, 7) 0 :: [] -(0)-> A(5, 13) 0 :: [] -(0)-> A(15, 5) a__div :: [A(13, 1) x A(0, 11)] -(10)-> A(2, 1) a__geq :: [A(1, 0) x A(0, 0)] -(1)-> A(2, 1) a__if :: [A(2, 1) x A(3, 11) x A(3, 11)] -(7)-> A(2, 1) a__minus :: [A(2, 0) x A(0, 0)] -(3)-> A(14, 2) div :: [A(14, 11) x A(0, 11)] -(11)-> A(3, 11) div :: [A(10, 1) x A(0, 1)] -(1)-> A(9, 1) false :: [] -(0)-> A(2, 1) false :: [] -(0)-> A(3, 11) false :: [] -(0)-> A(5, 7) geq :: [A(11, 0) x A(0, 0)] -(0)-> A(3, 11) geq :: [A(1, 0) x A(0, 0)] -(0)-> A(2, 1) if :: [A(3, 11) x A(3, 11) x A(14, 11)] -(11)-> A(3, 11) if :: [A(2, 1) x A(2, 1) x A(3, 1)] -(1)-> A(2, 1) mark :: [A(3, 11)] -(6)-> A(2, 1) minus :: [A(11, 0) x A(0, 0)] -(0)-> A(3, 11) minus :: [A(11, 0) x A(0, 0)] -(0)-> A(14, 11) minus :: [A(2, 0) x A(0, 0)] -(0)-> A(14, 2) s :: [A(0, 11)] -(0)-> A(0, 11) s :: [A(13, 1)] -(13)-> A(13, 1) s :: [A(0, 0)] -(0)-> A(0, 0) s :: [A(1, 0)] -(1)-> A(1, 0) s :: [A(2, 0)] -(2)-> A(2, 0) s :: [A(3, 11)] -(3)-> A(3, 11) s :: [A(2, 1)] -(2)-> A(2, 1) true :: [] -(0)-> A(2, 1) true :: [] -(0)-> A(3, 11) true :: [] -(0)-> A(5, 7) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) 0 :: [] -(0)-> A_cf(3, 3) 0 :: [] -(0)-> A_cf(11, 0) 0 :: [] -(0)-> A_cf(11, 3) 0 :: [] -(0)-> A_cf(15, 3) 0 :: [] -(0)-> A_cf(11, 2) a__div :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__div :: [A_cf(11, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 0) a__geq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__geq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 0) a__if :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__if :: [A_cf(11, 0) x A_cf(11, 0) x A_cf(12, 0)] -(0)-> A_cf(11, 0) a__if :: [A_cf(11, 0) x A_cf(11, 0) x A_cf(11, 0)] -(0)-> A_cf(11, 0) a__minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__minus :: [A_cf(0, 0) x A_cf(0, 0)] -(1)-> A_cf(0, 0) a__minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 0) div :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) div :: [A_cf(11, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 0) div :: [A_cf(13, 0) x A_cf(0, 0)] -(0)-> A_cf(13, 0) false :: [] -(0)-> A_cf(0, 0) false :: [] -(0)-> A_cf(11, 0) false :: [] -(0)-> A_cf(13, 2) false :: [] -(0)-> A_cf(11, 2) geq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) geq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 0) geq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 0) if :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) if :: [A_cf(11, 0) x A_cf(11, 0) x A_cf(11, 0)] -(0)-> A_cf(11, 0) mark :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) mark :: [A_cf(11, 0)] -(0)-> A_cf(11, 0) minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(3, 0) minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 0) minus :: [A_cf(2, 0) x A_cf(0, 0)] -(0)-> A_cf(13, 2) minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(11, 0)] -(11)-> A_cf(11, 0) true :: [] -(0)-> A_cf(0, 0) true :: [] -(0)-> A_cf(11, 0) true :: [] -(0)-> A_cf(11, 2) true :: [] -(0)-> A_cf(13, 2) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) div_A :: [A(1, 0) x A(0, 0)] -(0)-> A(1, 0) div_A :: [A(1, 1) x A(0, 1)] -(1)-> A(0, 1) false_A :: [] -(0)-> A(1, 0) false_A :: [] -(0)-> A(0, 1) geq_A :: [A(0, 0) x A(0, 0)] -(0)-> A(1, 0) geq_A :: [A(1, 0) x A(0, 0)] -(0)-> A(0, 1) if_A :: [A(1, 0) x A(1, 0) x A(1, 0)] -(0)-> A(1, 0) if_A :: [A(0, 1) x A(0, 1) x A(1, 1)] -(1)-> A(0, 1) minus_A :: [A(0, 0) x A(0, 0)] -(0)-> A(1, 0) minus_A :: [A(1, 0) x A(0, 0)] -(0)-> A(0, 1) s_A :: [A(1, 0)] -(1)-> A(1, 0) s_A :: [A(0, 1)] -(0)-> A(0, 1) true_A :: [] -(0)-> A(1, 0) true_A :: [] -(0)-> A(0, 1) * Step 2: Open MAYBE - Strict TRS: a__div(X1,X2) -> div(X1,X2) a__div(0(),s(Y)) -> 0() a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__geq(X,0()) -> true() a__geq(X1,X2) -> geq(X1,X2) a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) a__minus(X1,X2) -> minus(X1,X2) a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) mark(0()) -> 0() mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(false()) -> false() mark(geq(X1,X2)) -> a__geq(X1,X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(s(X)) -> s(mark(X)) mark(true()) -> true() - Signature: {a__div/2,a__geq/2,a__if/3,a__minus/2,mark/1} / {0/0,div/2,false/0,geq/2,if/3,minus/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__div,a__geq,a__if,a__minus,mark} and constructors {0 ,div,false,geq,if,minus,s,true} Following problems could not be solved: - Strict TRS: a__div(X1,X2) -> div(X1,X2) a__div(0(),s(Y)) -> 0() a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__geq(X,0()) -> true() a__geq(X1,X2) -> geq(X1,X2) a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) a__minus(X1,X2) -> minus(X1,X2) a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) mark(0()) -> 0() mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(false()) -> false() mark(geq(X1,X2)) -> a__geq(X1,X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(s(X)) -> s(mark(X)) mark(true()) -> true() - Signature: {a__div/2,a__geq/2,a__if/3,a__minus/2,mark/1} / {0/0,div/2,false/0,geq/2,if/3,minus/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__div,a__geq,a__if,a__minus,mark} and constructors {0 ,div,false,geq,if,minus,s,true} WORST_CASE(?,O(n^2))