WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: AND(false(),z0) -> c7() AND(true(),z0) -> c6() EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF1(false(),z0,z1,z2,z3,z4) -> c16(IF2(le(z2,size(z4)),z0,z1,z2,z3,z4),LE(z2,size(z4)),SIZE(z4)) IF1(true(),z0,z1,z2,z3,z4) -> c15() IF2(false(),z0,z1,z2,z3,z4) -> c17() IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c19(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,IF2(true(),z0,z1,z2,z5,z6)) IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c20(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,AND(eq(z0,z3),reach(z4,z1,s(z2),z6,z6)) ,EQ(z0,z3)) IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c21(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,AND(eq(z0,z3),reach(z4,z1,s(z2),z6,z6)) ,REACH(z4,z1,s(z2),z6,z6)) IF2(true(),z0,z1,z2,empty(),z3) -> c18() LE(0(),z0) -> c10() LE(s(z0),0()) -> c11() LE(s(z0),s(z1)) -> c12(LE(z0,z1)) OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,z2,z3,z4) -> c14(IF1(eq(z0,z1),z0,z1,z2,z3,z4),EQ(z0,z1)) REACHABLE(z0,z1,z2) -> c13(REACH(z0,z1,0(),z2,z2)) SIZE(edge(z0,z1,z2)) -> c9(SIZE(z2)) SIZE(empty()) -> c8() - Weak TRS: and(false(),z0) -> false() and(true(),z0) -> z0 eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if1(false(),z0,z1,z2,z3,z4) -> if2(le(z2,size(z4)),z0,z1,z2,z3,z4) if1(true(),z0,z1,z2,z3,z4) -> true() if2(false(),z0,z1,z2,z3,z4) -> false() if2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> or(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) if2(true(),z0,z1,z2,empty(),z3) -> false() le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,z2,z3,z4) -> if1(eq(z0,z1),z0,z1,z2,z3,z4) reachable(z0,z1,z2) -> reach(z0,z1,0(),z2,z2) size(edge(z0,z1,z2)) -> s(size(z2)) size(empty()) -> 0() - Signature: {AND/2,EQ/2,IF1/6,IF2/6,LE/2,OR/2,REACH/5,REACHABLE/3,SIZE/1,and/2,eq/2,if1/6,if2/6,le/2,or/2,reach/5 ,reachable/3,size/1} / {0/0,c/0,c1/0,c10/0,c11/0,c12/1,c13/1,c14/2,c15/0,c16/3,c17/0,c18/0,c19/2,c2/0,c20/3 ,c21/3,c3/1,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,edge/3,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQ,IF1,IF2,LE,OR,REACH,REACHABLE,SIZE,and,eq,if1,if2 ,le,or,reach,reachable,size} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c3 ,c4,c5,c6,c7,c8,c9,edge,empty,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: AND(false(),z0) -> c7() AND(true(),z0) -> c6() EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF1(false(),z0,z1,z2,z3,z4) -> c16(IF2(le(z2,size(z4)),z0,z1,z2,z3,z4),LE(z2,size(z4)),SIZE(z4)) IF1(true(),z0,z1,z2,z3,z4) -> c15() IF2(false(),z0,z1,z2,z3,z4) -> c17() IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c19(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,IF2(true(),z0,z1,z2,z5,z6)) IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c20(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,AND(eq(z0,z3),reach(z4,z1,s(z2),z6,z6)) ,EQ(z0,z3)) IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c21(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,AND(eq(z0,z3),reach(z4,z1,s(z2),z6,z6)) ,REACH(z4,z1,s(z2),z6,z6)) IF2(true(),z0,z1,z2,empty(),z3) -> c18() LE(0(),z0) -> c10() LE(s(z0),0()) -> c11() LE(s(z0),s(z1)) -> c12(LE(z0,z1)) OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,z2,z3,z4) -> c14(IF1(eq(z0,z1),z0,z1,z2,z3,z4),EQ(z0,z1)) REACHABLE(z0,z1,z2) -> c13(REACH(z0,z1,0(),z2,z2)) SIZE(edge(z0,z1,z2)) -> c9(SIZE(z2)) SIZE(empty()) -> c8() - Weak TRS: and(false(),z0) -> false() and(true(),z0) -> z0 eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if1(false(),z0,z1,z2,z3,z4) -> if2(le(z2,size(z4)),z0,z1,z2,z3,z4) if1(true(),z0,z1,z2,z3,z4) -> true() if2(false(),z0,z1,z2,z3,z4) -> false() if2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> or(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) if2(true(),z0,z1,z2,empty(),z3) -> false() le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,z2,z3,z4) -> if1(eq(z0,z1),z0,z1,z2,z3,z4) reachable(z0,z1,z2) -> reach(z0,z1,0(),z2,z2) size(edge(z0,z1,z2)) -> s(size(z2)) size(empty()) -> 0() - Signature: {AND/2,EQ/2,IF1/6,IF2/6,LE/2,OR/2,REACH/5,REACHABLE/3,SIZE/1,and/2,eq/2,if1/6,if2/6,le/2,or/2,reach/5 ,reachable/3,size/1} / {0/0,c/0,c1/0,c10/0,c11/0,c12/1,c13/1,c14/2,c15/0,c16/3,c17/0,c18/0,c19/2,c2/0,c20/3 ,c21/3,c3/1,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,edge/3,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQ,IF1,IF2,LE,OR,REACH,REACHABLE,SIZE,and,eq,if1,if2 ,le,or,reach,reachable,size} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c3 ,c4,c5,c6,c7,c8,c9,edge,empty,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: AND(false(),z0) -> c7() AND(true(),z0) -> c6() EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF1(false(),z0,z1,z2,z3,z4) -> c16(IF2(le(z2,size(z4)),z0,z1,z2,z3,z4),LE(z2,size(z4)),SIZE(z4)) IF1(true(),z0,z1,z2,z3,z4) -> c15() IF2(false(),z0,z1,z2,z3,z4) -> c17() IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c19(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,IF2(true(),z0,z1,z2,z5,z6)) IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c20(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,AND(eq(z0,z3),reach(z4,z1,s(z2),z6,z6)) ,EQ(z0,z3)) IF2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> c21(OR(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) ,AND(eq(z0,z3),reach(z4,z1,s(z2),z6,z6)) ,REACH(z4,z1,s(z2),z6,z6)) IF2(true(),z0,z1,z2,empty(),z3) -> c18() LE(0(),z0) -> c10() LE(s(z0),0()) -> c11() LE(s(z0),s(z1)) -> c12(LE(z0,z1)) OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,z2,z3,z4) -> c14(IF1(eq(z0,z1),z0,z1,z2,z3,z4),EQ(z0,z1)) REACHABLE(z0,z1,z2) -> c13(REACH(z0,z1,0(),z2,z2)) SIZE(edge(z0,z1,z2)) -> c9(SIZE(z2)) SIZE(empty()) -> c8() - Weak TRS: and(false(),z0) -> false() and(true(),z0) -> z0 eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if1(false(),z0,z1,z2,z3,z4) -> if2(le(z2,size(z4)),z0,z1,z2,z3,z4) if1(true(),z0,z1,z2,z3,z4) -> true() if2(false(),z0,z1,z2,z3,z4) -> false() if2(true(),z0,z1,z2,edge(z3,z4,z5),z6) -> or(if2(true(),z0,z1,z2,z5,z6) ,and(eq(z0,z3),reach(z4,z1,s(z2),z6,z6))) if2(true(),z0,z1,z2,empty(),z3) -> false() le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,z2,z3,z4) -> if1(eq(z0,z1),z0,z1,z2,z3,z4) reachable(z0,z1,z2) -> reach(z0,z1,0(),z2,z2) size(edge(z0,z1,z2)) -> s(size(z2)) size(empty()) -> 0() - Signature: {AND/2,EQ/2,IF1/6,IF2/6,LE/2,OR/2,REACH/5,REACHABLE/3,SIZE/1,and/2,eq/2,if1/6,if2/6,le/2,or/2,reach/5 ,reachable/3,size/1} / {0/0,c/0,c1/0,c10/0,c11/0,c12/1,c13/1,c14/2,c15/0,c16/3,c17/0,c18/0,c19/2,c2/0,c20/3 ,c21/3,c3/1,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,edge/3,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQ,IF1,IF2,LE,OR,REACH,REACHABLE,SIZE,and,eq,if1,if2 ,le,or,reach,reachable,size} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c3 ,c4,c5,c6,c7,c8,c9,edge,empty,false,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: EQ(x,y){x -> s(x),y -> s(y)} = EQ(s(x),s(y)) ->^+ c3(EQ(x,y)) = C[EQ(x,y) = EQ(x,y){}] WORST_CASE(Omega(n^1),?)