WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: fac(s(x)) -> *(fac(p(s(x))),s(x)) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1} / {*/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac,p} and constructors {*,0,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) p#(s(0())) -> c_2() p#(s(s(x))) -> c_3(p#(s(x))) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) p#(s(0())) -> c_2() p#(s(s(x))) -> c_3(p#(s(x))) - Weak TRS: fac(s(x)) -> *(fac(p(s(x))),s(x)) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/2,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {1,3}. Here rules are labelled as follows: 1: fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) 2: p#(s(0())) -> c_2() 3: p#(s(s(x))) -> c_3(p#(s(x))) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) p#(s(s(x))) -> c_3(p#(s(x))) - Weak DPs: p#(s(0())) -> c_2() - Weak TRS: fac(s(x)) -> *(fac(p(s(x))),s(x)) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/2,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) -->_2 p#(s(s(x))) -> c_3(p#(s(x))):2 -->_2 p#(s(0())) -> c_2():3 -->_1 fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))):1 2:S:p#(s(s(x))) -> c_3(p#(s(x))) -->_1 p#(s(0())) -> c_2():3 -->_1 p#(s(s(x))) -> c_3(p#(s(x))):2 3:W:p#(s(0())) -> c_2() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: p#(s(0())) -> c_2() * Step 4: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) p#(s(s(x))) -> c_3(p#(s(x))) - Weak TRS: fac(s(x)) -> *(fac(p(s(x))),s(x)) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/2,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) p#(s(s(x))) -> c_3(p#(s(x))) * Step 5: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) p#(s(s(x))) -> c_3(p#(s(x))) - Weak TRS: p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/2,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) and a lower component p#(s(s(x))) -> c_3(p#(s(x))) Further, following extension rules are added to the lower component. fac#(s(x)) -> fac#(p(s(x))) fac#(s(x)) -> p#(s(x)) ** Step 5.a:1: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) - Weak TRS: p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/2,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))) -->_1 fac#(s(x)) -> c_1(fac#(p(s(x))),p#(s(x))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: fac#(s(x)) -> c_1(fac#(p(s(x)))) ** Step 5.a:2: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: fac#(s(x)) -> c_1(fac#(p(s(x)))) - Weak TRS: p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/1,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(8, 8) 0 :: [] -(0)-> "A"(14, 14) p :: ["A"(0, 8)] -(0)-> "A"(8, 8) s :: ["A"(8, 8)] -(7)-> "A"(7, 8) s :: ["A"(8, 8)] -(0)-> "A"(0, 8) s :: ["A"(8, 8)] -(8)-> "A"(8, 8) s :: ["A"(8, 8)] -(4)-> "A"(4, 8) fac# :: ["A"(7, 8)] -(9)-> "A"(0, 1) c_1 :: ["A"(0, 0)] -(0)-> "A"(2, 8) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1, 0) "0_A" :: [] -(0)-> "A"(0, 1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1) "s_A" :: ["A"(0, 0)] -(1)-> "A"(1, 0) "s_A" :: ["A"(1, 1)] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: fac#(s(x)) -> c_1(fac#(p(s(x)))) 2. Weak: ** Step 5.b:1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: p#(s(s(x))) -> c_3(p#(s(x))) - Weak DPs: fac#(s(x)) -> fac#(p(s(x))) fac#(s(x)) -> p#(s(x)) - Weak TRS: p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/2,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(s) = {1}, uargs(fac#) = {1}, uargs(c_3) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(*) = [1] x1 + [1] x2 + [0] p(0) = [14] p(fac) = [4] p(p) = [1] x1 + [0] p(s) = [1] x1 + [4] p(fac#) = [1] x1 + [10] p(p#) = [1] x1 + [10] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] Following rules are strictly oriented: p#(s(s(x))) = [1] x + [18] > [1] x + [14] = c_3(p#(s(x))) Following rules are (at-least) weakly oriented: fac#(s(x)) = [1] x + [14] >= [1] x + [14] = fac#(p(s(x))) fac#(s(x)) = [1] x + [14] >= [1] x + [14] = p#(s(x)) p(s(0())) = [18] >= [14] = 0() p(s(s(x))) = [1] x + [8] >= [1] x + [8] = s(p(s(x))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 5.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: fac#(s(x)) -> fac#(p(s(x))) fac#(s(x)) -> p#(s(x)) p#(s(s(x))) -> c_3(p#(s(x))) - Weak TRS: p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) - Signature: {fac/1,p/1,fac#/1,p#/1} / {*/2,0/0,s/1,c_1/2,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {fac#,p#} and constructors {*,0,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))