WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3 ,mark/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1,if/3,nil/0 ,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__AND,A__FIRST,A__FROM,A__IF,MARK,a__add,a__and ,a__first,a__from,a__if,mark} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2 ,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3 ,mark/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1,if/3,nil/0 ,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__AND,A__FIRST,A__FROM,A__IF,MARK,a__add,a__and ,a__first,a__from,a__if,mark} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2 ,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3 ,mark/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1,if/3,nil/0 ,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__AND,A__FIRST,A__FROM,A__IF,MARK,a__add,a__and ,a__first,a__from,a__if,mark} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2 ,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> add(x,y)} = MARK(add(x,y)) ->^+ c16(A__ADD(mark(x),y),MARK(x)) = C[MARK(x) = MARK(x){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3 ,mark/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1,if/3,nil/0 ,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__AND,A__FIRST,A__FROM,A__IF,MARK,a__add,a__and ,a__first,a__from,a__if,mark} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2 ,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs A__ADD#(z0,z1) -> c_1() A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__ADD#(s(z0),z1) -> c_3() A__AND#(z0,z1) -> c_4() A__AND#(false(),z0) -> c_5() A__AND#(true(),z0) -> c_6(MARK#(z0)) A__FIRST#(z0,z1) -> c_7() A__FIRST#(0(),z0) -> c_8() A__FIRST#(s(z0),cons(z1,z2)) -> c_9() A__FROM#(z0) -> c_10() A__FROM#(z0) -> c_11() A__IF#(z0,z1,z2) -> c_12() A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(0()) -> c_15() MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(cons(z0,z1)) -> c_18() MARK#(false()) -> c_19() MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) MARK#(from(z0)) -> c_22(A__FROM#(z0)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) MARK#(nil()) -> c_24() MARK#(s(z0)) -> c_25() MARK#(true()) -> c_26() Weak DPs a__add#(z0,z1) -> c_27() a__add#(0(),z0) -> c_28(mark#(z0)) a__add#(s(z0),z1) -> c_29() a__and#(z0,z1) -> c_30() a__and#(false(),z0) -> c_31() a__and#(true(),z0) -> c_32(mark#(z0)) a__first#(z0,z1) -> c_33() a__first#(0(),z0) -> c_34() a__first#(s(z0),cons(z1,z2)) -> c_35() a__from#(z0) -> c_36() a__from#(z0) -> c_37() a__if#(z0,z1,z2) -> c_38() a__if#(false(),z0,z1) -> c_39(mark#(z1)) a__if#(true(),z0,z1) -> c_40(mark#(z0)) mark#(0()) -> c_41() mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) mark#(cons(z0,z1)) -> c_44() mark#(false()) -> c_45() mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) mark#(from(z0)) -> c_47(a__from#(z0)) mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) mark#(nil()) -> c_49() mark#(s(z0)) -> c_50() mark#(true()) -> c_51() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(z0,z1) -> c_1() A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__ADD#(s(z0),z1) -> c_3() A__AND#(z0,z1) -> c_4() A__AND#(false(),z0) -> c_5() A__AND#(true(),z0) -> c_6(MARK#(z0)) A__FIRST#(z0,z1) -> c_7() A__FIRST#(0(),z0) -> c_8() A__FIRST#(s(z0),cons(z1,z2)) -> c_9() A__FROM#(z0) -> c_10() A__FROM#(z0) -> c_11() A__IF#(z0,z1,z2) -> c_12() A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(0()) -> c_15() MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(cons(z0,z1)) -> c_18() MARK#(false()) -> c_19() MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) MARK#(from(z0)) -> c_22(A__FROM#(z0)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) MARK#(nil()) -> c_24() MARK#(s(z0)) -> c_25() MARK#(true()) -> c_26() - Weak DPs: a__add#(z0,z1) -> c_27() a__add#(0(),z0) -> c_28(mark#(z0)) a__add#(s(z0),z1) -> c_29() a__and#(z0,z1) -> c_30() a__and#(false(),z0) -> c_31() a__and#(true(),z0) -> c_32(mark#(z0)) a__first#(z0,z1) -> c_33() a__first#(0(),z0) -> c_34() a__first#(s(z0),cons(z1,z2)) -> c_35() a__from#(z0) -> c_36() a__from#(z0) -> c_37() a__if#(z0,z1,z2) -> c_38() a__if#(false(),z0,z1) -> c_39(mark#(z1)) a__if#(true(),z0,z1) -> c_40(mark#(z0)) mark#(0()) -> c_41() mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) mark#(cons(z0,z1)) -> c_44() mark#(false()) -> c_45() mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) mark#(from(z0)) -> c_47(a__from#(z0)) mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) mark#(nil()) -> c_49() mark#(s(z0)) -> c_50() mark#(true()) -> c_51() - Weak TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/3,c_17/3,c_18/0,c_19/0,c_20/4,c_21/4,c_22/1,c_23/3,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,4,5,7,8,9,10,11,12,15,18,19,24,25,26} by application of Pre({1,3,4,5,7,8,9,10,11,12,15,18,19,24,25,26}) = {2,6,13,14,16,17,20,21,22,23}. Here rules are labelled as follows: 1: A__ADD#(z0,z1) -> c_1() 2: A__ADD#(0(),z0) -> c_2(MARK#(z0)) 3: A__ADD#(s(z0),z1) -> c_3() 4: A__AND#(z0,z1) -> c_4() 5: A__AND#(false(),z0) -> c_5() 6: A__AND#(true(),z0) -> c_6(MARK#(z0)) 7: A__FIRST#(z0,z1) -> c_7() 8: A__FIRST#(0(),z0) -> c_8() 9: A__FIRST#(s(z0),cons(z1,z2)) -> c_9() 10: A__FROM#(z0) -> c_10() 11: A__FROM#(z0) -> c_11() 12: A__IF#(z0,z1,z2) -> c_12() 13: A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) 14: A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) 15: MARK#(0()) -> c_15() 16: MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) 17: MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) 18: MARK#(cons(z0,z1)) -> c_18() 19: MARK#(false()) -> c_19() 20: MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) 21: MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) 22: MARK#(from(z0)) -> c_22(A__FROM#(z0)) 23: MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) 24: MARK#(nil()) -> c_24() 25: MARK#(s(z0)) -> c_25() 26: MARK#(true()) -> c_26() 27: a__add#(z0,z1) -> c_27() 28: a__add#(0(),z0) -> c_28(mark#(z0)) 29: a__add#(s(z0),z1) -> c_29() 30: a__and#(z0,z1) -> c_30() 31: a__and#(false(),z0) -> c_31() 32: a__and#(true(),z0) -> c_32(mark#(z0)) 33: a__first#(z0,z1) -> c_33() 34: a__first#(0(),z0) -> c_34() 35: a__first#(s(z0),cons(z1,z2)) -> c_35() 36: a__from#(z0) -> c_36() 37: a__from#(z0) -> c_37() 38: a__if#(z0,z1,z2) -> c_38() 39: a__if#(false(),z0,z1) -> c_39(mark#(z1)) 40: a__if#(true(),z0,z1) -> c_40(mark#(z0)) 41: mark#(0()) -> c_41() 42: mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) 43: mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) 44: mark#(cons(z0,z1)) -> c_44() 45: mark#(false()) -> c_45() 46: mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) 47: mark#(from(z0)) -> c_47(a__from#(z0)) 48: mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) 49: mark#(nil()) -> c_49() 50: mark#(s(z0)) -> c_50() 51: mark#(true()) -> c_51() ** Step 1.b:3: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) MARK#(from(z0)) -> c_22(A__FROM#(z0)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) - Weak DPs: A__ADD#(z0,z1) -> c_1() A__ADD#(s(z0),z1) -> c_3() A__AND#(z0,z1) -> c_4() A__AND#(false(),z0) -> c_5() A__FIRST#(z0,z1) -> c_7() A__FIRST#(0(),z0) -> c_8() A__FIRST#(s(z0),cons(z1,z2)) -> c_9() A__FROM#(z0) -> c_10() A__FROM#(z0) -> c_11() A__IF#(z0,z1,z2) -> c_12() MARK#(0()) -> c_15() MARK#(cons(z0,z1)) -> c_18() MARK#(false()) -> c_19() MARK#(nil()) -> c_24() MARK#(s(z0)) -> c_25() MARK#(true()) -> c_26() a__add#(z0,z1) -> c_27() a__add#(0(),z0) -> c_28(mark#(z0)) a__add#(s(z0),z1) -> c_29() a__and#(z0,z1) -> c_30() a__and#(false(),z0) -> c_31() a__and#(true(),z0) -> c_32(mark#(z0)) a__first#(z0,z1) -> c_33() a__first#(0(),z0) -> c_34() a__first#(s(z0),cons(z1,z2)) -> c_35() a__from#(z0) -> c_36() a__from#(z0) -> c_37() a__if#(z0,z1,z2) -> c_38() a__if#(false(),z0,z1) -> c_39(mark#(z1)) a__if#(true(),z0,z1) -> c_40(mark#(z0)) mark#(0()) -> c_41() mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) mark#(cons(z0,z1)) -> c_44() mark#(false()) -> c_45() mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) mark#(from(z0)) -> c_47(a__from#(z0)) mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) mark#(nil()) -> c_49() mark#(s(z0)) -> c_50() mark#(true()) -> c_51() - Weak TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/3,c_17/3,c_18/0,c_19/0,c_20/4,c_21/4,c_22/1,c_23/3,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {9} by application of Pre({9}) = {1,2,3,4,5,6,7,8,10}. Here rules are labelled as follows: 1: A__ADD#(0(),z0) -> c_2(MARK#(z0)) 2: A__AND#(true(),z0) -> c_6(MARK#(z0)) 3: A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) 4: A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) 5: MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) 6: MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) 7: MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) 8: MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) 9: MARK#(from(z0)) -> c_22(A__FROM#(z0)) 10: MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) 11: A__ADD#(z0,z1) -> c_1() 12: A__ADD#(s(z0),z1) -> c_3() 13: A__AND#(z0,z1) -> c_4() 14: A__AND#(false(),z0) -> c_5() 15: A__FIRST#(z0,z1) -> c_7() 16: A__FIRST#(0(),z0) -> c_8() 17: A__FIRST#(s(z0),cons(z1,z2)) -> c_9() 18: A__FROM#(z0) -> c_10() 19: A__FROM#(z0) -> c_11() 20: A__IF#(z0,z1,z2) -> c_12() 21: MARK#(0()) -> c_15() 22: MARK#(cons(z0,z1)) -> c_18() 23: MARK#(false()) -> c_19() 24: MARK#(nil()) -> c_24() 25: MARK#(s(z0)) -> c_25() 26: MARK#(true()) -> c_26() 27: a__add#(z0,z1) -> c_27() 28: a__add#(0(),z0) -> c_28(mark#(z0)) 29: a__add#(s(z0),z1) -> c_29() 30: a__and#(z0,z1) -> c_30() 31: a__and#(false(),z0) -> c_31() 32: a__and#(true(),z0) -> c_32(mark#(z0)) 33: a__first#(z0,z1) -> c_33() 34: a__first#(0(),z0) -> c_34() 35: a__first#(s(z0),cons(z1,z2)) -> c_35() 36: a__from#(z0) -> c_36() 37: a__from#(z0) -> c_37() 38: a__if#(z0,z1,z2) -> c_38() 39: a__if#(false(),z0,z1) -> c_39(mark#(z1)) 40: a__if#(true(),z0,z1) -> c_40(mark#(z0)) 41: mark#(0()) -> c_41() 42: mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) 43: mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) 44: mark#(cons(z0,z1)) -> c_44() 45: mark#(false()) -> c_45() 46: mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) 47: mark#(from(z0)) -> c_47(a__from#(z0)) 48: mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) 49: mark#(nil()) -> c_49() 50: mark#(s(z0)) -> c_50() 51: mark#(true()) -> c_51() ** Step 1.b:4: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) - Weak DPs: A__ADD#(z0,z1) -> c_1() A__ADD#(s(z0),z1) -> c_3() A__AND#(z0,z1) -> c_4() A__AND#(false(),z0) -> c_5() A__FIRST#(z0,z1) -> c_7() A__FIRST#(0(),z0) -> c_8() A__FIRST#(s(z0),cons(z1,z2)) -> c_9() A__FROM#(z0) -> c_10() A__FROM#(z0) -> c_11() A__IF#(z0,z1,z2) -> c_12() MARK#(0()) -> c_15() MARK#(cons(z0,z1)) -> c_18() MARK#(false()) -> c_19() MARK#(from(z0)) -> c_22(A__FROM#(z0)) MARK#(nil()) -> c_24() MARK#(s(z0)) -> c_25() MARK#(true()) -> c_26() a__add#(z0,z1) -> c_27() a__add#(0(),z0) -> c_28(mark#(z0)) a__add#(s(z0),z1) -> c_29() a__and#(z0,z1) -> c_30() a__and#(false(),z0) -> c_31() a__and#(true(),z0) -> c_32(mark#(z0)) a__first#(z0,z1) -> c_33() a__first#(0(),z0) -> c_34() a__first#(s(z0),cons(z1,z2)) -> c_35() a__from#(z0) -> c_36() a__from#(z0) -> c_37() a__if#(z0,z1,z2) -> c_38() a__if#(false(),z0,z1) -> c_39(mark#(z1)) a__if#(true(),z0,z1) -> c_40(mark#(z0)) mark#(0()) -> c_41() mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) mark#(cons(z0,z1)) -> c_44() mark#(false()) -> c_45() mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) mark#(from(z0)) -> c_47(a__from#(z0)) mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) mark#(nil()) -> c_49() mark#(s(z0)) -> c_50() mark#(true()) -> c_51() - Weak TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/3,c_17/3,c_18/0,c_19/0,c_20/4,c_21/4,c_22/1,c_23/3,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:A__ADD#(0(),z0) -> c_2(MARK#(z0)) -->_1 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 MARK#(true()) -> c_26():26 -->_1 MARK#(s(z0)) -> c_25():25 -->_1 MARK#(nil()) -> c_24():24 -->_1 MARK#(false()) -> c_19():22 -->_1 MARK#(cons(z0,z1)) -> c_18():21 -->_1 MARK#(0()) -> c_15():20 2:S:A__AND#(true(),z0) -> c_6(MARK#(z0)) -->_1 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 MARK#(true()) -> c_26():26 -->_1 MARK#(s(z0)) -> c_25():25 -->_1 MARK#(nil()) -> c_24():24 -->_1 MARK#(false()) -> c_19():22 -->_1 MARK#(cons(z0,z1)) -> c_18():21 -->_1 MARK#(0()) -> c_15():20 3:S:A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) -->_1 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 MARK#(true()) -> c_26():26 -->_1 MARK#(s(z0)) -> c_25():25 -->_1 MARK#(nil()) -> c_24():24 -->_1 MARK#(false()) -> c_19():22 -->_1 MARK#(cons(z0,z1)) -> c_18():21 -->_1 MARK#(0()) -> c_15():20 4:S:A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) -->_1 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 MARK#(true()) -> c_26():26 -->_1 MARK#(s(z0)) -> c_25():25 -->_1 MARK#(nil()) -> c_24():24 -->_1 MARK#(false()) -> c_19():22 -->_1 MARK#(cons(z0,z1)) -> c_18():21 -->_1 MARK#(0()) -> c_15():20 5:S:MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_3 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_3 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_3 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_3 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_3 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_2 mark#(true()) -> c_51():51 -->_2 mark#(s(z0)) -> c_50():50 -->_2 mark#(nil()) -> c_49():49 -->_2 mark#(false()) -> c_45():45 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(0()) -> c_41():41 -->_3 MARK#(true()) -> c_26():26 -->_3 MARK#(s(z0)) -> c_25():25 -->_3 MARK#(nil()) -> c_24():24 -->_3 MARK#(false()) -> c_19():22 -->_3 MARK#(cons(z0,z1)) -> c_18():21 -->_3 MARK#(0()) -> c_15():20 -->_1 A__ADD#(s(z0),z1) -> c_3():11 -->_1 A__ADD#(z0,z1) -> c_1():10 -->_3 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 A__ADD#(0(),z0) -> c_2(MARK#(z0)):1 6:S:MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_3 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_3 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_3 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_3 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_2 mark#(true()) -> c_51():51 -->_2 mark#(s(z0)) -> c_50():50 -->_2 mark#(nil()) -> c_49():49 -->_2 mark#(false()) -> c_45():45 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(0()) -> c_41():41 -->_3 MARK#(true()) -> c_26():26 -->_3 MARK#(s(z0)) -> c_25():25 -->_3 MARK#(nil()) -> c_24():24 -->_3 MARK#(false()) -> c_19():22 -->_3 MARK#(cons(z0,z1)) -> c_18():21 -->_3 MARK#(0()) -> c_15():20 -->_1 A__AND#(false(),z0) -> c_5():13 -->_1 A__AND#(z0,z1) -> c_4():12 -->_3 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_3 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 A__AND#(true(),z0) -> c_6(MARK#(z0)):2 7:S:MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) -->_3 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_3 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_3 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_3 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_3 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_4 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_4 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_4 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_3 mark#(true()) -> c_51():51 -->_2 mark#(true()) -> c_51():51 -->_3 mark#(s(z0)) -> c_50():50 -->_2 mark#(s(z0)) -> c_50():50 -->_3 mark#(nil()) -> c_49():49 -->_2 mark#(nil()) -> c_49():49 -->_3 mark#(false()) -> c_45():45 -->_2 mark#(false()) -> c_45():45 -->_3 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_3 mark#(0()) -> c_41():41 -->_2 mark#(0()) -> c_41():41 -->_4 MARK#(true()) -> c_26():26 -->_4 MARK#(s(z0)) -> c_25():25 -->_4 MARK#(nil()) -> c_24():24 -->_4 MARK#(false()) -> c_19():22 -->_4 MARK#(cons(z0,z1)) -> c_18():21 -->_4 MARK#(0()) -> c_15():20 -->_1 A__FIRST#(s(z0),cons(z1,z2)) -> c_9():16 -->_1 A__FIRST#(0(),z0) -> c_8():15 -->_1 A__FIRST#(z0,z1) -> c_7():14 -->_4 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_4 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_4 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 8:S:MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) -->_3 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_3 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_3 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_3 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_3 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_4 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_4 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_3 mark#(true()) -> c_51():51 -->_2 mark#(true()) -> c_51():51 -->_3 mark#(s(z0)) -> c_50():50 -->_2 mark#(s(z0)) -> c_50():50 -->_3 mark#(nil()) -> c_49():49 -->_2 mark#(nil()) -> c_49():49 -->_3 mark#(false()) -> c_45():45 -->_2 mark#(false()) -> c_45():45 -->_3 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_3 mark#(0()) -> c_41():41 -->_2 mark#(0()) -> c_41():41 -->_4 MARK#(true()) -> c_26():26 -->_4 MARK#(s(z0)) -> c_25():25 -->_4 MARK#(nil()) -> c_24():24 -->_4 MARK#(false()) -> c_19():22 -->_4 MARK#(cons(z0,z1)) -> c_18():21 -->_4 MARK#(0()) -> c_15():20 -->_1 A__FIRST#(s(z0),cons(z1,z2)) -> c_9():16 -->_1 A__FIRST#(0(),z0) -> c_8():15 -->_1 A__FIRST#(z0,z1) -> c_7():14 -->_4 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_4 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_4 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_4 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 9:S:MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_3 MARK#(from(z0)) -> c_22(A__FROM#(z0)):23 -->_2 mark#(true()) -> c_51():51 -->_2 mark#(s(z0)) -> c_50():50 -->_2 mark#(nil()) -> c_49():49 -->_2 mark#(false()) -> c_45():45 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(0()) -> c_41():41 -->_3 MARK#(true()) -> c_26():26 -->_3 MARK#(s(z0)) -> c_25():25 -->_3 MARK#(nil()) -> c_24():24 -->_3 MARK#(false()) -> c_19():22 -->_3 MARK#(cons(z0,z1)) -> c_18():21 -->_3 MARK#(0()) -> c_15():20 -->_1 A__IF#(z0,z1,z2) -> c_12():19 -->_3 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_3 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_3 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_3 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_3 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 A__IF#(true(),z0,z1) -> c_14(MARK#(z0)):4 -->_1 A__IF#(false(),z0,z1) -> c_13(MARK#(z1)):3 10:W:A__ADD#(z0,z1) -> c_1() 11:W:A__ADD#(s(z0),z1) -> c_3() 12:W:A__AND#(z0,z1) -> c_4() 13:W:A__AND#(false(),z0) -> c_5() 14:W:A__FIRST#(z0,z1) -> c_7() 15:W:A__FIRST#(0(),z0) -> c_8() 16:W:A__FIRST#(s(z0),cons(z1,z2)) -> c_9() 17:W:A__FROM#(z0) -> c_10() 18:W:A__FROM#(z0) -> c_11() 19:W:A__IF#(z0,z1,z2) -> c_12() 20:W:MARK#(0()) -> c_15() 21:W:MARK#(cons(z0,z1)) -> c_18() 22:W:MARK#(false()) -> c_19() 23:W:MARK#(from(z0)) -> c_22(A__FROM#(z0)) -->_1 A__FROM#(z0) -> c_11():18 -->_1 A__FROM#(z0) -> c_10():17 24:W:MARK#(nil()) -> c_24() 25:W:MARK#(s(z0)) -> c_25() 26:W:MARK#(true()) -> c_26() 27:W:a__add#(z0,z1) -> c_27() 28:W:a__add#(0(),z0) -> c_28(mark#(z0)) -->_1 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_1 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_1 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_1 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_1 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_1 mark#(true()) -> c_51():51 -->_1 mark#(s(z0)) -> c_50():50 -->_1 mark#(nil()) -> c_49():49 -->_1 mark#(false()) -> c_45():45 -->_1 mark#(cons(z0,z1)) -> c_44():44 -->_1 mark#(0()) -> c_41():41 29:W:a__add#(s(z0),z1) -> c_29() 30:W:a__and#(z0,z1) -> c_30() 31:W:a__and#(false(),z0) -> c_31() 32:W:a__and#(true(),z0) -> c_32(mark#(z0)) -->_1 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_1 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_1 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_1 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_1 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_1 mark#(true()) -> c_51():51 -->_1 mark#(s(z0)) -> c_50():50 -->_1 mark#(nil()) -> c_49():49 -->_1 mark#(false()) -> c_45():45 -->_1 mark#(cons(z0,z1)) -> c_44():44 -->_1 mark#(0()) -> c_41():41 33:W:a__first#(z0,z1) -> c_33() 34:W:a__first#(0(),z0) -> c_34() 35:W:a__first#(s(z0),cons(z1,z2)) -> c_35() 36:W:a__from#(z0) -> c_36() 37:W:a__from#(z0) -> c_37() 38:W:a__if#(z0,z1,z2) -> c_38() 39:W:a__if#(false(),z0,z1) -> c_39(mark#(z1)) -->_1 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_1 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_1 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_1 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_1 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_1 mark#(true()) -> c_51():51 -->_1 mark#(s(z0)) -> c_50():50 -->_1 mark#(nil()) -> c_49():49 -->_1 mark#(false()) -> c_45():45 -->_1 mark#(cons(z0,z1)) -> c_44():44 -->_1 mark#(0()) -> c_41():41 40:W:a__if#(true(),z0,z1) -> c_40(mark#(z0)) -->_1 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_1 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_1 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_1 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_1 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_1 mark#(true()) -> c_51():51 -->_1 mark#(s(z0)) -> c_50():50 -->_1 mark#(nil()) -> c_49():49 -->_1 mark#(false()) -> c_45():45 -->_1 mark#(cons(z0,z1)) -> c_44():44 -->_1 mark#(0()) -> c_41():41 41:W:mark#(0()) -> c_41() 42:W:mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(true()) -> c_51():51 -->_2 mark#(s(z0)) -> c_50():50 -->_2 mark#(nil()) -> c_49():49 -->_2 mark#(false()) -> c_45():45 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_2 mark#(0()) -> c_41():41 -->_1 a__add#(s(z0),z1) -> c_29():29 -->_1 a__add#(0(),z0) -> c_28(mark#(z0)):28 -->_1 a__add#(z0,z1) -> c_27():27 43:W:mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(true()) -> c_51():51 -->_2 mark#(s(z0)) -> c_50():50 -->_2 mark#(nil()) -> c_49():49 -->_2 mark#(false()) -> c_45():45 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_2 mark#(0()) -> c_41():41 -->_1 a__and#(true(),z0) -> c_32(mark#(z0)):32 -->_1 a__and#(false(),z0) -> c_31():31 -->_1 a__and#(z0,z1) -> c_30():30 44:W:mark#(cons(z0,z1)) -> c_44() 45:W:mark#(false()) -> c_45() 46:W:mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) -->_3 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_3 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_3 mark#(true()) -> c_51():51 -->_2 mark#(true()) -> c_51():51 -->_3 mark#(s(z0)) -> c_50():50 -->_2 mark#(s(z0)) -> c_50():50 -->_3 mark#(nil()) -> c_49():49 -->_2 mark#(nil()) -> c_49():49 -->_3 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_3 mark#(false()) -> c_45():45 -->_2 mark#(false()) -> c_45():45 -->_3 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_3 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_3 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_3 mark#(0()) -> c_41():41 -->_2 mark#(0()) -> c_41():41 -->_1 a__first#(s(z0),cons(z1,z2)) -> c_35():35 -->_1 a__first#(0(),z0) -> c_34():34 -->_1 a__first#(z0,z1) -> c_33():33 47:W:mark#(from(z0)) -> c_47(a__from#(z0)) -->_1 a__from#(z0) -> c_37():37 -->_1 a__from#(z0) -> c_36():36 48:W:mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) -->_2 mark#(true()) -> c_51():51 -->_2 mark#(s(z0)) -> c_50():50 -->_2 mark#(nil()) -> c_49():49 -->_2 mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)):48 -->_2 mark#(from(z0)) -> c_47(a__from#(z0)):47 -->_2 mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)):46 -->_2 mark#(false()) -> c_45():45 -->_2 mark#(cons(z0,z1)) -> c_44():44 -->_2 mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)):43 -->_2 mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)):42 -->_2 mark#(0()) -> c_41():41 -->_1 a__if#(true(),z0,z1) -> c_40(mark#(z0)):40 -->_1 a__if#(false(),z0,z1) -> c_39(mark#(z1)):39 -->_1 a__if#(z0,z1,z2) -> c_38():38 49:W:mark#(nil()) -> c_49() 50:W:mark#(s(z0)) -> c_50() 51:W:mark#(true()) -> c_51() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: A__ADD#(z0,z1) -> c_1() 11: A__ADD#(s(z0),z1) -> c_3() 12: A__AND#(z0,z1) -> c_4() 13: A__AND#(false(),z0) -> c_5() 14: A__FIRST#(z0,z1) -> c_7() 15: A__FIRST#(0(),z0) -> c_8() 16: A__FIRST#(s(z0),cons(z1,z2)) -> c_9() 19: A__IF#(z0,z1,z2) -> c_12() 20: MARK#(0()) -> c_15() 21: MARK#(cons(z0,z1)) -> c_18() 22: MARK#(false()) -> c_19() 24: MARK#(nil()) -> c_24() 25: MARK#(s(z0)) -> c_25() 26: MARK#(true()) -> c_26() 48: mark#(if(z0,z1,z2)) -> c_48(a__if#(mark(z0),z1,z2),mark#(z0)) 46: mark#(first(z0,z1)) -> c_46(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) 43: mark#(and(z0,z1)) -> c_43(a__and#(mark(z0),z1),mark#(z0)) 42: mark#(add(z0,z1)) -> c_42(a__add#(mark(z0),z1),mark#(z0)) 40: a__if#(true(),z0,z1) -> c_40(mark#(z0)) 39: a__if#(false(),z0,z1) -> c_39(mark#(z1)) 32: a__and#(true(),z0) -> c_32(mark#(z0)) 28: a__add#(0(),z0) -> c_28(mark#(z0)) 38: a__if#(z0,z1,z2) -> c_38() 33: a__first#(z0,z1) -> c_33() 34: a__first#(0(),z0) -> c_34() 35: a__first#(s(z0),cons(z1,z2)) -> c_35() 30: a__and#(z0,z1) -> c_30() 31: a__and#(false(),z0) -> c_31() 27: a__add#(z0,z1) -> c_27() 29: a__add#(s(z0),z1) -> c_29() 41: mark#(0()) -> c_41() 44: mark#(cons(z0,z1)) -> c_44() 45: mark#(false()) -> c_45() 47: mark#(from(z0)) -> c_47(a__from#(z0)) 36: a__from#(z0) -> c_36() 37: a__from#(z0) -> c_37() 49: mark#(nil()) -> c_49() 50: mark#(s(z0)) -> c_50() 51: mark#(true()) -> c_51() 23: MARK#(from(z0)) -> c_22(A__FROM#(z0)) 17: A__FROM#(z0) -> c_10() 18: A__FROM#(z0) -> c_11() ** Step 1.b:5: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) - Weak TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/3,c_17/3,c_18/0,c_19/0,c_20/4,c_21/4,c_22/1,c_23/3,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:A__ADD#(0(),z0) -> c_2(MARK#(z0)) -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 2:S:A__AND#(true(),z0) -> c_6(MARK#(z0)) -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 3:S:A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 4:S:A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) -->_1 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_1 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_1 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_1 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_1 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 5:S:MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)) -->_3 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_3 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_3 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_3 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_3 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 A__ADD#(0(),z0) -> c_2(MARK#(z0)):1 6:S:MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)) -->_3 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_3 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_3 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_3 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_3 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 A__AND#(true(),z0) -> c_6(MARK#(z0)):2 7:S:MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)) -->_4 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_4 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_4 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_4 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_4 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 8:S:MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)) -->_4 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_4 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_4 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_4 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_4 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 9:S:MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)) -->_3 MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),mark#(z0),MARK#(z0)):9 -->_3 MARK#(first(z0,z1)) -> c_21(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z1)):8 -->_3 MARK#(first(z0,z1)) -> c_20(A__FIRST#(mark(z0),mark(z1)),mark#(z0),mark#(z1),MARK#(z0)):7 -->_3 MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),mark#(z0),MARK#(z0)):6 -->_3 MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),mark#(z0),MARK#(z0)):5 -->_1 A__IF#(true(),z0,z1) -> c_14(MARK#(z0)):4 -->_1 A__IF#(false(),z0,z1) -> c_13(MARK#(z1)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) ** Step 1.b:6: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak TRS: A__ADD(z0,z1) -> c8() A__ADD(0(),z0) -> c6(MARK(z0)) A__ADD(s(z0),z1) -> c7() A__AND(z0,z1) -> c2() A__AND(false(),z0) -> c1() A__AND(true(),z0) -> c(MARK(z0)) A__FIRST(z0,z1) -> c11() A__FIRST(0(),z0) -> c9() A__FIRST(s(z0),cons(z1,z2)) -> c10() A__FROM(z0) -> c12() A__FROM(z0) -> c13() A__IF(z0,z1,z2) -> c5() A__IF(false(),z0,z1) -> c4(MARK(z1)) A__IF(true(),z0,z1) -> c3(MARK(z0)) MARK(0()) -> c22() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),z1),MARK(z0)) MARK(and(z0,z1)) -> c14(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c25() MARK(false()) -> c21() MARK(first(z0,z1)) -> c17(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c18(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(if(z0,z1,z2)) -> c15(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(nil()) -> c24() MARK(s(z0)) -> c23() MARK(true()) -> c20() a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) ** Step 1.b:7: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__add) = {1}, uargs(a__and) = {1}, uargs(a__first) = {1,2}, uargs(a__if) = {1}, uargs(A__ADD#) = {1}, uargs(A__AND#) = {1}, uargs(A__IF#) = {1}, uargs(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(A__ADD) = [0] p(A__AND) = [1] p(A__FIRST) = [0] p(A__FROM) = [0] p(A__IF) = [0] p(MARK) = [0] p(a__add) = [1] x1 + [0] p(a__and) = [1] x1 + [0] p(a__first) = [1] x1 + [1] x2 + [0] p(a__from) = [0] p(a__if) = [1] x1 + [0] p(add) = [1] x1 + [0] p(and) = [1] x1 + [0] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [1] x2 + [0] p(c17) = [1] x1 + [1] x2 + [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c3) = [1] x1 + [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(cons) = [0] p(false) = [0] p(first) = [1] x2 + [0] p(from) = [0] p(if) = [0] p(mark) = [0] p(nil) = [0] p(s) = [0] p(true) = [0] p(A__ADD#) = [1] x1 + [1] p(A__AND#) = [1] x1 + [0] p(A__FIRST#) = [0] p(A__FROM#) = [0] p(A__IF#) = [1] x1 + [6] p(MARK#) = [3] p(a__add#) = [0] p(a__and#) = [0] p(a__first#) = [0] p(a__from#) = [0] p(a__if#) = [0] p(mark#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [1] x1 + [2] p(c_22) = [0] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [1] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] Following rules are strictly oriented: A__IF#(false(),z0,z1) = [6] > [3] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [6] > [3] = c_14(MARK#(z0)) Following rules are (at-least) weakly oriented: A__ADD#(0(),z0) = [1] >= [3] = c_2(MARK#(z0)) A__AND#(true(),z0) = [0] >= [3] = c_6(MARK#(z0)) MARK#(add(z0,z1)) = [3] >= [4] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) = [3] >= [3] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [3] >= [3] = c_20(MARK#(z0)) MARK#(first(z0,z1)) = [3] >= [5] = c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) = [3] >= [9] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) a__add(z0,z1) = [1] z0 + [0] >= [1] z0 + [0] = add(z0,z1) a__add(0(),z0) = [0] >= [0] = mark(z0) a__add(s(z0),z1) = [0] >= [0] = s(add(z0,z1)) a__and(z0,z1) = [1] z0 + [0] >= [1] z0 + [0] = and(z0,z1) a__and(false(),z0) = [0] >= [0] = false() a__and(true(),z0) = [0] >= [0] = mark(z0) a__first(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z1 + [0] = first(z0,z1) a__first(0(),z0) = [1] z0 + [0] >= [0] = nil() a__first(s(z0),cons(z1,z2)) = [0] >= [0] = cons(z1,first(z0,z2)) a__from(z0) = [0] >= [0] = cons(z0,from(s(z0))) a__from(z0) = [0] >= [0] = from(z0) a__if(z0,z1,z2) = [1] z0 + [0] >= [0] = if(z0,z1,z2) a__if(false(),z0,z1) = [0] >= [0] = mark(z1) a__if(true(),z0,z1) = [0] >= [0] = mark(z0) mark(0()) = [0] >= [0] = 0() mark(add(z0,z1)) = [0] >= [0] = a__add(mark(z0),z1) mark(and(z0,z1)) = [0] >= [0] = a__and(mark(z0),z1) mark(cons(z0,z1)) = [0] >= [0] = cons(z0,z1) mark(false()) = [0] >= [0] = false() mark(first(z0,z1)) = [0] >= [0] = a__first(mark(z0),mark(z1)) mark(from(z0)) = [0] >= [0] = a__from(z0) mark(if(z0,z1,z2)) = [0] >= [0] = a__if(mark(z0),z1,z2) mark(nil()) = [0] >= [0] = nil() mark(s(z0)) = [0] >= [0] = s(z0) mark(true()) = [0] >= [0] = true() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:8: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak DPs: A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__add) = {1}, uargs(a__and) = {1}, uargs(a__first) = {1,2}, uargs(a__if) = {1}, uargs(A__ADD#) = {1}, uargs(A__AND#) = {1}, uargs(A__IF#) = {1}, uargs(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(A__ADD) = [0] p(A__AND) = [0] p(A__FIRST) = [0] p(A__FROM) = [0] p(A__IF) = [0] p(MARK) = [0] p(a__add) = [1] x1 + [0] p(a__and) = [1] x1 + [0] p(a__first) = [1] x1 + [1] x2 + [0] p(a__from) = [0] p(a__if) = [1] x1 + [0] p(add) = [1] x1 + [0] p(and) = [0] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [1] x2 + [0] p(c17) = [1] x1 + [1] x2 + [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c3) = [1] x1 + [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(cons) = [0] p(false) = [0] p(first) = [0] p(from) = [0] p(if) = [0] p(mark) = [0] p(nil) = [0] p(s) = [0] p(true) = [0] p(A__ADD#) = [1] x1 + [0] p(A__AND#) = [1] x1 + [5] p(A__FIRST#) = [0] p(A__FROM#) = [0] p(A__IF#) = [1] x1 + [0] p(MARK#) = [0] p(a__add#) = [0] p(a__and#) = [0] p(a__first#) = [0] p(a__from#) = [0] p(a__if#) = [0] p(mark#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [1] p(c_17) = [1] x1 + [1] x2 + [2] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [1] x1 + [0] p(c_22) = [0] p(c_23) = [1] x1 + [1] x2 + [1] p(c_24) = [0] p(c_25) = [2] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] Following rules are strictly oriented: A__AND#(true(),z0) = [5] > [0] = c_6(MARK#(z0)) Following rules are (at-least) weakly oriented: A__ADD#(0(),z0) = [0] >= [0] = c_2(MARK#(z0)) A__IF#(false(),z0,z1) = [0] >= [0] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [0] >= [0] = c_14(MARK#(z0)) MARK#(add(z0,z1)) = [0] >= [1] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) = [0] >= [7] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [0] >= [0] = c_20(MARK#(z0)) MARK#(first(z0,z1)) = [0] >= [0] = c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) = [0] >= [1] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) a__add(z0,z1) = [1] z0 + [0] >= [1] z0 + [0] = add(z0,z1) a__add(0(),z0) = [0] >= [0] = mark(z0) a__add(s(z0),z1) = [0] >= [0] = s(add(z0,z1)) a__and(z0,z1) = [1] z0 + [0] >= [0] = and(z0,z1) a__and(false(),z0) = [0] >= [0] = false() a__and(true(),z0) = [0] >= [0] = mark(z0) a__first(z0,z1) = [1] z0 + [1] z1 + [0] >= [0] = first(z0,z1) a__first(0(),z0) = [1] z0 + [0] >= [0] = nil() a__first(s(z0),cons(z1,z2)) = [0] >= [0] = cons(z1,first(z0,z2)) a__from(z0) = [0] >= [0] = cons(z0,from(s(z0))) a__from(z0) = [0] >= [0] = from(z0) a__if(z0,z1,z2) = [1] z0 + [0] >= [0] = if(z0,z1,z2) a__if(false(),z0,z1) = [0] >= [0] = mark(z1) a__if(true(),z0,z1) = [0] >= [0] = mark(z0) mark(0()) = [0] >= [0] = 0() mark(add(z0,z1)) = [0] >= [0] = a__add(mark(z0),z1) mark(and(z0,z1)) = [0] >= [0] = a__and(mark(z0),z1) mark(cons(z0,z1)) = [0] >= [0] = cons(z0,z1) mark(false()) = [0] >= [0] = false() mark(first(z0,z1)) = [0] >= [0] = a__first(mark(z0),mark(z1)) mark(from(z0)) = [0] >= [0] = a__from(z0) mark(if(z0,z1,z2)) = [0] >= [0] = a__if(mark(z0),z1,z2) mark(nil()) = [0] >= [0] = nil() mark(s(z0)) = [0] >= [0] = s(z0) mark(true()) = [0] >= [0] = true() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:9: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak DPs: A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__add) = {1}, uargs(a__and) = {1}, uargs(a__first) = {1,2}, uargs(a__if) = {1}, uargs(A__ADD#) = {1}, uargs(A__AND#) = {1}, uargs(A__IF#) = {1}, uargs(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(A__ADD) = [0] p(A__AND) = [0] p(A__FIRST) = [0] p(A__FROM) = [0] p(A__IF) = [0] p(MARK) = [0] p(a__add) = [1] x1 + [0] p(a__and) = [1] x1 + [0] p(a__first) = [1] x1 + [1] x2 + [0] p(a__from) = [0] p(a__if) = [1] x1 + [0] p(add) = [0] p(and) = [0] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [1] x2 + [0] p(c17) = [1] x1 + [1] x2 + [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c3) = [1] x1 + [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(cons) = [0] p(false) = [0] p(first) = [1] x1 + [1] x2 + [0] p(from) = [0] p(if) = [0] p(mark) = [0] p(nil) = [0] p(s) = [0] p(true) = [0] p(A__ADD#) = [1] x1 + [7] p(A__AND#) = [1] x1 + [4] p(A__FIRST#) = [0] p(A__FROM#) = [0] p(A__IF#) = [1] x1 + [4] p(MARK#) = [4] p(a__add#) = [0] p(a__and#) = [0] p(a__first#) = [0] p(a__from#) = [0] p(a__if#) = [0] p(mark#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [1] x1 + [0] p(c_22) = [0] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] Following rules are strictly oriented: A__ADD#(0(),z0) = [7] > [4] = c_2(MARK#(z0)) Following rules are (at-least) weakly oriented: A__AND#(true(),z0) = [4] >= [4] = c_6(MARK#(z0)) A__IF#(false(),z0,z1) = [4] >= [4] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [4] >= [4] = c_14(MARK#(z0)) MARK#(add(z0,z1)) = [4] >= [11] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) = [4] >= [8] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [4] >= [4] = c_20(MARK#(z0)) MARK#(first(z0,z1)) = [4] >= [4] = c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) = [4] >= [8] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) a__add(z0,z1) = [1] z0 + [0] >= [0] = add(z0,z1) a__add(0(),z0) = [0] >= [0] = mark(z0) a__add(s(z0),z1) = [0] >= [0] = s(add(z0,z1)) a__and(z0,z1) = [1] z0 + [0] >= [0] = and(z0,z1) a__and(false(),z0) = [0] >= [0] = false() a__and(true(),z0) = [0] >= [0] = mark(z0) a__first(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [0] = first(z0,z1) a__first(0(),z0) = [1] z0 + [0] >= [0] = nil() a__first(s(z0),cons(z1,z2)) = [0] >= [0] = cons(z1,first(z0,z2)) a__from(z0) = [0] >= [0] = cons(z0,from(s(z0))) a__from(z0) = [0] >= [0] = from(z0) a__if(z0,z1,z2) = [1] z0 + [0] >= [0] = if(z0,z1,z2) a__if(false(),z0,z1) = [0] >= [0] = mark(z1) a__if(true(),z0,z1) = [0] >= [0] = mark(z0) mark(0()) = [0] >= [0] = 0() mark(add(z0,z1)) = [0] >= [0] = a__add(mark(z0),z1) mark(and(z0,z1)) = [0] >= [0] = a__and(mark(z0),z1) mark(cons(z0,z1)) = [0] >= [0] = cons(z0,z1) mark(false()) = [0] >= [0] = false() mark(first(z0,z1)) = [0] >= [0] = a__first(mark(z0),mark(z1)) mark(from(z0)) = [0] >= [0] = a__from(z0) mark(if(z0,z1,z2)) = [0] >= [0] = a__if(mark(z0),z1,z2) mark(nil()) = [0] >= [0] = nil() mark(s(z0)) = [0] >= [0] = s(z0) mark(true()) = [0] >= [0] = true() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:10: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,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(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add#,a__and#,a__first#,a__from#,a__if#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__ADD) = [1] x1 + [1] p(A__AND) = [0] p(A__FIRST) = [1] x1 + [1] p(A__FROM) = [0] p(A__IF) = [1] x2 + [1] x3 + [0] p(MARK) = [1] p(a__add) = [2] x1 + [4] p(a__and) = [3] x1 + [0] p(a__first) = [1] x1 + [0] p(a__from) = [4] p(a__if) = [0] p(add) = [1] x1 + [1] x2 + [2] p(and) = [1] x1 + [1] x2 + [0] p(c) = [1] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] p(c13) = [1] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [1] p(c18) = [0] p(c19) = [1] p(c2) = [2] p(c20) = [1] p(c21) = [0] p(c22) = [2] p(c23) = [0] p(c24) = [1] p(c25) = [1] p(c3) = [1] p(c4) = [1] p(c5) = [0] p(c6) = [0] p(c7) = [2] p(c8) = [0] p(c9) = [1] p(cons) = [2] p(false) = [3] p(first) = [1] x1 + [1] x2 + [0] p(from) = [1] x1 + [6] p(if) = [1] x1 + [1] x2 + [1] x3 + [0] p(mark) = [0] p(nil) = [0] p(s) = [1] x1 + [4] p(true) = [0] p(A__ADD#) = [4] x2 + [0] p(A__AND#) = [4] x2 + [0] p(A__FIRST#) = [1] x1 + [0] p(A__FROM#) = [4] p(A__IF#) = [4] x2 + [4] x3 + [0] p(MARK#) = [4] x1 + [0] p(a__add#) = [1] x1 + [0] p(a__and#) = [2] x2 + [1] p(a__first#) = [1] p(a__from#) = [0] p(a__if#) = [1] p(mark#) = [0] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [1] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] x1 + [0] p(c_7) = [1] p(c_8) = [4] p(c_9) = [1] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [7] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [0] p(c_19) = [2] p(c_20) = [1] x1 + [0] p(c_21) = [1] x1 + [0] p(c_22) = [1] x1 + [1] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [2] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] p(c_28) = [1] x1 + [1] p(c_29) = [0] p(c_30) = [1] p(c_31) = [1] p(c_32) = [1] p(c_33) = [1] p(c_34) = [2] p(c_35) = [1] p(c_36) = [0] p(c_37) = [2] p(c_38) = [1] p(c_39) = [4] x1 + [0] p(c_40) = [2] x1 + [0] p(c_41) = [1] p(c_42) = [0] p(c_43) = [1] p(c_44) = [1] p(c_45) = [1] p(c_46) = [1] p(c_47) = [1] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [1] Following rules are strictly oriented: MARK#(add(z0,z1)) = [4] z0 + [4] z1 + [8] > [4] z0 + [4] z1 + [7] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) Following rules are (at-least) weakly oriented: A__ADD#(0(),z0) = [4] z0 + [0] >= [4] z0 + [0] = c_2(MARK#(z0)) A__AND#(true(),z0) = [4] z0 + [0] >= [4] z0 + [0] = c_6(MARK#(z0)) A__IF#(false(),z0,z1) = [4] z0 + [4] z1 + [0] >= [4] z1 + [0] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [4] z0 + [4] z1 + [0] >= [4] z0 + [0] = c_14(MARK#(z0)) MARK#(and(z0,z1)) = [4] z0 + [4] z1 + [0] >= [4] z0 + [4] z1 + [0] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [4] z0 + [4] z1 + [0] >= [4] z0 + [0] = c_20(MARK#(z0)) MARK#(first(z0,z1)) = [4] z0 + [4] z1 + [0] >= [4] z1 + [0] = c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) = [4] z0 + [4] z1 + [4] z2 + [0] >= [4] z0 + [4] z1 + [4] z2 + [0] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) ** Step 1.b:11: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,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(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add#,a__and#,a__first#,a__from#,a__if#,mark#} TcT has computed the following interpretation: p(0) = [2] p(A__ADD) = [2] x1 + [0] p(A__AND) = [1] x1 + [0] p(A__FIRST) = [1] x1 + [1] x2 + [0] p(A__FROM) = [2] x1 + [0] p(A__IF) = [4] x3 + [1] p(MARK) = [4] p(a__add) = [4] x1 + [4] p(a__and) = [1] x1 + [6] p(a__first) = [3] p(a__from) = [4] x1 + [0] p(a__if) = [2] x3 + [0] p(add) = [1] x1 + [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(c) = [1] x1 + [0] p(c1) = [1] p(c10) = [1] p(c11) = [2] p(c12) = [2] p(c13) = [1] p(c14) = [1] x2 + [1] p(c15) = [1] x1 + [0] p(c16) = [1] x1 + [1] p(c17) = [1] p(c18) = [1] p(c19) = [1] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [2] p(c23) = [1] p(c24) = [1] p(c25) = [2] p(c3) = [1] x1 + [2] p(c4) = [1] p(c5) = [0] p(c6) = [1] x1 + [1] p(c7) = [1] p(c8) = [0] p(c9) = [1] p(cons) = [1] x1 + [1] x2 + [4] p(false) = [1] p(first) = [1] x1 + [1] x2 + [0] p(from) = [0] p(if) = [1] x1 + [1] x2 + [1] x3 + [6] p(mark) = [0] p(nil) = [2] p(s) = [1] x1 + [0] p(true) = [0] p(A__ADD#) = [2] x2 + [0] p(A__AND#) = [2] x2 + [0] p(A__FIRST#) = [4] x1 + [1] p(A__FROM#) = [1] x1 + [2] p(A__IF#) = [2] x2 + [2] x3 + [4] p(MARK#) = [2] x1 + [0] p(a__add#) = [2] x1 + [1] p(a__and#) = [2] p(a__first#) = [2] x1 + [0] p(a__from#) = [4] x1 + [1] p(a__if#) = [1] x2 + [4] p(mark#) = [1] x1 + [1] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [4] p(c_12) = [0] p(c_13) = [1] x1 + [4] p(c_14) = [1] x1 + [1] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [2] p(c_19) = [2] p(c_20) = [1] x1 + [0] p(c_21) = [1] x1 + [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [1] x2 + [6] p(c_24) = [1] p(c_25) = [1] p(c_26) = [2] p(c_27) = [0] p(c_28) = [2] p(c_29) = [4] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [1] p(c_34) = [2] p(c_35) = [0] p(c_36) = [0] p(c_37) = [1] p(c_38) = [4] p(c_39) = [2] x1 + [0] p(c_40) = [1] x1 + [0] p(c_41) = [0] p(c_42) = [1] x2 + [2] p(c_43) = [0] p(c_44) = [1] p(c_45) = [4] p(c_46) = [4] x3 + [2] p(c_47) = [1] p(c_48) = [4] x2 + [1] p(c_49) = [0] p(c_50) = [4] p(c_51) = [1] Following rules are strictly oriented: MARK#(if(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [12] > [2] z0 + [2] z1 + [2] z2 + [10] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) Following rules are (at-least) weakly oriented: A__ADD#(0(),z0) = [2] z0 + [0] >= [2] z0 + [0] = c_2(MARK#(z0)) A__AND#(true(),z0) = [2] z0 + [0] >= [2] z0 + [0] = c_6(MARK#(z0)) A__IF#(false(),z0,z1) = [2] z0 + [2] z1 + [4] >= [2] z1 + [4] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [2] z0 + [2] z1 + [4] >= [2] z0 + [1] = c_14(MARK#(z0)) MARK#(add(z0,z1)) = [2] z0 + [2] z1 + [0] >= [2] z0 + [2] z1 + [0] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) = [2] z0 + [2] z1 + [0] >= [2] z0 + [2] z1 + [0] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [2] z0 + [2] z1 + [0] >= [2] z0 + [0] = c_20(MARK#(z0)) MARK#(first(z0,z1)) = [2] z0 + [2] z1 + [0] >= [2] z1 + [0] = c_21(MARK#(z1)) ** Step 1.b:12: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) - Weak DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,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(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add#,a__and#,a__first#,a__from#,a__if#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__ADD) = [0] p(A__AND) = [0] p(A__FIRST) = [0] p(A__FROM) = [0] p(A__IF) = [0] p(MARK) = [0] p(a__add) = [0] p(a__and) = [0] p(a__first) = [0] p(a__from) = [0] p(a__if) = [0] p(add) = [1] x1 + [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [2] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [1] x2 + [0] p(c17) = [1] x1 + [1] x2 + [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c3) = [1] x1 + [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(cons) = [1] x1 + [1] x2 + [0] p(false) = [0] p(first) = [1] x1 + [1] x2 + [0] p(from) = [1] x1 + [0] p(if) = [1] x1 + [1] x2 + [1] x3 + [0] p(mark) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(true) = [0] p(A__ADD#) = [2] x2 + [0] p(A__AND#) = [2] x2 + [0] p(A__FIRST#) = [0] p(A__FROM#) = [0] p(A__IF#) = [2] x2 + [2] x3 + [0] p(MARK#) = [2] x1 + [0] p(a__add#) = [0] p(a__and#) = [0] p(a__first#) = [0] p(a__from#) = [0] p(a__if#) = [0] p(mark#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [2] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [1] x1 + [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [2] x1 + [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [1] x1 + [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [1] x2 + [0] p(c_43) = [2] x1 + [4] x2 + [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [4] x2 + [1] x3 + [0] p(c_47) = [0] p(c_48) = [1] x2 + [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] Following rules are strictly oriented: MARK#(and(z0,z1)) = [2] z0 + [2] z1 + [4] > [2] z0 + [2] z1 + [2] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) Following rules are (at-least) weakly oriented: A__ADD#(0(),z0) = [2] z0 + [0] >= [2] z0 + [0] = c_2(MARK#(z0)) A__AND#(true(),z0) = [2] z0 + [0] >= [2] z0 + [0] = c_6(MARK#(z0)) A__IF#(false(),z0,z1) = [2] z0 + [2] z1 + [0] >= [2] z1 + [0] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [2] z0 + [2] z1 + [0] >= [2] z0 + [0] = c_14(MARK#(z0)) MARK#(add(z0,z1)) = [2] z0 + [2] z1 + [0] >= [2] z0 + [2] z1 + [0] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [2] z0 + [2] z1 + [0] >= [2] z0 + [0] = c_20(MARK#(z0)) MARK#(first(z0,z1)) = [2] z0 + [2] z1 + [0] >= [2] z1 + [0] = c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [0] >= [2] z0 + [2] z1 + [2] z2 + [0] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) ** Step 1.b:13: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) - Weak DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,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(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add#,a__and#,a__first#,a__from#,a__if#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__ADD) = [1] x2 + [0] p(A__AND) = [1] p(A__FIRST) = [2] x1 + [0] p(A__FROM) = [4] x1 + [1] p(A__IF) = [4] x1 + [0] p(MARK) = [0] p(a__add) = [6] p(a__and) = [1] x1 + [0] p(a__first) = [6] x1 + [6] p(a__from) = [2] x1 + [4] p(a__if) = [0] p(add) = [1] x1 + [1] x2 + [4] p(and) = [1] x1 + [1] x2 + [4] p(c) = [1] p(c1) = [1] p(c10) = [0] p(c11) = [0] p(c12) = [2] p(c13) = [0] p(c14) = [1] x2 + [0] p(c15) = [1] x2 + [0] p(c16) = [1] p(c17) = [1] p(c18) = [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [1] p(c21) = [1] p(c22) = [1] p(c23) = [0] p(c24) = [0] p(c25) = [4] p(c3) = [1] x1 + [0] p(c4) = [0] p(c5) = [0] p(c6) = [1] x1 + [1] p(c7) = [0] p(c8) = [2] p(c9) = [2] p(cons) = [1] x2 + [1] p(false) = [4] p(first) = [1] x1 + [1] x2 + [2] p(from) = [1] x1 + [7] p(if) = [1] x1 + [1] x2 + [1] x3 + [1] p(mark) = [0] p(nil) = [2] p(s) = [1] x1 + [1] p(true) = [0] p(A__ADD#) = [2] x2 + [4] p(A__AND#) = [2] x2 + [4] p(A__FIRST#) = [4] x1 + [1] x2 + [1] p(A__FROM#) = [0] p(A__IF#) = [2] x2 + [2] x3 + [2] p(MARK#) = [2] x1 + [1] p(a__add#) = [1] p(a__and#) = [4] x1 + [2] x2 + [0] p(a__first#) = [1] x1 + [1] p(a__from#) = [1] p(a__if#) = [2] x1 + [1] x2 + [1] x3 + [0] p(mark#) = [1] x1 + [0] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [4] p(c_4) = [1] p(c_5) = [1] p(c_6) = [1] x1 + [3] p(c_7) = [1] p(c_8) = [0] p(c_9) = [4] p(c_10) = [0] p(c_11) = [1] p(c_12) = [1] p(c_13) = [1] x1 + [1] p(c_14) = [1] x1 + [0] p(c_15) = [1] p(c_16) = [1] x1 + [1] x2 + [4] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [1] p(c_19) = [0] p(c_20) = [1] x1 + [4] p(c_21) = [1] x1 + [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] p(c_28) = [1] x1 + [0] p(c_29) = [1] p(c_30) = [0] p(c_31) = [0] p(c_32) = [1] x1 + [4] p(c_33) = [0] p(c_34) = [4] p(c_35) = [0] p(c_36) = [1] p(c_37) = [4] p(c_38) = [0] p(c_39) = [2] x1 + [0] p(c_40) = [0] p(c_41) = [1] p(c_42) = [0] p(c_43) = [1] x2 + [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [1] x2 + [1] x3 + [0] p(c_47) = [2] x1 + [0] p(c_48) = [1] x2 + [0] p(c_49) = [1] p(c_50) = [0] p(c_51) = [1] Following rules are strictly oriented: MARK#(first(z0,z1)) = [2] z0 + [2] z1 + [5] > [2] z1 + [1] = c_21(MARK#(z1)) Following rules are (at-least) weakly oriented: A__ADD#(0(),z0) = [2] z0 + [4] >= [2] z0 + [1] = c_2(MARK#(z0)) A__AND#(true(),z0) = [2] z0 + [4] >= [2] z0 + [4] = c_6(MARK#(z0)) A__IF#(false(),z0,z1) = [2] z0 + [2] z1 + [2] >= [2] z1 + [2] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [2] z0 + [2] z1 + [2] >= [2] z0 + [1] = c_14(MARK#(z0)) MARK#(add(z0,z1)) = [2] z0 + [2] z1 + [9] >= [2] z0 + [2] z1 + [9] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) = [2] z0 + [2] z1 + [9] >= [2] z0 + [2] z1 + [5] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [2] z0 + [2] z1 + [5] >= [2] z0 + [5] = c_20(MARK#(z0)) MARK#(if(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [3] >= [2] z0 + [2] z1 + [2] z2 + [3] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) ** Step 1.b:14: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(first(z0,z1)) -> c_20(MARK#(z0)) - Weak DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,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(c_2) = {1}, uargs(c_6) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2} Following symbols are considered usable: {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add#,a__and#,a__first#,a__from#,a__if#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__ADD) = [0] p(A__AND) = [0] p(A__FIRST) = [0] p(A__FROM) = [0] p(A__IF) = [0] p(MARK) = [0] p(a__add) = [1] x1 + [0] p(a__and) = [1] x1 + [0] p(a__first) = [0] p(a__from) = [0] p(a__if) = [0] p(add) = [1] x1 + [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [3] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [1] x2 + [0] p(c17) = [1] x1 + [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c3) = [1] x1 + [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(cons) = [1] x1 + [0] p(false) = [0] p(first) = [1] x1 + [1] x2 + [1] p(from) = [1] x1 + [0] p(if) = [1] x1 + [1] x2 + [1] x3 + [2] p(mark) = [4] x1 + [3] p(nil) = [0] p(s) = [3] p(true) = [0] p(A__ADD#) = [4] x2 + [0] p(A__AND#) = [4] x2 + [0] p(A__FIRST#) = [0] p(A__FROM#) = [0] p(A__IF#) = [4] x2 + [4] x3 + [4] p(MARK#) = [4] x1 + [0] p(a__add#) = [0] p(a__and#) = [0] p(a__first#) = [0] p(a__from#) = [0] p(a__if#) = [0] p(mark#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [4] p(c_14) = [1] x1 + [4] p(c_15) = [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [3] p(c_21) = [1] x1 + [4] p(c_22) = [0] p(c_23) = [1] x1 + [1] x2 + [4] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] Following rules are strictly oriented: MARK#(first(z0,z1)) = [4] z0 + [4] z1 + [4] > [4] z0 + [3] = c_20(MARK#(z0)) Following rules are (at-least) weakly oriented: A__ADD#(0(),z0) = [4] z0 + [0] >= [4] z0 + [0] = c_2(MARK#(z0)) A__AND#(true(),z0) = [4] z0 + [0] >= [4] z0 + [0] = c_6(MARK#(z0)) A__IF#(false(),z0,z1) = [4] z0 + [4] z1 + [4] >= [4] z1 + [4] = c_13(MARK#(z1)) A__IF#(true(),z0,z1) = [4] z0 + [4] z1 + [4] >= [4] z0 + [4] = c_14(MARK#(z0)) MARK#(add(z0,z1)) = [4] z0 + [4] z1 + [0] >= [4] z0 + [4] z1 + [0] = c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) = [4] z0 + [4] z1 + [12] >= [4] z0 + [4] z1 + [0] = c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) = [4] z0 + [4] z1 + [4] >= [4] z1 + [4] = c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) = [4] z0 + [4] z1 + [4] z2 + [8] >= [4] z0 + [4] z1 + [4] z2 + [8] = c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) ** Step 1.b:15: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: A__ADD#(0(),z0) -> c_2(MARK#(z0)) A__AND#(true(),z0) -> c_6(MARK#(z0)) A__IF#(false(),z0,z1) -> c_13(MARK#(z1)) A__IF#(true(),z0,z1) -> c_14(MARK#(z0)) MARK#(add(z0,z1)) -> c_16(A__ADD#(mark(z0),z1),MARK#(z0)) MARK#(and(z0,z1)) -> c_17(A__AND#(mark(z0),z1),MARK#(z0)) MARK#(first(z0,z1)) -> c_20(MARK#(z0)) MARK#(first(z0,z1)) -> c_21(MARK#(z1)) MARK#(if(z0,z1,z2)) -> c_23(A__IF#(mark(z0),z1,z2),MARK#(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__and(z0,z1) -> and(z0,z1) a__and(false(),z0) -> false() a__and(true(),z0) -> mark(z0) a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(z1,first(z0,z2)) a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),z1) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(z0,z1) mark(false()) -> false() mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(z0) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(true()) -> true() - Signature: {A__ADD/2,A__AND/2,A__FIRST/2,A__FROM/1,A__IF/3,MARK/1,a__add/2,a__and/2,a__first/2,a__from/1,a__if/3,mark/1 ,A__ADD#/2,A__AND#/2,A__FIRST#/2,A__FROM#/1,A__IF#/3,MARK#/1,a__add#/2,a__and#/2,a__first#/2,a__from#/1 ,a__if#/3,mark#/1} / {0/0,add/2,and/2,c/1,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1 ,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0,c25/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,first/2,from/1 ,if/3,nil/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1 ,c_14/1,c_15/0,c_16/2,c_17/2,c_18/0,c_19/0,c_20/1,c_21/1,c_22/1,c_23/2,c_24/0,c_25/0,c_26/0,c_27/0,c_28/1 ,c_29/0,c_30/0,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/1,c_40/1,c_41/0,c_42/2,c_43/2 ,c_44/0,c_45/0,c_46/3,c_47/1,c_48/2,c_49/0,c_50/0,c_51/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD#,A__AND#,A__FIRST#,A__FROM#,A__IF#,MARK#,a__add# ,a__and#,a__first#,a__from#,a__if#,mark#} and constructors {0,add,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,false,first,from,if,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))