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