MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: atom(Cons(x,xs)) -> xs atom(Nil()) -> Nil() eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs head(Cons(x,xs)) -> x member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() parsexp(xs) -> expr(xs) term(xs) -> term[Let](xs,factor(xs)) - 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() expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) - Signature: {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2 ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2} / {0/0,Cons/2,Div/0,False/0,LPar/0 ,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1,True/0,Val/1,expr[Let][Ite][False][Ite]/3 ,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,and,atom,eqAlph,expr,expr[Let],factor ,factor[Ite][True][Let],head,member,member[Ite][True][Ite],notEmpty,parsexp,term ,term[Let]} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs atom#(Cons(x,xs)) -> c_1() atom#(Nil()) -> c_2() eqAlph#(Div(),Div()) -> c_3() eqAlph#(Div(),LPar()) -> c_4() eqAlph#(Div(),Minus()) -> c_5() eqAlph#(Div(),Mul()) -> c_6() eqAlph#(Div(),Plus()) -> c_7() eqAlph#(Div(),RPar()) -> c_8() eqAlph#(Div(),Val(int2)) -> c_9() eqAlph#(LPar(),Div()) -> c_10() eqAlph#(LPar(),LPar()) -> c_11() eqAlph#(LPar(),Minus()) -> c_12() eqAlph#(LPar(),Mul()) -> c_13() eqAlph#(LPar(),Plus()) -> c_14() eqAlph#(LPar(),RPar()) -> c_15() eqAlph#(LPar(),Val(int2)) -> c_16() eqAlph#(Minus(),Div()) -> c_17() eqAlph#(Minus(),LPar()) -> c_18() eqAlph#(Minus(),Minus()) -> c_19() eqAlph#(Minus(),Mul()) -> c_20() eqAlph#(Minus(),Plus()) -> c_21() eqAlph#(Minus(),RPar()) -> c_22() eqAlph#(Minus(),Val(int2)) -> c_23() eqAlph#(Mul(),Div()) -> c_24() eqAlph#(Mul(),LPar()) -> c_25() eqAlph#(Mul(),Minus()) -> c_26() eqAlph#(Mul(),Mul()) -> c_27() eqAlph#(Mul(),Plus()) -> c_28() eqAlph#(Mul(),RPar()) -> c_29() eqAlph#(Mul(),Val(int2)) -> c_30() eqAlph#(Plus(),Div()) -> c_31() eqAlph#(Plus(),LPar()) -> c_32() eqAlph#(Plus(),Minus()) -> c_33() eqAlph#(Plus(),Mul()) -> c_34() eqAlph#(Plus(),Plus()) -> c_35() eqAlph#(Plus(),RPar()) -> c_36() eqAlph#(Plus(),Val(int2)) -> c_37() eqAlph#(RPar(),Div()) -> c_38() eqAlph#(RPar(),LPar()) -> c_39() eqAlph#(RPar(),Minus()) -> c_40() eqAlph#(RPar(),Mul()) -> c_41() eqAlph#(RPar(),Plus()) -> c_42() eqAlph#(RPar(),RPar()) -> c_43() eqAlph#(RPar(),Val(int2)) -> c_44() eqAlph#(Val(int),Div()) -> c_45() eqAlph#(Val(int),LPar()) -> c_46() eqAlph#(Val(int),Minus()) -> c_47() eqAlph#(Val(int),Mul()) -> c_48() eqAlph#(Val(int),Plus()) -> c_49() eqAlph#(Val(int),RPar()) -> c_50() eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) factor#(Cons(Div(),xs)) -> c_53() factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) factor#(Cons(Minus(),xs)) -> c_55() factor#(Cons(Mul(),xs)) -> c_56() factor#(Cons(Plus(),xs)) -> c_57() factor#(Cons(RPar(),xs)) -> c_58() factor#(Cons(Val(int),xs)) -> c_59() head#(Cons(x,xs)) -> c_60() member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) notEmpty#(Cons(x,xs)) -> c_63() notEmpty#(Nil()) -> c_64() parsexp#(xs) -> c_65(expr#(xs)) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) Weak DPs !EQ#(0(),0()) -> c_67() !EQ#(0(),S(y)) -> c_68() !EQ#(S(x),0()) -> c_69() !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) and#(False(),False()) -> c_71() and#(False(),True()) -> c_72() and#(True(),False()) -> c_73() and#(True(),True()) -> c_74() expr[Let]#(xs,Nil()) -> c_75() expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_86() term[Let]#(xs,Nil()) -> c_87() term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))) and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: atom#(Cons(x,xs)) -> c_1() atom#(Nil()) -> c_2() eqAlph#(Div(),Div()) -> c_3() eqAlph#(Div(),LPar()) -> c_4() eqAlph#(Div(),Minus()) -> c_5() eqAlph#(Div(),Mul()) -> c_6() eqAlph#(Div(),Plus()) -> c_7() eqAlph#(Div(),RPar()) -> c_8() eqAlph#(Div(),Val(int2)) -> c_9() eqAlph#(LPar(),Div()) -> c_10() eqAlph#(LPar(),LPar()) -> c_11() eqAlph#(LPar(),Minus()) -> c_12() eqAlph#(LPar(),Mul()) -> c_13() eqAlph#(LPar(),Plus()) -> c_14() eqAlph#(LPar(),RPar()) -> c_15() eqAlph#(LPar(),Val(int2)) -> c_16() eqAlph#(Minus(),Div()) -> c_17() eqAlph#(Minus(),LPar()) -> c_18() eqAlph#(Minus(),Minus()) -> c_19() eqAlph#(Minus(),Mul()) -> c_20() eqAlph#(Minus(),Plus()) -> c_21() eqAlph#(Minus(),RPar()) -> c_22() eqAlph#(Minus(),Val(int2)) -> c_23() eqAlph#(Mul(),Div()) -> c_24() eqAlph#(Mul(),LPar()) -> c_25() eqAlph#(Mul(),Minus()) -> c_26() eqAlph#(Mul(),Mul()) -> c_27() eqAlph#(Mul(),Plus()) -> c_28() eqAlph#(Mul(),RPar()) -> c_29() eqAlph#(Mul(),Val(int2)) -> c_30() eqAlph#(Plus(),Div()) -> c_31() eqAlph#(Plus(),LPar()) -> c_32() eqAlph#(Plus(),Minus()) -> c_33() eqAlph#(Plus(),Mul()) -> c_34() eqAlph#(Plus(),Plus()) -> c_35() eqAlph#(Plus(),RPar()) -> c_36() eqAlph#(Plus(),Val(int2)) -> c_37() eqAlph#(RPar(),Div()) -> c_38() eqAlph#(RPar(),LPar()) -> c_39() eqAlph#(RPar(),Minus()) -> c_40() eqAlph#(RPar(),Mul()) -> c_41() eqAlph#(RPar(),Plus()) -> c_42() eqAlph#(RPar(),RPar()) -> c_43() eqAlph#(RPar(),Val(int2)) -> c_44() eqAlph#(Val(int),Div()) -> c_45() eqAlph#(Val(int),LPar()) -> c_46() eqAlph#(Val(int),Minus()) -> c_47() eqAlph#(Val(int),Mul()) -> c_48() eqAlph#(Val(int),Plus()) -> c_49() eqAlph#(Val(int),RPar()) -> c_50() eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) factor#(Cons(Div(),xs)) -> c_53() factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) factor#(Cons(Minus(),xs)) -> c_55() factor#(Cons(Mul(),xs)) -> c_56() factor#(Cons(Plus(),xs)) -> c_57() factor#(Cons(RPar(),xs)) -> c_58() factor#(Cons(Val(int),xs)) -> c_59() head#(Cons(x,xs)) -> c_60() member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) notEmpty#(Cons(x,xs)) -> c_63() notEmpty#(Nil()) -> c_64() parsexp#(xs) -> c_65(expr#(xs)) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) - Weak DPs: !EQ#(0(),0()) -> c_67() !EQ#(0(),S(y)) -> c_68() !EQ#(S(x),0()) -> c_69() !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) and#(False(),False()) -> c_71() and#(False(),True()) -> c_72() and#(True(),False()) -> c_73() and#(True(),True()) -> c_74() expr[Let]#(xs,Nil()) -> c_75() expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_86() term[Let]#(xs,Nil()) -> c_87() term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),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() atom(Cons(x,xs)) -> xs atom(Nil()) -> Nil() eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) head(Cons(x,xs)) -> x member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() parsexp(xs) -> expr(xs) term(xs) -> term[Let](xs,factor(xs)) term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) - Signature: {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2 ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2,!EQ#/2,and#/2,atom#/1,eqAlph#/2,expr#/1 ,expr[Let]#/2,factor#/1,factor[Ite][True][Let]#/2,head#/1,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1 ,parsexp#/1,term#/1,term[Let]#/2} / {0/0,Cons/2,Div/0,False/0,LPar/0,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1 ,True/0,Val/1,expr[Let][Ite][False][Ite]/3,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3,c_1/0 ,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0 ,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0 ,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0 ,c_48/0,c_49/0,c_50/0,c_51/1,c_52/2,c_53/0,c_54/2,c_55/0,c_56/0,c_57/0,c_58/0,c_59/0,c_60/0,c_61/0,c_62/2 ,c_63/0,c_64/0,c_65/1,c_66/2,c_67/0,c_68/0,c_69/0,c_70/1,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/1,c_77/3 ,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0,c_83/0,c_84/0,c_85/1,c_86/0,c_87/0,c_88/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,atom#,eqAlph#,expr#,expr[Let]#,factor# ,factor[Ite][True][Let]#,head#,member#,member[Ite][True][Ite]#,notEmpty#,parsexp#,term# ,term[Let]#} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]} + 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) eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() term(xs) -> term[Let](xs,factor(xs)) term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) !EQ#(0(),0()) -> c_67() !EQ#(0(),S(y)) -> c_68() !EQ#(S(x),0()) -> c_69() !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) and#(False(),False()) -> c_71() and#(False(),True()) -> c_72() and#(True(),False()) -> c_73() and#(True(),True()) -> c_74() atom#(Cons(x,xs)) -> c_1() atom#(Nil()) -> c_2() eqAlph#(Div(),Div()) -> c_3() eqAlph#(Div(),LPar()) -> c_4() eqAlph#(Div(),Minus()) -> c_5() eqAlph#(Div(),Mul()) -> c_6() eqAlph#(Div(),Plus()) -> c_7() eqAlph#(Div(),RPar()) -> c_8() eqAlph#(Div(),Val(int2)) -> c_9() eqAlph#(LPar(),Div()) -> c_10() eqAlph#(LPar(),LPar()) -> c_11() eqAlph#(LPar(),Minus()) -> c_12() eqAlph#(LPar(),Mul()) -> c_13() eqAlph#(LPar(),Plus()) -> c_14() eqAlph#(LPar(),RPar()) -> c_15() eqAlph#(LPar(),Val(int2)) -> c_16() eqAlph#(Minus(),Div()) -> c_17() eqAlph#(Minus(),LPar()) -> c_18() eqAlph#(Minus(),Minus()) -> c_19() eqAlph#(Minus(),Mul()) -> c_20() eqAlph#(Minus(),Plus()) -> c_21() eqAlph#(Minus(),RPar()) -> c_22() eqAlph#(Minus(),Val(int2)) -> c_23() eqAlph#(Mul(),Div()) -> c_24() eqAlph#(Mul(),LPar()) -> c_25() eqAlph#(Mul(),Minus()) -> c_26() eqAlph#(Mul(),Mul()) -> c_27() eqAlph#(Mul(),Plus()) -> c_28() eqAlph#(Mul(),RPar()) -> c_29() eqAlph#(Mul(),Val(int2)) -> c_30() eqAlph#(Plus(),Div()) -> c_31() eqAlph#(Plus(),LPar()) -> c_32() eqAlph#(Plus(),Minus()) -> c_33() eqAlph#(Plus(),Mul()) -> c_34() eqAlph#(Plus(),Plus()) -> c_35() eqAlph#(Plus(),RPar()) -> c_36() eqAlph#(Plus(),Val(int2)) -> c_37() eqAlph#(RPar(),Div()) -> c_38() eqAlph#(RPar(),LPar()) -> c_39() eqAlph#(RPar(),Minus()) -> c_40() eqAlph#(RPar(),Mul()) -> c_41() eqAlph#(RPar(),Plus()) -> c_42() eqAlph#(RPar(),RPar()) -> c_43() eqAlph#(RPar(),Val(int2)) -> c_44() eqAlph#(Val(int),Div()) -> c_45() eqAlph#(Val(int),LPar()) -> c_46() eqAlph#(Val(int),Minus()) -> c_47() eqAlph#(Val(int),Mul()) -> c_48() eqAlph#(Val(int),Plus()) -> c_49() eqAlph#(Val(int),RPar()) -> c_50() eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) expr[Let]#(xs,Nil()) -> c_75() expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) factor#(Cons(Div(),xs)) -> c_53() factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) factor#(Cons(Minus(),xs)) -> c_55() factor#(Cons(Mul(),xs)) -> c_56() factor#(Cons(Plus(),xs)) -> c_57() factor#(Cons(RPar(),xs)) -> c_58() factor#(Cons(Val(int),xs)) -> c_59() factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() head#(Cons(x,xs)) -> c_60() member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_86() notEmpty#(Cons(x,xs)) -> c_63() notEmpty#(Nil()) -> c_64() parsexp#(xs) -> c_65(expr#(xs)) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) term[Let]#(xs,Nil()) -> c_87() term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: atom#(Cons(x,xs)) -> c_1() atom#(Nil()) -> c_2() eqAlph#(Div(),Div()) -> c_3() eqAlph#(Div(),LPar()) -> c_4() eqAlph#(Div(),Minus()) -> c_5() eqAlph#(Div(),Mul()) -> c_6() eqAlph#(Div(),Plus()) -> c_7() eqAlph#(Div(),RPar()) -> c_8() eqAlph#(Div(),Val(int2)) -> c_9() eqAlph#(LPar(),Div()) -> c_10() eqAlph#(LPar(),LPar()) -> c_11() eqAlph#(LPar(),Minus()) -> c_12() eqAlph#(LPar(),Mul()) -> c_13() eqAlph#(LPar(),Plus()) -> c_14() eqAlph#(LPar(),RPar()) -> c_15() eqAlph#(LPar(),Val(int2)) -> c_16() eqAlph#(Minus(),Div()) -> c_17() eqAlph#(Minus(),LPar()) -> c_18() eqAlph#(Minus(),Minus()) -> c_19() eqAlph#(Minus(),Mul()) -> c_20() eqAlph#(Minus(),Plus()) -> c_21() eqAlph#(Minus(),RPar()) -> c_22() eqAlph#(Minus(),Val(int2)) -> c_23() eqAlph#(Mul(),Div()) -> c_24() eqAlph#(Mul(),LPar()) -> c_25() eqAlph#(Mul(),Minus()) -> c_26() eqAlph#(Mul(),Mul()) -> c_27() eqAlph#(Mul(),Plus()) -> c_28() eqAlph#(Mul(),RPar()) -> c_29() eqAlph#(Mul(),Val(int2)) -> c_30() eqAlph#(Plus(),Div()) -> c_31() eqAlph#(Plus(),LPar()) -> c_32() eqAlph#(Plus(),Minus()) -> c_33() eqAlph#(Plus(),Mul()) -> c_34() eqAlph#(Plus(),Plus()) -> c_35() eqAlph#(Plus(),RPar()) -> c_36() eqAlph#(Plus(),Val(int2)) -> c_37() eqAlph#(RPar(),Div()) -> c_38() eqAlph#(RPar(),LPar()) -> c_39() eqAlph#(RPar(),Minus()) -> c_40() eqAlph#(RPar(),Mul()) -> c_41() eqAlph#(RPar(),Plus()) -> c_42() eqAlph#(RPar(),RPar()) -> c_43() eqAlph#(RPar(),Val(int2)) -> c_44() eqAlph#(Val(int),Div()) -> c_45() eqAlph#(Val(int),LPar()) -> c_46() eqAlph#(Val(int),Minus()) -> c_47() eqAlph#(Val(int),Mul()) -> c_48() eqAlph#(Val(int),Plus()) -> c_49() eqAlph#(Val(int),RPar()) -> c_50() eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) factor#(Cons(Div(),xs)) -> c_53() factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) factor#(Cons(Minus(),xs)) -> c_55() factor#(Cons(Mul(),xs)) -> c_56() factor#(Cons(Plus(),xs)) -> c_57() factor#(Cons(RPar(),xs)) -> c_58() factor#(Cons(Val(int),xs)) -> c_59() head#(Cons(x,xs)) -> c_60() member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) notEmpty#(Cons(x,xs)) -> c_63() notEmpty#(Nil()) -> c_64() parsexp#(xs) -> c_65(expr#(xs)) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) - Weak DPs: !EQ#(0(),0()) -> c_67() !EQ#(0(),S(y)) -> c_68() !EQ#(S(x),0()) -> c_69() !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) and#(False(),False()) -> c_71() and#(False(),True()) -> c_72() and#(True(),False()) -> c_73() and#(True(),True()) -> c_74() expr[Let]#(xs,Nil()) -> c_75() expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_86() term[Let]#(xs,Nil()) -> c_87() term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),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) eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() term(xs) -> term[Let](xs,factor(xs)) term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) - Signature: {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2 ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2,!EQ#/2,and#/2,atom#/1,eqAlph#/2,expr#/1 ,expr[Let]#/2,factor#/1,factor[Ite][True][Let]#/2,head#/1,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1 ,parsexp#/1,term#/1,term[Let]#/2} / {0/0,Cons/2,Div/0,False/0,LPar/0,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1 ,True/0,Val/1,expr[Let][Ite][False][Ite]/3,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3,c_1/0 ,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0 ,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0 ,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0 ,c_48/0,c_49/0,c_50/0,c_51/1,c_52/2,c_53/0,c_54/2,c_55/0,c_56/0,c_57/0,c_58/0,c_59/0,c_60/0,c_61/0,c_62/2 ,c_63/0,c_64/0,c_65/1,c_66/2,c_67/0,c_68/0,c_69/0,c_70/1,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/1,c_77/3 ,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0,c_83/0,c_84/0,c_85/1,c_86/0,c_87/0,c_88/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,atom#,eqAlph#,expr#,expr[Let]#,factor# ,factor[Ite][True][Let]#,head#,member#,member[Ite][True][Ite]#,notEmpty#,parsexp#,term# ,term[Let]#} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38 ,39,40,41,42,43,44,45,46,47,48,49,50,51,53,55,56,57,58,59,60,63,64} by application of Pre({1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37 ,38,39,40,41,42,43,44,45,46,47,48,49,50,51,53,55,56,57,58,59,60,63,64}) = {62,66}. Here rules are labelled as follows: 1: atom#(Cons(x,xs)) -> c_1() 2: atom#(Nil()) -> c_2() 3: eqAlph#(Div(),Div()) -> c_3() 4: eqAlph#(Div(),LPar()) -> c_4() 5: eqAlph#(Div(),Minus()) -> c_5() 6: eqAlph#(Div(),Mul()) -> c_6() 7: eqAlph#(Div(),Plus()) -> c_7() 8: eqAlph#(Div(),RPar()) -> c_8() 9: eqAlph#(Div(),Val(int2)) -> c_9() 10: eqAlph#(LPar(),Div()) -> c_10() 11: eqAlph#(LPar(),LPar()) -> c_11() 12: eqAlph#(LPar(),Minus()) -> c_12() 13: eqAlph#(LPar(),Mul()) -> c_13() 14: eqAlph#(LPar(),Plus()) -> c_14() 15: eqAlph#(LPar(),RPar()) -> c_15() 16: eqAlph#(LPar(),Val(int2)) -> c_16() 17: eqAlph#(Minus(),Div()) -> c_17() 18: eqAlph#(Minus(),LPar()) -> c_18() 19: eqAlph#(Minus(),Minus()) -> c_19() 20: eqAlph#(Minus(),Mul()) -> c_20() 21: eqAlph#(Minus(),Plus()) -> c_21() 22: eqAlph#(Minus(),RPar()) -> c_22() 23: eqAlph#(Minus(),Val(int2)) -> c_23() 24: eqAlph#(Mul(),Div()) -> c_24() 25: eqAlph#(Mul(),LPar()) -> c_25() 26: eqAlph#(Mul(),Minus()) -> c_26() 27: eqAlph#(Mul(),Mul()) -> c_27() 28: eqAlph#(Mul(),Plus()) -> c_28() 29: eqAlph#(Mul(),RPar()) -> c_29() 30: eqAlph#(Mul(),Val(int2)) -> c_30() 31: eqAlph#(Plus(),Div()) -> c_31() 32: eqAlph#(Plus(),LPar()) -> c_32() 33: eqAlph#(Plus(),Minus()) -> c_33() 34: eqAlph#(Plus(),Mul()) -> c_34() 35: eqAlph#(Plus(),Plus()) -> c_35() 36: eqAlph#(Plus(),RPar()) -> c_36() 37: eqAlph#(Plus(),Val(int2)) -> c_37() 38: eqAlph#(RPar(),Div()) -> c_38() 39: eqAlph#(RPar(),LPar()) -> c_39() 40: eqAlph#(RPar(),Minus()) -> c_40() 41: eqAlph#(RPar(),Mul()) -> c_41() 42: eqAlph#(RPar(),Plus()) -> c_42() 43: eqAlph#(RPar(),RPar()) -> c_43() 44: eqAlph#(RPar(),Val(int2)) -> c_44() 45: eqAlph#(Val(int),Div()) -> c_45() 46: eqAlph#(Val(int),LPar()) -> c_46() 47: eqAlph#(Val(int),Minus()) -> c_47() 48: eqAlph#(Val(int),Mul()) -> c_48() 49: eqAlph#(Val(int),Plus()) -> c_49() 50: eqAlph#(Val(int),RPar()) -> c_50() 51: eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) 52: expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) 53: factor#(Cons(Div(),xs)) -> c_53() 54: factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) 55: factor#(Cons(Minus(),xs)) -> c_55() 56: factor#(Cons(Mul(),xs)) -> c_56() 57: factor#(Cons(Plus(),xs)) -> c_57() 58: factor#(Cons(RPar(),xs)) -> c_58() 59: factor#(Cons(Val(int),xs)) -> c_59() 60: head#(Cons(x,xs)) -> c_60() 61: member#(x,Nil()) -> c_61() 62: member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) 63: notEmpty#(Cons(x,xs)) -> c_63() 64: notEmpty#(Nil()) -> c_64() 65: parsexp#(xs) -> c_65(expr#(xs)) 66: term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) 67: !EQ#(0(),0()) -> c_67() 68: !EQ#(0(),S(y)) -> c_68() 69: !EQ#(S(x),0()) -> c_69() 70: !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) 71: and#(False(),False()) -> c_71() 72: and#(False(),True()) -> c_72() 73: and#(True(),False()) -> c_73() 74: and#(True(),True()) -> c_74() 75: expr[Let]#(xs,Nil()) -> c_75() 76: expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) 77: factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) 78: factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() 79: factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() 80: factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() 81: factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() 82: factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() 83: factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() 84: factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() 85: member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) 86: member[Ite][True][Ite]#(True(),x,xs) -> c_86() 87: term[Let]#(xs,Nil()) -> c_87() 88: term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) parsexp#(xs) -> c_65(expr#(xs)) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) - Weak DPs: !EQ#(0(),0()) -> c_67() !EQ#(0(),S(y)) -> c_68() !EQ#(S(x),0()) -> c_69() !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) and#(False(),False()) -> c_71() and#(False(),True()) -> c_72() and#(True(),False()) -> c_73() and#(True(),True()) -> c_74() atom#(Cons(x,xs)) -> c_1() atom#(Nil()) -> c_2() eqAlph#(Div(),Div()) -> c_3() eqAlph#(Div(),LPar()) -> c_4() eqAlph#(Div(),Minus()) -> c_5() eqAlph#(Div(),Mul()) -> c_6() eqAlph#(Div(),Plus()) -> c_7() eqAlph#(Div(),RPar()) -> c_8() eqAlph#(Div(),Val(int2)) -> c_9() eqAlph#(LPar(),Div()) -> c_10() eqAlph#(LPar(),LPar()) -> c_11() eqAlph#(LPar(),Minus()) -> c_12() eqAlph#(LPar(),Mul()) -> c_13() eqAlph#(LPar(),Plus()) -> c_14() eqAlph#(LPar(),RPar()) -> c_15() eqAlph#(LPar(),Val(int2)) -> c_16() eqAlph#(Minus(),Div()) -> c_17() eqAlph#(Minus(),LPar()) -> c_18() eqAlph#(Minus(),Minus()) -> c_19() eqAlph#(Minus(),Mul()) -> c_20() eqAlph#(Minus(),Plus()) -> c_21() eqAlph#(Minus(),RPar()) -> c_22() eqAlph#(Minus(),Val(int2)) -> c_23() eqAlph#(Mul(),Div()) -> c_24() eqAlph#(Mul(),LPar()) -> c_25() eqAlph#(Mul(),Minus()) -> c_26() eqAlph#(Mul(),Mul()) -> c_27() eqAlph#(Mul(),Plus()) -> c_28() eqAlph#(Mul(),RPar()) -> c_29() eqAlph#(Mul(),Val(int2)) -> c_30() eqAlph#(Plus(),Div()) -> c_31() eqAlph#(Plus(),LPar()) -> c_32() eqAlph#(Plus(),Minus()) -> c_33() eqAlph#(Plus(),Mul()) -> c_34() eqAlph#(Plus(),Plus()) -> c_35() eqAlph#(Plus(),RPar()) -> c_36() eqAlph#(Plus(),Val(int2)) -> c_37() eqAlph#(RPar(),Div()) -> c_38() eqAlph#(RPar(),LPar()) -> c_39() eqAlph#(RPar(),Minus()) -> c_40() eqAlph#(RPar(),Mul()) -> c_41() eqAlph#(RPar(),Plus()) -> c_42() eqAlph#(RPar(),RPar()) -> c_43() eqAlph#(RPar(),Val(int2)) -> c_44() eqAlph#(Val(int),Div()) -> c_45() eqAlph#(Val(int),LPar()) -> c_46() eqAlph#(Val(int),Minus()) -> c_47() eqAlph#(Val(int),Mul()) -> c_48() eqAlph#(Val(int),Plus()) -> c_49() eqAlph#(Val(int),RPar()) -> c_50() eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) expr[Let]#(xs,Nil()) -> c_75() expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) factor#(Cons(Div(),xs)) -> c_53() factor#(Cons(Minus(),xs)) -> c_55() factor#(Cons(Mul(),xs)) -> c_56() factor#(Cons(Plus(),xs)) -> c_57() factor#(Cons(RPar(),xs)) -> c_58() factor#(Cons(Val(int),xs)) -> c_59() factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() head#(Cons(x,xs)) -> c_60() member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_86() notEmpty#(Cons(x,xs)) -> c_63() notEmpty#(Nil()) -> c_64() term[Let]#(xs,Nil()) -> c_87() term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),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) eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() term(xs) -> term[Let](xs,factor(xs)) term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) - Signature: {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2 ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2,!EQ#/2,and#/2,atom#/1,eqAlph#/2,expr#/1 ,expr[Let]#/2,factor#/1,factor[Ite][True][Let]#/2,head#/1,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1 ,parsexp#/1,term#/1,term[Let]#/2} / {0/0,Cons/2,Div/0,False/0,LPar/0,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1 ,True/0,Val/1,expr[Let][Ite][False][Ite]/3,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3,c_1/0 ,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0 ,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0 ,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0 ,c_48/0,c_49/0,c_50/0,c_51/1,c_52/2,c_53/0,c_54/2,c_55/0,c_56/0,c_57/0,c_58/0,c_59/0,c_60/0,c_61/0,c_62/2 ,c_63/0,c_64/0,c_65/1,c_66/2,c_67/0,c_68/0,c_69/0,c_70/1,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/1,c_77/3 ,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0,c_83/0,c_84/0,c_85/1,c_86/0,c_87/0,c_88/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,atom#,eqAlph#,expr#,expr[Let]#,factor# ,factor[Ite][True][Let]#,head#,member#,member[Ite][True][Ite]#,notEmpty#,parsexp#,term# ,term[Let]#} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) -->_1 expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))):67 -->_2 term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)):6 -->_1 expr[Let]#(xs,Nil()) -> c_75():66 2:S:factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) -->_1 factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84():81 -->_1 factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83():80 -->_1 factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82():79 -->_1 factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81():78 -->_1 factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80():77 -->_1 factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79():76 -->_1 factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78():75 -->_1 factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())):74 -->_2 expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)):1 3:S:member#(x,Nil()) -> c_61() 4:S:member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) -->_1 member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)):83 -->_2 eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)):65 -->_1 member[Ite][True][Ite]#(True(),x,xs) -> c_86():84 -->_2 eqAlph#(Val(int),RPar()) -> c_50():64 -->_2 eqAlph#(Val(int),Plus()) -> c_49():63 -->_2 eqAlph#(Val(int),Mul()) -> c_48():62 -->_2 eqAlph#(Val(int),Minus()) -> c_47():61 -->_2 eqAlph#(Val(int),LPar()) -> c_46():60 -->_2 eqAlph#(Val(int),Div()) -> c_45():59 -->_2 eqAlph#(RPar(),Val(int2)) -> c_44():58 -->_2 eqAlph#(RPar(),RPar()) -> c_43():57 -->_2 eqAlph#(RPar(),Plus()) -> c_42():56 -->_2 eqAlph#(RPar(),Mul()) -> c_41():55 -->_2 eqAlph#(RPar(),Minus()) -> c_40():54 -->_2 eqAlph#(RPar(),LPar()) -> c_39():53 -->_2 eqAlph#(RPar(),Div()) -> c_38():52 -->_2 eqAlph#(Plus(),Val(int2)) -> c_37():51 -->_2 eqAlph#(Plus(),RPar()) -> c_36():50 -->_2 eqAlph#(Plus(),Plus()) -> c_35():49 -->_2 eqAlph#(Plus(),Mul()) -> c_34():48 -->_2 eqAlph#(Plus(),Minus()) -> c_33():47 -->_2 eqAlph#(Plus(),LPar()) -> c_32():46 -->_2 eqAlph#(Plus(),Div()) -> c_31():45 -->_2 eqAlph#(Mul(),Val(int2)) -> c_30():44 -->_2 eqAlph#(Mul(),RPar()) -> c_29():43 -->_2 eqAlph#(Mul(),Plus()) -> c_28():42 -->_2 eqAlph#(Mul(),Mul()) -> c_27():41 -->_2 eqAlph#(Mul(),Minus()) -> c_26():40 -->_2 eqAlph#(Mul(),LPar()) -> c_25():39 -->_2 eqAlph#(Mul(),Div()) -> c_24():38 -->_2 eqAlph#(Minus(),Val(int2)) -> c_23():37 -->_2 eqAlph#(Minus(),RPar()) -> c_22():36 -->_2 eqAlph#(Minus(),Plus()) -> c_21():35 -->_2 eqAlph#(Minus(),Mul()) -> c_20():34 -->_2 eqAlph#(Minus(),Minus()) -> c_19():33 -->_2 eqAlph#(Minus(),LPar()) -> c_18():32 -->_2 eqAlph#(Minus(),Div()) -> c_17():31 -->_2 eqAlph#(LPar(),Val(int2)) -> c_16():30 -->_2 eqAlph#(LPar(),RPar()) -> c_15():29 -->_2 eqAlph#(LPar(),Plus()) -> c_14():28 -->_2 eqAlph#(LPar(),Mul()) -> c_13():27 -->_2 eqAlph#(LPar(),Minus()) -> c_12():26 -->_2 eqAlph#(LPar(),LPar()) -> c_11():25 -->_2 eqAlph#(LPar(),Div()) -> c_10():24 -->_2 eqAlph#(Div(),Val(int2)) -> c_9():23 -->_2 eqAlph#(Div(),RPar()) -> c_8():22 -->_2 eqAlph#(Div(),Plus()) -> c_7():21 -->_2 eqAlph#(Div(),Mul()) -> c_6():20 -->_2 eqAlph#(Div(),Minus()) -> c_5():19 -->_2 eqAlph#(Div(),LPar()) -> c_4():18 -->_2 eqAlph#(Div(),Div()) -> c_3():17 5:S:parsexp#(xs) -> c_65(expr#(xs)) -->_1 expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)):1 6:S:term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) -->_1 term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))):88 -->_1 term[Let]#(xs,Nil()) -> c_87():87 -->_2 factor#(Cons(Val(int),xs)) -> c_59():73 -->_2 factor#(Cons(RPar(),xs)) -> c_58():72 -->_2 factor#(Cons(Plus(),xs)) -> c_57():71 -->_2 factor#(Cons(Mul(),xs)) -> c_56():70 -->_2 factor#(Cons(Minus(),xs)) -> c_55():69 -->_2 factor#(Cons(Div(),xs)) -> c_53():68 -->_2 factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))):2 7:W:!EQ#(0(),0()) -> c_67() 8:W:!EQ#(0(),S(y)) -> c_68() 9:W:!EQ#(S(x),0()) -> c_69() 10:W:!EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) -->_1 !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)):10 -->_1 !EQ#(S(x),0()) -> c_69():9 -->_1 !EQ#(0(),S(y)) -> c_68():8 -->_1 !EQ#(0(),0()) -> c_67():7 11:W:and#(False(),False()) -> c_71() 12:W:and#(False(),True()) -> c_72() 13:W:and#(True(),False()) -> c_73() 14:W:and#(True(),True()) -> c_74() 15:W:atom#(Cons(x,xs)) -> c_1() 16:W:atom#(Nil()) -> c_2() 17:W:eqAlph#(Div(),Div()) -> c_3() 18:W:eqAlph#(Div(),LPar()) -> c_4() 19:W:eqAlph#(Div(),Minus()) -> c_5() 20:W:eqAlph#(Div(),Mul()) -> c_6() 21:W:eqAlph#(Div(),Plus()) -> c_7() 22:W:eqAlph#(Div(),RPar()) -> c_8() 23:W:eqAlph#(Div(),Val(int2)) -> c_9() 24:W:eqAlph#(LPar(),Div()) -> c_10() 25:W:eqAlph#(LPar(),LPar()) -> c_11() 26:W:eqAlph#(LPar(),Minus()) -> c_12() 27:W:eqAlph#(LPar(),Mul()) -> c_13() 28:W:eqAlph#(LPar(),Plus()) -> c_14() 29:W:eqAlph#(LPar(),RPar()) -> c_15() 30:W:eqAlph#(LPar(),Val(int2)) -> c_16() 31:W:eqAlph#(Minus(),Div()) -> c_17() 32:W:eqAlph#(Minus(),LPar()) -> c_18() 33:W:eqAlph#(Minus(),Minus()) -> c_19() 34:W:eqAlph#(Minus(),Mul()) -> c_20() 35:W:eqAlph#(Minus(),Plus()) -> c_21() 36:W:eqAlph#(Minus(),RPar()) -> c_22() 37:W:eqAlph#(Minus(),Val(int2)) -> c_23() 38:W:eqAlph#(Mul(),Div()) -> c_24() 39:W:eqAlph#(Mul(),LPar()) -> c_25() 40:W:eqAlph#(Mul(),Minus()) -> c_26() 41:W:eqAlph#(Mul(),Mul()) -> c_27() 42:W:eqAlph#(Mul(),Plus()) -> c_28() 43:W:eqAlph#(Mul(),RPar()) -> c_29() 44:W:eqAlph#(Mul(),Val(int2)) -> c_30() 45:W:eqAlph#(Plus(),Div()) -> c_31() 46:W:eqAlph#(Plus(),LPar()) -> c_32() 47:W:eqAlph#(Plus(),Minus()) -> c_33() 48:W:eqAlph#(Plus(),Mul()) -> c_34() 49:W:eqAlph#(Plus(),Plus()) -> c_35() 50:W:eqAlph#(Plus(),RPar()) -> c_36() 51:W:eqAlph#(Plus(),Val(int2)) -> c_37() 52:W:eqAlph#(RPar(),Div()) -> c_38() 53:W:eqAlph#(RPar(),LPar()) -> c_39() 54:W:eqAlph#(RPar(),Minus()) -> c_40() 55:W:eqAlph#(RPar(),Mul()) -> c_41() 56:W:eqAlph#(RPar(),Plus()) -> c_42() 57:W:eqAlph#(RPar(),RPar()) -> c_43() 58:W:eqAlph#(RPar(),Val(int2)) -> c_44() 59:W:eqAlph#(Val(int),Div()) -> c_45() 60:W:eqAlph#(Val(int),LPar()) -> c_46() 61:W:eqAlph#(Val(int),Minus()) -> c_47() 62:W:eqAlph#(Val(int),Mul()) -> c_48() 63:W:eqAlph#(Val(int),Plus()) -> c_49() 64:W:eqAlph#(Val(int),RPar()) -> c_50() 65:W:eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) -->_1 !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)):10 -->_1 !EQ#(S(x),0()) -> c_69():9 -->_1 !EQ#(0(),S(y)) -> c_68():8 -->_1 !EQ#(0(),0()) -> c_67():7 66:W:expr[Let]#(xs,Nil()) -> c_75() 67:W:expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')):4 68:W:factor#(Cons(Div(),xs)) -> c_53() 69:W:factor#(Cons(Minus(),xs)) -> c_55() 70:W:factor#(Cons(Mul(),xs)) -> c_56() 71:W:factor#(Cons(Plus(),xs)) -> c_57() 72:W:factor#(Cons(RPar(),xs)) -> c_58() 73:W:factor#(Cons(Val(int),xs)) -> c_59() 74:W:factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) 75:W:factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() 76:W:factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() 77:W:factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() 78:W:factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() 79:W:factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() 80:W:factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() 81:W:factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() 82:W:head#(Cons(x,xs)) -> c_60() 83:W:member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')):4 -->_1 member#(x,Nil()) -> c_61():3 84:W:member[Ite][True][Ite]#(True(),x,xs) -> c_86() 85:W:notEmpty#(Cons(x,xs)) -> c_63() 86:W:notEmpty#(Nil()) -> c_64() 87:W:term[Let]#(xs,Nil()) -> c_87() 88:W:term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 86: notEmpty#(Nil()) -> c_64() 85: notEmpty#(Cons(x,xs)) -> c_63() 82: head#(Cons(x,xs)) -> c_60() 16: atom#(Nil()) -> c_2() 15: atom#(Cons(x,xs)) -> c_1() 14: and#(True(),True()) -> c_74() 13: and#(True(),False()) -> c_73() 12: and#(False(),True()) -> c_72() 11: and#(False(),False()) -> c_71() 66: expr[Let]#(xs,Nil()) -> c_75() 74: factor[Ite][True][Let]#(xs,Nil()) -> c_77(and#(False(),eqAlph(head(Nil()),RPar())) ,eqAlph#(head(Nil()),RPar()) ,head#(Nil())) 75: factor[Ite][True][Let]#(xs',Cons(Div(),xs)) -> c_78() 76: factor[Ite][True][Let]#(xs',Cons(LPar(),xs)) -> c_79() 77: factor[Ite][True][Let]#(xs',Cons(Minus(),xs)) -> c_80() 78: factor[Ite][True][Let]#(xs',Cons(Mul(),xs)) -> c_81() 79: factor[Ite][True][Let]#(xs',Cons(Plus(),xs)) -> c_82() 80: factor[Ite][True][Let]#(xs',Cons(RPar(),xs)) -> c_83() 81: factor[Ite][True][Let]#(xs',Cons(Val(int),xs)) -> c_84() 68: factor#(Cons(Div(),xs)) -> c_53() 69: factor#(Cons(Minus(),xs)) -> c_55() 70: factor#(Cons(Mul(),xs)) -> c_56() 71: factor#(Cons(Plus(),xs)) -> c_57() 72: factor#(Cons(RPar(),xs)) -> c_58() 73: factor#(Cons(Val(int),xs)) -> c_59() 87: term[Let]#(xs,Nil()) -> c_87() 17: eqAlph#(Div(),Div()) -> c_3() 18: eqAlph#(Div(),LPar()) -> c_4() 19: eqAlph#(Div(),Minus()) -> c_5() 20: eqAlph#(Div(),Mul()) -> c_6() 21: eqAlph#(Div(),Plus()) -> c_7() 22: eqAlph#(Div(),RPar()) -> c_8() 23: eqAlph#(Div(),Val(int2)) -> c_9() 24: eqAlph#(LPar(),Div()) -> c_10() 25: eqAlph#(LPar(),LPar()) -> c_11() 26: eqAlph#(LPar(),Minus()) -> c_12() 27: eqAlph#(LPar(),Mul()) -> c_13() 28: eqAlph#(LPar(),Plus()) -> c_14() 29: eqAlph#(LPar(),RPar()) -> c_15() 30: eqAlph#(LPar(),Val(int2)) -> c_16() 31: eqAlph#(Minus(),Div()) -> c_17() 32: eqAlph#(Minus(),LPar()) -> c_18() 33: eqAlph#(Minus(),Minus()) -> c_19() 34: eqAlph#(Minus(),Mul()) -> c_20() 35: eqAlph#(Minus(),Plus()) -> c_21() 36: eqAlph#(Minus(),RPar()) -> c_22() 37: eqAlph#(Minus(),Val(int2)) -> c_23() 38: eqAlph#(Mul(),Div()) -> c_24() 39: eqAlph#(Mul(),LPar()) -> c_25() 40: eqAlph#(Mul(),Minus()) -> c_26() 41: eqAlph#(Mul(),Mul()) -> c_27() 42: eqAlph#(Mul(),Plus()) -> c_28() 43: eqAlph#(Mul(),RPar()) -> c_29() 44: eqAlph#(Mul(),Val(int2)) -> c_30() 45: eqAlph#(Plus(),Div()) -> c_31() 46: eqAlph#(Plus(),LPar()) -> c_32() 47: eqAlph#(Plus(),Minus()) -> c_33() 48: eqAlph#(Plus(),Mul()) -> c_34() 49: eqAlph#(Plus(),Plus()) -> c_35() 50: eqAlph#(Plus(),RPar()) -> c_36() 51: eqAlph#(Plus(),Val(int2)) -> c_37() 52: eqAlph#(RPar(),Div()) -> c_38() 53: eqAlph#(RPar(),LPar()) -> c_39() 54: eqAlph#(RPar(),Minus()) -> c_40() 55: eqAlph#(RPar(),Mul()) -> c_41() 56: eqAlph#(RPar(),Plus()) -> c_42() 57: eqAlph#(RPar(),RPar()) -> c_43() 58: eqAlph#(RPar(),Val(int2)) -> c_44() 59: eqAlph#(Val(int),Div()) -> c_45() 60: eqAlph#(Val(int),LPar()) -> c_46() 61: eqAlph#(Val(int),Minus()) -> c_47() 62: eqAlph#(Val(int),Mul()) -> c_48() 63: eqAlph#(Val(int),Plus()) -> c_49() 64: eqAlph#(Val(int),RPar()) -> c_50() 84: member[Ite][True][Ite]#(True(),x,xs) -> c_86() 65: eqAlph#(Val(int),Val(int2)) -> c_51(!EQ#(int2,int)) 10: !EQ#(S(x),S(y)) -> c_70(!EQ#(x,y)) 7: !EQ#(0(),0()) -> c_67() 8: !EQ#(0(),S(y)) -> c_68() 9: !EQ#(S(x),0()) -> c_69() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) parsexp#(xs) -> c_65(expr#(xs)) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) - Weak DPs: expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),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) eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() term(xs) -> term[Let](xs,factor(xs)) term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) - Signature: {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2 ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2,!EQ#/2,and#/2,atom#/1,eqAlph#/2,expr#/1 ,expr[Let]#/2,factor#/1,factor[Ite][True][Let]#/2,head#/1,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1 ,parsexp#/1,term#/1,term[Let]#/2} / {0/0,Cons/2,Div/0,False/0,LPar/0,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1 ,True/0,Val/1,expr[Let][Ite][False][Ite]/3,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3,c_1/0 ,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0 ,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0 ,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0 ,c_48/0,c_49/0,c_50/0,c_51/1,c_52/2,c_53/0,c_54/2,c_55/0,c_56/0,c_57/0,c_58/0,c_59/0,c_60/0,c_61/0,c_62/2 ,c_63/0,c_64/0,c_65/1,c_66/2,c_67/0,c_68/0,c_69/0,c_70/1,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/1,c_77/3 ,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0,c_83/0,c_84/0,c_85/1,c_86/0,c_87/0,c_88/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,atom#,eqAlph#,expr#,expr[Let]#,factor# ,factor[Ite][True][Let]#,head#,member#,member[Ite][True][Ite]#,notEmpty#,parsexp#,term# ,term[Let]#} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) -->_1 expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))):67 -->_2 term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)):6 2:S:factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))) -->_2 expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)):1 3:S:member#(x,Nil()) -> c_61() 4:S:member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')) -->_1 member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)):83 5:S:parsexp#(xs) -> c_65(expr#(xs)) -->_1 expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)):1 6:S:term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) -->_1 term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))):88 -->_2 factor#(Cons(LPar(),xs)) -> c_54(factor[Ite][True][Let]#(Cons(LPar(),xs),expr(Cons(LPar(),xs))) ,expr#(Cons(LPar(),xs))):2 67:W:expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')):4 83:W:member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')):4 -->_1 member#(x,Nil()) -> c_61():3 88:W:term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs)),eqAlph#(x,x')):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: factor#(Cons(LPar(),xs)) -> c_54(expr#(Cons(LPar(),xs))) member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs))) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) factor#(Cons(LPar(),xs)) -> c_54(expr#(Cons(LPar(),xs))) member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs))) parsexp#(xs) -> c_65(expr#(xs)) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) - Weak DPs: expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),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) eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() term(xs) -> term[Let](xs,factor(xs)) term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) - Signature: {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2 ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2,!EQ#/2,and#/2,atom#/1,eqAlph#/2,expr#/1 ,expr[Let]#/2,factor#/1,factor[Ite][True][Let]#/2,head#/1,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1 ,parsexp#/1,term#/1,term[Let]#/2} / {0/0,Cons/2,Div/0,False/0,LPar/0,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1 ,True/0,Val/1,expr[Let][Ite][False][Ite]/3,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3,c_1/0 ,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0 ,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0 ,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0 ,c_48/0,c_49/0,c_50/0,c_51/1,c_52/2,c_53/0,c_54/1,c_55/0,c_56/0,c_57/0,c_58/0,c_59/0,c_60/0,c_61/0,c_62/1 ,c_63/0,c_64/0,c_65/1,c_66/2,c_67/0,c_68/0,c_69/0,c_70/1,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/1,c_77/3 ,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0,c_83/0,c_84/0,c_85/1,c_86/0,c_87/0,c_88/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,atom#,eqAlph#,expr#,expr[Let]#,factor# ,factor[Ite][True][Let]#,head#,member#,member[Ite][True][Ite]#,notEmpty#,parsexp#,term# ,term[Let]#} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) -->_1 expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))):7 -->_2 term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)):6 2:S:factor#(Cons(LPar(),xs)) -> c_54(expr#(Cons(LPar(),xs))) -->_1 expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)):1 3:S:member#(x,Nil()) -> c_61() 4:S:member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs))) -->_1 member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)):8 5:S:parsexp#(xs) -> c_65(expr#(xs)) -->_1 expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)):1 6:S:term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) -->_1 term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))):9 -->_2 factor#(Cons(LPar(),xs)) -> c_54(expr#(Cons(LPar(),xs))):2 7:W:expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs))):4 8:W:member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs))):4 -->_1 member#(x,Nil()) -> c_61():3 9:W:term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),Nil())))) -->_1 member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs))):4 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). [(5,parsexp#(xs) -> c_65(expr#(xs)))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: expr#(xs) -> c_52(expr[Let]#(xs,term(xs)),term#(xs)) factor#(Cons(LPar(),xs)) -> c_54(expr#(Cons(LPar(),xs))) member#(x,Nil()) -> c_61() member#(x',Cons(x,xs)) -> c_62(member[Ite][True][Ite]#(eqAlph(x,x'),x',Cons(x,xs))) term#(xs) -> c_66(term[Let]#(xs,factor(xs)),factor#(xs)) - Weak DPs: expr[Let]#(xs',Cons(x,xs)) -> c_76(member#(x,Cons(Plus(),Cons(Minus(),Nil())))) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_85(member#(x',xs)) term[Let]#(xs',Cons(x,xs)) -> c_88(member#(x,Cons(Mul(),Cons(Div(),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) eqAlph(Div(),Div()) -> True() eqAlph(Div(),LPar()) -> False() eqAlph(Div(),Minus()) -> False() eqAlph(Div(),Mul()) -> False() eqAlph(Div(),Plus()) -> False() eqAlph(Div(),RPar()) -> False() eqAlph(Div(),Val(int2)) -> False() eqAlph(LPar(),Div()) -> False() eqAlph(LPar(),LPar()) -> True() eqAlph(LPar(),Minus()) -> False() eqAlph(LPar(),Mul()) -> False() eqAlph(LPar(),Plus()) -> False() eqAlph(LPar(),RPar()) -> False() eqAlph(LPar(),Val(int2)) -> False() eqAlph(Minus(),Div()) -> False() eqAlph(Minus(),LPar()) -> False() eqAlph(Minus(),Minus()) -> True() eqAlph(Minus(),Mul()) -> False() eqAlph(Minus(),Plus()) -> False() eqAlph(Minus(),RPar()) -> False() eqAlph(Minus(),Val(int2)) -> False() eqAlph(Mul(),Div()) -> False() eqAlph(Mul(),LPar()) -> False() eqAlph(Mul(),Minus()) -> False() eqAlph(Mul(),Mul()) -> True() eqAlph(Mul(),Plus()) -> False() eqAlph(Mul(),RPar()) -> False() eqAlph(Mul(),Val(int2)) -> False() eqAlph(Plus(),Div()) -> False() eqAlph(Plus(),LPar()) -> False() eqAlph(Plus(),Minus()) -> False() eqAlph(Plus(),Mul()) -> False() eqAlph(Plus(),Plus()) -> True() eqAlph(Plus(),RPar()) -> False() eqAlph(Plus(),Val(int2)) -> False() eqAlph(RPar(),Div()) -> False() eqAlph(RPar(),LPar()) -> False() eqAlph(RPar(),Minus()) -> False() eqAlph(RPar(),Mul()) -> False() eqAlph(RPar(),Plus()) -> False() eqAlph(RPar(),RPar()) -> True() eqAlph(RPar(),Val(int2)) -> False() eqAlph(Val(int),Div()) -> False() eqAlph(Val(int),LPar()) -> False() eqAlph(Val(int),Minus()) -> False() eqAlph(Val(int),Mul()) -> False() eqAlph(Val(int),Plus()) -> False() eqAlph(Val(int),RPar()) -> False() eqAlph(Val(int),Val(int2)) -> !EQ(int2,int) expr(xs) -> expr[Let](xs,term(xs)) expr[Let](xs,Nil()) -> Nil() expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil()))) ,xs' ,Cons(x,xs)) factor(Cons(Div(),xs)) -> xs factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs))) factor(Cons(Minus(),xs)) -> xs factor(Cons(Mul(),xs)) -> xs factor(Cons(Plus(),xs)) -> xs factor(Cons(RPar(),xs)) -> xs factor(Cons(Val(int),xs)) -> xs factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar())) ,xs ,Nil()) factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs)) factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs)) factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs)) factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs)) factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs)) factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs)) factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs)) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() term(xs) -> term[Let](xs,factor(xs)) term[Let](xs,Nil()) -> Nil() term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil()))) ,xs' ,Cons(x,xs)) - Signature: {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2 ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2,!EQ#/2,and#/2,atom#/1,eqAlph#/2,expr#/1 ,expr[Let]#/2,factor#/1,factor[Ite][True][Let]#/2,head#/1,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1 ,parsexp#/1,term#/1,term[Let]#/2} / {0/0,Cons/2,Div/0,False/0,LPar/0,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1 ,True/0,Val/1,expr[Let][Ite][False][Ite]/3,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3,c_1/0 ,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0 ,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0 ,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/0,c_46/0,c_47/0 ,c_48/0,c_49/0,c_50/0,c_51/1,c_52/2,c_53/0,c_54/1,c_55/0,c_56/0,c_57/0,c_58/0,c_59/0,c_60/0,c_61/0,c_62/1 ,c_63/0,c_64/0,c_65/1,c_66/2,c_67/0,c_68/0,c_69/0,c_70/1,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/1,c_77/3 ,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0,c_83/0,c_84/0,c_85/1,c_86/0,c_87/0,c_88/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,atom#,eqAlph#,expr#,expr[Let]#,factor# ,factor[Ite][True][Let]#,head#,member#,member[Ite][True][Ite]#,notEmpty#,parsexp#,term# ,term[Let]#} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE