WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_string_dec_s_s0_3(False(),x2,x1) -> False() cond_string_dec_s_s0_3(True(),x2,x1) -> string_dec#2(x2,x1) eq#2(0(),0()) -> True() eq#2(0(),S(x16)) -> False() eq#2(S(x16),0()) -> False() eq#2(S(x4),S(x2)) -> eq#2(x4,x2) main(x2,x1) -> string_dec#2(x2,x1) string_dec#2(Cons(x4,x2),Nil()) -> False() string_dec#2(Cons(x8,x6),Cons(x4,x2)) -> cond_string_dec_s_s0_3(eq#2(x8,x4),x6,x2) string_dec#2(Nil(),Cons(x4,x2)) -> False() string_dec#2(Nil(),Nil()) -> True() - Signature: {cond_string_dec_s_s0_3/3,eq#2/2,main/2,string_dec#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_string_dec_s_s0_3,eq#2,main ,string_dec#2} and constructors {0,Cons,False,Nil,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(cond_string_dec_s_s0_3) = {1} Following symbols are considered usable: {cond_string_dec_s_s0_3,eq#2,main,string_dec#2} TcT has computed the following interpretation: p(0) = 0 p(Cons) = 4 + x1 + x2 p(False) = 0 p(Nil) = 4 p(S) = 0 p(True) = 0 p(cond_string_dec_s_s0_3) = 2 + 8*x1 + 4*x3 p(eq#2) = 0 p(main) = 1 + x1 + 5*x2 p(string_dec#2) = 4*x2 Following rules are strictly oriented: cond_string_dec_s_s0_3(False(),x2,x1) = 2 + 4*x1 > 0 = False() cond_string_dec_s_s0_3(True(),x2,x1) = 2 + 4*x1 > 4*x1 = string_dec#2(x2,x1) main(x2,x1) = 1 + 5*x1 + x2 > 4*x1 = string_dec#2(x2,x1) string_dec#2(Cons(x4,x2),Nil()) = 16 > 0 = False() string_dec#2(Cons(x8,x6),Cons(x4,x2)) = 16 + 4*x2 + 4*x4 > 2 + 4*x2 = cond_string_dec_s_s0_3(eq#2(x8,x4),x6,x2) string_dec#2(Nil(),Cons(x4,x2)) = 16 + 4*x2 + 4*x4 > 0 = False() string_dec#2(Nil(),Nil()) = 16 > 0 = True() Following rules are (at-least) weakly oriented: eq#2(0(),0()) = 0 >= 0 = True() eq#2(0(),S(x16)) = 0 >= 0 = False() eq#2(S(x16),0()) = 0 >= 0 = False() eq#2(S(x4),S(x2)) = 0 >= 0 = eq#2(x4,x2) * Step 2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: eq#2(0(),0()) -> True() eq#2(0(),S(x16)) -> False() eq#2(S(x16),0()) -> False() eq#2(S(x4),S(x2)) -> eq#2(x4,x2) - Weak TRS: cond_string_dec_s_s0_3(False(),x2,x1) -> False() cond_string_dec_s_s0_3(True(),x2,x1) -> string_dec#2(x2,x1) main(x2,x1) -> string_dec#2(x2,x1) string_dec#2(Cons(x4,x2),Nil()) -> False() string_dec#2(Cons(x8,x6),Cons(x4,x2)) -> cond_string_dec_s_s0_3(eq#2(x8,x4),x6,x2) string_dec#2(Nil(),Cons(x4,x2)) -> False() string_dec#2(Nil(),Nil()) -> True() - Signature: {cond_string_dec_s_s0_3/3,eq#2/2,main/2,string_dec#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_string_dec_s_s0_3,eq#2,main ,string_dec#2} and constructors {0,Cons,False,Nil,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(cond_string_dec_s_s0_3) = {1} Following symbols are considered usable: {cond_string_dec_s_s0_3,eq#2,main,string_dec#2} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [0] p(False) = [0] p(Nil) = [0] p(S) = [0] p(True) = [1] p(cond_string_dec_s_s0_3) = [8] x1 + [0] p(eq#2) = [1] p(main) = [8] p(string_dec#2) = [8] Following rules are strictly oriented: eq#2(0(),S(x16)) = [1] > [0] = False() eq#2(S(x16),0()) = [1] > [0] = False() Following rules are (at-least) weakly oriented: cond_string_dec_s_s0_3(False(),x2,x1) = [0] >= [0] = False() cond_string_dec_s_s0_3(True(),x2,x1) = [8] >= [8] = string_dec#2(x2,x1) eq#2(0(),0()) = [1] >= [1] = True() eq#2(S(x4),S(x2)) = [1] >= [1] = eq#2(x4,x2) main(x2,x1) = [8] >= [8] = string_dec#2(x2,x1) string_dec#2(Cons(x4,x2),Nil()) = [8] >= [0] = False() string_dec#2(Cons(x8,x6),Cons(x4,x2)) = [8] >= [8] = cond_string_dec_s_s0_3(eq#2(x8,x4),x6,x2) string_dec#2(Nil(),Cons(x4,x2)) = [8] >= [0] = False() string_dec#2(Nil(),Nil()) = [8] >= [1] = True() * Step 3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: eq#2(0(),0()) -> True() eq#2(S(x4),S(x2)) -> eq#2(x4,x2) - Weak TRS: cond_string_dec_s_s0_3(False(),x2,x1) -> False() cond_string_dec_s_s0_3(True(),x2,x1) -> string_dec#2(x2,x1) eq#2(0(),S(x16)) -> False() eq#2(S(x16),0()) -> False() main(x2,x1) -> string_dec#2(x2,x1) string_dec#2(Cons(x4,x2),Nil()) -> False() string_dec#2(Cons(x8,x6),Cons(x4,x2)) -> cond_string_dec_s_s0_3(eq#2(x8,x4),x6,x2) string_dec#2(Nil(),Cons(x4,x2)) -> False() string_dec#2(Nil(),Nil()) -> True() - Signature: {cond_string_dec_s_s0_3/3,eq#2/2,main/2,string_dec#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_string_dec_s_s0_3,eq#2,main ,string_dec#2} and constructors {0,Cons,False,Nil,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(cond_string_dec_s_s0_3) = {1} Following symbols are considered usable: {cond_string_dec_s_s0_3,eq#2,main,string_dec#2} TcT has computed the following interpretation: p(0) = [1] p(Cons) = [1] x1 + [1] x2 + [3] p(False) = [0] p(Nil) = [1] p(S) = [1] x1 + [2] p(True) = [0] p(cond_string_dec_s_s0_3) = [4] x1 + [8] x2 + [1] x3 + [0] p(eq#2) = [2] x1 + [3] p(main) = [12] x1 + [1] x2 + [10] p(string_dec#2) = [8] x1 + [1] x2 + [0] Following rules are strictly oriented: eq#2(0(),0()) = [5] > [0] = True() eq#2(S(x4),S(x2)) = [2] x4 + [7] > [2] x4 + [3] = eq#2(x4,x2) Following rules are (at-least) weakly oriented: cond_string_dec_s_s0_3(False(),x2,x1) = [1] x1 + [8] x2 + [0] >= [0] = False() cond_string_dec_s_s0_3(True(),x2,x1) = [1] x1 + [8] x2 + [0] >= [1] x1 + [8] x2 + [0] = string_dec#2(x2,x1) eq#2(0(),S(x16)) = [5] >= [0] = False() eq#2(S(x16),0()) = [2] x16 + [7] >= [0] = False() main(x2,x1) = [1] x1 + [12] x2 + [10] >= [1] x1 + [8] x2 + [0] = string_dec#2(x2,x1) string_dec#2(Cons(x4,x2),Nil()) = [8] x2 + [8] x4 + [25] >= [0] = False() string_dec#2(Cons(x8,x6),Cons(x4,x2)) = [1] x2 + [1] x4 + [8] x6 + [8] x8 + [27] >= [1] x2 + [8] x6 + [8] x8 + [12] = cond_string_dec_s_s0_3(eq#2(x8,x4),x6,x2) string_dec#2(Nil(),Cons(x4,x2)) = [1] x2 + [1] x4 + [11] >= [0] = False() string_dec#2(Nil(),Nil()) = [9] >= [0] = True() * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: cond_string_dec_s_s0_3(False(),x2,x1) -> False() cond_string_dec_s_s0_3(True(),x2,x1) -> string_dec#2(x2,x1) eq#2(0(),0()) -> True() eq#2(0(),S(x16)) -> False() eq#2(S(x16),0()) -> False() eq#2(S(x4),S(x2)) -> eq#2(x4,x2) main(x2,x1) -> string_dec#2(x2,x1) string_dec#2(Cons(x4,x2),Nil()) -> False() string_dec#2(Cons(x8,x6),Cons(x4,x2)) -> cond_string_dec_s_s0_3(eq#2(x8,x4),x6,x2) string_dec#2(Nil(),Cons(x4,x2)) -> False() string_dec#2(Nil(),Nil()) -> True() - Signature: {cond_string_dec_s_s0_3/3,eq#2/2,main/2,string_dec#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_string_dec_s_s0_3,eq#2,main ,string_dec#2} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))