WORST_CASE(?,O(n^1)) * Step 1: Sum WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) not(false()) -> true() not(true()) -> false() - Signature: {evenodd/2,not/1} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd,not} and constructors {0,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) not(false()) -> true() not(true()) -> false() - Signature: {evenodd/2,not/1} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd,not} and constructors {0,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))) evenodd#(0(),s(0())) -> c_2() evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) not#(false()) -> c_4() not#(true()) -> c_5() Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))) evenodd#(0(),s(0())) -> c_2() evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) not#(false()) -> c_4() not#(true()) -> c_5() - Weak TRS: evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) not(false()) -> true() not(true()) -> false() - Signature: {evenodd/2,not/1,evenodd#/2,not#/1} / {0/0,false/0,s/1,true/0,c_1/2,c_2/0,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd#,not#} and constructors {0,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,5} by application of Pre({2,4,5}) = {1}. Here rules are labelled as follows: 1: evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))) 2: evenodd#(0(),s(0())) -> c_2() 3: evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) 4: not#(false()) -> c_4() 5: not#(true()) -> c_5() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))) evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) - Weak DPs: evenodd#(0(),s(0())) -> c_2() not#(false()) -> c_4() not#(true()) -> c_5() - Weak TRS: evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) not(false()) -> true() not(true()) -> false() - Signature: {evenodd/2,not/1,evenodd#/2,not#/1} / {0/0,false/0,s/1,true/0,c_1/2,c_2/0,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd#,not#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))) -->_2 evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())):2 -->_1 not#(true()) -> c_5():5 -->_1 not#(false()) -> c_4():4 -->_2 evenodd#(0(),s(0())) -> c_2():3 2:S:evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) -->_1 evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))):1 3:W:evenodd#(0(),s(0())) -> c_2() 4:W:not#(false()) -> c_4() 5:W:not#(true()) -> c_5() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: evenodd#(0(),s(0())) -> c_2() 4: not#(false()) -> c_4() 5: not#(true()) -> c_5() * Step 5: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))) evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) - Weak TRS: evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) not(false()) -> true() not(true()) -> false() - Signature: {evenodd/2,not/1,evenodd#/2,not#/1} / {0/0,false/0,s/1,true/0,c_1/2,c_2/0,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd#,not#} and constructors {0,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))) -->_2 evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())):2 2:S:evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) -->_1 evenodd#(x,0()) -> c_1(not#(evenodd(x,s(0()))),evenodd#(x,s(0()))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: evenodd#(x,0()) -> c_1(evenodd#(x,s(0()))) * Step 6: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: evenodd#(x,0()) -> c_1(evenodd#(x,s(0()))) evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) - Weak TRS: evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) not(false()) -> true() not(true()) -> false() - Signature: {evenodd/2,not/1,evenodd#/2,not#/1} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd#,not#} and constructors {0,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: evenodd#(x,0()) -> c_1(evenodd#(x,s(0()))) evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) * Step 7: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: evenodd#(x,0()) -> c_1(evenodd#(x,s(0()))) evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) - Signature: {evenodd/2,not/1,evenodd#/2,not#/1} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd#,not#} and constructors {0,false,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_3) = {1} Following symbols are considered usable: {evenodd#,not#} TcT has computed the following interpretation: p(0) = [2] p(evenodd) = [2] p(false) = [1] p(not) = [4] p(s) = [1] x1 + [2] p(true) = [1] p(evenodd#) = [8] x1 + [14] p(not#) = [1] p(c_1) = [1] x1 + [0] p(c_2) = [1] p(c_3) = [1] x1 + [14] p(c_4) = [1] p(c_5) = [0] Following rules are strictly oriented: evenodd#(s(x),s(0())) = [8] x + [30] > [8] x + [28] = c_3(evenodd#(x,0())) Following rules are (at-least) weakly oriented: evenodd#(x,0()) = [8] x + [14] >= [8] x + [14] = c_1(evenodd#(x,s(0()))) * Step 8: MI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: evenodd#(x,0()) -> c_1(evenodd#(x,s(0()))) - Weak DPs: evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) - Signature: {evenodd/2,not/1,evenodd#/2,not#/1} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd#,not#} and constructors {0,false,s,true} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_3) = {1} Following symbols are considered usable: {evenodd#,not#} TcT has computed the following interpretation: p(0) = [1] [4] p(evenodd) = [2 2] x_1 + [1] [2 0] [8] p(false) = [1] [0] p(not) = [0 1] x_1 + [4] [1 0] [0] p(s) = [1 0] x_1 + [2] [0 0] [1] p(true) = [1] [1] p(evenodd#) = [ 2 0] x_1 + [1 1] x_2 + [10] [10 10] [0 0] [0] p(not#) = [0 0] x_1 + [2] [0 8] [2] p(c_1) = [1 0] x_1 + [0] [0 0] [0] p(c_2) = [0] [0] p(c_3) = [1 0] x_1 + [1] [0 0] [8] p(c_4) = [1] [4] p(c_5) = [0] [1] Following rules are strictly oriented: evenodd#(x,0()) = [ 2 0] x + [15] [10 10] [0] > [2 0] x + [14] [0 0] [0] = c_1(evenodd#(x,s(0()))) Following rules are (at-least) weakly oriented: evenodd#(s(x),s(0())) = [ 2 0] x + [18] [10 0] [30] >= [2 0] x + [16] [0 0] [8] = c_3(evenodd#(x,0())) * Step 9: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: evenodd#(x,0()) -> c_1(evenodd#(x,s(0()))) evenodd#(s(x),s(0())) -> c_3(evenodd#(x,0())) - Signature: {evenodd/2,not/1,evenodd#/2,not#/1} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {evenodd#,not#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))