WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_prefix_s1_s2_2(False(),x2,x1) -> False() cond_prefix_s1_s2_2(True(),x2,x1) -> prefix#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) -> prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) -> False() prefix#2(Cons(x8,x6),Cons(x4,x2)) -> cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) prefix#2(Nil(),x2) -> True() - Signature: {cond_prefix_s1_s2_2/3,eq#2/2,main/2,prefix#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_prefix_s1_s2_2,eq#2,main ,prefix#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_prefix_s1_s2_2) = {1} Following symbols are considered usable: {cond_prefix_s1_s2_2,eq#2,main,prefix#2} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [0] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(True) = [0] p(cond_prefix_s1_s2_2) = [8] x1 + [2] p(eq#2) = [0] p(main) = [1] x1 + [8] x2 + [8] p(prefix#2) = [2] Following rules are strictly oriented: cond_prefix_s1_s2_2(False(),x2,x1) = [2] > [0] = False() main(x2,x1) = [8] x1 + [1] x2 + [8] > [2] = prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) = [2] > [0] = False() prefix#2(Nil(),x2) = [2] > [0] = True() Following rules are (at-least) weakly oriented: cond_prefix_s1_s2_2(True(),x2,x1) = [2] >= [2] = prefix#2(x2,x1) 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) prefix#2(Cons(x8,x6),Cons(x4,x2)) = [2] >= [2] = cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_prefix_s1_s2_2(True(),x2,x1) -> prefix#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) prefix#2(Cons(x8,x6),Cons(x4,x2)) -> cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) - Weak TRS: cond_prefix_s1_s2_2(False(),x2,x1) -> False() main(x2,x1) -> prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) -> False() prefix#2(Nil(),x2) -> True() - Signature: {cond_prefix_s1_s2_2/3,eq#2/2,main/2,prefix#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_prefix_s1_s2_2,eq#2,main ,prefix#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_prefix_s1_s2_2) = {1} Following symbols are considered usable: {cond_prefix_s1_s2_2,eq#2,main,prefix#2} TcT has computed the following interpretation: p(0) = 0 p(Cons) = 4 + x2 p(False) = 0 p(Nil) = 3 p(S) = 8 + x1 p(True) = 0 p(cond_prefix_s1_s2_2) = 8*x1 + 6*x3 p(eq#2) = 2 p(main) = 13 + 9*x1 + 6*x2 p(prefix#2) = 6*x2 Following rules are strictly oriented: eq#2(0(),0()) = 2 > 0 = True() eq#2(0(),S(x16)) = 2 > 0 = False() eq#2(S(x16),0()) = 2 > 0 = False() prefix#2(Cons(x8,x6),Cons(x4,x2)) = 24 + 6*x2 > 16 + 6*x2 = cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) Following rules are (at-least) weakly oriented: cond_prefix_s1_s2_2(False(),x2,x1) = 6*x1 >= 0 = False() cond_prefix_s1_s2_2(True(),x2,x1) = 6*x1 >= 6*x1 = prefix#2(x2,x1) eq#2(S(x4),S(x2)) = 2 >= 2 = eq#2(x4,x2) main(x2,x1) = 13 + 6*x1 + 9*x2 >= 6*x1 = prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) = 18 >= 0 = False() prefix#2(Nil(),x2) = 6*x2 >= 0 = True() * Step 3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_prefix_s1_s2_2(True(),x2,x1) -> prefix#2(x2,x1) eq#2(S(x4),S(x2)) -> eq#2(x4,x2) - Weak TRS: cond_prefix_s1_s2_2(False(),x2,x1) -> False() eq#2(0(),0()) -> True() eq#2(0(),S(x16)) -> False() eq#2(S(x16),0()) -> False() main(x2,x1) -> prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) -> False() prefix#2(Cons(x8,x6),Cons(x4,x2)) -> cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) prefix#2(Nil(),x2) -> True() - Signature: {cond_prefix_s1_s2_2/3,eq#2/2,main/2,prefix#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_prefix_s1_s2_2,eq#2,main ,prefix#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_prefix_s1_s2_2) = {1} Following symbols are considered usable: {cond_prefix_s1_s2_2,eq#2,main,prefix#2} TcT has computed the following interpretation: p(0) = 0 p(Cons) = 2 + x1 + x2 p(False) = 0 p(Nil) = 4 p(S) = x1 p(True) = 0 p(cond_prefix_s1_s2_2) = 6 + x1 + 4*x3 p(eq#2) = 4*x2 p(main) = 2 + 3*x1 + 6*x2 p(prefix#2) = 1 + 4*x2 Following rules are strictly oriented: cond_prefix_s1_s2_2(True(),x2,x1) = 6 + 4*x1 > 1 + 4*x1 = prefix#2(x2,x1) Following rules are (at-least) weakly oriented: cond_prefix_s1_s2_2(False(),x2,x1) = 6 + 4*x1 >= 0 = False() eq#2(0(),0()) = 0 >= 0 = True() eq#2(0(),S(x16)) = 4*x16 >= 0 = False() eq#2(S(x16),0()) = 0 >= 0 = False() eq#2(S(x4),S(x2)) = 4*x2 >= 4*x2 = eq#2(x4,x2) main(x2,x1) = 2 + 6*x1 + 3*x2 >= 1 + 4*x1 = prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) = 17 >= 0 = False() prefix#2(Cons(x8,x6),Cons(x4,x2)) = 9 + 4*x2 + 4*x4 >= 6 + 4*x2 + 4*x4 = cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) prefix#2(Nil(),x2) = 1 + 4*x2 >= 0 = True() * Step 4: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: eq#2(S(x4),S(x2)) -> eq#2(x4,x2) - Weak TRS: cond_prefix_s1_s2_2(False(),x2,x1) -> False() cond_prefix_s1_s2_2(True(),x2,x1) -> prefix#2(x2,x1) eq#2(0(),0()) -> True() eq#2(0(),S(x16)) -> False() eq#2(S(x16),0()) -> False() main(x2,x1) -> prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) -> False() prefix#2(Cons(x8,x6),Cons(x4,x2)) -> cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) prefix#2(Nil(),x2) -> True() - Signature: {cond_prefix_s1_s2_2/3,eq#2/2,main/2,prefix#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_prefix_s1_s2_2,eq#2,main ,prefix#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_prefix_s1_s2_2) = {1} Following symbols are considered usable: {cond_prefix_s1_s2_2,eq#2,main,prefix#2} TcT has computed the following interpretation: p(0) = [2] p(Cons) = [1] x1 + [1] x2 + [0] p(False) = [5] p(Nil) = [0] p(S) = [1] x1 + [1] p(True) = [8] p(cond_prefix_s1_s2_2) = [1] x1 + [4] x2 + [7] p(eq#2) = [4] x1 + [1] p(main) = [4] x1 + [4] x2 + [12] p(prefix#2) = [4] x1 + [12] Following rules are strictly oriented: eq#2(S(x4),S(x2)) = [4] x4 + [5] > [4] x4 + [1] = eq#2(x4,x2) Following rules are (at-least) weakly oriented: cond_prefix_s1_s2_2(False(),x2,x1) = [4] x2 + [12] >= [5] = False() cond_prefix_s1_s2_2(True(),x2,x1) = [4] x2 + [15] >= [4] x2 + [12] = prefix#2(x2,x1) eq#2(0(),0()) = [9] >= [8] = True() eq#2(0(),S(x16)) = [9] >= [5] = False() eq#2(S(x16),0()) = [4] x16 + [5] >= [5] = False() main(x2,x1) = [4] x1 + [4] x2 + [12] >= [4] x2 + [12] = prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) = [4] x2 + [4] x4 + [12] >= [5] = False() prefix#2(Cons(x8,x6),Cons(x4,x2)) = [4] x6 + [4] x8 + [12] >= [4] x6 + [4] x8 + [8] = cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) prefix#2(Nil(),x2) = [12] >= [8] = True() * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: cond_prefix_s1_s2_2(False(),x2,x1) -> False() cond_prefix_s1_s2_2(True(),x2,x1) -> prefix#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) -> prefix#2(x2,x1) prefix#2(Cons(x4,x2),Nil()) -> False() prefix#2(Cons(x8,x6),Cons(x4,x2)) -> cond_prefix_s1_s2_2(eq#2(x8,x4),x6,x2) prefix#2(Nil(),x2) -> True() - Signature: {cond_prefix_s1_s2_2/3,eq#2/2,main/2,prefix#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_prefix_s1_s2_2,eq#2,main ,prefix#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))