MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: colorednoderest(cs,Cons(x,xs),N(n,ns),colorednodes,rest) -> colorednoderest[Ite][True][Ite](possible(x ,ns ,colorednodes) ,cs ,Cons(x,xs) ,N(n,ns) ,colorednodes ,rest) colorednoderest(cs,Nil(),node,colorednodes,rest) -> Nil() colornode(Cons(x,xs),N(n,ns),colorednodes) -> colornode[Ite][True][Ite](possible(x,ns,colorednodes) ,Cons(x,xs) ,N(n,ns) ,colorednodes) colornode(Nil(),node,colorednodes) -> NotPossible() colorof(node,Cons(CN(cl,N(name,adjs)),xs)) -> colorof[Ite][True][Ite](!EQ(name,node) ,node ,Cons(CN(cl,N(name,adjs)),xs)) colorof(node,Nil()) -> NoColor() colorrest(cs,ncs,colorednodes,Cons(x,xs)) -> colorednoderest(cs,ncs,x,colorednodes,Cons(x,xs)) colorrest(cs,ncs,colorednodes,Nil()) -> colorednodes colorrestthetrick(cs1,cs,ncs,colorednodes,rest) -> colorrestthetrick[Ite](eqColorList(cs1,ncs) ,cs1 ,cs ,ncs ,colorednodes ,rest) eqColor(Blue(),Blue()) -> True() eqColor(Blue(),NoColor()) -> False() eqColor(Blue(),Red()) -> False() eqColor(Blue(),Yellow()) -> False() eqColor(NoColor(),b) -> False() eqColor(Red(),Blue()) -> False() eqColor(Red(),NoColor()) -> False() eqColor(Red(),Red()) -> True() eqColor(Red(),Yellow()) -> False() eqColor(Yellow(),Blue()) -> False() eqColor(Yellow(),NoColor()) -> False() eqColor(Yellow(),Red()) -> False() eqColor(Yellow(),Yellow()) -> True() eqColorList(Cons(c1,cs1),Nil()) -> False() eqColorList(Cons(Blue(),cs1),Cons(Blue(),cs2)) -> and(True(),eqColorList(cs1,cs2)) eqColorList(Cons(Blue(),cs1),Cons(NoColor(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Blue(),cs1),Cons(Red(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Blue(),cs1),Cons(Yellow(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(NoColor(),cs1),Cons(b,cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Red(),cs1),Cons(Blue(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Red(),cs1),Cons(NoColor(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Red(),cs1),Cons(Red(),cs2)) -> and(True(),eqColorList(cs1,cs2)) eqColorList(Cons(Red(),cs1),Cons(Yellow(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Yellow(),cs1),Cons(Blue(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Yellow(),cs1),Cons(NoColor(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Yellow(),cs1),Cons(Red(),cs2)) -> and(False(),eqColorList(cs1,cs2)) eqColorList(Cons(Yellow(),cs1),Cons(Yellow(),cs2)) -> and(True(),eqColorList(cs1,cs2)) eqColorList(Nil(),Cons(c2,cs2)) -> False() eqColorList(Nil(),Nil()) -> True() getAdjs(N(n,ns)) -> ns getColorListFromCN(CN(cl,n)) -> cl getNodeFromCN(CN(cl,n)) -> n getNodeName(N(name,adjs)) -> name graphcolour(Cons(x,xs),cs) -> reverse(colorrest(cs,cs,Cons(colornode(cs,x,Nil()),Nil()),xs)) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() possible(color,Cons(x,xs),colorednodes) -> possible[Ite][True][Ite](eqColor(color,colorof(x,colorednodes)) ,color ,Cons(x,xs) ,colorednodes) possible(color,Nil(),colorednodes) -> True() revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) revapp(Nil(),rest) -> rest reverse(xs) -> revapp(xs,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() colorednoderest[Ite][True][Ite](False(),cs,Cons(x,xs),node,colorednodes,rest) -> colorednoderest(cs ,xs ,node ,colorednodes ,rest) colorednoderest[Ite][True][Ite](True(),cs,ncs,node,colorednodes,Cons(x,xs)) -> colorednoderest[Ite][True][Ite][True][Let](cs ,ncs ,node ,colorednodes ,Cons(x,xs) ,colorrest(cs,cs,Cons(CN(ncs,node),colorednodes),xs)) colornode[Ite][True][Ite](False(),Cons(x,xs),node,colorednodes) -> colornode(xs,node,colorednodes) colornode[Ite][True][Ite](True(),cs,node,colorednodes) -> CN(cs,node) colorof[Ite][True][Ite](False(),node,Cons(x,xs)) -> colorof(node,xs) colorof[Ite][True][Ite](True(),node,Cons(CN(Cons(x,xs),n),xs')) -> x colorrestthetrick[Ite](False(),Cons(x,xs),cs,ncs,colorednodes,rest) -> colorrestthetrick(xs ,cs ,ncs ,colorednodes ,rest) colorrestthetrick[Ite](True(),cs1,cs,ncs,colorednodes,rest) -> colorrest(cs,cs1,colorednodes,rest) possible[Ite][True][Ite](False(),color,Cons(x,xs),colorednodes) -> possible(color,xs,colorednodes) possible[Ite][True][Ite](True(),color,adjs,colorednodes) -> False() - Signature: {!EQ/2,and/2,colorednoderest/5,colorednoderest[Ite][True][Ite]/6,colornode/3,colornode[Ite][True][Ite]/4 ,colorof/2,colorof[Ite][True][Ite]/3,colorrest/4,colorrestthetrick/5,colorrestthetrick[Ite]/6,eqColor/2 ,eqColorList/2,getAdjs/1,getColorListFromCN/1,getNodeFromCN/1,getNodeName/1,graphcolour/2,notEmpty/1 ,possible/3,possible[Ite][True][Ite]/4,revapp/2,reverse/1} / {0/0,Blue/0,CN/2,Cons/2,False/0,N/2,Nil/0 ,NoColor/0,NotPossible/0,Red/0,S/1,True/0,Yellow/0,colorednoderest[Ite][True][Ite][True][Let]/6} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,and,colorednoderest,colorednoderest[Ite][True][Ite] ,colornode,colornode[Ite][True][Ite],colorof,colorof[Ite][True][Ite],colorrest,colorrestthetrick ,colorrestthetrick[Ite],eqColor,eqColorList,getAdjs,getColorListFromCN,getNodeFromCN,getNodeName,graphcolour ,notEmpty,possible,possible[Ite][True][Ite],revapp,reverse} and constructors {0,Blue,CN,Cons,False,N,Nil ,NoColor,NotPossible,Red,S,True,Yellow,colorednoderest[Ite][True][Ite][True][Let]} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE