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