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