WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,DOMATCH,DOMATCH[ITE],EQNATLIST ,EQNATLIST[ITE],NOTEMPTY,PREFIX,STRMATCH,and,domatch,domatch[Ite],eqNatList,eqNatList[Ite],notEmpty,prefix ,strmatch} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,DOMATCH,DOMATCH[ITE],EQNATLIST ,EQNATLIST[ITE],NOTEMPTY,PREFIX,STRMATCH,and,domatch,domatch[Ite],eqNatList,eqNatList[Ite],notEmpty,prefix ,strmatch} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,DOMATCH,DOMATCH[ITE],EQNATLIST ,EQNATLIST[ITE],NOTEMPTY,PREFIX,STRMATCH,and,domatch,domatch[Ite],eqNatList,eqNatList[Ite],notEmpty,prefix ,strmatch} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: PREFIX(y,u){y -> Cons(x,y),u -> Cons(z,u)} = PREFIX(Cons(x,y),Cons(z,u)) ->^+ c13(AND(!EQ(x,z),prefix(y,u)),PREFIX(y,u)) = C[PREFIX(y,u) = PREFIX(y,u){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,DOMATCH,DOMATCH[ITE],EQNATLIST ,EQNATLIST[ITE],NOTEMPTY,PREFIX,STRMATCH,and,domatch,domatch[Ite],eqNatList,eqNatList[Ite],notEmpty,prefix ,strmatch} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2),!EQ'#(z0,z2)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)) PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)) PREFIX#(Cons(z0,z1),Nil()) -> c_12() PREFIX#(Nil(),z0) -> c_13() STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) Weak DPs !EQ#(0(),0()) -> c_15() !EQ#(0(),S(z0)) -> c_16() !EQ#(S(z0),0()) -> c_17() !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)) !EQ'#(0(),0()) -> c_19() !EQ'#(0(),S(z0)) -> c_20() !EQ'#(S(z0),0()) -> c_21() !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)) AND#(False(),False()) -> c_23() AND#(False(),True()) -> c_24() AND#(True(),False()) -> c_25() AND#(True(),True()) -> c_26() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE]#(False(),z0,z1,z2,z3) -> c_29() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) and#(False(),False()) -> c_31() and#(False(),True()) -> c_32() and#(True(),False()) -> c_33() and#(True(),True()) -> c_34() domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))) domatch#(Cons(z0,z1),Nil(),z2) -> c_36() domatch#(Nil(),Nil(),z0) -> c_37() domatch[Ite]#(False(),z0,Cons(z1,z2),z3) -> c_38(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) domatch[Ite]#(True(),z0,Cons(z1,z2),z3) -> c_39(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList#(Cons(z0,z1),Cons(z2,z3)) -> c_40(eqNatList[Ite]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2)) eqNatList#(Cons(z0,z1),Nil()) -> c_41() eqNatList#(Nil(),Cons(z0,z1)) -> c_42() eqNatList#(Nil(),Nil()) -> c_43() eqNatList[Ite]#(False(),z0,z1,z2,z3) -> c_44() eqNatList[Ite]#(True(),z0,z1,z2,z3) -> c_45(eqNatList#(z3,z1)) notEmpty#(Cons(z0,z1)) -> c_46() notEmpty#(Nil()) -> c_47() prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)),!EQ#(z0,z2),prefix#(z1,z3)) prefix#(Cons(z0,z1),Nil()) -> c_49() prefix#(Nil(),z0) -> c_50() strmatch#(z0,z1) -> c_51(domatch#(z0,z1,Nil())) and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2),!EQ'#(z0,z2)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)) PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)) PREFIX#(Cons(z0,z1),Nil()) -> c_12() PREFIX#(Nil(),z0) -> c_13() STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) - Weak DPs: !EQ#(0(),0()) -> c_15() !EQ#(0(),S(z0)) -> c_16() !EQ#(S(z0),0()) -> c_17() !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)) !EQ'#(0(),0()) -> c_19() !EQ'#(0(),S(z0)) -> c_20() !EQ'#(S(z0),0()) -> c_21() !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)) AND#(False(),False()) -> c_23() AND#(False(),True()) -> c_24() AND#(True(),False()) -> c_25() AND#(True(),True()) -> c_26() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE]#(False(),z0,z1,z2,z3) -> c_29() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) and#(False(),False()) -> c_31() and#(False(),True()) -> c_32() and#(True(),False()) -> c_33() and#(True(),True()) -> c_34() domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))) domatch#(Cons(z0,z1),Nil(),z2) -> c_36() domatch#(Nil(),Nil(),z0) -> c_37() domatch[Ite]#(False(),z0,Cons(z1,z2),z3) -> c_38(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) domatch[Ite]#(True(),z0,Cons(z1,z2),z3) -> c_39(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList#(Cons(z0,z1),Cons(z2,z3)) -> c_40(eqNatList[Ite]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2)) eqNatList#(Cons(z0,z1),Nil()) -> c_41() eqNatList#(Nil(),Cons(z0,z1)) -> c_42() eqNatList#(Nil(),Nil()) -> c_43() eqNatList[Ite]#(False(),z0,z1,z2,z3) -> c_44() eqNatList[Ite]#(True(),z0,z1,z2,z3) -> c_45(eqNatList#(z3,z1)) notEmpty#(Cons(z0,z1)) -> c_46() notEmpty#(Nil()) -> c_47() prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)),!EQ#(z0,z2),prefix#(z1,z3)) prefix#(Cons(z0,z1),Nil()) -> c_49() prefix#(Nil(),z0) -> c_50() strmatch#(z0,z1) -> c_51(domatch#(z0,z1,Nil())) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/3,c_2/0,c_3/0,c_4/3,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/4,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {8,9,10,12,13} by application of Pre({8,9,10,12,13}) = {1,11}. Here rules are labelled as follows: 1: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))) 2: DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() 3: DOMATCH#(Nil(),Nil(),z0) -> c_3() 4: EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) ,!EQ#(z0,z2) ,!EQ'#(z0,z2)) 5: EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() 6: EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() 7: EQNATLIST#(Nil(),Nil()) -> c_7() 8: NOTEMPTY#(Cons(z0,z1)) -> c_8() 9: NOTEMPTY#(Nil()) -> c_9() 10: PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)) 11: PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)) 12: PREFIX#(Cons(z0,z1),Nil()) -> c_12() 13: PREFIX#(Nil(),z0) -> c_13() 14: STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) 15: !EQ#(0(),0()) -> c_15() 16: !EQ#(0(),S(z0)) -> c_16() 17: !EQ#(S(z0),0()) -> c_17() 18: !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)) 19: !EQ'#(0(),0()) -> c_19() 20: !EQ'#(0(),S(z0)) -> c_20() 21: !EQ'#(S(z0),0()) -> c_21() 22: !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)) 23: AND#(False(),False()) -> c_23() 24: AND#(False(),True()) -> c_24() 25: AND#(True(),False()) -> c_25() 26: AND#(True(),True()) -> c_26() 27: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) 28: DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) 29: EQNATLIST[ITE]#(False(),z0,z1,z2,z3) -> c_29() 30: EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) 31: and#(False(),False()) -> c_31() 32: and#(False(),True()) -> c_32() 33: and#(True(),False()) -> c_33() 34: and#(True(),True()) -> c_34() 35: domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))) 36: domatch#(Cons(z0,z1),Nil(),z2) -> c_36() 37: domatch#(Nil(),Nil(),z0) -> c_37() 38: domatch[Ite]#(False(),z0,Cons(z1,z2),z3) -> c_38(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) 39: domatch[Ite]#(True(),z0,Cons(z1,z2),z3) -> c_39(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) 40: eqNatList#(Cons(z0,z1),Cons(z2,z3)) -> c_40(eqNatList[Ite]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2)) 41: eqNatList#(Cons(z0,z1),Nil()) -> c_41() 42: eqNatList#(Nil(),Cons(z0,z1)) -> c_42() 43: eqNatList#(Nil(),Nil()) -> c_43() 44: eqNatList[Ite]#(False(),z0,z1,z2,z3) -> c_44() 45: eqNatList[Ite]#(True(),z0,z1,z2,z3) -> c_45(eqNatList#(z3,z1)) 46: notEmpty#(Cons(z0,z1)) -> c_46() 47: notEmpty#(Nil()) -> c_47() 48: prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)),!EQ#(z0,z2),prefix#(z1,z3)) 49: prefix#(Cons(z0,z1),Nil()) -> c_49() 50: prefix#(Nil(),z0) -> c_50() 51: strmatch#(z0,z1) -> c_51(domatch#(z0,z1,Nil())) ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2),!EQ'#(z0,z2)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)) STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) - Weak DPs: !EQ#(0(),0()) -> c_15() !EQ#(0(),S(z0)) -> c_16() !EQ#(S(z0),0()) -> c_17() !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)) !EQ'#(0(),0()) -> c_19() !EQ'#(0(),S(z0)) -> c_20() !EQ'#(S(z0),0()) -> c_21() !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)) AND#(False(),False()) -> c_23() AND#(False(),True()) -> c_24() AND#(True(),False()) -> c_25() AND#(True(),True()) -> c_26() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE]#(False(),z0,z1,z2,z3) -> c_29() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)) PREFIX#(Cons(z0,z1),Nil()) -> c_12() PREFIX#(Nil(),z0) -> c_13() and#(False(),False()) -> c_31() and#(False(),True()) -> c_32() and#(True(),False()) -> c_33() and#(True(),True()) -> c_34() domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))) domatch#(Cons(z0,z1),Nil(),z2) -> c_36() domatch#(Nil(),Nil(),z0) -> c_37() domatch[Ite]#(False(),z0,Cons(z1,z2),z3) -> c_38(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) domatch[Ite]#(True(),z0,Cons(z1,z2),z3) -> c_39(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList#(Cons(z0,z1),Cons(z2,z3)) -> c_40(eqNatList[Ite]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2)) eqNatList#(Cons(z0,z1),Nil()) -> c_41() eqNatList#(Nil(),Cons(z0,z1)) -> c_42() eqNatList#(Nil(),Nil()) -> c_43() eqNatList[Ite]#(False(),z0,z1,z2,z3) -> c_44() eqNatList[Ite]#(True(),z0,z1,z2,z3) -> c_45(eqNatList#(z3,z1)) notEmpty#(Cons(z0,z1)) -> c_46() notEmpty#(Nil()) -> c_47() prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)),!EQ#(z0,z2),prefix#(z1,z3)) prefix#(Cons(z0,z1),Nil()) -> c_49() prefix#(Nil(),z0) -> c_50() strmatch#(z0,z1) -> c_51(domatch#(z0,z1,Nil())) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/3,c_2/0,c_3/0,c_4/3,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/4,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))) -->_2 prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3)):48 -->_3 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)):28 -->_1 DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):23 -->_1 DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):22 -->_3 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)):8 -->_2 prefix#(Nil(),z0) -> c_50():50 -->_3 PREFIX#(Nil(),z0) -> c_13():30 2:S:DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() 3:S:DOMATCH#(Nil(),Nil(),z0) -> c_3() 4:S:EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) ,!EQ#(z0,z2) ,!EQ'#(z0,z2)) -->_1 EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)):25 -->_3 !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)):17 -->_2 !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)):13 -->_1 EQNATLIST[ITE]#(False(),z0,z1,z2,z3) -> c_29():24 -->_3 !EQ'#(S(z0),0()) -> c_21():16 -->_3 !EQ'#(0(),S(z0)) -> c_20():15 -->_3 !EQ'#(0(),0()) -> c_19():14 -->_2 !EQ#(S(z0),0()) -> c_17():12 -->_2 !EQ#(0(),S(z0)) -> c_16():11 -->_2 !EQ#(0(),0()) -> c_15():10 5:S:EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() 6:S:EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() 7:S:EQNATLIST#(Nil(),Nil()) -> c_7() 8:S:PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)) -->_3 prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3)):48 -->_4 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)):28 -->_2 !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)):13 -->_3 prefix#(Nil(),z0) -> c_50():50 -->_3 prefix#(Cons(z0,z1),Nil()) -> c_49():49 -->_4 PREFIX#(Nil(),z0) -> c_13():30 -->_4 PREFIX#(Cons(z0,z1),Nil()) -> c_12():29 -->_1 AND#(True(),True()) -> c_26():21 -->_1 AND#(True(),False()) -> c_25():20 -->_1 AND#(False(),True()) -> c_24():19 -->_1 AND#(False(),False()) -> c_23():18 -->_2 !EQ#(S(z0),0()) -> c_17():12 -->_2 !EQ#(0(),S(z0)) -> c_16():11 -->_2 !EQ#(0(),0()) -> c_15():10 -->_4 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)):8 9:S:STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))):1 10:W:!EQ#(0(),0()) -> c_15() 11:W:!EQ#(0(),S(z0)) -> c_16() 12:W:!EQ#(S(z0),0()) -> c_17() 13:W:!EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)) -->_1 !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)):13 -->_1 !EQ#(S(z0),0()) -> c_17():12 -->_1 !EQ#(0(),S(z0)) -> c_16():11 -->_1 !EQ#(0(),0()) -> c_15():10 14:W:!EQ'#(0(),0()) -> c_19() 15:W:!EQ'#(0(),S(z0)) -> c_20() 16:W:!EQ'#(S(z0),0()) -> c_21() 17:W:!EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)) -->_1 !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)):17 -->_1 !EQ'#(S(z0),0()) -> c_21():16 -->_1 !EQ'#(0(),S(z0)) -> c_20():15 -->_1 !EQ'#(0(),0()) -> c_19():14 18:W:AND#(False(),False()) -> c_23() 19:W:AND#(False(),True()) -> c_24() 20:W:AND#(True(),False()) -> c_25() 21:W:AND#(True(),True()) -> c_26() 22:W:DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))):1 23:W:DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))):1 24:W:EQNATLIST[ITE]#(False(),z0,z1,z2,z3) -> c_29() 25:W:EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) -->_1 EQNATLIST#(Nil(),Nil()) -> c_7():7 -->_1 EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6():6 -->_1 EQNATLIST#(Cons(z0,z1),Nil()) -> c_5():5 -->_1 EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) ,!EQ#(z0,z2) ,!EQ'#(z0,z2)):4 26:W:NOTEMPTY#(Cons(z0,z1)) -> c_8() 27:W:NOTEMPTY#(Nil()) -> c_9() 28:W:PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)) -->_3 prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3)):48 -->_3 prefix#(Nil(),z0) -> c_50():50 -->_3 prefix#(Cons(z0,z1),Nil()) -> c_49():49 -->_1 AND#(True(),True()) -> c_26():21 -->_1 AND#(True(),False()) -> c_25():20 -->_1 AND#(False(),True()) -> c_24():19 -->_1 AND#(False(),False()) -> c_23():18 -->_4 !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)):17 -->_4 !EQ'#(S(z0),0()) -> c_21():16 -->_4 !EQ'#(0(),S(z0)) -> c_20():15 -->_4 !EQ'#(0(),0()) -> c_19():14 -->_2 !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)):13 -->_2 !EQ#(S(z0),0()) -> c_17():12 -->_2 !EQ#(0(),S(z0)) -> c_16():11 -->_2 !EQ#(0(),0()) -> c_15():10 29:W:PREFIX#(Cons(z0,z1),Nil()) -> c_12() 30:W:PREFIX#(Nil(),z0) -> c_13() 31:W:and#(False(),False()) -> c_31() 32:W:and#(False(),True()) -> c_32() 33:W:and#(True(),False()) -> c_33() 34:W:and#(True(),True()) -> c_34() 35:W:domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))) -->_2 prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3)):48 -->_1 domatch[Ite]#(True(),z0,Cons(z1,z2),z3) -> c_39(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):39 -->_1 domatch[Ite]#(False(),z0,Cons(z1,z2),z3) -> c_38(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):38 -->_2 prefix#(Nil(),z0) -> c_50():50 36:W:domatch#(Cons(z0,z1),Nil(),z2) -> c_36() 37:W:domatch#(Nil(),Nil(),z0) -> c_37() 38:W:domatch[Ite]#(False(),z0,Cons(z1,z2),z3) -> c_38(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),z0) -> c_37():37 -->_1 domatch#(Cons(z0,z1),Nil(),z2) -> c_36():36 -->_1 domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))):35 39:W:domatch[Ite]#(True(),z0,Cons(z1,z2),z3) -> c_39(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),z0) -> c_37():37 -->_1 domatch#(Cons(z0,z1),Nil(),z2) -> c_36():36 -->_1 domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))):35 40:W:eqNatList#(Cons(z0,z1),Cons(z2,z3)) -> c_40(eqNatList[Ite]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2)) -->_1 eqNatList[Ite]#(True(),z0,z1,z2,z3) -> c_45(eqNatList#(z3,z1)):45 -->_1 eqNatList[Ite]#(False(),z0,z1,z2,z3) -> c_44():44 -->_2 !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)):13 -->_2 !EQ#(S(z0),0()) -> c_17():12 -->_2 !EQ#(0(),S(z0)) -> c_16():11 -->_2 !EQ#(0(),0()) -> c_15():10 41:W:eqNatList#(Cons(z0,z1),Nil()) -> c_41() 42:W:eqNatList#(Nil(),Cons(z0,z1)) -> c_42() 43:W:eqNatList#(Nil(),Nil()) -> c_43() 44:W:eqNatList[Ite]#(False(),z0,z1,z2,z3) -> c_44() 45:W:eqNatList[Ite]#(True(),z0,z1,z2,z3) -> c_45(eqNatList#(z3,z1)) -->_1 eqNatList#(Nil(),Nil()) -> c_43():43 -->_1 eqNatList#(Nil(),Cons(z0,z1)) -> c_42():42 -->_1 eqNatList#(Cons(z0,z1),Nil()) -> c_41():41 -->_1 eqNatList#(Cons(z0,z1),Cons(z2,z3)) -> c_40(eqNatList[Ite]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2)):40 46:W:notEmpty#(Cons(z0,z1)) -> c_46() 47:W:notEmpty#(Nil()) -> c_47() 48:W:prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)),!EQ#(z0,z2),prefix#(z1,z3)) -->_3 prefix#(Nil(),z0) -> c_50():50 -->_3 prefix#(Cons(z0,z1),Nil()) -> c_49():49 -->_3 prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3)):48 -->_1 and#(True(),True()) -> c_34():34 -->_1 and#(True(),False()) -> c_33():33 -->_1 and#(False(),True()) -> c_32():32 -->_1 and#(False(),False()) -> c_31():31 -->_2 !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)):13 -->_2 !EQ#(S(z0),0()) -> c_17():12 -->_2 !EQ#(0(),S(z0)) -> c_16():11 -->_2 !EQ#(0(),0()) -> c_15():10 49:W:prefix#(Cons(z0,z1),Nil()) -> c_49() 50:W:prefix#(Nil(),z0) -> c_50() 51:W:strmatch#(z0,z1) -> c_51(domatch#(z0,z1,Nil())) -->_1 domatch#(Nil(),Nil(),z0) -> c_37():37 -->_1 domatch#(Cons(z0,z1),Nil(),z2) -> c_36():36 -->_1 domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))):35 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 51: strmatch#(z0,z1) -> c_51(domatch#(z0,z1,Nil())) 47: notEmpty#(Nil()) -> c_47() 46: notEmpty#(Cons(z0,z1)) -> c_46() 40: eqNatList#(Cons(z0,z1),Cons(z2,z3)) -> c_40(eqNatList[Ite]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2)) 45: eqNatList[Ite]#(True(),z0,z1,z2,z3) -> c_45(eqNatList#(z3,z1)) 44: eqNatList[Ite]#(False(),z0,z1,z2,z3) -> c_44() 41: eqNatList#(Cons(z0,z1),Nil()) -> c_41() 42: eqNatList#(Nil(),Cons(z0,z1)) -> c_42() 43: eqNatList#(Nil(),Nil()) -> c_43() 35: domatch#(z0,Cons(z1,z2),z3) -> c_35(domatch[Ite]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2))) 39: domatch[Ite]#(True(),z0,Cons(z1,z2),z3) -> c_39(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) 38: domatch[Ite]#(False(),z0,Cons(z1,z2),z3) -> c_38(domatch#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) 36: domatch#(Cons(z0,z1),Nil(),z2) -> c_36() 37: domatch#(Nil(),Nil(),z0) -> c_37() 27: NOTEMPTY#(Nil()) -> c_9() 26: NOTEMPTY#(Cons(z0,z1)) -> c_8() 24: EQNATLIST[ITE]#(False(),z0,z1,z2,z3) -> c_29() 29: PREFIX#(Cons(z0,z1),Nil()) -> c_12() 30: PREFIX#(Nil(),z0) -> c_13() 28: PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_10(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,!EQ'#(z0,z2)) 17: !EQ'#(S(z0),S(z1)) -> c_22(!EQ'#(z0,z1)) 14: !EQ'#(0(),0()) -> c_19() 15: !EQ'#(0(),S(z0)) -> c_20() 16: !EQ'#(S(z0),0()) -> c_21() 18: AND#(False(),False()) -> c_23() 19: AND#(False(),True()) -> c_24() 20: AND#(True(),False()) -> c_25() 21: AND#(True(),True()) -> c_26() 48: prefix#(Cons(z0,z1),Cons(z2,z3)) -> c_48(and#(!EQ(z0,z2),prefix(z1,z3)),!EQ#(z0,z2),prefix#(z1,z3)) 13: !EQ#(S(z0),S(z1)) -> c_18(!EQ#(z0,z1)) 10: !EQ#(0(),0()) -> c_15() 11: !EQ#(0(),S(z0)) -> c_16() 12: !EQ#(S(z0),0()) -> c_17() 31: and#(False(),False()) -> c_31() 32: and#(False(),True()) -> c_32() 33: and#(True(),False()) -> c_33() 34: and#(True(),True()) -> c_34() 49: prefix#(Cons(z0,z1),Nil()) -> c_49() 50: prefix#(Nil(),z0) -> c_50() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1),!EQ#(z0,z2),!EQ'#(z0,z2)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)) STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) - Weak DPs: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/3,c_2/0,c_3/0,c_4/3,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/4,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))) -->_1 DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):23 -->_1 DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):22 -->_3 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)):8 2:S:DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() 3:S:DOMATCH#(Nil(),Nil(),z0) -> c_3() 4:S:EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) ,!EQ#(z0,z2) ,!EQ'#(z0,z2)) -->_1 EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)):25 5:S:EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() 6:S:EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() 7:S:EQNATLIST#(Nil(),Nil()) -> c_7() 8:S:PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)) -->_4 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(AND#(!EQ(z0,z2),prefix(z1,z3)) ,!EQ#(z0,z2) ,prefix#(z1,z3) ,PREFIX#(z1,z3)):8 9:S:STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))):1 22:W:DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))):1 23:W:DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,prefix#(z0,Cons(z1,z2)) ,PREFIX#(z0,Cons(z1,z2))):1 25:W:EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) -->_1 EQNATLIST#(Nil(),Nil()) -> c_7():7 -->_1 EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6():6 -->_1 EQNATLIST#(Cons(z0,z1),Nil()) -> c_5():5 -->_1 EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) ,!EQ#(z0,z2) ,!EQ'#(z0,z2)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) - Weak DPs: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() DOMATCH(z0,Cons(z1,z2),z3) -> c18(DOMATCH[ITE](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX(z0,Cons(z1,z2))) DOMATCH(Cons(z0,z1),Nil(),z2) -> c16() DOMATCH(Nil(),Nil(),z0) -> c17() DOMATCH[ITE](False(),z0,Cons(z1,z2),z3) -> c8(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE](True(),z0,Cons(z1,z2),z3) -> c9(DOMATCH(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST(Cons(z0,z1),Cons(z2,z3)) -> c19(EQNATLIST[ITE](!EQ(z0,z2),z2,z3,z0,z1),!EQ'(z0,z2)) EQNATLIST(Cons(z0,z1),Nil()) -> c20() EQNATLIST(Nil(),Cons(z0,z1)) -> c21() EQNATLIST(Nil(),Nil()) -> c22() EQNATLIST[ITE](False(),z0,z1,z2,z3) -> c10() EQNATLIST[ITE](True(),z0,z1,z2,z3) -> c11(EQNATLIST(z3,z1)) NOTEMPTY(Cons(z0,z1)) -> c23() NOTEMPTY(Nil()) -> c24() PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c12(AND(!EQ(z0,z2),prefix(z1,z3)),!EQ'(z0,z2)) PREFIX(Cons(z0,z1),Cons(z2,z3)) -> c13(AND(!EQ(z0,z2),prefix(z1,z3)),PREFIX(z1,z3)) PREFIX(Cons(z0,z1),Nil()) -> c14() PREFIX(Nil(),z0) -> c15() STRMATCH(z0,z1) -> c25(DOMATCH(z0,z1,Nil())) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(z0,Cons(z1,z2),z3) -> domatch[Ite](prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) domatch(Cons(z0,z1),Nil(),z2) -> Nil() domatch(Nil(),Nil(),z0) -> Cons(z0,Nil()) domatch[Ite](False(),z0,Cons(z1,z2),z3) -> domatch(z0,z2,Cons(z3,Cons(Nil(),Nil()))) domatch[Ite](True(),z0,Cons(z1,z2),z3) -> Cons(z3,domatch(z0,z2,Cons(z3,Cons(Nil(),Nil())))) eqNatList(Cons(z0,z1),Cons(z2,z3)) -> eqNatList[Ite](!EQ(z0,z2),z2,z3,z0,z1) eqNatList(Cons(z0,z1),Nil()) -> False() eqNatList(Nil(),Cons(z0,z1)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),z0,z1,z2,z3) -> False() eqNatList[Ite](True(),z0,z1,z2,z3) -> eqNatList(z3,z1) notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() strmatch(z0,z1) -> domatch(z0,z1,Nil()) - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) ** Step 1.b:6: RemoveHeads. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) - Weak DPs: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) -->_1 DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):11 -->_1 DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):10 -->_2 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)):8 2:S:DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() 3:S:DOMATCH#(Nil(),Nil(),z0) -> c_3() 4:S:EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) -->_1 EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)):12 5:S:EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() 6:S:EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() 7:S:EQNATLIST#(Nil(),Nil()) -> c_7() 8:S:PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) -->_1 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)):8 9:S:STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))):1 10:W:DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))):1 11:W:DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():3 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():2 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))):1 12:W:EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) -->_1 EQNATLIST#(Nil(),Nil()) -> c_7():7 -->_1 EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6():6 -->_1 EQNATLIST#(Cons(z0,z1),Nil()) -> c_5():5 -->_1 EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)):4 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(9,STRMATCH#(z0,z1) -> c_14(DOMATCH#(z0,z1,Nil())))] ** Step 1.b:7: DecomposeDG. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) - Weak DPs: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) and a lower component DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) Further, following extension rules are added to the lower component. DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> EQNATLIST#(z3,z1) *** Step 1.b:7.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() - Weak DPs: EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))) -->_1 DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):3 -->_1 DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))):2 2:S:DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))):1 3:S:DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) ,PREFIX#(z0,Cons(z1,z2))):1 4:S:EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) -->_1 EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)):8 5:S:EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() 6:S:EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() 7:S:EQNATLIST#(Nil(),Nil()) -> c_7() 8:W:EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) -->_1 EQNATLIST#(Nil(),Nil()) -> c_7():7 -->_1 EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6():6 -->_1 EQNATLIST#(Cons(z0,z1),Nil()) -> c_5():5 -->_1 EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) *** Step 1.b:7.a:2: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() - Weak DPs: EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + 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(and) = {1,2}, uargs(DOMATCH[ITE]#) = {1}, uargs(EQNATLIST[ITE]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1}, uargs(c_30) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(!EQ') = [2] x1 + [0] p(0) = [0] p(AND) = [0] p(Cons) = [0] p(DOMATCH) = [0] p(DOMATCH[ITE]) = [0] p(EQNATLIST) = [0] p(EQNATLIST[ITE]) = [0] p(False) = [0] p(NOTEMPTY) = [0] p(Nil) = [0] p(PREFIX) = [0] p(S) = [1] x1 + [0] p(STRMATCH) = [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [1] x1 + [0] p(c12) = [1] x1 + [1] x2 + [0] p(c13) = [1] x1 + [1] x2 + [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [1] x1 + [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [1] x1 + [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [2] x1 + [0] p(prefix) = [0] p(strmatch) = [0] p(!EQ#) = [0] p(!EQ'#) = [0] p(AND#) = [0] p(DOMATCH#) = [4] p(DOMATCH[ITE]#) = [1] x1 + [1] p(EQNATLIST#) = [1] p(EQNATLIST[ITE]#) = [1] x1 + [2] p(NOTEMPTY#) = [0] p(PREFIX#) = [0] p(STRMATCH#) = [0] p(and#) = [2] x1 + [0] p(domatch#) = [0] p(domatch[Ite]#) = [2] x2 + [0] p(eqNatList#) = [0] p(eqNatList[Ite]#) = [0] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [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) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [0] p(c_28) = [1] x1 + [0] p(c_29) = [0] p(c_30) = [1] x1 + [1] p(c_31) = [2] p(c_32) = [2] p(c_33) = [0] p(c_34) = [0] p(c_35) = [2] x1 + [1] p(c_36) = [2] p(c_37) = [0] p(c_38) = [1] p(c_39) = [1] x1 + [0] p(c_40) = [1] x1 + [1] x2 + [1] p(c_41) = [1] p(c_42) = [0] p(c_43) = [1] p(c_44) = [0] p(c_45) = [1] x1 + [1] p(c_46) = [2] p(c_47) = [2] p(c_48) = [2] x3 + [0] p(c_49) = [1] p(c_50) = [1] p(c_51) = [1] x1 + [0] Following rules are strictly oriented: DOMATCH#(z0,Cons(z1,z2),z3) = [4] > [1] = c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) EQNATLIST#(Cons(z0,z1),Nil()) = [1] > [0] = c_5() EQNATLIST#(Nil(),Cons(z0,z1)) = [1] > [0] = c_6() EQNATLIST#(Nil(),Nil()) = [1] > [0] = c_7() Following rules are (at-least) weakly oriented: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) = [1] >= [4] = c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) = [1] >= [4] = c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) = [1] >= [2] = c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST[ITE]#(True(),z0,z1,z2,z3) = [2] >= [2] = c_30(EQNATLIST#(z3,z1)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(z0)) = [0] >= [0] = False() !EQ(S(z0),0()) = [0] >= [0] = False() !EQ(S(z0),S(z1)) = [0] >= [0] = !EQ(z0,z1) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(z0,z1),Cons(z2,z3)) = [0] >= [0] = and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) = [0] >= [0] = False() prefix(Nil(),z0) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:7.a:3: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + 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(and) = {1,2}, uargs(DOMATCH[ITE]#) = {1}, uargs(EQNATLIST[ITE]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1}, uargs(c_30) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(!EQ') = [0] p(0) = [0] p(AND) = [1] x2 + [2] p(Cons) = [1] x1 + [1] x2 + [1] p(DOMATCH) = [1] x2 + [0] p(DOMATCH[ITE]) = [4] x1 + [1] x2 + [2] x3 + [0] p(EQNATLIST) = [2] x2 + [0] p(EQNATLIST[ITE]) = [2] x2 + [4] x3 + [4] x5 + [1] p(False) = [0] p(NOTEMPTY) = [1] p(Nil) = [1] p(PREFIX) = [4] x1 + [0] p(S) = [2] p(STRMATCH) = [1] x1 + [2] x2 + [2] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(c) = [1] p(c1) = [0] p(c10) = [0] p(c11) = [1] x1 + [1] p(c12) = [1] x2 + [1] p(c13) = [1] x1 + [1] x2 + [0] p(c14) = [0] p(c15) = [0] p(c16) = [1] p(c17) = [1] p(c18) = [1] x1 + [1] x2 + [1] p(c19) = [1] x2 + [0] p(c2) = [1] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [1] p(c24) = [0] p(c25) = [0] p(c3) = [0] p(c4) = [1] x1 + [1] p(c5) = [0] p(c6) = [2] p(c7) = [1] p(c8) = [0] p(c9) = [1] x1 + [0] p(domatch) = [4] x1 + [1] x2 + [1] x3 + [1] p(domatch[Ite]) = [1] x3 + [1] x4 + [1] p(eqNatList) = [1] x2 + [0] p(eqNatList[Ite]) = [1] x1 + [1] x5 + [0] p(notEmpty) = [1] x1 + [2] p(prefix) = [0] p(strmatch) = [1] x1 + [1] p(!EQ#) = [2] x2 + [1] p(!EQ'#) = [1] x1 + [1] x2 + [0] p(AND#) = [0] p(DOMATCH#) = [1] x2 + [0] p(DOMATCH[ITE]#) = [1] x1 + [1] x3 + [0] p(EQNATLIST#) = [0] p(EQNATLIST[ITE]#) = [1] x1 + [1] p(NOTEMPTY#) = [1] x1 + [4] p(PREFIX#) = [2] x1 + [2] x2 + [1] p(STRMATCH#) = [2] x2 + [4] p(and#) = [2] x1 + [1] p(domatch#) = [1] x3 + [4] p(domatch[Ite]#) = [1] x2 + [1] x3 + [0] p(eqNatList#) = [1] x1 + [2] p(eqNatList[Ite]#) = [0] p(notEmpty#) = [1] p(prefix#) = [1] x1 + [4] x2 + [1] p(strmatch#) = [1] x2 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [2] p(c_3) = [1] p(c_4) = [1] x1 + [6] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [4] p(c_10) = [1] x2 + [1] x3 + [1] x4 + [4] p(c_11) = [2] p(c_12) = [0] p(c_13) = [0] p(c_14) = [1] x1 + [1] p(c_15) = [1] p(c_16) = [1] p(c_17) = [1] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [1] p(c_22) = [1] x1 + [1] p(c_23) = [2] p(c_24) = [1] p(c_25) = [0] p(c_26) = [1] p(c_27) = [1] x1 + [0] p(c_28) = [1] x1 + [2] p(c_29) = [2] p(c_30) = [1] x1 + [0] p(c_31) = [0] p(c_32) = [1] p(c_33) = [1] p(c_34) = [4] p(c_35) = [1] x1 + [1] x2 + [1] p(c_36) = [0] p(c_37) = [2] p(c_38) = [0] p(c_39) = [0] p(c_40) = [1] p(c_41) = [2] p(c_42) = [0] p(c_43) = [2] p(c_44) = [0] p(c_45) = [1] x1 + [0] p(c_46) = [0] p(c_47) = [4] p(c_48) = [1] x2 + [2] x3 + [4] p(c_49) = [1] p(c_50) = [4] p(c_51) = [0] Following rules are strictly oriented: DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) = [1] z1 + [1] z2 + [1] > [1] z2 + [0] = c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) Following rules are (at-least) weakly oriented: DOMATCH#(z0,Cons(z1,z2),z3) = [1] z1 + [1] z2 + [1] >= [1] z1 + [1] z2 + [1] = c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) = [1] z1 + [1] z2 + [1] >= [1] z2 + [2] = c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) = [0] >= [7] = c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) = [0] >= [0] = c_5() EQNATLIST#(Nil(),Cons(z0,z1)) = [0] >= [0] = c_6() EQNATLIST#(Nil(),Nil()) = [0] >= [0] = c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) = [1] >= [0] = c_30(EQNATLIST#(z3,z1)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(z0)) = [0] >= [0] = False() !EQ(S(z0),0()) = [0] >= [0] = False() !EQ(S(z0),S(z1)) = [0] >= [0] = !EQ(z0,z1) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(z0,z1),Cons(z2,z3)) = [0] >= [0] = and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) = [0] >= [0] = False() prefix(Nil(),z0) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:7.a:4: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + 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(and) = {1,2}, uargs(DOMATCH[ITE]#) = {1}, uargs(EQNATLIST[ITE]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1}, uargs(c_30) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(!EQ') = [0] p(0) = [0] p(AND) = [0] p(Cons) = [1] x1 + [1] x2 + [1] p(DOMATCH) = [0] p(DOMATCH[ITE]) = [0] p(EQNATLIST) = [0] p(EQNATLIST[ITE]) = [0] p(False) = [0] p(NOTEMPTY) = [0] p(Nil) = [0] p(PREFIX) = [0] p(S) = [1] x1 + [0] p(STRMATCH) = [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [1] x1 + [0] p(c12) = [1] x1 + [1] x2 + [0] p(c13) = [1] x1 + [1] x2 + [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [1] x1 + [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [1] x1 + [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [0] p(strmatch) = [0] p(!EQ#) = [0] p(!EQ'#) = [0] p(AND#) = [0] p(DOMATCH#) = [2] x2 + [2] p(DOMATCH[ITE]#) = [1] x1 + [2] x3 + [2] p(EQNATLIST#) = [2] p(EQNATLIST[ITE]#) = [1] x1 + [2] p(NOTEMPTY#) = [0] p(PREFIX#) = [0] p(STRMATCH#) = [0] p(and#) = [0] p(domatch#) = [0] p(domatch[Ite]#) = [0] p(eqNatList#) = [0] p(eqNatList[Ite]#) = [0] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [1] x1 + [2] x2 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [4] p(c_3) = [1] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [2] p(c_7) = [2] p(c_8) = [1] p(c_9) = [1] p(c_10) = [4] x3 + [1] x4 + [1] p(c_11) = [1] x1 + [1] p(c_12) = [2] p(c_13) = [1] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] p(c_19) = [0] p(c_20) = [2] p(c_21) = [0] p(c_22) = [1] p(c_23) = [0] p(c_24) = [4] p(c_25) = [1] p(c_26) = [0] p(c_27) = [1] x1 + [2] p(c_28) = [1] x1 + [1] p(c_29) = [0] p(c_30) = [1] x1 + [0] p(c_31) = [1] p(c_32) = [4] p(c_33) = [4] p(c_34) = [1] p(c_35) = [4] x1 + [0] p(c_36) = [0] p(c_37) = [2] p(c_38) = [1] x1 + [0] p(c_39) = [0] p(c_40) = [1] x1 + [1] x2 + [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [4] p(c_44) = [1] p(c_45) = [2] p(c_46) = [1] p(c_47) = [0] p(c_48) = [1] x1 + [1] x2 + [0] p(c_49) = [1] p(c_50) = [1] p(c_51) = [2] x1 + [2] Following rules are strictly oriented: DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) = [2] z1 + [2] z2 + [4] > [2] z2 + [3] = c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) Following rules are (at-least) weakly oriented: DOMATCH#(z0,Cons(z1,z2),z3) = [2] z1 + [2] z2 + [4] >= [2] z1 + [2] z2 + [4] = c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) = [2] z1 + [2] z2 + [4] >= [2] z2 + [4] = c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) = [2] >= [2] = c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) = [2] >= [0] = c_5() EQNATLIST#(Nil(),Cons(z0,z1)) = [2] >= [2] = c_6() EQNATLIST#(Nil(),Nil()) = [2] >= [2] = c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) = [2] >= [2] = c_30(EQNATLIST#(z3,z1)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(z0)) = [0] >= [0] = False() !EQ(S(z0),0()) = [0] >= [0] = False() !EQ(S(z0),S(z1)) = [0] >= [0] = !EQ(z0,z1) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(z0,z1),Cons(z2,z3)) = [0] >= [0] = and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) = [0] >= [0] = False() prefix(Nil(),z0) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:7.a:5: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + 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_1) = {1}, uargs(c_4) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1}, uargs(c_30) = {1} Following symbols are considered usable: {!EQ,!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST#,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and# ,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} TcT has computed the following interpretation: p(!EQ) = [1] x1 + [1] x2 + [4] p(!EQ') = [4] x1 + [1] p(0) = [0] p(AND) = [1] x2 + [0] p(Cons) = [1] x1 + [1] x2 + [1] p(DOMATCH) = [2] x3 + [0] p(DOMATCH[ITE]) = [4] x1 + [1] x3 + [4] p(EQNATLIST) = [1] p(EQNATLIST[ITE]) = [0] p(False) = [2] p(NOTEMPTY) = [1] x1 + [0] p(Nil) = [2] p(PREFIX) = [1] x1 + [1] p(S) = [1] x1 + [0] p(STRMATCH) = [1] p(True) = [4] p(and) = [2] p(c) = [0] p(c1) = [1] p(c10) = [1] p(c11) = [1] x1 + [1] p(c12) = [0] p(c13) = [0] p(c14) = [1] p(c15) = [1] p(c16) = [2] p(c17) = [1] p(c18) = [0] p(c19) = [1] p(c2) = [4] p(c20) = [0] p(c21) = [1] p(c22) = [1] p(c23) = [1] p(c24) = [4] p(c25) = [2] p(c3) = [0] p(c4) = [1] p(c5) = [4] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [1] x1 + [1] p(domatch) = [2] x2 + [2] x3 + [2] p(domatch[Ite]) = [1] x4 + [2] p(eqNatList) = [1] x1 + [1] p(eqNatList[Ite]) = [4] x3 + [1] p(notEmpty) = [1] p(prefix) = [5] x2 + [0] p(strmatch) = [2] x1 + [0] p(!EQ#) = [4] p(!EQ'#) = [1] p(AND#) = [4] x1 + [0] p(DOMATCH#) = [0] p(DOMATCH[ITE]#) = [0] p(EQNATLIST#) = [3] x1 + [2] x2 + [4] p(EQNATLIST[ITE]#) = [2] x1 + [2] x3 + [1] x4 + [3] x5 + [0] p(NOTEMPTY#) = [4] p(PREFIX#) = [0] p(STRMATCH#) = [1] x1 + [1] x2 + [2] p(and#) = [1] x1 + [1] x2 + [2] p(domatch#) = [2] x1 + [1] x3 + [0] p(domatch[Ite]#) = [0] p(eqNatList#) = [4] p(eqNatList[Ite]#) = [4] x4 + [1] x5 + [0] p(notEmpty#) = [4] p(prefix#) = [0] p(strmatch#) = [2] x1 + [4] x2 + [0] p(c_1) = [4] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [1] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] x2 + [1] x4 + [4] p(c_11) = [1] x1 + [2] p(c_12) = [4] p(c_13) = [1] p(c_14) = [4] x1 + [1] p(c_15) = [2] p(c_16) = [0] p(c_17) = [1] p(c_18) = [4] x1 + [0] p(c_19) = [0] p(c_20) = [1] p(c_21) = [4] p(c_22) = [1] p(c_23) = [1] p(c_24) = [4] p(c_25) = [1] p(c_26) = [1] p(c_27) = [2] x1 + [0] p(c_28) = [4] x1 + [0] p(c_29) = [0] p(c_30) = [1] x1 + [2] p(c_31) = [4] p(c_32) = [0] p(c_33) = [1] p(c_34) = [0] p(c_35) = [4] x2 + [0] p(c_36) = [4] p(c_37) = [0] p(c_38) = [1] x1 + [0] p(c_39) = [1] x1 + [1] p(c_40) = [4] x1 + [1] x2 + [1] p(c_41) = [0] p(c_42) = [2] p(c_43) = [0] p(c_44) = [0] p(c_45) = [1] p(c_46) = [1] p(c_47) = [4] p(c_48) = [0] p(c_49) = [1] p(c_50) = [1] p(c_51) = [4] x1 + [4] Following rules are strictly oriented: EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) = [3] z0 + [3] z1 + [2] z2 + [2] z3 + [9] > [3] z0 + [3] z1 + [2] z2 + [2] z3 + [8] = c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) Following rules are (at-least) weakly oriented: DOMATCH#(z0,Cons(z1,z2),z3) = [0] >= [0] = c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) = [0] >= [0] = c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) = [0] >= [0] = c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Nil()) = [3] z0 + [3] z1 + [11] >= [0] = c_5() EQNATLIST#(Nil(),Cons(z0,z1)) = [2] z0 + [2] z1 + [12] >= [1] = c_6() EQNATLIST#(Nil(),Nil()) = [14] >= [0] = c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) = [2] z1 + [1] z2 + [3] z3 + [8] >= [2] z1 + [3] z3 + [6] = c_30(EQNATLIST#(z3,z1)) !EQ(0(),0()) = [4] >= [4] = True() !EQ(0(),S(z0)) = [1] z0 + [4] >= [2] = False() !EQ(S(z0),0()) = [1] z0 + [4] >= [2] = False() !EQ(S(z0),S(z1)) = [1] z0 + [1] z1 + [4] >= [1] z0 + [1] z1 + [4] = !EQ(z0,z1) *** Step 1.b:7.a:6: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> c_1(DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> c_27(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> c_28(DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil())))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> c_4(EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1)) EQNATLIST#(Cons(z0,z1),Nil()) -> c_5() EQNATLIST#(Nil(),Cons(z0,z1)) -> c_6() EQNATLIST#(Nil(),Nil()) -> c_7() EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> c_30(EQNATLIST#(z3,z1)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:7.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> EQNATLIST#(z3,z1) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() 2:S:DOMATCH#(Nil(),Nil(),z0) -> c_3() 3:S:PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) -->_1 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)):3 4:W:DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) -->_1 DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))):7 -->_1 DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))):6 5:W:DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)) -->_1 PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)):3 6:W:DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)):5 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3):4 -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():2 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():1 7:W:DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)):5 -->_1 DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3):4 -->_1 DOMATCH#(Nil(),Nil(),z0) -> c_3():2 -->_1 DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2():1 8:W:EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) -->_1 EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> EQNATLIST#(z3,z1):9 9:W:EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> EQNATLIST#(z3,z1) -->_1 EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1):8 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: EQNATLIST#(Cons(z0,z1),Cons(z2,z3)) -> EQNATLIST[ITE]#(!EQ(z0,z2),z2,z3,z0,z1) 9: EQNATLIST[ITE]#(True(),z0,z1,z2,z3) -> EQNATLIST#(z3,z1) *** Step 1.b:7.b:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)) DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + 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_11) = {1} Following symbols are considered usable: {!EQ,and,prefix,!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST#,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX# ,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} TcT has computed the following interpretation: p(!EQ) = [3] p(!EQ') = [0] p(0) = [0] p(AND) = [0] p(Cons) = [0] p(DOMATCH) = [0] p(DOMATCH[ITE]) = [0] p(EQNATLIST) = [0] p(EQNATLIST[ITE]) = [0] p(False) = [3] p(NOTEMPTY) = [0] p(Nil) = [0] p(PREFIX) = [0] p(S) = [0] p(STRMATCH) = [0] p(True) = [0] p(and) = [3] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [3] p(strmatch) = [0] p(!EQ#) = [0] p(!EQ'#) = [0] p(AND#) = [0] p(DOMATCH#) = [13] p(DOMATCH[ITE]#) = [13] p(EQNATLIST#) = [0] p(EQNATLIST[ITE]#) = [0] p(NOTEMPTY#) = [0] p(PREFIX#) = [0] p(STRMATCH#) = [0] p(and#) = [0] p(domatch#) = [0] p(domatch[Ite]#) = [0] p(eqNatList#) = [0] p(eqNatList[Ite]#) = [0] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [0] p(c_1) = [0] p(c_2) = [9] p(c_3) = [13] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [2] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [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: DOMATCH#(Cons(z0,z1),Nil(),z2) = [13] > [9] = c_2() Following rules are (at-least) weakly oriented: DOMATCH#(z0,Cons(z1,z2),z3) = [13] >= [13] = DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) = [13] >= [0] = PREFIX#(z0,Cons(z1,z2)) DOMATCH#(Nil(),Nil(),z0) = [13] >= [13] = c_3() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) = [13] >= [13] = DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) = [13] >= [13] = DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) PREFIX#(Cons(z0,z1),Cons(z2,z3)) = [0] >= [0] = c_11(PREFIX#(z1,z3)) !EQ(0(),0()) = [3] >= [0] = True() !EQ(0(),S(z0)) = [3] >= [3] = False() !EQ(S(z0),0()) = [3] >= [3] = False() !EQ(S(z0),S(z1)) = [3] >= [3] = !EQ(z0,z1) and(False(),False()) = [3] >= [3] = False() and(False(),True()) = [3] >= [3] = False() and(True(),False()) = [3] >= [3] = False() and(True(),True()) = [3] >= [0] = True() prefix(Cons(z0,z1),Cons(z2,z3)) = [3] >= [3] = and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) = [3] >= [3] = False() prefix(Nil(),z0) = [3] >= [0] = True() *** Step 1.b:7.b:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DOMATCH#(Nil(),Nil(),z0) -> c_3() PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + 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_11) = {1} Following symbols are considered usable: {!EQ,and,prefix,!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST#,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX# ,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} TcT has computed the following interpretation: p(!EQ) = [10] p(!EQ') = [0] p(0) = [0] p(AND) = [0] p(Cons) = [0] p(DOMATCH) = [0] p(DOMATCH[ITE]) = [0] p(EQNATLIST) = [0] p(EQNATLIST[ITE]) = [0] p(False) = [10] p(NOTEMPTY) = [0] p(Nil) = [0] p(PREFIX) = [0] p(S) = [0] p(STRMATCH) = [0] p(True) = [10] p(and) = [10] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [10] p(strmatch) = [0] p(!EQ#) = [0] p(!EQ'#) = [0] p(AND#) = [0] p(DOMATCH#) = [2] p(DOMATCH[ITE]#) = [2] p(EQNATLIST#) = [0] p(EQNATLIST[ITE]#) = [0] p(NOTEMPTY#) = [0] p(PREFIX#) = [2] p(STRMATCH#) = [0] p(and#) = [0] p(domatch#) = [0] p(domatch[Ite]#) = [0] p(eqNatList#) = [0] p(eqNatList[Ite]#) = [0] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [0] p(c_1) = [0] p(c_2) = [2] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [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: DOMATCH#(Nil(),Nil(),z0) = [2] > [0] = c_3() Following rules are (at-least) weakly oriented: DOMATCH#(z0,Cons(z1,z2),z3) = [2] >= [2] = DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) = [2] >= [2] = PREFIX#(z0,Cons(z1,z2)) DOMATCH#(Cons(z0,z1),Nil(),z2) = [2] >= [2] = c_2() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) = [2] >= [2] = DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) = [2] >= [2] = DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) PREFIX#(Cons(z0,z1),Cons(z2,z3)) = [2] >= [2] = c_11(PREFIX#(z1,z3)) !EQ(0(),0()) = [10] >= [10] = True() !EQ(0(),S(z0)) = [10] >= [10] = False() !EQ(S(z0),0()) = [10] >= [10] = False() !EQ(S(z0),S(z1)) = [10] >= [10] = !EQ(z0,z1) and(False(),False()) = [10] >= [10] = False() and(False(),True()) = [10] >= [10] = False() and(True(),False()) = [10] >= [10] = False() and(True(),True()) = [10] >= [10] = True() prefix(Cons(z0,z1),Cons(z2,z3)) = [10] >= [10] = and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) = [10] >= [10] = False() prefix(Nil(),z0) = [10] >= [10] = True() *** Step 1.b:7.b:4: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + 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(and) = {1,2}, uargs(DOMATCH[ITE]#) = {1}, uargs(c_11) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(!EQ') = [0] p(0) = [0] p(AND) = [0] p(Cons) = [1] x2 + [2] p(DOMATCH) = [0] p(DOMATCH[ITE]) = [0] p(EQNATLIST) = [0] p(EQNATLIST[ITE]) = [0] p(False) = [0] p(NOTEMPTY) = [0] p(Nil) = [0] p(PREFIX) = [0] p(S) = [1] x1 + [0] p(STRMATCH) = [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [1] x1 + [0] p(c12) = [1] x1 + [1] x2 + [0] p(c13) = [1] x1 + [1] x2 + [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [1] x1 + [1] x2 + [0] p(c19) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [1] x1 + [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [1] x1 + [0] p(domatch) = [0] p(domatch[Ite]) = [1] x1 + [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [2] p(strmatch) = [0] p(!EQ#) = [0] p(!EQ'#) = [0] p(AND#) = [0] p(DOMATCH#) = [4] x2 + [4] p(DOMATCH[ITE]#) = [1] x1 + [4] x3 + [0] p(EQNATLIST#) = [0] p(EQNATLIST[ITE]#) = [0] p(NOTEMPTY#) = [1] x1 + [0] p(PREFIX#) = [4] x2 + [0] p(STRMATCH#) = [0] p(and#) = [0] p(domatch#) = [0] p(domatch[Ite]#) = [1] x1 + [1] x2 + [2] x4 + [0] p(eqNatList#) = [1] p(eqNatList[Ite]#) = [1] x1 + [4] x4 + [0] p(notEmpty#) = [1] p(prefix#) = [1] x1 + [0] p(strmatch#) = [1] x1 + [1] x2 + [1] p(c_1) = [4] x2 + [0] p(c_2) = [4] p(c_3) = [0] p(c_4) = [4] x1 + [4] p(c_5) = [0] p(c_6) = [1] p(c_7) = [4] p(c_8) = [0] p(c_9) = [0] p(c_10) = [4] x2 + [1] x3 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [2] p(c_26) = [0] p(c_27) = [1] x1 + [2] p(c_28) = [0] p(c_29) = [1] p(c_30) = [1] x1 + [4] p(c_31) = [0] p(c_32) = [1] p(c_33) = [0] p(c_34) = [0] p(c_35) = [2] x1 + [2] p(c_36) = [1] p(c_37) = [0] p(c_38) = [4] p(c_39) = [1] x1 + [0] p(c_40) = [4] x1 + [0] p(c_41) = [0] p(c_42) = [1] p(c_43) = [4] p(c_44) = [0] p(c_45) = [4] p(c_46) = [0] p(c_47) = [1] p(c_48) = [4] x1 + [0] p(c_49) = [0] p(c_50) = [1] p(c_51) = [2] x1 + [0] Following rules are strictly oriented: PREFIX#(Cons(z0,z1),Cons(z2,z3)) = [4] z3 + [8] > [4] z3 + [0] = c_11(PREFIX#(z1,z3)) Following rules are (at-least) weakly oriented: DOMATCH#(z0,Cons(z1,z2),z3) = [4] z2 + [12] >= [4] z2 + [10] = DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) = [4] z2 + [12] >= [4] z2 + [8] = PREFIX#(z0,Cons(z1,z2)) DOMATCH#(Cons(z0,z1),Nil(),z2) = [4] >= [4] = c_2() DOMATCH#(Nil(),Nil(),z0) = [4] >= [0] = c_3() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) = [4] z2 + [8] >= [4] z2 + [4] = DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) = [4] z2 + [8] >= [4] z2 + [4] = DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(z0)) = [0] >= [0] = False() !EQ(S(z0),0()) = [0] >= [0] = False() !EQ(S(z0),S(z1)) = [0] >= [0] = !EQ(z0,z1) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(z0,z1),Cons(z2,z3)) = [2] >= [2] = and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) = [2] >= [0] = False() prefix(Nil(),z0) = [2] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:7.b:5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: DOMATCH#(z0,Cons(z1,z2),z3) -> DOMATCH[ITE]#(prefix(z0,Cons(z1,z2)),z0,Cons(z1,z2),z3) DOMATCH#(z0,Cons(z1,z2),z3) -> PREFIX#(z0,Cons(z1,z2)) DOMATCH#(Cons(z0,z1),Nil(),z2) -> c_2() DOMATCH#(Nil(),Nil(),z0) -> c_3() DOMATCH[ITE]#(False(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) DOMATCH[ITE]#(True(),z0,Cons(z1,z2),z3) -> DOMATCH#(z0,z2,Cons(z3,Cons(Nil(),Nil()))) PREFIX#(Cons(z0,z1),Cons(z2,z3)) -> c_11(PREFIX#(z1,z3)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(z0,z1),Cons(z2,z3)) -> and(!EQ(z0,z2),prefix(z1,z3)) prefix(Cons(z0,z1),Nil()) -> False() prefix(Nil(),z0) -> True() - Signature: {!EQ/2,!EQ'/2,AND/2,DOMATCH/3,DOMATCH[ITE]/4,EQNATLIST/2,EQNATLIST[ITE]/5,NOTEMPTY/1,PREFIX/2,STRMATCH/2 ,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2,!EQ'#/2 ,AND#/2,DOMATCH#/3,DOMATCH[ITE]#/4,EQNATLIST#/2,EQNATLIST[ITE]#/5,NOTEMPTY#/1,PREFIX#/2,STRMATCH#/2,and#/2 ,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0,Cons/2 ,False/0,Nil/0,S/1,True/0,c/0,c1/0,c10/0,c11/1,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0 ,c21/0,c22/0,c23/0,c24/0,c25/1,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/1,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/1 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/0,c_35/2,c_36/0,c_37/0 ,c_38/1,c_39/1,c_40/2,c_41/0,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/0,c_48/3,c_49/0,c_50/0,c_51/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,!EQ'#,AND#,DOMATCH#,DOMATCH[ITE]#,EQNATLIST# ,EQNATLIST[ITE]#,NOTEMPTY#,PREFIX#,STRMATCH#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]# ,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True,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} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))