WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF_REACH_1(false(),z0,z1,edge(z2,z3,z4),z5) -> c11(REACH(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1(true(),z0,z1,edge(z2,z3,z4),z5) -> c10(IF_REACH_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5),EQ(z1,z3)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c13(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z0,z1,z4,z5)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c14(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z3,z1,union(z4,z5),empty()) ,UNION(z4,z5)) IF_REACH_2(true(),z0,z1,edge(z2,z3,z4),z5) -> c12() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,edge(z2,z3,z4),z5) -> c9(IF_REACH_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ(z0,z2)) REACH(z0,z1,empty(),z2) -> c8() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4 ,union/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ,IF_REACH_1,IF_REACH_2,OR,REACH,UNION,eq,if_reach_1 ,if_reach_2,or,reach,union} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,edge,empty ,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF_REACH_1(false(),z0,z1,edge(z2,z3,z4),z5) -> c11(REACH(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1(true(),z0,z1,edge(z2,z3,z4),z5) -> c10(IF_REACH_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5),EQ(z1,z3)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c13(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z0,z1,z4,z5)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c14(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z3,z1,union(z4,z5),empty()) ,UNION(z4,z5)) IF_REACH_2(true(),z0,z1,edge(z2,z3,z4),z5) -> c12() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,edge(z2,z3,z4),z5) -> c9(IF_REACH_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ(z0,z2)) REACH(z0,z1,empty(),z2) -> c8() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4 ,union/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ,IF_REACH_1,IF_REACH_2,OR,REACH,UNION,eq,if_reach_1 ,if_reach_2,or,reach,union} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,edge,empty ,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF_REACH_1(false(),z0,z1,edge(z2,z3,z4),z5) -> c11(REACH(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1(true(),z0,z1,edge(z2,z3,z4),z5) -> c10(IF_REACH_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5),EQ(z1,z3)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c13(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z0,z1,z4,z5)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c14(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z3,z1,union(z4,z5),empty()) ,UNION(z4,z5)) IF_REACH_2(true(),z0,z1,edge(z2,z3,z4),z5) -> c12() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,edge(z2,z3,z4),z5) -> c9(IF_REACH_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ(z0,z2)) REACH(z0,z1,empty(),z2) -> c8() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4 ,union/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ,IF_REACH_1,IF_REACH_2,OR,REACH,UNION,eq,if_reach_1 ,if_reach_2,or,reach,union} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,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){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF_REACH_1(false(),z0,z1,edge(z2,z3,z4),z5) -> c11(REACH(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1(true(),z0,z1,edge(z2,z3,z4),z5) -> c10(IF_REACH_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5),EQ(z1,z3)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c13(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z0,z1,z4,z5)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c14(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z3,z1,union(z4,z5),empty()) ,UNION(z4,z5)) IF_REACH_2(true(),z0,z1,edge(z2,z3,z4),z5) -> c12() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,edge(z2,z3,z4),z5) -> c9(IF_REACH_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ(z0,z2)) REACH(z0,z1,empty(),z2) -> c8() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4 ,union/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ,IF_REACH_1,IF_REACH_2,OR,REACH,UNION,eq,if_reach_1 ,if_reach_2,or,reach,union} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,edge,empty ,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs EQ#(0(),0()) -> c_1() EQ#(0(),s(z0)) -> c_2() EQ#(s(z0),0()) -> c_3() EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() OR#(false(),z0) -> c_10() OR#(true(),z0) -> c_11() REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) REACH#(z0,z1,empty(),z2) -> c_13() UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) UNION#(empty(),z0) -> c_15() Weak DPs eq#(0(),0()) -> c_16() eq#(0(),s(z0)) -> c_17() eq#(s(z0),0()) -> c_18() eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() or#(false(),z0) -> c_24() or#(true(),z0) -> c_25() reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) reach#(z0,z1,empty(),z2) -> c_27() union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) union#(empty(),z0) -> c_29() and mark the set of starting terms. ** Step 1.b:2: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(0(),0()) -> c_1() EQ#(0(),s(z0)) -> c_2() EQ#(s(z0),0()) -> c_3() EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() OR#(false(),z0) -> c_10() OR#(true(),z0) -> c_11() REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) REACH#(z0,z1,empty(),z2) -> c_13() UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) UNION#(empty(),z0) -> c_15() - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) IF_REACH_1(false(),z0,z1,edge(z2,z3,z4),z5) -> c11(REACH(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1(true(),z0,z1,edge(z2,z3,z4),z5) -> c10(IF_REACH_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5),EQ(z1,z3)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c13(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z0,z1,z4,z5)) IF_REACH_2(false(),z0,z1,edge(z2,z3,z4),z5) -> c14(OR(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) ,REACH(z3,z1,union(z4,z5),empty()) ,UNION(z4,z5)) IF_REACH_2(true(),z0,z1,edge(z2,z3,z4),z5) -> c12() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,edge(z2,z3,z4),z5) -> c9(IF_REACH_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ(z0,z2)) REACH(z0,z1,empty(),z2) -> c8() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak DPs: eq#(0(),0()) -> c_16() eq#(0(),s(z0)) -> c_17() eq#(s(z0),0()) -> c_18() eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() or#(false(),z0) -> c_24() or#(true(),z0) -> c_25() reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) reach#(z0,z1,empty(),z2) -> c_27() union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) union#(empty(),z0) -> c_29() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/2,c_8/3,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + 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) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 EQ#(0(),0()) -> c_1() EQ#(0(),s(z0)) -> c_2() EQ#(s(z0),0()) -> c_3() EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() OR#(false(),z0) -> c_10() OR#(true(),z0) -> c_11() REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) REACH#(z0,z1,empty(),z2) -> c_13() UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) UNION#(empty(),z0) -> c_15() eq#(0(),0()) -> c_16() eq#(0(),s(z0)) -> c_17() eq#(s(z0),0()) -> c_18() eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() or#(false(),z0) -> c_24() or#(true(),z0) -> c_25() reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) reach#(z0,z1,empty(),z2) -> c_27() union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) union#(empty(),z0) -> c_29() ** Step 1.b:3: PredecessorEstimation. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(0(),0()) -> c_1() EQ#(0(),s(z0)) -> c_2() EQ#(s(z0),0()) -> c_3() EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() OR#(false(),z0) -> c_10() OR#(true(),z0) -> c_11() REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) REACH#(z0,z1,empty(),z2) -> c_13() UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) UNION#(empty(),z0) -> c_15() - Weak DPs: eq#(0(),0()) -> c_16() eq#(0(),s(z0)) -> c_17() eq#(s(z0),0()) -> c_18() eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() or#(false(),z0) -> c_24() or#(true(),z0) -> c_25() reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) reach#(z0,z1,empty(),z2) -> c_27() union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) union#(empty(),z0) -> c_29() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/2,c_8/3,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,9,10,11,13,15} by application of Pre({1,2,3,9,10,11,13,15}) = {4,5,6,7,8,12,14}. Here rules are labelled as follows: 1: EQ#(0(),0()) -> c_1() 2: EQ#(0(),s(z0)) -> c_2() 3: EQ#(s(z0),0()) -> c_3() 4: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) 5: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) 6: IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) 7: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) 8: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) 9: IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() 10: OR#(false(),z0) -> c_10() 11: OR#(true(),z0) -> c_11() 12: REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) 13: REACH#(z0,z1,empty(),z2) -> c_13() 14: UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) 15: UNION#(empty(),z0) -> c_15() 16: eq#(0(),0()) -> c_16() 17: eq#(0(),s(z0)) -> c_17() 18: eq#(s(z0),0()) -> c_18() 19: eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) 20: if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) 21: if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) 22: if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) 23: if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() 24: or#(false(),z0) -> c_24() 25: or#(true(),z0) -> c_25() 26: reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) 27: reach#(z0,z1,empty(),z2) -> c_27() 28: union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) 29: union#(empty(),z0) -> c_29() ** Step 1.b:4: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) - Weak DPs: EQ#(0(),0()) -> c_1() EQ#(0(),s(z0)) -> c_2() EQ#(s(z0),0()) -> c_3() IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() OR#(false(),z0) -> c_10() OR#(true(),z0) -> c_11() REACH#(z0,z1,empty(),z2) -> c_13() UNION#(empty(),z0) -> c_15() eq#(0(),0()) -> c_16() eq#(0(),s(z0)) -> c_17() eq#(s(z0),0()) -> c_18() eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() or#(false(),z0) -> c_24() or#(true(),z0) -> c_25() reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) reach#(z0,z1,empty(),z2) -> c_27() union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) union#(empty(),z0) -> c_29() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/2,c_8/3,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) -->_1 EQ#(s(z0),0()) -> c_3():10 -->_1 EQ#(0(),s(z0)) -> c_2():9 -->_1 EQ#(0(),0()) -> c_1():8 -->_1 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 2:S:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 -->_1 REACH#(z0,z1,empty(),z2) -> c_13():14 3:S:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)):5 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)):4 -->_1 IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9():11 -->_2 EQ#(s(z0),0()) -> c_3():10 -->_2 EQ#(0(),s(z0)) -> c_2():9 -->_2 EQ#(0(),0()) -> c_1():8 -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 4:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) -->_2 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 -->_2 REACH#(z0,z1,empty(),z2) -> c_13():14 -->_1 OR#(true(),z0) -> c_11():13 -->_1 OR#(false(),z0) -> c_10():12 5:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) -->_3 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):7 -->_2 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)):6 -->_3 UNION#(empty(),z0) -> c_15():15 -->_2 REACH#(z0,z1,empty(),z2) -> c_13():14 -->_1 OR#(true(),z0) -> c_11():13 -->_1 OR#(false(),z0) -> c_10():12 6:S:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) -->_2 EQ#(s(z0),0()) -> c_3():10 -->_2 EQ#(0(),s(z0)) -> c_2():9 -->_2 EQ#(0(),0()) -> c_1():8 -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)):3 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):2 -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 7:S:UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) -->_1 UNION#(empty(),z0) -> c_15():15 -->_1 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):7 8:W:EQ#(0(),0()) -> c_1() 9:W:EQ#(0(),s(z0)) -> c_2() 10:W:EQ#(s(z0),0()) -> c_3() 11:W:IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() 12:W:OR#(false(),z0) -> c_10() 13:W:OR#(true(),z0) -> c_11() 14:W:REACH#(z0,z1,empty(),z2) -> c_13() 15:W:UNION#(empty(),z0) -> c_15() 16:W:eq#(0(),0()) -> c_16() 17:W:eq#(0(),s(z0)) -> c_17() 18:W:eq#(s(z0),0()) -> c_18() 19:W:eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) -->_1 eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)):19 -->_1 eq#(s(z0),0()) -> c_18():18 -->_1 eq#(0(),s(z0)) -> c_17():17 -->_1 eq#(0(),0()) -> c_16():16 20:W:if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) -->_1 reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)):26 -->_1 reach#(z0,z1,empty(),z2) -> c_27():27 21:W:if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) -->_1 if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))):22 -->_1 if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23():23 22:W:if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) -->_1 or#(true(),z0) -> c_25():25 -->_1 or#(false(),z0) -> c_24():24 23:W:if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() 24:W:or#(false(),z0) -> c_24() 25:W:or#(true(),z0) -> c_25() 26:W:reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) -->_1 if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3) ,z0 ,z1 ,edge(z2,z3,z4) ,z5)):21 -->_1 if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))):20 27:W:reach#(z0,z1,empty(),z2) -> c_27() 28:W:union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) -->_1 union#(empty(),z0) -> c_29():29 -->_1 union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)):28 29:W:union#(empty(),z0) -> c_29() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 28: union#(edge(z0,z1,z2),z3) -> c_28(union#(z2,z3)) 29: union#(empty(),z0) -> c_29() 20: if_reach_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_20(reach#(z0,z1,z4,edge(z2,z3,z5))) 26: reach#(z0,z1,edge(z2,z3,z4),z5) -> c_26(if_reach_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) 27: reach#(z0,z1,empty(),z2) -> c_27() 21: if_reach_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_21(if_reach_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) 23: if_reach_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_23() 22: if_reach_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_22(or#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty()))) 24: or#(false(),z0) -> c_24() 25: or#(true(),z0) -> c_25() 19: eq#(s(z0),s(z1)) -> c_19(eq#(z0,z1)) 18: eq#(s(z0),0()) -> c_18() 17: eq#(0(),s(z0)) -> c_17() 16: eq#(0(),0()) -> c_16() 11: IF_REACH_2#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_9() 12: OR#(false(),z0) -> c_10() 13: OR#(true(),z0) -> c_11() 14: REACH#(z0,z1,empty(),z2) -> c_13() 15: UNION#(empty(),z0) -> c_15() 8: EQ#(0(),0()) -> c_1() 9: EQ#(0(),s(z0)) -> c_2() 10: EQ#(s(z0),0()) -> c_3() ** Step 1.b:5: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/2,c_8/3,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) -->_1 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 2:S:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 3:S:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)):5 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)):4 -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 4:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z0,z1,z4,z5)) -->_2 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 5:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(OR#(reach(z0,z1,z4,z5) ,reach(z3,z1,union(z4,z5),empty())) ,REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)) -->_3 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):7 -->_2 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)):6 6:S:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)):3 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):2 -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 7:S:UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) -->_1 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):7 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) ** Step 1.b:6: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) if_reach_1(false(),z0,z1,edge(z2,z3,z4),z5) -> reach(z0,z1,z4,edge(z2,z3,z5)) if_reach_1(true(),z0,z1,edge(z2,z3,z4),z5) -> if_reach_2(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) if_reach_2(false(),z0,z1,edge(z2,z3,z4),z5) -> or(reach(z0,z1,z4,z5),reach(z3,z1,union(z4,z5),empty())) if_reach_2(true(),z0,z1,edge(z2,z3,z4),z5) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,edge(z2,z3,z4),z5) -> if_reach_1(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) reach(z0,z1,empty(),z2) -> false() union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + 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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) ** Step 1.b:7: Decompose. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) - Weak DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2 ,reach#/4,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2 ,edge/3,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0 ,c_12/2,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1 ,c_27/0,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} Problem (S) - Strict DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) - Weak DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2 ,reach#/4,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2 ,edge/3,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0 ,c_12/2,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1 ,c_27/0,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} *** Step 1.b:7.a:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) - Weak DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) -->_1 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 2:W:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 3:W:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)):5 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)):4 4:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 5:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) -->_2 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):7 -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)):6 6:W:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):2 -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)):3 7:W:UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) -->_1 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) *** Step 1.b:7.a:2: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) - Weak DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) -->_1 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 2:W:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 3:W:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)):5 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)):4 4:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 5:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 6:W:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):2 -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())) *** Step 1.b:7.a:3: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) - Weak DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) The strictly oriented rules are moved into the weak component. **** Step 1.b:7.a:3.a:1: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) - Weak DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_12) = {1,2} Following symbols are considered usable: {union,EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq#,if_reach_1#,if_reach_2#,or#,reach#,union#} TcT has computed the following interpretation: p(0) = 1 p(EQ) = x1*x2 + 2*x2 p(IF_REACH_1) = 2 + x1*x3 + x2 + 2*x2*x5 + x5 + 2*x5^2 p(IF_REACH_2) = 2*x2 + 2*x5 + x5^2 p(OR) = 2*x1 + x1^2 + x2 p(REACH) = x1*x4 + 2*x1^2 + 2*x4 + 2*x4^2 p(UNION) = x2 + 2*x2^2 p(c) = 2 p(c1) = 0 p(c10) = 0 p(c11) = 2 p(c12) = 2 p(c13) = 0 p(c14) = 0 p(c2) = 0 p(c3) = 0 p(c4) = 0 p(c5) = 0 p(c6) = 0 p(c7) = 2 + x1 p(c8) = 0 p(c9) = 0 p(edge) = 1 + x2 + x3 p(empty) = 0 p(eq) = 0 p(false) = 0 p(if_reach_1) = 1 + x1 + 2*x1*x3 + x1^2 + 2*x2 + 2*x2*x3 + x2*x5 + x2^2 + 2*x3 + x3*x4 + x3^2 + x4 + 2*x4*x5 p(if_reach_2) = x1^2 + x2*x4 + 2*x2*x5 + x3^2 + x4 + 2*x5 p(or) = x1*x2 + 2*x1^2 + 2*x2^2 p(reach) = 2*x1 + 2*x1*x2 + x1*x4 + x1^2 + 2*x2*x3 + 2*x3 + 2*x3^2 p(s) = 2 + x1 p(true) = 1 p(union) = x1 + x2 p(EQ#) = x1 p(IF_REACH_1#) = x2*x4 + 2*x3 + 2*x3*x4 + 2*x3*x5 + 2*x4*x5 + x4^2 + x5^2 p(IF_REACH_2#) = x2*x4 + 2*x3*x4 + 2*x3*x5 + 2*x4*x5 + x4^2 + x5^2 p(OR#) = x1^2 + 2*x2 p(REACH#) = x1 + x1*x3 + 2*x2 + 2*x2*x3 + 2*x2*x4 + 2*x3*x4 + x3^2 + x4^2 p(UNION#) = 2 + x1 + 2*x1*x2 p(eq#) = 1 + 2*x1*x2 + 2*x2 p(if_reach_1#) = x2 + x2*x3 + 2*x2*x5 + 2*x2^2 + 2*x3 + x4 p(if_reach_2#) = 1 + x1 + x3 + 2*x3*x4 + 2*x3*x5 + x3^2 + x5 + 2*x5^2 p(or#) = 2 + 2*x1 p(reach#) = x2^2 + 2*x4 p(union#) = x1^2 p(c_1) = 0 p(c_2) = 2 p(c_3) = 0 p(c_4) = x1 p(c_5) = x1 p(c_6) = x1 + x2 p(c_7) = 1 + x1 p(c_8) = x1 p(c_9) = 2 p(c_10) = 0 p(c_11) = 0 p(c_12) = x1 + x2 p(c_13) = 0 p(c_14) = 1 p(c_15) = 0 p(c_16) = 2 p(c_17) = 0 p(c_18) = 1 p(c_19) = 0 p(c_20) = 0 p(c_21) = 1 p(c_22) = 0 p(c_23) = 2 p(c_24) = 2 p(c_25) = 0 p(c_26) = 2 p(c_27) = 0 p(c_28) = 0 p(c_29) = 1 Following rules are strictly oriented: EQ#(s(z0),s(z1)) = 2 + z0 > z0 = c_4(EQ#(z0,z1)) Following rules are (at-least) weakly oriented: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) = 1 + z0 + z0*z3 + z0*z4 + 4*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 >= 1 + z0 + z0*z4 + 4*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 = c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) = 1 + z0 + z0*z3 + z0*z4 + 4*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 >= 1 + z0 + z0*z3 + z0*z4 + 3*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 = c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5),EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) = 1 + z0 + z0*z3 + z0*z4 + 2*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 >= 1 + z0 + z0*z4 + 2*z1 + 2*z1*z4 + 2*z1*z5 + 2*z4*z5 + z4^2 + z5^2 = c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) = 1 + z0 + z0*z3 + z0*z4 + 2*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 >= 2*z1 + 2*z1*z4 + 2*z1*z5 + z3 + z3*z4 + z3*z5 + 2*z4*z5 + z4^2 + z5^2 = c_8(REACH#(z3,z1,union(z4,z5),empty())) REACH#(z0,z1,edge(z2,z3,z4),z5) = 1 + 2*z0 + z0*z3 + z0*z4 + 4*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 >= 1 + 2*z0 + z0*z3 + z0*z4 + 4*z1 + 2*z1*z3 + 2*z1*z4 + 2*z1*z5 + 2*z3 + 2*z3*z4 + 2*z3*z5 + z3^2 + 2*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 = c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) union(edge(z0,z1,z2),z3) = 1 + z1 + z2 + z3 >= 1 + z1 + z2 + z3 = edge(z0,z1,union(z2,z3)) union(empty(),z0) = z0 >= z0 = z0 **** Step 1.b:7.a:3.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () **** Step 1.b:7.a:3.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) -->_1 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 2:W:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 3:W:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())):5 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)):4 -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 4:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 5:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):6 6:W:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)):3 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):2 -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) 6: REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) 5: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty())) 3: IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) 4: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) 1: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) **** Step 1.b:7.a:3.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + 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^2)) + Considered Problem: - Strict DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) - Weak DPs: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):5 2:S:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):7 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)):4 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)):3 3:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):5 4:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) -->_2 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):6 -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)):5 5:S:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) -->_2 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):7 -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)):2 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):1 6:S:UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) -->_1 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):6 7:W:EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) -->_1 EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)):7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: EQ#(s(z0),s(z1)) -> c_4(EQ#(z0,z1)) *** Step 1.b:7.b:2: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):5 2:S:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)) -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)):4 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)):3 3:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z0,z2)):5 4:S:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) -->_2 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):6 -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)):5 5:S:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5),EQ#(z0,z2)) -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5) ,EQ#(z1,z3)):2 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):1 6:S:UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) -->_1 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) *** Step 1.b:7.b:3: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) 3: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) 5: REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) 6: UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) Consider the set of all dependency pairs 1: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) 2: IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) 3: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) 4: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) 5: REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) 6: UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) BEST_CASE TIME (?,?) SPACE(?,?)on application of the dependency pairs {1,3,5,6} These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 1.b:7.b:3.a:1: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1,2}, uargs(c_12) = {1}, uargs(c_14) = {1} Following symbols are considered usable: {eq,union,EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq#,if_reach_1#,if_reach_2#,or#,reach#,union#} TcT has computed the following interpretation: p(0) = 0 p(EQ) = 2 + 2*x2 p(IF_REACH_1) = 1 + x1 + x1*x4 + x2*x3 + 2*x2*x4 + x2^2 + x3*x4 + x4^2 p(IF_REACH_2) = x1*x3 + 2*x1^2 + x2 + 2*x2*x3 + x3*x5 + x3^2 + 2*x4^2 p(OR) = 0 p(REACH) = 2 + x1 + x1^2 + x2 + 2*x3^2 p(UNION) = 2*x1*x2 + 2*x2 + x2^2 p(c) = 2 p(c1) = 1 p(c10) = 2 + x1 p(c11) = 0 p(c12) = 1 p(c13) = 2 p(c14) = 1 + x1 + x2 p(c2) = 1 p(c3) = 1 p(c4) = 2 p(c5) = 0 p(c6) = 0 p(c7) = 0 p(c8) = 2 p(c9) = x1 p(edge) = 1 + x1 + x3 p(empty) = 0 p(eq) = 1 p(false) = 1 p(if_reach_1) = x1 + 2*x1*x3 + 2*x1^2 + x2 + x2*x4 + 2*x2^2 + 2*x3 + x3*x4 + x3*x5 + 2*x4*x5 + 2*x5^2 p(if_reach_2) = 2*x1 + x1*x4 + x2*x3 + x3^2 + x4 + 2*x5 + x5^2 p(or) = 1 + 2*x1 + x2 + 2*x2^2 p(reach) = 1 + x1 + 2*x1*x4 + x1^2 + 2*x2 + 2*x2*x3 + x2^2 + 2*x4^2 p(s) = 2 p(true) = 1 p(union) = x1 + x2 p(EQ#) = 2 + 2*x1^2 p(IF_REACH_1#) = x1*x3 + 2*x1*x4 + x3 + 2*x4*x5 + x4^2 + x5^2 p(IF_REACH_2#) = 1 + 2*x3 + x4 + 2*x4*x5 + x4^2 + x5^2 p(OR#) = x1^2 p(REACH#) = 1 + 2*x2 + 2*x3 + 2*x3*x4 + x3^2 + x4^2 p(UNION#) = x1 p(eq#) = 2*x2 + 2*x2^2 p(if_reach_1#) = 2*x1 + x1*x4 + 2*x1*x5 + 2*x3*x4 + x3*x5 + x5 + 2*x5^2 p(if_reach_2#) = 1 + 2*x1 + x1*x2 + 2*x1*x4 + 2*x1^2 + 2*x4^2 p(or#) = 0 p(reach#) = 1 + 2*x1*x2 + x1*x3 + 2*x1^2 + 2*x2 + x2*x3 + 2*x4 p(union#) = x1 + 2*x1*x2 + x2 + 2*x2^2 p(c_1) = 0 p(c_2) = 1 p(c_3) = 0 p(c_4) = 2 + x1 p(c_5) = x1 p(c_6) = x1 p(c_7) = 1 + x1 p(c_8) = 2 + x1 + x2 p(c_9) = 1 p(c_10) = 0 p(c_11) = 1 p(c_12) = x1 p(c_13) = 1 p(c_14) = x1 p(c_15) = 1 p(c_16) = 2 p(c_17) = 1 p(c_18) = 0 p(c_19) = 0 p(c_20) = x1 p(c_21) = 1 p(c_22) = x1 p(c_23) = 0 p(c_24) = 0 p(c_25) = 0 p(c_26) = 1 p(c_27) = 2 p(c_28) = 1 p(c_29) = 0 Following rules are strictly oriented: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) = 3 + 2*z1 + 4*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 4*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 > 2 + 2*z1 + 2*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 4*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 = c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) = 3 + 2*z1 + 3*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 3*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 > 2 + 2*z1 + 2*z4 + 2*z4*z5 + z4^2 + z5^2 = c_7(REACH#(z0,z1,z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) = 4 + 2*z1 + 4*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 4*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 > 3 + 2*z1 + 4*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 4*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 = c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) UNION#(edge(z0,z1,z2),z3) = 1 + z0 + z2 > z2 = c_14(UNION#(z2,z3)) Following rules are (at-least) weakly oriented: IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) = 3 + 2*z1 + 4*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 4*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 >= 3 + 2*z1 + 3*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 3*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 = c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) = 3 + 2*z1 + 3*z2 + 2*z2*z4 + 2*z2*z5 + z2^2 + 3*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 >= 3 + 2*z1 + 3*z4 + 2*z4*z5 + z4^2 + 2*z5 + z5^2 = c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) eq(0(),0()) = 1 >= 1 = true() eq(0(),s(z0)) = 1 >= 1 = false() eq(s(z0),0()) = 1 >= 1 = false() eq(s(z0),s(z1)) = 1 >= 1 = eq(z0,z1) union(edge(z0,z1,z2),z3) = 1 + z0 + z2 + z3 >= 1 + z0 + z2 + z3 = edge(z0,z1,union(z2,z3)) union(empty(),z0) = z0 >= z0 = z0 **** Step 1.b:7.b:3.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) - Weak DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () **** Step 1.b:7.b:3.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,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) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)):5 2:W:IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()) ,UNION#(z4,z5)):4 -->_1 IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)):3 3:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)):5 4:W:IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) -->_2 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):6 -->_1 REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)):5 5:W:REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) -->_1 IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3) ,z0 ,z1 ,edge(z2,z3,z4) ,z5)):2 -->_1 IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))):1 6:W:UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) -->_1 UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: IF_REACH_1#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_5(REACH#(z0,z1,z4,edge(z2,z3,z5))) 5: REACH#(z0,z1,edge(z2,z3,z4),z5) -> c_12(IF_REACH_1#(eq(z0,z2),z0,z1,edge(z2,z3,z4),z5)) 4: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_8(REACH#(z3,z1,union(z4,z5),empty()),UNION#(z4,z5)) 2: IF_REACH_1#(true(),z0,z1,edge(z2,z3,z4),z5) -> c_6(IF_REACH_2#(eq(z1,z3),z0,z1,edge(z2,z3,z4),z5)) 3: IF_REACH_2#(false(),z0,z1,edge(z2,z3,z4),z5) -> c_7(REACH#(z0,z1,z4,z5)) 6: UNION#(edge(z0,z1,z2),z3) -> c_14(UNION#(z2,z3)) **** Step 1.b:7.b:3.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,IF_REACH_1/5,IF_REACH_2/5,OR/2,REACH/4,UNION/2,eq/2,if_reach_1/5,if_reach_2/5,or/2,reach/4,union/2 ,EQ#/2,IF_REACH_1#/5,IF_REACH_2#/5,OR#/2,REACH#/4,UNION#/2,eq#/2,if_reach_1#/5,if_reach_2#/5,or#/2,reach#/4 ,union#/2} / {0/0,c/0,c1/0,c10/2,c11/1,c12/0,c13/2,c14/3,c2/0,c3/1,c4/0,c5/0,c6/0,c7/1,c8/0,c9/2,edge/3 ,empty/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1 ,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0 ,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ#,IF_REACH_1#,IF_REACH_2#,OR#,REACH#,UNION#,eq# ,if_reach_1#,if_reach_2#,or#,reach#,union#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7 ,c8,c9,edge,empty,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))