WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(x,g(y,z)) -> g(f(x,y),z) f(x,nil()) -> g(nil(),x) norm(g(x,y)) -> s(norm(x)) norm(nil()) -> 0() rem(g(x,y),0()) -> g(x,y) rem(g(x,y),s(z)) -> rem(x,z) rem(nil(),y) -> nil() - Signature: {f/2,norm/1,rem/2} / {0/0,g/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,norm,rem} and constructors {0,g,nil,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(6) f :: [A(12) x A(13)] -(5)-> A(0) g :: [A(13) x A(0)] -(13)-> A(13) g :: [A(12) x A(0)] -(12)-> A(12) g :: [A(6) x A(0)] -(6)-> A(6) g :: [A(0) x A(0)] -(0)-> A(0) g :: [A(1) x A(0)] -(1)-> A(1) nil :: [] -(0)-> A(13) nil :: [] -(0)-> A(12) nil :: [] -(0)-> A(6) nil :: [] -(0)-> A(0) nil :: [] -(0)-> A(14) norm :: [A(12)] -(7)-> A(2) rem :: [A(6) x A(0)] -(15)-> A(0) s :: [A(0)] -(0)-> A(0) s :: [A(0)] -(2)-> A(2) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) f :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) g :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) norm :: [A_cf(0)] -(0)-> A_cf(0) rem :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) g_A :: [A(1) x A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) s_A :: [A(0)] -(1)-> A(1) * Step 2: Open MAYBE - Strict TRS: f(x,g(y,z)) -> g(f(x,y),z) f(x,nil()) -> g(nil(),x) norm(g(x,y)) -> s(norm(x)) norm(nil()) -> 0() rem(g(x,y),0()) -> g(x,y) rem(g(x,y),s(z)) -> rem(x,z) rem(nil(),y) -> nil() - Signature: {f/2,norm/1,rem/2} / {0/0,g/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,norm,rem} and constructors {0,g,nil,s} Following problems could not be solved: - Strict TRS: f(x,g(y,z)) -> g(f(x,y),z) f(x,nil()) -> g(nil(),x) norm(g(x,y)) -> s(norm(x)) norm(nil()) -> 0() rem(g(x,y),0()) -> g(x,y) rem(g(x,y),s(z)) -> rem(x,z) rem(nil(),y) -> nil() - Signature: {f/2,norm/1,rem/2} / {0/0,g/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,norm,rem} and constructors {0,g,nil,s} WORST_CASE(?,O(n^1))