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 = MiniSMT} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) f :: [A(3) x A(4)] -(15)-> A(0) g :: [A(4) x A(0)] -(4)-> A(4) g :: [A(8) x A(0)] -(8)-> A(8) g :: [A(1) x A(0)] -(1)-> A(1) g :: [A(0) x A(0)] -(0)-> A(0) g :: [A(5) x A(0)] -(5)-> A(5) nil :: [] -(0)-> A(4) nil :: [] -(0)-> A(8) nil :: [] -(0)-> A(1) nil :: [] -(0)-> A(10) norm :: [A(8)] -(4)-> A(1) rem :: [A(1) x A(2)] -(1)-> A(0) s :: [A(2)] -(2)-> A(2) s :: [A(1)] -(1)-> A(1) 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(1)] -(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))