MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) from(edge(x,y,i)) -> x if1(false(),b1,b2,b3,x,y,i,h) -> if2(b1,b2,b3,x,y,i,h) if1(true(),b1,b2,b3,x,y,i,h) -> true() if2(false(),b2,b3,x,y,i,h) -> if3(b2,b3,x,y,i,h) if2(true(),b2,b3,x,y,i,h) -> false() if3(false(),b3,x,y,i,h) -> reach(x,y,rest(i),edge(from(i),to(i),h)) if3(true(),b3,x,y,i,h) -> if4(b3,x,y,i,h) if4(false(),x,y,i,h) -> or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) if4(true(),x,y,i,h) -> true() isEmpty(edge(x,y,i)) -> false() isEmpty(empty()) -> true() or(false(),y) -> y or(true(),y) -> true() reach(x,y,i,h) -> if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) rest(edge(x,y,i)) -> i rest(empty()) -> empty() to(edge(x,y,i)) -> y union(edge(x,y,i),h) -> edge(x,y,union(i,h)) union(empty(),h) -> h - Signature: {eq/2,from/1,if1/8,if2/7,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2} / {0/0,edge/3,empty/0 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq,from,if1,if2,if3,if4,isEmpty,or,reach,rest,to ,union} and constructors {0,edge,empty,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs eq#(0(),0()) -> c_1() eq#(0(),s(x)) -> c_2() eq#(s(x),0()) -> c_3() eq#(s(x),s(y)) -> c_4(eq#(x,y)) from#(edge(x,y,i)) -> c_5() if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) if1#(true(),b1,b2,b3,x,y,i,h) -> c_7() if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) if2#(true(),b2,b3,x,y,i,h) -> c_9() if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)),rest#(i),from#(i),to#(i)) if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)) if4#(true(),x,y,i,h) -> c_13() isEmpty#(edge(x,y,i)) -> c_14() isEmpty#(empty()) -> c_15() or#(false(),y) -> c_16() or#(true(),y) -> c_17() reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)) rest#(edge(x,y,i)) -> c_19() rest#(empty()) -> c_20() to#(edge(x,y,i)) -> c_21() union#(edge(x,y,i),h) -> c_22(union#(i,h)) union#(empty(),h) -> c_23() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: eq#(0(),0()) -> c_1() eq#(0(),s(x)) -> c_2() eq#(s(x),0()) -> c_3() eq#(s(x),s(y)) -> c_4(eq#(x,y)) from#(edge(x,y,i)) -> c_5() if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) if1#(true(),b1,b2,b3,x,y,i,h) -> c_7() if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) if2#(true(),b2,b3,x,y,i,h) -> c_9() if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)),rest#(i),from#(i),to#(i)) if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)) if4#(true(),x,y,i,h) -> c_13() isEmpty#(edge(x,y,i)) -> c_14() isEmpty#(empty()) -> c_15() or#(false(),y) -> c_16() or#(true(),y) -> c_17() reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)) rest#(edge(x,y,i)) -> c_19() rest#(empty()) -> c_20() to#(edge(x,y,i)) -> c_21() union#(edge(x,y,i),h) -> c_22(union#(i,h)) union#(empty(),h) -> c_23() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) from(edge(x,y,i)) -> x if1(false(),b1,b2,b3,x,y,i,h) -> if2(b1,b2,b3,x,y,i,h) if1(true(),b1,b2,b3,x,y,i,h) -> true() if2(false(),b2,b3,x,y,i,h) -> if3(b2,b3,x,y,i,h) if2(true(),b2,b3,x,y,i,h) -> false() if3(false(),b3,x,y,i,h) -> reach(x,y,rest(i),edge(from(i),to(i),h)) if3(true(),b3,x,y,i,h) -> if4(b3,x,y,i,h) if4(false(),x,y,i,h) -> or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) if4(true(),x,y,i,h) -> true() isEmpty(edge(x,y,i)) -> false() isEmpty(empty()) -> true() or(false(),y) -> y or(true(),y) -> true() reach(x,y,i,h) -> if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) rest(edge(x,y,i)) -> i rest(empty()) -> empty() to(edge(x,y,i)) -> y union(edge(x,y,i),h) -> edge(x,y,union(i,h)) union(empty(),h) -> h - Signature: {eq/2,from/1,if1/8,if2/7,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2,eq#/2,from#/1,if1#/8,if2#/7 ,if3#/6,if4#/5,isEmpty#/1,or#/2,reach#/4,rest#/1,to#/1,union#/2} / {0/0,edge/3,empty/0,false/0,s/1,true/0 ,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/4,c_11/1,c_12/7,c_13/0,c_14/0,c_15/0,c_16/0 ,c_17/0,c_18/7,c_19/0,c_20/0,c_21/0,c_22/1,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,from#,if1#,if2#,if3#,if4#,isEmpty#,or#,reach#,rest# ,to#,union#} and constructors {0,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,5,7,9,13,14,15,16,17,19,20,21,23} by application of Pre({1,2,3,5,7,9,13,14,15,16,17,19,20,21,23}) = {4,6,10,11,12,18,22}. Here rules are labelled as follows: 1: eq#(0(),0()) -> c_1() 2: eq#(0(),s(x)) -> c_2() 3: eq#(s(x),0()) -> c_3() 4: eq#(s(x),s(y)) -> c_4(eq#(x,y)) 5: from#(edge(x,y,i)) -> c_5() 6: if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) 7: if1#(true(),b1,b2,b3,x,y,i,h) -> c_7() 8: if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) 9: if2#(true(),b2,b3,x,y,i,h) -> c_9() 10: if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)),rest#(i),from#(i),to#(i)) 11: if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) 12: if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)) 13: if4#(true(),x,y,i,h) -> c_13() 14: isEmpty#(edge(x,y,i)) -> c_14() 15: isEmpty#(empty()) -> c_15() 16: or#(false(),y) -> c_16() 17: or#(true(),y) -> c_17() 18: reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)) 19: rest#(edge(x,y,i)) -> c_19() 20: rest#(empty()) -> c_20() 21: to#(edge(x,y,i)) -> c_21() 22: union#(edge(x,y,i),h) -> c_22(union#(i,h)) 23: union#(empty(),h) -> c_23() * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_4(eq#(x,y)) if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)),rest#(i),from#(i),to#(i)) if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)) reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)) union#(edge(x,y,i),h) -> c_22(union#(i,h)) - Weak DPs: eq#(0(),0()) -> c_1() eq#(0(),s(x)) -> c_2() eq#(s(x),0()) -> c_3() from#(edge(x,y,i)) -> c_5() if1#(true(),b1,b2,b3,x,y,i,h) -> c_7() if2#(true(),b2,b3,x,y,i,h) -> c_9() if4#(true(),x,y,i,h) -> c_13() isEmpty#(edge(x,y,i)) -> c_14() isEmpty#(empty()) -> c_15() or#(false(),y) -> c_16() or#(true(),y) -> c_17() rest#(edge(x,y,i)) -> c_19() rest#(empty()) -> c_20() to#(edge(x,y,i)) -> c_21() union#(empty(),h) -> c_23() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) from(edge(x,y,i)) -> x if1(false(),b1,b2,b3,x,y,i,h) -> if2(b1,b2,b3,x,y,i,h) if1(true(),b1,b2,b3,x,y,i,h) -> true() if2(false(),b2,b3,x,y,i,h) -> if3(b2,b3,x,y,i,h) if2(true(),b2,b3,x,y,i,h) -> false() if3(false(),b3,x,y,i,h) -> reach(x,y,rest(i),edge(from(i),to(i),h)) if3(true(),b3,x,y,i,h) -> if4(b3,x,y,i,h) if4(false(),x,y,i,h) -> or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) if4(true(),x,y,i,h) -> true() isEmpty(edge(x,y,i)) -> false() isEmpty(empty()) -> true() or(false(),y) -> y or(true(),y) -> true() reach(x,y,i,h) -> if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) rest(edge(x,y,i)) -> i rest(empty()) -> empty() to(edge(x,y,i)) -> y union(edge(x,y,i),h) -> edge(x,y,union(i,h)) union(empty(),h) -> h - Signature: {eq/2,from/1,if1/8,if2/7,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2,eq#/2,from#/1,if1#/8,if2#/7 ,if3#/6,if4#/5,isEmpty#/1,or#/2,reach#/4,rest#/1,to#/1,union#/2} / {0/0,edge/3,empty/0,false/0,s/1,true/0 ,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/4,c_11/1,c_12/7,c_13/0,c_14/0,c_15/0,c_16/0 ,c_17/0,c_18/7,c_19/0,c_20/0,c_21/0,c_22/1,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,from#,if1#,if2#,if3#,if4#,isEmpty#,or#,reach#,rest# ,to#,union#} and constructors {0,edge,empty,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eq#(s(x),s(y)) -> c_4(eq#(x,y)) -->_1 eq#(s(x),0()) -> c_3():11 -->_1 eq#(0(),s(x)) -> c_2():10 -->_1 eq#(0(),0()) -> c_1():9 -->_1 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 2:S:if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) -->_1 if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)):3 -->_1 if2#(true(),b2,b3,x,y,i,h) -> c_9():14 3:S:if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) -->_1 if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)):5 -->_1 if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)) ,rest#(i) ,from#(i) ,to#(i)):4 4:S:if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)),rest#(i),from#(i),to#(i)) -->_1 reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)):7 -->_4 to#(edge(x,y,i)) -> c_21():22 -->_2 rest#(empty()) -> c_20():21 -->_2 rest#(edge(x,y,i)) -> c_19():20 -->_3 from#(edge(x,y,i)) -> c_5():12 5:S:if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) -->_1 if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)):6 -->_1 if4#(true(),x,y,i,h) -> c_13():15 6:S:if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)) -->_6 union#(edge(x,y,i),h) -> c_22(union#(i,h)):8 -->_4 reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)):7 -->_2 reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)):7 -->_6 union#(empty(),h) -> c_23():23 -->_5 to#(edge(x,y,i)) -> c_21():22 -->_7 rest#(empty()) -> c_20():21 -->_3 rest#(empty()) -> c_20():21 -->_7 rest#(edge(x,y,i)) -> c_19():20 -->_3 rest#(edge(x,y,i)) -> c_19():20 -->_1 or#(true(),y) -> c_17():19 -->_1 or#(false(),y) -> c_16():18 7:S:reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)) -->_7 to#(edge(x,y,i)) -> c_21():22 -->_3 isEmpty#(empty()) -> c_15():17 -->_3 isEmpty#(edge(x,y,i)) -> c_14():16 -->_1 if1#(true(),b1,b2,b3,x,y,i,h) -> c_7():13 -->_5 from#(edge(x,y,i)) -> c_5():12 -->_6 eq#(s(x),0()) -> c_3():11 -->_4 eq#(s(x),0()) -> c_3():11 -->_2 eq#(s(x),0()) -> c_3():11 -->_6 eq#(0(),s(x)) -> c_2():10 -->_4 eq#(0(),s(x)) -> c_2():10 -->_2 eq#(0(),s(x)) -> c_2():10 -->_6 eq#(0(),0()) -> c_1():9 -->_4 eq#(0(),0()) -> c_1():9 -->_2 eq#(0(),0()) -> c_1():9 -->_1 if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)):2 -->_6 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 -->_4 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 -->_2 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 8:S:union#(edge(x,y,i),h) -> c_22(union#(i,h)) -->_1 union#(empty(),h) -> c_23():23 -->_1 union#(edge(x,y,i),h) -> c_22(union#(i,h)):8 9:W:eq#(0(),0()) -> c_1() 10:W:eq#(0(),s(x)) -> c_2() 11:W:eq#(s(x),0()) -> c_3() 12:W:from#(edge(x,y,i)) -> c_5() 13:W:if1#(true(),b1,b2,b3,x,y,i,h) -> c_7() 14:W:if2#(true(),b2,b3,x,y,i,h) -> c_9() 15:W:if4#(true(),x,y,i,h) -> c_13() 16:W:isEmpty#(edge(x,y,i)) -> c_14() 17:W:isEmpty#(empty()) -> c_15() 18:W:or#(false(),y) -> c_16() 19:W:or#(true(),y) -> c_17() 20:W:rest#(edge(x,y,i)) -> c_19() 21:W:rest#(empty()) -> c_20() 22:W:to#(edge(x,y,i)) -> c_21() 23:W:union#(empty(),h) -> c_23() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: if2#(true(),b2,b3,x,y,i,h) -> c_9() 15: if4#(true(),x,y,i,h) -> c_13() 18: or#(false(),y) -> c_16() 19: or#(true(),y) -> c_17() 20: rest#(edge(x,y,i)) -> c_19() 21: rest#(empty()) -> c_20() 12: from#(edge(x,y,i)) -> c_5() 13: if1#(true(),b1,b2,b3,x,y,i,h) -> c_7() 16: isEmpty#(edge(x,y,i)) -> c_14() 17: isEmpty#(empty()) -> c_15() 22: to#(edge(x,y,i)) -> c_21() 23: union#(empty(),h) -> c_23() 9: eq#(0(),0()) -> c_1() 10: eq#(0(),s(x)) -> c_2() 11: eq#(s(x),0()) -> c_3() * Step 4: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_4(eq#(x,y)) if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)),rest#(i),from#(i),to#(i)) if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)) reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)) union#(edge(x,y,i),h) -> c_22(union#(i,h)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) from(edge(x,y,i)) -> x if1(false(),b1,b2,b3,x,y,i,h) -> if2(b1,b2,b3,x,y,i,h) if1(true(),b1,b2,b3,x,y,i,h) -> true() if2(false(),b2,b3,x,y,i,h) -> if3(b2,b3,x,y,i,h) if2(true(),b2,b3,x,y,i,h) -> false() if3(false(),b3,x,y,i,h) -> reach(x,y,rest(i),edge(from(i),to(i),h)) if3(true(),b3,x,y,i,h) -> if4(b3,x,y,i,h) if4(false(),x,y,i,h) -> or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) if4(true(),x,y,i,h) -> true() isEmpty(edge(x,y,i)) -> false() isEmpty(empty()) -> true() or(false(),y) -> y or(true(),y) -> true() reach(x,y,i,h) -> if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) rest(edge(x,y,i)) -> i rest(empty()) -> empty() to(edge(x,y,i)) -> y union(edge(x,y,i),h) -> edge(x,y,union(i,h)) union(empty(),h) -> h - Signature: {eq/2,from/1,if1/8,if2/7,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2,eq#/2,from#/1,if1#/8,if2#/7 ,if3#/6,if4#/5,isEmpty#/1,or#/2,reach#/4,rest#/1,to#/1,union#/2} / {0/0,edge/3,empty/0,false/0,s/1,true/0 ,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/4,c_11/1,c_12/7,c_13/0,c_14/0,c_15/0,c_16/0 ,c_17/0,c_18/7,c_19/0,c_20/0,c_21/0,c_22/1,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,from#,if1#,if2#,if3#,if4#,isEmpty#,or#,reach#,rest# ,to#,union#} and constructors {0,edge,empty,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:eq#(s(x),s(y)) -> c_4(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 2:S:if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) -->_1 if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)):3 3:S:if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) -->_1 if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)):5 -->_1 if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)) ,rest#(i) ,from#(i) ,to#(i)):4 4:S:if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h)),rest#(i),from#(i),to#(i)) -->_1 reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)):7 5:S:if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) -->_1 if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)):6 6:S:if4#(false(),x,y,i,h) -> c_12(or#(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) ,reach#(x,y,rest(i),h) ,rest#(i) ,reach#(to(i),y,union(rest(i),h),empty()) ,to#(i) ,union#(rest(i),h) ,rest#(i)) -->_6 union#(edge(x,y,i),h) -> c_22(union#(i,h)):8 -->_4 reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)):7 -->_2 reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)):7 7:S:reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,isEmpty#(i) ,eq#(x,from(i)) ,from#(i) ,eq#(y,to(i)) ,to#(i)) -->_1 if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)):2 -->_6 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 -->_4 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 -->_2 eq#(s(x),s(y)) -> c_4(eq#(x,y)):1 8:S:union#(edge(x,y,i),h) -> c_22(union#(i,h)) -->_1 union#(edge(x,y,i),h) -> c_22(union#(i,h)):8 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h))) if4#(false(),x,y,i,h) -> c_12(reach#(x,y,rest(i),h) ,reach#(to(i),y,union(rest(i),h),empty()) ,union#(rest(i),h)) reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,eq#(x,from(i)) ,eq#(y,to(i))) * Step 5: UsableRules MAYBE + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_4(eq#(x,y)) if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h))) if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) if4#(false(),x,y,i,h) -> c_12(reach#(x,y,rest(i),h) ,reach#(to(i),y,union(rest(i),h),empty()) ,union#(rest(i),h)) reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,eq#(x,from(i)) ,eq#(y,to(i))) union#(edge(x,y,i),h) -> c_22(union#(i,h)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) from(edge(x,y,i)) -> x if1(false(),b1,b2,b3,x,y,i,h) -> if2(b1,b2,b3,x,y,i,h) if1(true(),b1,b2,b3,x,y,i,h) -> true() if2(false(),b2,b3,x,y,i,h) -> if3(b2,b3,x,y,i,h) if2(true(),b2,b3,x,y,i,h) -> false() if3(false(),b3,x,y,i,h) -> reach(x,y,rest(i),edge(from(i),to(i),h)) if3(true(),b3,x,y,i,h) -> if4(b3,x,y,i,h) if4(false(),x,y,i,h) -> or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty())) if4(true(),x,y,i,h) -> true() isEmpty(edge(x,y,i)) -> false() isEmpty(empty()) -> true() or(false(),y) -> y or(true(),y) -> true() reach(x,y,i,h) -> if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) rest(edge(x,y,i)) -> i rest(empty()) -> empty() to(edge(x,y,i)) -> y union(edge(x,y,i),h) -> edge(x,y,union(i,h)) union(empty(),h) -> h - Signature: {eq/2,from/1,if1/8,if2/7,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2,eq#/2,from#/1,if1#/8,if2#/7 ,if3#/6,if4#/5,isEmpty#/1,or#/2,reach#/4,rest#/1,to#/1,union#/2} / {0/0,edge/3,empty/0,false/0,s/1,true/0 ,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/3,c_13/0,c_14/0,c_15/0,c_16/0 ,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0,c_22/1,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,from#,if1#,if2#,if3#,if4#,isEmpty#,or#,reach#,rest# ,to#,union#} and constructors {0,edge,empty,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) from(edge(x,y,i)) -> x isEmpty(edge(x,y,i)) -> false() isEmpty(empty()) -> true() rest(edge(x,y,i)) -> i rest(empty()) -> empty() to(edge(x,y,i)) -> y union(edge(x,y,i),h) -> edge(x,y,union(i,h)) union(empty(),h) -> h eq#(s(x),s(y)) -> c_4(eq#(x,y)) if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h))) if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) if4#(false(),x,y,i,h) -> c_12(reach#(x,y,rest(i),h) ,reach#(to(i),y,union(rest(i),h),empty()) ,union#(rest(i),h)) reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,eq#(x,from(i)) ,eq#(y,to(i))) union#(edge(x,y,i),h) -> c_22(union#(i,h)) * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_4(eq#(x,y)) if1#(false(),b1,b2,b3,x,y,i,h) -> c_6(if2#(b1,b2,b3,x,y,i,h)) if2#(false(),b2,b3,x,y,i,h) -> c_8(if3#(b2,b3,x,y,i,h)) if3#(false(),b3,x,y,i,h) -> c_10(reach#(x,y,rest(i),edge(from(i),to(i),h))) if3#(true(),b3,x,y,i,h) -> c_11(if4#(b3,x,y,i,h)) if4#(false(),x,y,i,h) -> c_12(reach#(x,y,rest(i),h) ,reach#(to(i),y,union(rest(i),h),empty()) ,union#(rest(i),h)) reach#(x,y,i,h) -> c_18(if1#(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ,eq#(x,y) ,eq#(x,from(i)) ,eq#(y,to(i))) union#(edge(x,y,i),h) -> c_22(union#(i,h)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) from(edge(x,y,i)) -> x isEmpty(edge(x,y,i)) -> false() isEmpty(empty()) -> true() rest(edge(x,y,i)) -> i rest(empty()) -> empty() to(edge(x,y,i)) -> y union(edge(x,y,i),h) -> edge(x,y,union(i,h)) union(empty(),h) -> h - Signature: {eq/2,from/1,if1/8,if2/7,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2,eq#/2,from#/1,if1#/8,if2#/7 ,if3#/6,if4#/5,isEmpty#/1,or#/2,reach#/4,rest#/1,to#/1,union#/2} / {0/0,edge/3,empty/0,false/0,s/1,true/0 ,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/3,c_13/0,c_14/0,c_15/0,c_16/0 ,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0,c_22/1,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,from#,if1#,if2#,if3#,if4#,isEmpty#,or#,reach#,rest# ,to#,union#} and constructors {0,edge,empty,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE