WORST_CASE(?,O(n^1)) * Step 1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: mem(x,nil()) -> false() mem(x,set(y)) -> =(x,y) mem(x,union(y,z)) -> or(mem(x,y),mem(x,z)) or(x,true()) -> true() or(false(),false()) -> false() or(true(),y) -> true() - Signature: {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2} - Obligation: innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union} + 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(or) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(=) = [0] p(false) = [3] p(mem) = [4] x2 + [4] p(nil) = [1] p(or) = [1] x1 + [1] x2 + [12] p(set) = [3] p(true) = [8] p(union) = [1] x1 + [1] x2 + [6] Following rules are strictly oriented: mem(x,nil()) = [8] > [3] = false() mem(x,set(y)) = [16] > [0] = =(x,y) mem(x,union(y,z)) = [4] y + [4] z + [28] > [4] y + [4] z + [20] = or(mem(x,y),mem(x,z)) or(x,true()) = [1] x + [20] > [8] = true() or(false(),false()) = [18] > [3] = false() or(true(),y) = [1] y + [20] > [8] = true() Following rules are (at-least) weakly oriented: Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: mem(x,nil()) -> false() mem(x,set(y)) -> =(x,y) mem(x,union(y,z)) -> or(mem(x,y),mem(x,z)) or(x,true()) -> true() or(false(),false()) -> false() or(true(),y) -> true() - Signature: {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2} - Obligation: innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))