WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs)) anyEq(nr,NilNat()) -> False() lookup(nr,Leaf(xs)) -> anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt) - Weak TRS: eq(0(),0()) -> True() eq(0(),S(m)) -> False() eq(S(n),0()) -> False() eq(S(n),S(m)) -> eq(n,m) ite(False(),t,e) -> e ite(True(),t,e) -> t leq(0(),0()) -> True() leq(0(),S(m)) -> True() leq(S(n),0()) -> False() leq(S(n),S(m)) -> leq(n,m) - Signature: {anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree ,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(ite) = {1,2,3} Following symbols are considered usable: {anyEq,eq,ite,leq,lookup} TcT has computed the following interpretation: p(0) = 1 p(ConsBTree) = x1 + x2 p(ConsNat) = x2 p(False) = 0 p(Leaf) = 0 p(NilBTree) = 1 p(NilNat) = 0 p(Node) = x1 + x2 p(S) = 2 p(True) = 0 p(anyEq) = 0 p(eq) = 0 p(ite) = 4*x1 + x2 + x3 p(leq) = 0 p(lookup) = 2*x2 Following rules are strictly oriented: lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = 2 + 2*tGt > 2*tGt = lookup(nr,tGt) Following rules are (at-least) weakly oriented: anyEq(nr,ConsNat(x,xs)) = 0 >= 0 = ite(eq(nr,x),True(),anyEq(nr,xs)) anyEq(nr,NilNat()) = 0 >= 0 = False() eq(0(),0()) = 0 >= 0 = True() eq(0(),S(m)) = 0 >= 0 = False() eq(S(n),0()) = 0 >= 0 = False() eq(S(n),S(m)) = 0 >= 0 = eq(n,m) ite(False(),t,e) = e + t >= e = e ite(True(),t,e) = e + t >= t = t leq(0(),0()) = 0 >= 0 = True() leq(0(),S(m)) = 0 >= 0 = True() leq(S(n),0()) = 0 >= 0 = False() leq(S(n),S(m)) = 0 >= 0 = leq(n,m) lookup(nr,Leaf(xs)) = 0 >= 0 = anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = 2*nrs + 2*t + 2*ts >= 2*nrs + 2*t + 2*ts = ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs)) anyEq(nr,NilNat()) -> False() lookup(nr,Leaf(xs)) -> anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) - Weak TRS: eq(0(),0()) -> True() eq(0(),S(m)) -> False() eq(S(n),0()) -> False() eq(S(n),S(m)) -> eq(n,m) ite(False(),t,e) -> e ite(True(),t,e) -> t leq(0(),0()) -> True() leq(0(),S(m)) -> True() leq(S(n),0()) -> False() leq(S(n),S(m)) -> leq(n,m) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt) - Signature: {anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree ,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(ite) = {1,2,3} Following symbols are considered usable: {anyEq,eq,ite,leq,lookup} TcT has computed the following interpretation: p(0) = 0 p(ConsBTree) = 7 + x1 + x2 p(ConsNat) = 1 + x2 p(False) = 0 p(Leaf) = 0 p(NilBTree) = 2 p(NilNat) = 0 p(Node) = x1 + x2 p(S) = 0 p(True) = 0 p(anyEq) = 0 p(eq) = 0 p(ite) = 4*x1 + x2 + x3 p(leq) = 0 p(lookup) = 4 + x2 Following rules are strictly oriented: lookup(nr,Leaf(xs)) = 4 > 0 = anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = 12 + nrs + t + ts > 8 + nrs + t + ts = ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) Following rules are (at-least) weakly oriented: anyEq(nr,ConsNat(x,xs)) = 0 >= 0 = ite(eq(nr,x),True(),anyEq(nr,xs)) anyEq(nr,NilNat()) = 0 >= 0 = False() eq(0(),0()) = 0 >= 0 = True() eq(0(),S(m)) = 0 >= 0 = False() eq(S(n),0()) = 0 >= 0 = False() eq(S(n),S(m)) = 0 >= 0 = eq(n,m) ite(False(),t,e) = e + t >= e = e ite(True(),t,e) = e + t >= t = t leq(0(),0()) = 0 >= 0 = True() leq(0(),S(m)) = 0 >= 0 = True() leq(S(n),0()) = 0 >= 0 = False() leq(S(n),S(m)) = 0 >= 0 = leq(n,m) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = 13 + tGt >= 4 + tGt = lookup(nr,tGt) * Step 3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs)) anyEq(nr,NilNat()) -> False() - Weak TRS: eq(0(),0()) -> True() eq(0(),S(m)) -> False() eq(S(n),0()) -> False() eq(S(n),S(m)) -> eq(n,m) ite(False(),t,e) -> e ite(True(),t,e) -> t leq(0(),0()) -> True() leq(0(),S(m)) -> True() leq(S(n),0()) -> False() leq(S(n),S(m)) -> leq(n,m) lookup(nr,Leaf(xs)) -> anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt) - Signature: {anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree ,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(ite) = {1,2,3} Following symbols are considered usable: {anyEq,eq,ite,leq,lookup} TcT has computed the following interpretation: p(0) = [6] p(ConsBTree) = [1] x1 + [1] x2 + [2] p(ConsNat) = [1] x1 + [1] x2 + [0] p(False) = [0] p(Leaf) = [0] p(NilBTree) = [0] p(NilNat) = [0] p(Node) = [1] x1 + [1] x2 + [0] p(S) = [1] x1 + [5] p(True) = [0] p(anyEq) = [1] p(eq) = [0] p(ite) = [2] x1 + [1] x2 + [1] x3 + [0] p(leq) = [1] x2 + [3] p(lookup) = [8] x2 + [1] Following rules are strictly oriented: anyEq(nr,NilNat()) = [1] > [0] = False() Following rules are (at-least) weakly oriented: anyEq(nr,ConsNat(x,xs)) = [1] >= [1] = ite(eq(nr,x),True(),anyEq(nr,xs)) eq(0(),0()) = [0] >= [0] = True() eq(0(),S(m)) = [0] >= [0] = False() eq(S(n),0()) = [0] >= [0] = False() eq(S(n),S(m)) = [0] >= [0] = eq(n,m) ite(False(),t,e) = [1] e + [1] t + [0] >= [1] e + [0] = e ite(True(),t,e) = [1] e + [1] t + [0] >= [1] t + [0] = t leq(0(),0()) = [9] >= [0] = True() leq(0(),S(m)) = [1] m + [8] >= [0] = True() leq(S(n),0()) = [9] >= [0] = False() leq(S(n),S(m)) = [1] m + [8] >= [1] m + [3] = leq(n,m) lookup(nr,Leaf(xs)) = [1] >= [1] = anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = [8] nrs + [8] t + [8] ts + [8] up + [17] >= [8] nrs + [8] t + [8] ts + [2] up + [8] = ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = [8] tGt + [17] >= [8] tGt + [1] = lookup(nr,tGt) * Step 4: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs)) - Weak TRS: anyEq(nr,NilNat()) -> False() eq(0(),0()) -> True() eq(0(),S(m)) -> False() eq(S(n),0()) -> False() eq(S(n),S(m)) -> eq(n,m) ite(False(),t,e) -> e ite(True(),t,e) -> t leq(0(),0()) -> True() leq(0(),S(m)) -> True() leq(S(n),0()) -> False() leq(S(n),S(m)) -> leq(n,m) lookup(nr,Leaf(xs)) -> anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt) - Signature: {anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree ,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(ite) = {1,2,3} Following symbols are considered usable: {anyEq,eq,ite,leq,lookup} TcT has computed the following interpretation: p(0) = 4 p(ConsBTree) = 4 + x1 + x2 p(ConsNat) = 4 + x1 + x2 p(False) = 0 p(Leaf) = 4 + x1 p(NilBTree) = 0 p(NilNat) = 2 p(Node) = x2 p(S) = x1 p(True) = 1 p(anyEq) = 4 + 2*x2 p(eq) = x2 p(ite) = 4 + x1 + x2 + x3 p(leq) = 2 p(lookup) = 2*x2 Following rules are strictly oriented: anyEq(nr,ConsNat(x,xs)) = 12 + 2*x + 2*xs > 9 + x + 2*xs = ite(eq(nr,x),True(),anyEq(nr,xs)) Following rules are (at-least) weakly oriented: anyEq(nr,NilNat()) = 8 >= 0 = False() eq(0(),0()) = 4 >= 1 = True() eq(0(),S(m)) = m >= 0 = False() eq(S(n),0()) = 4 >= 0 = False() eq(S(n),S(m)) = m >= m = eq(n,m) ite(False(),t,e) = 4 + e + t >= e = e ite(True(),t,e) = 5 + e + t >= t = t leq(0(),0()) = 2 >= 1 = True() leq(0(),S(m)) = 2 >= 1 = True() leq(S(n),0()) = 2 >= 0 = False() leq(S(n),S(m)) = 2 >= 2 = leq(n,m) lookup(nr,Leaf(xs)) = 8 + 2*xs >= 4 + 2*xs = anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = 8 + 2*t + 2*ts >= 6 + 2*t + 2*ts = ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = 8 + 2*tGt >= 2*tGt = lookup(nr,tGt) * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs)) anyEq(nr,NilNat()) -> False() eq(0(),0()) -> True() eq(0(),S(m)) -> False() eq(S(n),0()) -> False() eq(S(n),S(m)) -> eq(n,m) ite(False(),t,e) -> e ite(True(),t,e) -> t leq(0(),0()) -> True() leq(0(),S(m)) -> True() leq(S(n),0()) -> False() leq(S(n),S(m)) -> leq(n,m) lookup(nr,Leaf(xs)) -> anyEq(nr,xs) lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts))) lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt) - Signature: {anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree ,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))