WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: div(0(),s(Y)) -> 0() div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) geq(X,0()) -> true() geq(0(),s(Y)) -> false() geq(s(X),s(Y)) -> geq(X,Y) if(false(),X,Y) -> Y if(true(),X,Y) -> X minus(0(),Y) -> 0() minus(s(X),s(Y)) -> minus(X,Y) - Signature: {div/2,geq/2,if/3,minus/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div,geq,if,minus} and constructors {0,false,s,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(5) 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(1) 0 :: [] -(0)-> A(2) 0 :: [] -(0)-> A(6) div :: [A(5) x A(1)] -(0)-> A(0) false :: [] -(0)-> A(1) false :: [] -(0)-> A(2) geq :: [A(1) x A(0)] -(1)-> A(2) if :: [A(1) x A(0) x A(0)] -(1)-> A(0) minus :: [A(2) x A(0)] -(1)-> A(6) s :: [A(1)] -(1)-> A(1) s :: [A(5)] -(5)-> A(5) s :: [A(0)] -(0)-> A(0) s :: [A(2)] -(2)-> A(2) true :: [] -(0)-> A(1) true :: [] -(0)-> A(2) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) div :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) false :: [] -(0)-> A_cf(0) geq :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) if :: [A_cf(0) x A_cf(0) x A_cf(0)] -(0)-> A_cf(0) minus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) true :: [] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) false_A :: [] -(0)-> A(1) s_A :: [A(1)] -(1)-> A(1) true_A :: [] -(0)-> A(1) * Step 2: Open MAYBE - Strict TRS: div(0(),s(Y)) -> 0() div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) geq(X,0()) -> true() geq(0(),s(Y)) -> false() geq(s(X),s(Y)) -> geq(X,Y) if(false(),X,Y) -> Y if(true(),X,Y) -> X minus(0(),Y) -> 0() minus(s(X),s(Y)) -> minus(X,Y) - Signature: {div/2,geq/2,if/3,minus/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div,geq,if,minus} and constructors {0,false,s,true} Following problems could not be solved: - Strict TRS: div(0(),s(Y)) -> 0() div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) geq(X,0()) -> true() geq(0(),s(Y)) -> false() geq(s(X),s(Y)) -> geq(X,Y) if(false(),X,Y) -> Y if(true(),X,Y) -> X minus(0(),Y) -> 0() minus(s(X),s(Y)) -> minus(X,Y) - Signature: {div/2,geq/2,if/3,minus/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div,geq,if,minus} and constructors {0,false,s,true} WORST_CASE(?,O(n^1))