MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) getNodeFromEdge(0(),E(x,y)) -> x getNodeFromEdge(S(0()),E(x,y)) -> x getNodeFromEdge(S(S(x')),E(x,y)) -> y goal(u,v,edges) -> reach(u,v,edges) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5} / {0/0,Cons/2,E/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,and,eqEdge,eqEdge[Ite],getNodeFromEdge,goal,member ,member[Ite],notEmpty,reach,reach[Ite],via,via[Ite],via[Let]} and constructors {0,Cons,E,False,Nil,S,True} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) getNodeFromEdge#(0(),E(x,y)) -> c_2() getNodeFromEdge#(S(0()),E(x,y)) -> c_3() getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() goal#(u,v,edges) -> c_5(reach#(u,v,edges)) member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) via#(u,v,Nil(),edges) -> c_12() Weak DPs !EQ#(0(),0()) -> c_13() !EQ#(0(),S(y)) -> c_14() !EQ#(S(x),0()) -> c_15() !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) and#(False(),False()) -> c_17() and#(False(),True()) -> c_18() and#(True(),False()) -> c_19() and#(True(),True()) -> c_20() eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) member[Ite]#(True(),x,xs) -> c_24() reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) reach[Ite]#(True(),u,v,edges) -> c_26() via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) getNodeFromEdge#(0(),E(x,y)) -> c_2() getNodeFromEdge#(S(0()),E(x,y)) -> c_3() getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() goal#(u,v,edges) -> c_5(reach#(u,v,edges)) member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: !EQ#(0(),0()) -> c_13() !EQ#(0(),S(y)) -> c_14() !EQ#(S(x),0()) -> c_15() !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) and#(False(),False()) -> c_17() and#(False(),True()) -> c_18() and#(True(),False()) -> c_19() and#(True(),True()) -> c_20() eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) member[Ite]#(True(),x,xs) -> c_24() reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) reach[Ite]#(True(),u,v,edges) -> c_26() via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() getNodeFromEdge(0(),E(x,y)) -> x getNodeFromEdge(S(0()),E(x,y)) -> x getNodeFromEdge(S(S(x')),E(x,y)) -> y goal(u,v,edges) -> reach(u,v,edges) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) !EQ#(0(),0()) -> c_13() !EQ#(0(),S(y)) -> c_14() !EQ#(S(x),0()) -> c_15() !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) and#(False(),False()) -> c_17() and#(False(),True()) -> c_18() and#(True(),False()) -> c_19() and#(True(),True()) -> c_20() eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() getNodeFromEdge#(0(),E(x,y)) -> c_2() getNodeFromEdge#(S(0()),E(x,y)) -> c_3() getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() goal#(u,v,edges) -> c_5(reach#(u,v,edges)) member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) member[Ite]#(True(),x,xs) -> c_24() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) reach[Ite]#(True(),u,v,edges) -> c_26() via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) via#(u,v,Nil(),edges) -> c_12() via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) getNodeFromEdge#(0(),E(x,y)) -> c_2() getNodeFromEdge#(S(0()),E(x,y)) -> c_3() getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() goal#(u,v,edges) -> c_5(reach#(u,v,edges)) member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: !EQ#(0(),0()) -> c_13() !EQ#(0(),S(y)) -> c_14() !EQ#(S(x),0()) -> c_15() !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) and#(False(),False()) -> c_17() and#(False(),True()) -> c_18() and#(True(),False()) -> c_19() and#(True(),True()) -> c_20() eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) member[Ite]#(True(),x,xs) -> c_24() reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) reach[Ite]#(True(),u,v,edges) -> c_26() via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,8,9} by application of Pre({1,2,3,4,8,9}) = {7}. Here rules are labelled as follows: 1: eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) 2: getNodeFromEdge#(0(),E(x,y)) -> c_2() 3: getNodeFromEdge#(S(0()),E(x,y)) -> c_3() 4: getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() 5: goal#(u,v,edges) -> c_5(reach#(u,v,edges)) 6: member#(x,Nil()) -> c_6() 7: member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) 8: notEmpty#(Cons(x,xs)) -> c_8() 9: notEmpty#(Nil()) -> c_9() 10: reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) 11: via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) 12: via#(u,v,Nil(),edges) -> c_12() 13: !EQ#(0(),0()) -> c_13() 14: !EQ#(0(),S(y)) -> c_14() 15: !EQ#(S(x),0()) -> c_15() 16: !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) 17: and#(False(),False()) -> c_17() 18: and#(False(),True()) -> c_18() 19: and#(True(),False()) -> c_19() 20: and#(True(),True()) -> c_20() 21: eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() 22: eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() 23: member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) 24: member[Ite]#(True(),x,xs) -> c_24() 25: reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) 26: reach[Ite]#(True(),u,v,edges) -> c_26() 27: via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) 28: via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u ,v ,Cons(E(x,y),xs) ,edges ,reach(y,v,edges)) ,reach#(y,v,edges)) 29: via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() 30: via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: goal#(u,v,edges) -> c_5(reach#(u,v,edges)) member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: !EQ#(0(),0()) -> c_13() !EQ#(0(),S(y)) -> c_14() !EQ#(S(x),0()) -> c_15() !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) and#(False(),False()) -> c_17() and#(False(),True()) -> c_18() and#(True(),False()) -> c_19() and#(True(),True()) -> c_20() eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() getNodeFromEdge#(0(),E(x,y)) -> c_2() getNodeFromEdge#(S(0()),E(x,y)) -> c_3() getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) member[Ite]#(True(),x,xs) -> c_24() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) reach[Ite]#(True(),u,v,edges) -> c_26() via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:goal#(u,v,edges) -> c_5(reach#(u,v,edges)) -->_1 reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)):4 2:S:member#(x,Nil()) -> c_6() 3:S:member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) -->_1 member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)):21 -->_2 eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)):15 -->_1 member[Ite]#(True(),x,xs) -> c_24():22 4:S:reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) -->_1 reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)):25 -->_1 reach[Ite]#(True(),u,v,edges) -> c_26():26 -->_2 member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)):3 -->_2 member#(x,Nil()) -> c_6():2 5:S:via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) -->_1 via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u ,v ,Cons(E(x,y),xs) ,edges ,reach(y,v,edges)) ,reach#(y,v,edges)):28 -->_1 via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)):27 -->_2 !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)):10 -->_2 !EQ#(S(x),0()) -> c_15():9 -->_2 !EQ#(0(),S(y)) -> c_14():8 -->_2 !EQ#(0(),0()) -> c_13():7 6:S:via#(u,v,Nil(),edges) -> c_12() 7:W:!EQ#(0(),0()) -> c_13() 8:W:!EQ#(0(),S(y)) -> c_14() 9:W:!EQ#(S(x),0()) -> c_15() 10:W:!EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) -->_1 !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)):10 -->_1 !EQ#(S(x),0()) -> c_15():9 -->_1 !EQ#(0(),S(y)) -> c_14():8 -->_1 !EQ#(0(),0()) -> c_13():7 11:W:and#(False(),False()) -> c_17() 12:W:and#(False(),True()) -> c_18() 13:W:and#(True(),False()) -> c_19() 14:W:and#(True(),True()) -> c_20() 15:W:eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) -->_1 eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22():17 -->_1 eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21():16 -->_2 and#(True(),True()) -> c_20():14 -->_2 and#(True(),False()) -> c_19():13 -->_2 and#(False(),True()) -> c_18():12 -->_2 and#(False(),False()) -> c_17():11 -->_4 !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)):10 -->_3 !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)):10 -->_4 !EQ#(S(x),0()) -> c_15():9 -->_3 !EQ#(S(x),0()) -> c_15():9 -->_4 !EQ#(0(),S(y)) -> c_14():8 -->_3 !EQ#(0(),S(y)) -> c_14():8 -->_4 !EQ#(0(),0()) -> c_13():7 -->_3 !EQ#(0(),0()) -> c_13():7 16:W:eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() 17:W:eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() 18:W:getNodeFromEdge#(0(),E(x,y)) -> c_2() 19:W:getNodeFromEdge#(S(0()),E(x,y)) -> c_3() 20:W:getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() 21:W:member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)):3 -->_1 member#(x,Nil()) -> c_6():2 22:W:member[Ite]#(True(),x,xs) -> c_24() 23:W:notEmpty#(Cons(x,xs)) -> c_8() 24:W:notEmpty#(Nil()) -> c_9() 25:W:reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)):5 26:W:reach[Ite]#(True(),u,v,edges) -> c_26() 27:W:via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)):5 28:W:via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u ,v ,Cons(E(x,y),xs) ,edges ,reach(y,v,edges)) ,reach#(y,v,edges)) -->_1 via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)):30 -->_1 via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29():29 -->_2 reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)):4 29:W:via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() 30:W:via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 24: notEmpty#(Nil()) -> c_9() 23: notEmpty#(Cons(x,xs)) -> c_8() 20: getNodeFromEdge#(S(S(x')),E(x,y)) -> c_4() 19: getNodeFromEdge#(S(0()),E(x,y)) -> c_3() 18: getNodeFromEdge#(0(),E(x,y)) -> c_2() 22: member[Ite]#(True(),x,xs) -> c_24() 15: eqEdge#(E(e11,e12),E(e21,e22)) -> c_1(eqEdge[Ite]#(and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) ,and#(!EQ(e11,e21),!EQ(e12,e22)) ,!EQ#(e11,e21) ,!EQ#(e12,e22)) 11: and#(False(),False()) -> c_17() 12: and#(False(),True()) -> c_18() 13: and#(True(),False()) -> c_19() 14: and#(True(),True()) -> c_20() 16: eqEdge[Ite]#(False(),e21,e22,e11,e12) -> c_21() 17: eqEdge[Ite]#(True(),e21,e22,e11,e12) -> c_22() 26: reach[Ite]#(True(),u,v,edges) -> c_26() 10: !EQ#(S(x),S(y)) -> c_16(!EQ#(x,y)) 7: !EQ#(0(),0()) -> c_13() 8: !EQ#(0(),S(y)) -> c_14() 9: !EQ#(S(x),0()) -> c_15() 29: via[Let]#(u,v,Cons(x,xs),edges,Cons(x',xs')) -> c_29() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: goal#(u,v,edges) -> c_5(reach#(u,v,edges)) member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:goal#(u,v,edges) -> c_5(reach#(u,v,edges)) -->_1 reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)):4 2:S:member#(x,Nil()) -> c_6() 3:S:member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)) -->_1 member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)):21 4:S:reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) -->_1 reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)):25 -->_2 member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)):3 -->_2 member#(x,Nil()) -> c_6():2 5:S:via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)) -->_1 via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u ,v ,Cons(E(x,y),xs) ,edges ,reach(y,v,edges)) ,reach#(y,v,edges)):28 -->_1 via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)):27 6:S:via#(u,v,Nil(),edges) -> c_12() 21:W:member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs)),eqEdge#(x',x)):3 -->_1 member#(x,Nil()) -> c_6():2 25:W:reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)):5 27:W:via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)):5 28:W:via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u ,v ,Cons(E(x,y),xs) ,edges ,reach(y,v,edges)) ,reach#(y,v,edges)) -->_1 via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)):30 -->_2 reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)):4 30:W:via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges),!EQ#(u,x)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: goal#(u,v,edges) -> c_5(reach#(u,v,edges)) member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/2,c_11/1,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:goal#(u,v,edges) -> c_5(reach#(u,v,edges)) -->_1 reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)):4 2:S:member#(x,Nil()) -> c_6() 3:S:member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) -->_1 member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)):7 4:S:reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) -->_1 reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)):8 -->_2 member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))):3 -->_2 member#(x,Nil()) -> c_6():2 5:S:via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) -->_1 via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u ,v ,Cons(E(x,y),xs) ,edges ,reach(y,v,edges)) ,reach#(y,v,edges)):10 -->_1 via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)):9 6:S:via#(u,v,Nil(),edges) -> c_12() 7:W:member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))):3 -->_1 member#(x,Nil()) -> c_6():2 8:W:reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)):5 9:W:via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)):5 10:W:via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u ,v ,Cons(E(x,y),xs) ,edges ,reach(y,v,edges)) ,reach#(y,v,edges)) -->_1 via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)):11 -->_2 reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)):4 11:W:via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) -->_1 via#(u,v,Nil(),edges) -> c_12():6 -->_1 via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)):5 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). [(1,goal#(u,v,edges) -> c_5(reach#(u,v,edges)))] * Step 7: WeightGap MAYBE + Considered Problem: - Strict DPs: member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/2,c_11/1,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(and) = {1,2}, uargs(eqEdge[Ite]) = {1}, uargs(member[Ite]) = {1}, uargs(reach[Ite]) = {1}, uargs(via[Ite]) = {1}, uargs(via[Let]) = {5}, uargs(member[Ite]#) = {1}, uargs(reach[Ite]#) = {1}, uargs(via[Ite]#) = {1}, uargs(via[Let]#) = {5}, uargs(c_7) = {1}, uargs(c_10) = {1,2}, uargs(c_11) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1,2}, uargs(c_30) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [0] p(E) = [2] p(False) = [0] p(Nil) = [0] p(S) = [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(eqEdge) = [0] p(eqEdge[Ite]) = [1] x1 + [0] p(getNodeFromEdge) = [0] p(goal) = [0] p(member) = [0] p(member[Ite]) = [1] x1 + [0] p(notEmpty) = [0] p(reach) = [0] p(reach[Ite]) = [1] x1 + [0] p(via) = [0] p(via[Ite]) = [1] x1 + [0] p(via[Let]) = [1] x5 + [0] p(!EQ#) = [0] p(and#) = [0] p(eqEdge#) = [0] p(eqEdge[Ite]#) = [2] x2 + [2] x3 + [1] x4 + [0] p(getNodeFromEdge#) = [1] x1 + [1] x2 + [0] p(goal#) = [2] x1 + [4] x3 + [1] p(member#) = [0] p(member[Ite]#) = [1] x1 + [4] x3 + [0] p(notEmpty#) = [1] x1 + [1] p(reach#) = [2] p(reach[Ite]#) = [1] x1 + [0] p(via#) = [0] p(via[Ite]#) = [1] x1 + [7] p(via[Let]#) = [1] x5 + [5] p(c_1) = [2] x2 + [4] x4 + [0] p(c_2) = [2] p(c_3) = [1] p(c_4) = [2] p(c_5) = [1] p(c_6) = [1] p(c_7) = [1] x1 + [2] p(c_8) = [2] p(c_9) = [1] p(c_10) = [1] x1 + [1] x2 + [1] p(c_11) = [1] x1 + [1] p(c_12) = [0] p(c_13) = [0] p(c_14) = [1] p(c_15) = [0] p(c_16) = [2] x1 + [1] p(c_17) = [0] p(c_18) = [4] p(c_19) = [0] p(c_20) = [0] p(c_21) = [4] p(c_22) = [2] p(c_23) = [1] x1 + [0] p(c_24) = [0] p(c_25) = [1] x1 + [0] p(c_26) = [1] p(c_27) = [1] x1 + [2] p(c_28) = [1] x1 + [1] x2 + [0] p(c_29) = [0] p(c_30) = [1] x1 + [3] Following rules are strictly oriented: reach#(u,v,edges) = [2] > [1] = c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) Following rules are (at-least) weakly oriented: member#(x,Nil()) = [0] >= [1] = c_6() member#(x',Cons(x,xs)) = [0] >= [2] = c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) member[Ite]#(False(),x',Cons(x,xs)) = [0] >= [0] = c_23(member#(x',xs)) reach[Ite]#(False(),u,v,edges) = [0] >= [0] = c_25(via#(u,v,edges,edges)) via#(u,v,Cons(E(x,y),xs),edges) = [0] >= [8] = c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) via#(u,v,Nil(),edges) = [0] >= [0] = c_12() via[Ite]#(False(),u,v,Cons(x,xs),edges) = [7] >= [2] = c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) = [7] >= [7] = c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)),reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) = [5] >= [3] = c_30(via#(u,v,xs,edges)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() eqEdge(E(e11,e12),E(e21,e22)) = [0] >= [0] = eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) = [0] >= [0] = False() eqEdge[Ite](True(),e21,e22,e11,e12) = [0] >= [0] = True() member(x,Nil()) = [0] >= [0] = False() member(x',Cons(x,xs)) = [0] >= [0] = member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) = [0] >= [0] = member(x',xs) member[Ite](True(),x,xs) = [0] >= [0] = True() reach(u,v,edges) = [0] >= [0] = reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) = [0] >= [0] = via(u,v,edges,edges) reach[Ite](True(),u,v,edges) = [0] >= [0] = Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) = [0] >= [0] = via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) = [0] >= [0] = Nil() via[Ite](False(),u,v,Cons(x,xs),edges) = [0] >= [0] = via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) = [0] >= [0] = via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) = [0] >= [0] = Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) = [0] >= [0] = via(u,v,xs,edges) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: WeightGap MAYBE + Considered Problem: - Strict DPs: member#(x,Nil()) -> c_6() member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/2,c_11/1,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(and) = {1,2}, uargs(eqEdge[Ite]) = {1}, uargs(member[Ite]) = {1}, uargs(reach[Ite]) = {1}, uargs(via[Ite]) = {1}, uargs(via[Let]) = {5}, uargs(member[Ite]#) = {1}, uargs(reach[Ite]#) = {1}, uargs(via[Ite]#) = {1}, uargs(via[Let]#) = {5}, uargs(c_7) = {1}, uargs(c_10) = {1,2}, uargs(c_11) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1,2}, uargs(c_30) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [0] p(E) = [0] p(False) = [0] p(Nil) = [0] p(S) = [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(eqEdge) = [0] p(eqEdge[Ite]) = [1] x1 + [0] p(getNodeFromEdge) = [0] p(goal) = [0] p(member) = [3] x1 + [0] p(member[Ite]) = [1] x1 + [3] x2 + [0] p(notEmpty) = [0] p(reach) = [0] p(reach[Ite]) = [1] x1 + [0] p(via) = [0] p(via[Ite]) = [1] x1 + [0] p(via[Let]) = [1] x5 + [0] p(!EQ#) = [0] p(and#) = [0] p(eqEdge#) = [0] p(eqEdge[Ite]#) = [0] p(getNodeFromEdge#) = [2] x1 + [2] x2 + [0] p(goal#) = [2] x1 + [4] p(member#) = [1] p(member[Ite]#) = [1] x1 + [2] p(notEmpty#) = [0] p(reach#) = [4] p(reach[Ite]#) = [1] x1 + [0] p(via#) = [0] p(via[Ite]#) = [1] x1 + [7] p(via[Let]#) = [1] x5 + [2] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [2] p(c_10) = [1] x1 + [1] x2 + [1] p(c_11) = [1] x1 + [0] p(c_12) = [1] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [1] x1 + [0] p(c_24) = [0] p(c_25) = [1] x1 + [0] p(c_26) = [0] p(c_27) = [1] x1 + [2] p(c_28) = [1] x1 + [1] x2 + [1] p(c_29) = [0] p(c_30) = [1] x1 + [1] Following rules are strictly oriented: member#(x,Nil()) = [1] > [0] = c_6() Following rules are (at-least) weakly oriented: member#(x',Cons(x,xs)) = [1] >= [2] = c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) member[Ite]#(False(),x',Cons(x,xs)) = [2] >= [1] = c_23(member#(x',xs)) reach#(u,v,edges) = [4] >= [2] = c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) reach[Ite]#(False(),u,v,edges) = [0] >= [0] = c_25(via#(u,v,edges,edges)) via#(u,v,Cons(E(x,y),xs),edges) = [0] >= [7] = c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) via#(u,v,Nil(),edges) = [0] >= [1] = c_12() via[Ite]#(False(),u,v,Cons(x,xs),edges) = [7] >= [2] = c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) = [7] >= [7] = c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)),reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) = [2] >= [1] = c_30(via#(u,v,xs,edges)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() eqEdge(E(e11,e12),E(e21,e22)) = [0] >= [0] = eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) = [0] >= [0] = False() eqEdge[Ite](True(),e21,e22,e11,e12) = [0] >= [0] = True() member(x,Nil()) = [3] x + [0] >= [0] = False() member(x',Cons(x,xs)) = [3] x' + [0] >= [3] x' + [0] = member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) = [3] x' + [0] >= [3] x' + [0] = member(x',xs) member[Ite](True(),x,xs) = [3] x + [0] >= [0] = True() reach(u,v,edges) = [0] >= [0] = reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) = [0] >= [0] = via(u,v,edges,edges) reach[Ite](True(),u,v,edges) = [0] >= [0] = Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) = [0] >= [0] = via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) = [0] >= [0] = Nil() via[Ite](False(),u,v,Cons(x,xs),edges) = [0] >= [0] = via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) = [0] >= [0] = via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) = [0] >= [0] = Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) = [0] >= [0] = via(u,v,xs,edges) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: WeightGap MAYBE + Considered Problem: - Strict DPs: member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) via#(u,v,Nil(),edges) -> c_12() - Weak DPs: member#(x,Nil()) -> c_6() member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/2,c_11/1,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(and) = {1,2}, uargs(eqEdge[Ite]) = {1}, uargs(member[Ite]) = {1}, uargs(reach[Ite]) = {1}, uargs(via[Ite]) = {1}, uargs(via[Let]) = {5}, uargs(member[Ite]#) = {1}, uargs(reach[Ite]#) = {1}, uargs(via[Ite]#) = {1}, uargs(via[Let]#) = {5}, uargs(c_7) = {1}, uargs(c_10) = {1,2}, uargs(c_11) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1,2}, uargs(c_30) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [0] p(E) = [0] p(False) = [0] p(Nil) = [0] p(S) = [1] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(eqEdge) = [0] p(eqEdge[Ite]) = [1] x1 + [0] p(getNodeFromEdge) = [0] p(goal) = [1] x1 + [0] p(member) = [0] p(member[Ite]) = [1] x1 + [0] p(notEmpty) = [1] x1 + [0] p(reach) = [0] p(reach[Ite]) = [1] x1 + [0] p(via) = [0] p(via[Ite]) = [1] x1 + [0] p(via[Let]) = [1] x5 + [0] p(!EQ#) = [4] p(and#) = [2] x1 + [0] p(eqEdge#) = [1] x1 + [0] p(eqEdge[Ite]#) = [1] x5 + [4] p(getNodeFromEdge#) = [0] p(goal#) = [2] x3 + [0] p(member#) = [2] x1 + [1] p(member[Ite]#) = [1] x1 + [2] x2 + [4] x3 + [1] p(notEmpty#) = [2] p(reach#) = [4] p(reach[Ite]#) = [1] x1 + [3] p(via#) = [1] p(via[Ite]#) = [1] x1 + [5] p(via[Let]#) = [1] x3 + [1] x5 + [1] p(c_1) = [2] x1 + [2] x2 + [4] x3 + [0] p(c_2) = [0] p(c_3) = [1] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [2] p(c_10) = [1] x1 + [1] x2 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [4] x1 + [1] p(c_17) = [1] p(c_18) = [0] p(c_19) = [1] p(c_20) = [0] p(c_21) = [4] p(c_22) = [0] p(c_23) = [1] x1 + [0] p(c_24) = [1] p(c_25) = [1] x1 + [2] p(c_26) = [2] p(c_27) = [1] x1 + [3] p(c_28) = [1] x1 + [1] x2 + [0] p(c_29) = [2] p(c_30) = [1] x1 + [0] Following rules are strictly oriented: via#(u,v,Nil(),edges) = [1] > [0] = c_12() Following rules are (at-least) weakly oriented: member#(x,Nil()) = [2] x + [1] >= [1] = c_6() member#(x',Cons(x,xs)) = [2] x' + [1] >= [2] x' + [1] = c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) member[Ite]#(False(),x',Cons(x,xs)) = [2] x' + [1] >= [2] x' + [1] = c_23(member#(x',xs)) reach#(u,v,edges) = [4] >= [4] = c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) reach[Ite]#(False(),u,v,edges) = [3] >= [3] = c_25(via#(u,v,edges,edges)) via#(u,v,Cons(E(x,y),xs),edges) = [1] >= [5] = c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) via[Ite]#(False(),u,v,Cons(x,xs),edges) = [5] >= [4] = c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) = [5] >= [5] = c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)),reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) = [1] >= [1] = c_30(via#(u,v,xs,edges)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() eqEdge(E(e11,e12),E(e21,e22)) = [0] >= [0] = eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) = [0] >= [0] = False() eqEdge[Ite](True(),e21,e22,e11,e12) = [0] >= [0] = True() member(x,Nil()) = [0] >= [0] = False() member(x',Cons(x,xs)) = [0] >= [0] = member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) = [0] >= [0] = member(x',xs) member[Ite](True(),x,xs) = [0] >= [0] = True() reach(u,v,edges) = [0] >= [0] = reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) = [0] >= [0] = via(u,v,edges,edges) reach[Ite](True(),u,v,edges) = [0] >= [0] = Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) = [0] >= [0] = via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) = [0] >= [0] = Nil() via[Ite](False(),u,v,Cons(x,xs),edges) = [0] >= [0] = via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) = [0] >= [0] = via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) = [0] >= [0] = Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) = [0] >= [0] = via(u,v,xs,edges) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 10: Failure MAYBE + Considered Problem: - Strict DPs: member#(x',Cons(x,xs)) -> c_7(member[Ite]#(eqEdge(x',x),x',Cons(x,xs))) via#(u,v,Cons(E(x,y),xs),edges) -> c_11(via[Ite]#(!EQ(u,x),u,v,Cons(E(x,y),xs),edges)) - Weak DPs: member#(x,Nil()) -> c_6() member[Ite]#(False(),x',Cons(x,xs)) -> c_23(member#(x',xs)) reach#(u,v,edges) -> c_10(reach[Ite]#(member(E(u,v),edges),u,v,edges),member#(E(u,v),edges)) reach[Ite]#(False(),u,v,edges) -> c_25(via#(u,v,edges,edges)) via#(u,v,Nil(),edges) -> c_12() via[Ite]#(False(),u,v,Cons(x,xs),edges) -> c_27(via#(u,v,xs,edges)) via[Ite]#(True(),u,v,Cons(E(x,y),xs),edges) -> c_28(via[Let]#(u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) ,reach#(y,v,edges)) via[Let]#(u,v,Cons(x,xs),edges,Nil()) -> c_30(via#(u,v,xs,edges)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqEdge(E(e11,e12),E(e21,e22)) -> eqEdge[Ite](and(!EQ(e11,e21),!EQ(e12,e22)),e21,e22,e11,e12) eqEdge[Ite](False(),e21,e22,e11,e12) -> False() eqEdge[Ite](True(),e21,e22,e11,e12) -> True() member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite](eqEdge(x',x),x',Cons(x,xs)) member[Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite](True(),x,xs) -> True() reach(u,v,edges) -> reach[Ite](member(E(u,v),edges),u,v,edges) reach[Ite](False(),u,v,edges) -> via(u,v,edges,edges) reach[Ite](True(),u,v,edges) -> Cons(E(u,v),Nil()) via(u,v,Cons(E(x,y),xs),edges) -> via[Ite](!EQ(u,x),u,v,Cons(E(x,y),xs),edges) via(u,v,Nil(),edges) -> Nil() via[Ite](False(),u,v,Cons(x,xs),edges) -> via(u,v,xs,edges) via[Ite](True(),u,v,Cons(E(x,y),xs),edges) -> via[Let](u,v,Cons(E(x,y),xs),edges,reach(y,v,edges)) via[Let](u,v,Cons(x,xs),edges,Cons(x',xs')) -> Cons(x,Cons(x',xs')) via[Let](u,v,Cons(x,xs),edges,Nil()) -> via(u,v,xs,edges) - Signature: {!EQ/2,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3,member/2,member[Ite]/3,notEmpty/1,reach/3 ,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5,!EQ#/2,and#/2,eqEdge#/2,eqEdge[Ite]#/5,getNodeFromEdge#/2,goal#/3 ,member#/2,member[Ite]#/3,notEmpty#/1,reach#/3,reach[Ite]#/4,via#/4,via[Ite]#/5,via[Let]#/5} / {0/0,Cons/2 ,E/2,False/0,Nil/0,S/1,True/0,c_1/4,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/2,c_11/1,c_12/0 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/1,c_24/0,c_25/1,c_26/0,c_27/1 ,c_28/2,c_29/0,c_30/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,eqEdge#,eqEdge[Ite]#,getNodeFromEdge#,goal# ,member#,member[Ite]#,notEmpty#,reach#,reach[Ite]#,via#,via[Ite]#,via[Let]#} and constructors {0,Cons,E ,False,Nil,S,True} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE