WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) -> Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() lt#2(S(x4),S(x2)) -> lt#2(x4,x2) main(x4,Nil()) -> Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48) ,Node(x100,x132,x164) ,Node(x48,x64,x80) ,x28) - Signature: {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2 ,main} and constructors {0,Cons,Elem,False,Nil,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(Cons) = {1}, uargs(cond_insTree_t_xs_1) = {1}, uargs(cond_link_t1_t2_2) = {1} Following symbols are considered usable: {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2,main} TcT has computed the following interpretation: p(0) = 0 p(Cons) = x1 p(Elem) = 4 p(False) = 0 p(Nil) = 0 p(Node) = 2 p(S) = 0 p(True) = 0 p(cond_insTree_t_xs_1) = x1 + 4*x2 p(cond_link_t1_t2_2) = 2 + 4*x1 p(leq#2) = 0 p(lt#2) = 0 p(main) = 4*x1 Following rules are strictly oriented: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) = 8 > 2 = Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) = 8 > 2 = Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) Following rules are (at-least) weakly oriented: cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = 2 >= 2 = Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = 2 >= 2 = Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) = 0 >= 0 = True() leq#2(S(x24),0()) = 0 >= 0 = False() leq#2(S(x4),S(x2)) = 0 >= 0 = leq#2(x4,x2) lt#2(0(),0()) = 0 >= 0 = False() lt#2(0(),S(x20)) = 0 >= 0 = True() lt#2(S(x20),0()) = 0 >= 0 = False() lt#2(S(x4),S(x2)) = 0 >= 0 = lt#2(x4,x2) main(x4,Nil()) = 4*x4 >= x4 = Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) = 8 >= 8 = cond_insTree_t_xs_1(lt#2(x100,x48),Node(x100,x132,x164),Node(x48,x64,x80),x28) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() lt#2(S(x4),S(x2)) -> lt#2(x4,x2) main(x4,Nil()) -> Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48) ,Node(x100,x132,x164) ,Node(x48,x64,x80) ,x28) - Weak TRS: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) -> Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) - Signature: {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2 ,main} and constructors {0,Cons,Elem,False,Nil,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(Cons) = {1}, uargs(cond_insTree_t_xs_1) = {1}, uargs(cond_link_t1_t2_2) = {1} Following symbols are considered usable: {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2,main} TcT has computed the following interpretation: p(0) = 1 p(Cons) = 2 + x1 p(Elem) = 4 p(False) = 0 p(Nil) = 4 p(Node) = 0 p(S) = 0 p(True) = 0 p(cond_insTree_t_xs_1) = 2 + 4*x1 + x2 p(cond_link_t1_t2_2) = 4*x1 p(leq#2) = 0 p(lt#2) = 1 p(main) = 6 + 4*x1 Following rules are strictly oriented: lt#2(0(),0()) = 1 > 0 = False() lt#2(0(),S(x20)) = 1 > 0 = True() lt#2(S(x20),0()) = 1 > 0 = False() main(x4,Nil()) = 6 + 4*x4 > 2 + x4 = Cons(x4,Nil()) Following rules are (at-least) weakly oriented: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) = 2 >= 2 = Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) = 2 >= 2 = Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = 0 >= 0 = Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = 0 >= 0 = Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) = 0 >= 0 = True() leq#2(S(x24),0()) = 0 >= 0 = False() leq#2(S(x4),S(x2)) = 0 >= 0 = leq#2(x4,x2) lt#2(S(x4),S(x2)) = 1 >= 1 = lt#2(x4,x2) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) = 6 >= 6 = cond_insTree_t_xs_1(lt#2(x100,x48),Node(x100,x132,x164),Node(x48,x64,x80),x28) * Step 3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) lt#2(S(x4),S(x2)) -> lt#2(x4,x2) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48) ,Node(x100,x132,x164) ,Node(x48,x64,x80) ,x28) - Weak TRS: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) -> Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() main(x4,Nil()) -> Cons(x4,Nil()) - Signature: {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2 ,main} and constructors {0,Cons,Elem,False,Nil,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(Cons) = {1}, uargs(cond_insTree_t_xs_1) = {1}, uargs(cond_link_t1_t2_2) = {1} Following symbols are considered usable: {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2,main} TcT has computed the following interpretation: p(0) = 0 p(Cons) = 1 + x1 + x2 p(Elem) = 1 p(False) = 0 p(Nil) = 2 p(Node) = 1 p(S) = 0 p(True) = 0 p(cond_insTree_t_xs_1) = 4 + 2*x1 + 6*x3 + x4 p(cond_link_t1_t2_2) = 2*x1 + 3*x2 + x3 + 4*x7 p(leq#2) = 0 p(lt#2) = 1 p(main) = x1 + 7*x2 Following rules are strictly oriented: cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = 8 > 1 = Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = 8 > 1 = Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) = 15 + 7*x28 > 12 + x28 = cond_insTree_t_xs_1(lt#2(x100,x48),Node(x100,x132,x164),Node(x48,x64,x80),x28) Following rules are (at-least) weakly oriented: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) = 12 >= 11 = Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) = 10 + x1 >= 4 + x1 = Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) leq#2(0(),x20) = 0 >= 0 = True() leq#2(S(x24),0()) = 0 >= 0 = False() leq#2(S(x4),S(x2)) = 0 >= 0 = leq#2(x4,x2) lt#2(0(),0()) = 1 >= 0 = False() lt#2(0(),S(x20)) = 1 >= 0 = True() lt#2(S(x20),0()) = 1 >= 0 = False() lt#2(S(x4),S(x2)) = 1 >= 1 = lt#2(x4,x2) main(x4,Nil()) = 14 + x4 >= 3 + x4 = Cons(x4,Nil()) * Step 4: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) lt#2(S(x4),S(x2)) -> lt#2(x4,x2) - Weak TRS: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) -> Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() main(x4,Nil()) -> Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48) ,Node(x100,x132,x164) ,Node(x48,x64,x80) ,x28) - Signature: {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2 ,main} and constructors {0,Cons,Elem,False,Nil,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(Cons) = {1}, uargs(cond_insTree_t_xs_1) = {1}, uargs(cond_link_t1_t2_2) = {1} Following symbols are considered usable: {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2,main} TcT has computed the following interpretation: p(0) = [4] p(Cons) = [1] x1 + [1] x2 + [0] p(Elem) = [1] p(False) = [6] p(Nil) = [4] p(Node) = [1] p(S) = [1] p(True) = [4] p(cond_insTree_t_xs_1) = [1] x1 + [2] x4 + [0] p(cond_link_t1_t2_2) = [1] x1 + [2] x5 + [0] p(leq#2) = [7] p(lt#2) = [6] p(main) = [6] x1 + [2] x2 + [7] Following rules are strictly oriented: leq#2(0(),x20) = [7] > [4] = True() leq#2(S(x24),0()) = [7] > [6] = False() Following rules are (at-least) weakly oriented: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) = [14] >= [13] = Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) = [2] x1 + [4] >= [1] x1 + [2] = Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = [8] >= [1] = Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = [6] >= [1] = Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(S(x4),S(x2)) = [7] >= [7] = leq#2(x4,x2) lt#2(0(),0()) = [6] >= [6] = False() lt#2(0(),S(x20)) = [6] >= [4] = True() lt#2(S(x20),0()) = [6] >= [6] = False() lt#2(S(x4),S(x2)) = [6] >= [6] = lt#2(x4,x2) main(x4,Nil()) = [6] x4 + [15] >= [1] x4 + [4] = Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) = [2] x28 + [15] >= [2] x28 + [6] = cond_insTree_t_xs_1(lt#2(x100,x48),Node(x100,x132,x164),Node(x48,x64,x80),x28) * Step 5: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: leq#2(S(x4),S(x2)) -> leq#2(x4,x2) lt#2(S(x4),S(x2)) -> lt#2(x4,x2) - Weak TRS: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) -> Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() main(x4,Nil()) -> Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48) ,Node(x100,x132,x164) ,Node(x48,x64,x80) ,x28) - Signature: {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2 ,main} and constructors {0,Cons,Elem,False,Nil,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(Cons) = {1}, uargs(cond_insTree_t_xs_1) = {1}, uargs(cond_link_t1_t2_2) = {1} Following symbols are considered usable: {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2,main} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [3] p(Elem) = [4] p(False) = [1] p(Nil) = [2] p(Node) = [1] x1 + [1] x2 + [0] p(S) = [1] x1 + [4] p(True) = [1] p(cond_insTree_t_xs_1) = [2] x1 + [2] x2 + [1] p(cond_link_t1_t2_2) = [2] x1 + [1] x4 + [1] x5 + [2] p(leq#2) = [1] p(lt#2) = [2] x2 + [5] p(main) = [3] x1 + [4] x2 + [1] Following rules are strictly oriented: lt#2(S(x4),S(x2)) = [2] x2 + [13] > [2] x2 + [5] = lt#2(x4,x2) Following rules are (at-least) weakly oriented: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) = [2] x54 + [11] >= [1] x54 + [11] = Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) = [2] x5 + [2] x6 + [3] >= [1] x5 + [1] x6 + [3] = Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = [1] x5 + [8] >= [1] x5 + [8] = Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = [1] x5 + [8] >= [1] x5 + [8] = Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) = [1] >= [1] = True() leq#2(S(x24),0()) = [1] >= [1] = False() leq#2(S(x4),S(x2)) = [1] >= [1] = leq#2(x4,x2) lt#2(0(),0()) = [5] >= [1] = False() lt#2(0(),S(x20)) = [2] x20 + [13] >= [1] = True() lt#2(S(x20),0()) = [5] >= [1] = False() main(x4,Nil()) = [3] x4 + [9] >= [1] x4 + [3] = Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) = [3] x100 + [3] x132 + [4] x48 + [4] x64 + [13] >= [2] x100 + [2] x132 + [4] x48 + [11] = cond_insTree_t_xs_1(lt#2(x100,x48),Node(x100,x132,x164),Node(x48,x64,x80),x28) * Step 6: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: leq#2(S(x4),S(x2)) -> leq#2(x4,x2) - Weak TRS: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) -> Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() lt#2(S(x4),S(x2)) -> lt#2(x4,x2) main(x4,Nil()) -> Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48) ,Node(x100,x132,x164) ,Node(x48,x64,x80) ,x28) - Signature: {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2 ,main} and constructors {0,Cons,Elem,False,Nil,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(Cons) = {1}, uargs(cond_insTree_t_xs_1) = {1}, uargs(cond_link_t1_t2_2) = {1} Following symbols are considered usable: {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2,main} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [4] p(Elem) = [1] x1 + [0] p(False) = [3] p(Nil) = [3] p(Node) = [1] x2 + [1] x3 + [0] p(S) = [1] x1 + [1] p(True) = [4] p(cond_insTree_t_xs_1) = [2] x1 + [7] x2 + [3] x3 + [3] x4 + [0] p(cond_link_t1_t2_2) = [2] x1 + [1] x2 + [2] x3 + [4] x5 + [2] x6 + [1] x7 + [1] x8 + [0] p(leq#2) = [1] x1 + [4] p(lt#2) = [5] p(main) = [7] x1 + [3] x2 + [2] Following rules are strictly oriented: leq#2(S(x4),S(x2)) = [1] x4 + [5] > [1] x4 + [4] = leq#2(x4,x2) Following rules are (at-least) weakly oriented: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) = [3] x14 + [7] x38 + [3] x4 + [7] x8 + [15] >= [3] x14 + [3] x38 + [3] x4 + [7] x8 + [15] = Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) = [3] x1 + [3] x3 + [3] x4 + [7] x6 + [7] x7 + [8] >= [1] x1 + [1] x3 + [1] x4 + [1] x6 + [1] x7 + [8] = Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = [1] x1 + [1] x10 + [1] x2 + [2] x3 + [4] x4 + [2] x6 + [2] x7 + [1] x9 + [6] >= [1] x1 + [1] x10 + [1] x2 + [1] x9 + [4] = Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) = [1] x1 + [1] x10 + [1] x2 + [2] x3 + [4] x4 + [2] x6 + [2] x7 + [1] x9 + [8] >= [1] x3 + [1] x4 + [1] x6 + [1] x7 + [4] = Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) = [4] >= [4] = True() leq#2(S(x24),0()) = [1] x24 + [5] >= [3] = False() lt#2(0(),0()) = [5] >= [3] = False() lt#2(0(),S(x20)) = [5] >= [4] = True() lt#2(S(x20),0()) = [5] >= [3] = False() lt#2(S(x4),S(x2)) = [5] >= [5] = lt#2(x4,x2) main(x4,Nil()) = [7] x4 + [11] >= [1] x4 + [7] = Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) = [7] x132 + [7] x164 + [3] x28 + [3] x64 + [3] x80 + [14] >= [7] x132 + [7] x164 + [3] x28 + [3] x64 + [3] x80 + [10] = cond_insTree_t_xs_1(lt#2(x100,x48),Node(x100,x132,x164),Node(x48,x64,x80),x28) * Step 7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) -> Cons(cond_link_t1_t2_2(leq#2(x8,x4) ,Node(x54,Elem(x8),x38) ,Node(x30,Elem(x4),x14) ,x54 ,Elem(x8) ,x38 ,Elem(x4) ,x14) ,Nil()) cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),x1)) cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1)) cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) -> Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3)) leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() lt#2(S(x4),S(x2)) -> lt#2(x4,x2) main(x4,Nil()) -> Cons(x4,Nil()) main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48) ,Node(x100,x132,x164) ,Node(x48,x64,x80) ,x28) - Signature: {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2,leq#2,lt#2 ,main} and constructors {0,Cons,Elem,False,Nil,Node,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))