WORST_CASE(?,O(n^1)) * Step 1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) admit#(x,nil()) -> c_2() cond#(true(),y) -> c_3() Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) admit#(x,nil()) -> c_2() cond#(true(),y) -> c_3() - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2,admit#/2,cond#/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0,c_1/1,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit#,cond#} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) admit#(x,nil()) -> c_2() cond#(true(),y) -> c_3() * Step 3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) admit#(x,nil()) -> c_2() cond#(true(),y) -> c_3() - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() - Signature: {admit/2,cond/2,admit#/2,cond#/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0,c_1/1,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit#,cond#} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnTrs} + 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(.) = {2}, uargs(cond) = {2}, uargs(cond#) = {2}, uargs(c_1) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(.) = [1] x1 + [1] x2 + [0] p(=) = [0] p(admit) = [4] x1 + [6] x2 + [1] p(carry) = [2] p(cond) = [1] x2 + [0] p(nil) = [0] p(sum) = [1] x1 + [1] x2 + [1] x3 + [0] p(true) = [0] p(w) = [2] p(admit#) = [1] x1 + [6] x2 + [0] p(cond#) = [1] x2 + [0] p(c_1) = [1] x1 + [2] p(c_2) = [0] p(c_3) = [0] Following rules are strictly oriented: admit(x,.(u,.(v,.(w(),z)))) = [6] u + [6] v + [4] x + [6] z + [13] > [1] u + [1] v + [6] z + [11] = cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) = [4] x + [1] > [0] = nil() Following rules are (at-least) weakly oriented: admit#(x,.(u,.(v,.(w(),z)))) = [6] u + [6] v + [1] x + [6] z + [12] >= [1] u + [1] v + [6] z + [13] = c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) admit#(x,nil()) = [1] x + [0] >= [0] = c_2() cond#(true(),y) = [1] y + [0] >= [0] = c_3() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) admit#(x,nil()) -> c_2() cond#(true(),y) -> c_3() - Weak TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() - Signature: {admit/2,cond/2,admit#/2,cond#/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0,c_1/1,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit#,cond#} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3} by application of Pre({1,2,3}) = {}. Here rules are labelled as follows: 1: admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) 2: admit#(x,nil()) -> c_2() 3: cond#(true(),y) -> c_3() * Step 5: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) admit#(x,nil()) -> c_2() cond#(true(),y) -> c_3() - Weak TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() - Signature: {admit/2,cond/2,admit#/2,cond#/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0,c_1/1,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit#,cond#} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) 2:W:admit#(x,nil()) -> c_2() 3:W:cond#(true(),y) -> c_3() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: cond#(true(),y) -> c_3() 2: admit#(x,nil()) -> c_2() 1: admit#(x,.(u,.(v,.(w(),z)))) -> c_1(cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))) * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() - Signature: {admit/2,cond/2,admit#/2,cond#/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0,c_1/1,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit#,cond#} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))