* Step 1: WeightGap 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: 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 = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(.) = {2}, uargs(f) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(.) = [1] x2 + [0] p(=) = [0] p(and) = [1] x1 + [1] x2 + [0] p(del) = [0] p(f) = [1] x1 + [5] p(false) = [0] p(nil) = [0] p(true) = [0] p(u) = [0] p(v) = [0] Following rules are strictly oriented: f(false(),x,y,z) = [5] > [0] = .(x,del(.(y,z))) f(true(),x,y,z) = [5] > [0] = del(.(y,z)) Following rules are (at-least) weakly oriented: =(.(x,y),.(u(),v())) = [0] >= [0] = and(=(x,u()),=(y,v())) =(.(x,y),nil()) = [0] >= [0] = false() =(nil(),.(y,z)) = [0] >= [0] = false() =(nil(),nil()) = [0] >= [0] = true() del(.(x,.(y,z))) = [0] >= [5] = f(=(x,y),x,y,z) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap 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) - Weak TRS: 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: 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 = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(.) = {2}, uargs(f) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(.) = [1] x1 + [1] x2 + [4] p(=) = [1] x1 + [0] p(and) = [0] p(del) = [2] x1 + [1] p(f) = [1] x1 + [1] x2 + [2] x3 + [2] x4 + [9] p(false) = [4] p(nil) = [8] p(true) = [0] p(u) = [8] p(v) = [0] Following rules are strictly oriented: =(.(x,y),.(u(),v())) = [1] x + [1] y + [4] > [0] = and(=(x,u()),=(y,v())) =(nil(),.(y,z)) = [8] > [4] = false() =(nil(),nil()) = [8] > [0] = true() del(.(x,.(y,z))) = [2] x + [2] y + [2] z + [17] > [2] x + [2] y + [2] z + [9] = f(=(x,y),x,y,z) Following rules are (at-least) weakly oriented: =(.(x,y),nil()) = [1] x + [1] y + [4] >= [4] = false() f(false(),x,y,z) = [1] x + [2] y + [2] z + [13] >= [1] x + [2] y + [2] z + [13] = .(x,del(.(y,z))) f(true(),x,y,z) = [1] x + [2] y + [2] z + [9] >= [2] y + [2] z + [9] = del(.(y,z)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: =(.(x,y),nil()) -> false() - Weak TRS: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v())) =(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: 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 = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(.) = {2}, uargs(f) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(.) = [1] x1 + [1] x2 + [1] p(=) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [1] p(del) = [2] x1 + [2] p(f) = [1] x1 + [1] x2 + [2] x3 + [2] x4 + [6] p(false) = [0] p(nil) = [0] p(true) = [0] p(u) = [1] p(v) = [0] Following rules are strictly oriented: =(.(x,y),nil()) = [1] x + [1] y + [1] > [0] = false() Following rules are (at-least) weakly oriented: =(.(x,y),.(u(),v())) = [1] x + [1] y + [1] >= [1] x + [1] y + [1] = and(=(x,u()),=(y,v())) =(nil(),.(y,z)) = [0] >= [0] = false() =(nil(),nil()) = [0] >= [0] = true() del(.(x,.(y,z))) = [2] x + [2] y + [2] z + [6] >= [2] x + [2] y + [2] z + [6] = f(=(x,y),x,y,z) f(false(),x,y,z) = [1] x + [2] y + [2] z + [6] >= [1] x + [2] y + [2] z + [5] = .(x,del(.(y,z))) f(true(),x,y,z) = [1] x + [2] y + [2] z + [6] >= [2] y + [2] z + [4] = del(.(y,z)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: 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() 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: 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))