WORST_CASE(?,O(n^1)) * Step 1: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: 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: {mem,or} TcT has computed the following interpretation: p(=) = [1] x2 + [10] p(false) = [4] p(mem) = [1] x2 + [0] p(nil) = [7] p(or) = [1] x1 + [1] x2 + [2] p(set) = [1] x1 + [12] p(true) = [0] p(union) = [1] x1 + [1] x2 + [3] Following rules are strictly oriented: mem(x,nil()) = [7] > [4] = false() mem(x,set(y)) = [1] y + [12] > [1] y + [10] = =(x,y) mem(x,union(y,z)) = [1] y + [1] z + [3] > [1] y + [1] z + [2] = or(mem(x,y),mem(x,z)) or(x,true()) = [1] x + [2] > [0] = true() or(false(),false()) = [10] > [4] = false() or(true(),y) = [1] y + [2] > [0] = true() Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))