WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() del(.(x,.(y,z))) -> f(=(x,y),x,y,z) f(false(),x,y,z) -> .(x,del(.(y,z))) f(true(),x,y,z) -> del(.(y,z)) - Signature: {=/2,del/1,f/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0} - Obligation: innermost runtime complexity wrt. defined symbols {=,del,f} and constructors {.,and,false,nil,true,u,v} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() del(.(x,.(y,z))) -> f(=(x,y),x,y,z) f(false(),x,y,z) -> .(x,del(.(y,z))) f(true(),x,y,z) -> del(.(y,z)) - Signature: {=/2,del/1,f/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0} - Obligation: innermost runtime complexity wrt. defined symbols {=,del,f} and constructors {.,and,false,nil,true,u,v} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs =#(.(x,y),.(u(),v())) -> c_1(=#(x,u()),=#(y,v())) =#(.(x,y),nil()) -> c_2() =#(nil(),.(y,z)) -> c_3() =#(nil(),nil()) -> c_4() del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) Weak DPs and mark the set of starting terms. * Step 3: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: =#(.(x,y),.(u(),v())) -> c_1(=#(x,u()),=#(y,v())) =#(.(x,y),nil()) -> c_2() =#(nil(),.(y,z)) -> c_3() =#(nil(),nil()) -> c_4() del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) - Strict TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() del(.(x,.(y,z))) -> f(=(x,y),x,y,z) f(false(),x,y,z) -> .(x,del(.(y,z))) f(true(),x,y,z) -> del(.(y,z)) - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() =#(.(x,y),.(u(),v())) -> c_1(=#(x,u()),=#(y,v())) =#(.(x,y),nil()) -> c_2() =#(nil(),.(y,z)) -> c_3() =#(nil(),nil()) -> c_4() del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) * Step 4: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: =#(.(x,y),.(u(),v())) -> c_1(=#(x,u()),=#(y,v())) =#(.(x,y),nil()) -> c_2() =#(nil(),.(y,z)) -> c_3() =#(nil(),nil()) -> c_4() del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) - Strict TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + 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(f#) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(.) = [1] x2 + [1] p(=) = [14] p(and) = [13] p(del) = [2] x1 + [2] p(f) = [1] x3 + [0] p(false) = [1] p(nil) = [1] p(true) = [1] p(u) = [0] p(v) = [15] p(=#) = [8] p(del#) = [4] x1 + [14] p(f#) = [1] x1 + [4] x4 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [8] Following rules are strictly oriented: =#(.(x,y),.(u(),v())) = [8] > [0] = c_1(=#(x,u()),=#(y,v())) =#(.(x,y),nil()) = [8] > [0] = c_2() =#(nil(),.(y,z)) = [8] > [0] = c_3() =#(nil(),nil()) = [8] > [0] = c_4() del#(.(x,.(y,z))) = [4] z + [22] > [4] z + [14] = c_5(f#(=(x,y),x,y,z)) =(.(x,y),.(u(),v())) = [14] > [13] = and(=(x,u()),=(y,v())) =(.(x,y),nil()) = [14] > [1] = false() =(nil(),.(y,z)) = [14] > [1] = false() =(nil(),nil()) = [14] > [1] = true() Following rules are (at-least) weakly oriented: f#(false(),x,y,z) = [4] z + [1] >= [4] z + [18] = c_6(del#(.(y,z))) f#(true(),x,y,z) = [4] z + [1] >= [4] z + [26] = c_7(del#(.(y,z))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) - Weak DPs: =#(.(x,y),.(u(),v())) -> c_1(=#(x,u()),=#(y,v())) =#(.(x,y),nil()) -> c_2() =#(nil(),.(y,z)) -> c_3() =#(nil(),nil()) -> c_4() del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) - Weak TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(false(),x,y,z) -> c_6(del#(.(y,z))) -->_1 del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)):7 2:S:f#(true(),x,y,z) -> c_7(del#(.(y,z))) -->_1 del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)):7 3:W:=#(.(x,y),.(u(),v())) -> c_1(=#(x,u()),=#(y,v())) 4:W:=#(.(x,y),nil()) -> c_2() 5:W:=#(nil(),.(y,z)) -> c_3() 6:W:=#(nil(),nil()) -> c_4() 7:W:del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) -->_1 f#(true(),x,y,z) -> c_7(del#(.(y,z))):2 -->_1 f#(false(),x,y,z) -> c_6(del#(.(y,z))):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: =#(nil(),nil()) -> c_4() 5: =#(nil(),.(y,z)) -> c_3() 4: =#(.(x,y),nil()) -> c_2() 3: =#(.(x,y),.(u(),v())) -> c_1(=#(x,u()),=#(y,v())) * Step 6: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) - Weak DPs: del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) - Weak TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: f#(false(),x,y,z) -> c_6(del#(.(y,z))) 2: f#(true(),x,y,z) -> c_7(del#(.(y,z))) Consider the set of all dependency pairs 1: f#(false(),x,y,z) -> c_6(del#(.(y,z))) 2: f#(true(),x,y,z) -> c_7(del#(.(y,z))) 7: del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) BEST_CASE TIME (?,?) SPACE(?,?)on application of the dependency pairs {1,2} These cover all (indirect) predecessors of dependency pairs {1,2,7} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ** Step 6.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) - Weak DPs: del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) - Weak TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1} Following symbols are considered usable: {=,=#,del#,f#} TcT has computed the following interpretation: p(.) = [1] x2 + [2] p(=) = [1] p(and) = [1] x1 + [0] p(del) = [1] x1 + [1] p(f) = [2] x1 + [8] x3 + [1] x4 + [0] p(false) = [1] p(nil) = [0] p(true) = [1] p(u) = [0] p(v) = [1] p(=#) = [1] x1 + [8] p(del#) = [4] x1 + [0] p(f#) = [8] x1 + [4] x4 + [4] p(c_1) = [2] x2 + [2] p(c_2) = [1] p(c_3) = [0] p(c_4) = [1] p(c_5) = [1] x1 + [4] p(c_6) = [1] x1 + [1] p(c_7) = [1] x1 + [0] Following rules are strictly oriented: f#(false(),x,y,z) = [4] z + [12] > [4] z + [9] = c_6(del#(.(y,z))) f#(true(),x,y,z) = [4] z + [12] > [4] z + [8] = c_7(del#(.(y,z))) Following rules are (at-least) weakly oriented: del#(.(x,.(y,z))) = [4] z + [16] >= [4] z + [16] = c_5(f#(=(x,y),x,y,z)) =(.(x,y),.(u(),v())) = [1] >= [1] = and(=(x,u()),=(y,v())) =(.(x,y),nil()) = [1] >= [1] = false() =(nil(),.(y,z)) = [1] >= [1] = false() =(nil(),nil()) = [1] >= [1] = true() ** Step 6.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) - Weak TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ** Step 6.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) f#(false(),x,y,z) -> c_6(del#(.(y,z))) f#(true(),x,y,z) -> c_7(del#(.(y,z))) - Weak TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) -->_1 f#(true(),x,y,z) -> c_7(del#(.(y,z))):3 -->_1 f#(false(),x,y,z) -> c_6(del#(.(y,z))):2 2:W:f#(false(),x,y,z) -> c_6(del#(.(y,z))) -->_1 del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)):1 3:W:f#(true(),x,y,z) -> c_7(del#(.(y,z))) -->_1 del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: del#(.(x,.(y,z))) -> c_5(f#(=(x,y),x,y,z)) 3: f#(true(),x,y,z) -> c_7(del#(.(y,z))) 2: f#(false(),x,y,z) -> c_6(del#(.(y,z))) ** Step 6.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(.(x,y),nil()) -> false() =(nil(),.(y,z)) -> false() =(nil(),nil()) -> true() - Signature: {=/2,del/1,f/4,=#/2,del#/1,f#/4} / {./2,and/2,false/0,nil/0,true/0,u/0,v/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {=#,del#,f#} and constructors {.,and,false,nil,true,u,v} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))