*** Error in `z3': free(): corrupted unsorted chunks: 0x00000000020ea2f0 *** /bin/sh: line 1: 25157 Segmentation fault (core dumped) z3 -T:1.5 -smt2 /tmp/SMTP24310-18 > /tmp/SMTS24310-19 WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPLY(z0,z1,z2) -> c188(APPLY[ITE](eqExp(z1,z2),z0,z1,z2),EQEXP(z1,z2)) CHECKCONSTREXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c164() CHECKCONSTREXP(Bsf(z0,z1,z2),Eq(z3,z4)) -> c162() CHECKCONSTREXP(Bsf(z0,z1,z2),Error(z3,z4)) -> c158() CHECKCONSTREXP(Bsf(z0,z1,z2),F()) -> c159() CHECKCONSTREXP(Bsf(z0,z1,z2),Fun(z3,z4)) -> c161() CHECKCONSTREXP(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> c163() CHECKCONSTREXP(Bsf(z0,z1,z2),T()) -> c160() CHECKCONSTREXP(Bsf(z0,z1,z2),Var(z3)) -> c165() CHECKCONSTREXP(Eq(z0,z1),Bsf(z2,z3,z4)) -> c148() CHECKCONSTREXP(Eq(z0,z1),Eq(z2,z3)) -> c146() CHECKCONSTREXP(Eq(z0,z1),Error(z2,z3)) -> c142() CHECKCONSTREXP(Eq(z0,z1),F()) -> c143() CHECKCONSTREXP(Eq(z0,z1),Fun(z2,z3)) -> c145() CHECKCONSTREXP(Eq(z0,z1),ITE(z2,z3,z4)) -> c147() CHECKCONSTREXP(Eq(z0,z1),T()) -> c144() CHECKCONSTREXP(Eq(z0,z1),Var(z2)) -> c149() CHECKCONSTREXP(Error(z0,z1),Bsf(z2,z3,z4)) -> c116() CHECKCONSTREXP(Error(z0,z1),Eq(z2,z3)) -> c114() CHECKCONSTREXP(Error(z0,z1),Error(z2,z3)) -> c110() CHECKCONSTREXP(Error(z0,z1),F()) -> c111() CHECKCONSTREXP(Error(z0,z1),Fun(z2,z3)) -> c113() CHECKCONSTREXP(Error(z0,z1),ITE(z2,z3,z4)) -> c115() CHECKCONSTREXP(Error(z0,z1),T()) -> c112() CHECKCONSTREXP(Error(z0,z1),Var(z2)) -> c117() CHECKCONSTREXP(F(),Bsf(z0,z1,z2)) -> c124() CHECKCONSTREXP(F(),Eq(z0,z1)) -> c122() CHECKCONSTREXP(F(),Error(z0,z1)) -> c118() CHECKCONSTREXP(F(),F()) -> c119() CHECKCONSTREXP(F(),Fun(z0,z1)) -> c121() CHECKCONSTREXP(F(),ITE(z0,z1,z2)) -> c123() CHECKCONSTREXP(F(),T()) -> c120() CHECKCONSTREXP(F(),Var(z0)) -> c125() CHECKCONSTREXP(Fun(z0,z1),Bsf(z2,z3,z4)) -> c140() CHECKCONSTREXP(Fun(z0,z1),Eq(z2,z3)) -> c138() CHECKCONSTREXP(Fun(z0,z1),Error(z2,z3)) -> c134() CHECKCONSTREXP(Fun(z0,z1),F()) -> c135() CHECKCONSTREXP(Fun(z0,z1),Fun(z2,z3)) -> c137() CHECKCONSTREXP(Fun(z0,z1),ITE(z2,z3,z4)) -> c139() CHECKCONSTREXP(Fun(z0,z1),T()) -> c136() CHECKCONSTREXP(Fun(z0,z1),Var(z2)) -> c141() CHECKCONSTREXP(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> c156() CHECKCONSTREXP(ITE(z0,z1,z2),Eq(z3,z4)) -> c154() CHECKCONSTREXP(ITE(z0,z1,z2),Error(z3,z4)) -> c150() CHECKCONSTREXP(ITE(z0,z1,z2),F()) -> c151() CHECKCONSTREXP(ITE(z0,z1,z2),Fun(z3,z4)) -> c153() CHECKCONSTREXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c155() CHECKCONSTREXP(ITE(z0,z1,z2),T()) -> c152() CHECKCONSTREXP(ITE(z0,z1,z2),Var(z3)) -> c157() CHECKCONSTREXP(T(),Bsf(z0,z1,z2)) -> c132() CHECKCONSTREXP(T(),Eq(z0,z1)) -> c130() CHECKCONSTREXP(T(),Error(z0,z1)) -> c126() CHECKCONSTREXP(T(),F()) -> c127() CHECKCONSTREXP(T(),Fun(z0,z1)) -> c129() CHECKCONSTREXP(T(),ITE(z0,z1,z2)) -> c131() CHECKCONSTREXP(T(),T()) -> c128() CHECKCONSTREXP(T(),Var(z0)) -> c133() CHECKCONSTREXP(Var(z0),Bsf(z1,z2,z3)) -> c172() CHECKCONSTREXP(Var(z0),Eq(z1,z2)) -> c170() CHECKCONSTREXP(Var(z0),Error(z1,z2)) -> c166() CHECKCONSTREXP(Var(z0),F()) -> c167() CHECKCONSTREXP(Var(z0),Fun(z1,z2)) -> c169() CHECKCONSTREXP(Var(z0),ITE(z1,z2,z3)) -> c171() CHECKCONSTREXP(Var(z0),T()) -> c168() CHECKCONSTREXP(Var(z0),Var(z1)) -> c173() EEVAL(Bsf(z0,z1,z2),z3,z4,z5) -> c37(EEVAL[LET](Bsf(z0,z1,z2),z3,z4,z5,eeval(z1,z3,z4,z5)) ,EEVAL(z1,z3,z4,z5)) EEVAL(Eq(z0,z1),z2,z3,z4) -> c31(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z0,z2,z3,z4)) EEVAL(Eq(z0,z1),z2,z3,z4) -> c32(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL(Error(z0,z1),z2,z3,z4) -> c33(EEVAL[FALSE][ITE](False(),Error(z0,z1),z2,z3,z4)) EEVAL(F(),z0,z1,z2) -> c34() EEVAL(Fun(z0,z1),z2,z3,z4) -> c30(EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)),LOOKBODY(z0,z4)) EEVAL(ITE(z0,z1,z2),z3,z4,z5) -> c36(EEVAL[ITE](checkConstrExp(eeval(z0,z3,z4,z5),T()) ,ITE(z0,z1,z2) ,z3 ,z4 ,z5) ,CHECKCONSTREXP(eeval(z0,z3,z4,z5),T()) ,EEVAL(z0,z3,z4,z5)) EEVAL(T(),z0,z1,z2) -> c35() EEVAL(Var(z0),z1,z2,z3) -> c38(LOOKVAR(z0,z1,z2)) EQEXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c100(AND(True(),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z2,z5)) EQEXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c99(AND(True(),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z1,z4)) EQEXP(Bsf(z0,z1,z2),Eq(z3,z4)) -> c97() EQEXP(Bsf(z0,z1,z2),Error(z3,z4)) -> c93() EQEXP(Bsf(z0,z1,z2),F()) -> c94() EQEXP(Bsf(z0,z1,z2),Fun(z3,z4)) -> c96() EQEXP(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> c98() EQEXP(Bsf(z0,z1,z2),T()) -> c95() EQEXP(Bsf(z0,z1,z2),Var(z3)) -> c101() EQEXP(Eq(z0,z1),Bsf(z2,z3,z4)) -> c81() EQEXP(Eq(z0,z1),Eq(z2,z3)) -> c78(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z0,z2)) EQEXP(Eq(z0,z1),Eq(z2,z3)) -> c79(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Eq(z0,z1),Error(z2,z3)) -> c74() EQEXP(Eq(z0,z1),F()) -> c75() EQEXP(Eq(z0,z1),Fun(z2,z3)) -> c77() EQEXP(Eq(z0,z1),ITE(z2,z3,z4)) -> c80() EQEXP(Eq(z0,z1),T()) -> c76() EQEXP(Eq(z0,z1),Var(z2)) -> c82() EQEXP(Error(z0,z1),Bsf(z2,z3,z4)) -> c47() EQEXP(Error(z0,z1),Eq(z2,z3)) -> c45() EQEXP(Error(z0,z1),Error(z2,z3)) -> c40(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z0,z2)) EQEXP(Error(z0,z1),Error(z2,z3)) -> c41(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Error(z0,z1),F()) -> c42() EQEXP(Error(z0,z1),Fun(z2,z3)) -> c44() EQEXP(Error(z0,z1),ITE(z2,z3,z4)) -> c46() EQEXP(Error(z0,z1),T()) -> c43() EQEXP(Error(z0,z1),Var(z2)) -> c48() EQEXP(F(),Bsf(z0,z1,z2)) -> c55() EQEXP(F(),Eq(z0,z1)) -> c53() EQEXP(F(),Error(z0,z1)) -> c49() EQEXP(F(),F()) -> c50() EQEXP(F(),Fun(z0,z1)) -> c52() EQEXP(F(),ITE(z0,z1,z2)) -> c54() EQEXP(F(),T()) -> c51() EQEXP(F(),Var(z0)) -> c56() EQEXP(Fun(z0,z1),Bsf(z2,z3,z4)) -> c72() EQEXP(Fun(z0,z1),Eq(z2,z3)) -> c70() EQEXP(Fun(z0,z1),Error(z2,z3)) -> c65() EQEXP(Fun(z0,z1),F()) -> c66() EQEXP(Fun(z0,z1),Fun(z2,z3)) -> c68(AND(!EQ(z0,z2),eqExp(z1,z3)),!EQ'(z0,z2)) EQEXP(Fun(z0,z1),Fun(z2,z3)) -> c69(AND(!EQ(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Fun(z0,z1),ITE(z2,z3,z4)) -> c71() EQEXP(Fun(z0,z1),T()) -> c67() EQEXP(Fun(z0,z1),Var(z2)) -> c73() EQEXP(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> c91() EQEXP(ITE(z0,z1,z2),Eq(z3,z4)) -> c87() EQEXP(ITE(z0,z1,z2),Error(z3,z4)) -> c83() EQEXP(ITE(z0,z1,z2),F()) -> c84() EQEXP(ITE(z0,z1,z2),Fun(z3,z4)) -> c86() EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c88(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))),EQEXP(z0,z3)) EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c89(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z1,z4)) EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c90(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z2,z5)) EQEXP(ITE(z0,z1,z2),T()) -> c85() EQEXP(ITE(z0,z1,z2),Var(z3)) -> c92() EQEXP(T(),Bsf(z0,z1,z2)) -> c63() EQEXP(T(),Eq(z0,z1)) -> c61() EQEXP(T(),Error(z0,z1)) -> c57() EQEXP(T(),F()) -> c58() EQEXP(T(),Fun(z0,z1)) -> c60() EQEXP(T(),ITE(z0,z1,z2)) -> c62() EQEXP(T(),T()) -> c59() EQEXP(T(),Var(z0)) -> c64() EQEXP(Var(z0),Bsf(z1,z2,z3)) -> c108() EQEXP(Var(z0),Eq(z1,z2)) -> c106() EQEXP(Var(z0),Error(z1,z2)) -> c102() EQEXP(Var(z0),F()) -> c103() EQEXP(Var(z0),Fun(z1,z2)) -> c105() EQEXP(Var(z0),ITE(z1,z2,z3)) -> c107() EQEXP(Var(z0),T()) -> c104() EQEXP(Var(z0),Var(z1)) -> c109(!EQ'(z0,z1)) EQOPS(z0,z1) -> c190() GETBSFFIRSTTERM(Bsf(z0,z1,z2)) -> c187() GETBSFOP(Bsf(z0,z1,z2)) -> c186() GETBSFSECONDTERM(Bsf(z0,z1,z2)) -> c185() GETCONST(Cst(z0)) -> c184() GETEQFIRST(Eq(z0,z1)) -> c183() GETEQSECOND(Eq(z0,z1)) -> c182() GETFUNCEXP(Fun(z0,z1)) -> c181() GETFUNCNAME(Fun(z0,z1)) -> c180() GETIFFALSE(ITE(z0,z1,z2)) -> c179() GETIFGUARD(ITE(z0,z1,z2)) -> c178() GETIFTRUE(ITE(z0,z1,z2)) -> c177() GETVAR(Var(z0)) -> c176() LOOKBODY(z0,Cons(Fun(z1,z2),z3)) -> c175(LOOKBODY[ITE](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)),!EQ'(z0,z1)) LOOKNAME(z0,Cons(Fun(z1,z2),z3)) -> c174(LOOKNAME[ITE](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)),!EQ'(z0,z1)) LOOKVAR(z0,Cons(z1,z2),z3) -> c189(LOOKVAR[ITE](!EQ(z0,z1),z0,Cons(z1,z2),z3),!EQ'(z0,z1)) RUN(Cons(Fun(z0,z1),z2),z3) -> c39(RUN[LET][LET](Cons(Fun(z0,z1),z2),z3,z0,lookbody(z0,Cons(Fun(z0,z1),z2))) ,LOOKBODY(z0,Cons(Fun(z0,z1),z2))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c3() !EQ'(0(),S(z0)) -> c1() !EQ'(S(z0),0()) -> c2() !EQ'(S(z0),S(z1)) -> c(!EQ'(z0,z1)) AND(False(),False()) -> c4() AND(False(),True()) -> c6() AND(True(),False()) -> c5() AND(True(),True()) -> c7() APPLY[ITE](False(),z0,z1,z2) -> c25() APPLY[ITE](True(),z0,z1,z2) -> c26() EEVAL[FALSE][ITE](False(),Fun(z0,z1),z2,z3,z4) -> c10(EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) ,LOOKBODY(z0,z4)) EEVAL[FALSE][ITE](True(),Eq(z0,z1),z2,z3,z4) -> c8(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z0,z2,z3,z4)) EEVAL[FALSE][ITE](True(),Eq(z0,z1),z2,z3,z4) -> c9(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,z5) -> c19(EEVAL[FALSE][LET][LET](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,lookname(z0,z4)) ,LOOKNAME(z0,z4)) EEVAL[FALSE][LET][LET](Fun(z0,z1),z2,z3,z4,z5,z6) -> c20(EEVAL[LET][LET][LET](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,z6 ,eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL[ITE](False(),ITE(z0,z1,z2),z3,z4,z5) -> c17(EEVAL(z2,z3,z4,z5)) EEVAL[ITE](True(),ITE(z0,z1,z2),z3,z4,z5) -> c18(EEVAL(z1,z3,z4,z5)) EEVAL[LET](Bsf(z0,z1,z2),z3,z4,z5,z6) -> c21(EEVAL[LET][LET](Bsf(z0,z1,z2),z3,z4,z5,z6,eeval(z2,z3,z4,z5)) ,EEVAL(z2,z3,z4,z5)) EEVAL[LET][LET](Bsf(z0,z1,z2),z3,z4,z5,z6,z7) -> c22(APPLY(z0,z6,z7)) EEVAL[LET][LET][LET](z0,z1,z2,z3,z4,z5,z6) -> c29(EEVAL(z4,Cons(z5,Nil()),Cons(z6,Nil()),z3)) EEVAL[TRUE][ITE](False(),z0,z1,z2,z3) -> c23() EEVAL[TRUE][ITE](True(),z0,z1,z2,z3) -> c24() LOOKBODY[ITE](False(),z0,Cons(z1,z2)) -> c16(LOOKBODY(z0,z2)) LOOKBODY[ITE](True(),z0,Cons(Fun(z1,z2),z3)) -> c15() LOOKNAME[ITE](False(),z0,Cons(z1,z2)) -> c14(LOOKNAME(z0,z2)) LOOKNAME[ITE](True(),z0,Cons(Fun(z1,z2),z3)) -> c13() LOOKVAR[ITE](False(),z0,Cons(z1,z2),Cons(z3,z4)) -> c11(LOOKVAR(z0,z2,z4)) LOOKVAR[ITE](True(),z0,z1,Cons(z2,z3)) -> c12() RUN[LET](z0,z1,z2,z3,z4) -> c28(EEVAL(z3,Cons(z4,Nil()),Cons(z1,Nil()),z0)) RUN[LET][LET](z0,z1,z2,z3) -> c27(RUN[LET](z0,z1,z2,z3,lookname(z2,z0)),LOOKNAME(z2,z0)) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() apply(z0,z1,z2) -> apply[Ite](eqExp(z1,z2),z0,z1,z2) apply[Ite](False(),z0,z1,z2) -> F() apply[Ite](True(),z0,z1,z2) -> T() checkConstrExp(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> True() checkConstrExp(Bsf(z0,z1,z2),Eq(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),Error(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),F()) -> False() checkConstrExp(Bsf(z0,z1,z2),Fun(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> False() checkConstrExp(Bsf(z0,z1,z2),T()) -> False() checkConstrExp(Bsf(z0,z1,z2),Var(z3)) -> False() checkConstrExp(Eq(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Eq(z0,z1),Eq(z2,z3)) -> True() checkConstrExp(Eq(z0,z1),Error(z2,z3)) -> False() checkConstrExp(Eq(z0,z1),F()) -> False() checkConstrExp(Eq(z0,z1),Fun(z2,z3)) -> False() checkConstrExp(Eq(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Eq(z0,z1),T()) -> False() checkConstrExp(Eq(z0,z1),Var(z2)) -> False() checkConstrExp(Error(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Error(z0,z1),Eq(z2,z3)) -> False() checkConstrExp(Error(z0,z1),Error(z2,z3)) -> True() checkConstrExp(Error(z0,z1),F()) -> False() checkConstrExp(Error(z0,z1),Fun(z2,z3)) -> False() checkConstrExp(Error(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Error(z0,z1),T()) -> False() checkConstrExp(Error(z0,z1),Var(z2)) -> False() checkConstrExp(F(),Bsf(z0,z1,z2)) -> False() checkConstrExp(F(),Eq(z0,z1)) -> False() checkConstrExp(F(),Error(z0,z1)) -> False() checkConstrExp(F(),F()) -> True() checkConstrExp(F(),Fun(z0,z1)) -> False() checkConstrExp(F(),ITE(z0,z1,z2)) -> False() checkConstrExp(F(),T()) -> False() checkConstrExp(F(),Var(z0)) -> False() checkConstrExp(Fun(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Fun(z0,z1),Eq(z2,z3)) -> False() checkConstrExp(Fun(z0,z1),Error(z2,z3)) -> False() checkConstrExp(Fun(z0,z1),F()) -> False() checkConstrExp(Fun(z0,z1),Fun(z2,z3)) -> True() checkConstrExp(Fun(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Fun(z0,z1),T()) -> False() checkConstrExp(Fun(z0,z1),Var(z2)) -> False() checkConstrExp(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> False() checkConstrExp(ITE(z0,z1,z2),Eq(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),Error(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),F()) -> False() checkConstrExp(ITE(z0,z1,z2),Fun(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> True() checkConstrExp(ITE(z0,z1,z2),T()) -> False() checkConstrExp(ITE(z0,z1,z2),Var(z3)) -> False() checkConstrExp(T(),Bsf(z0,z1,z2)) -> False() checkConstrExp(T(),Eq(z0,z1)) -> False() checkConstrExp(T(),Error(z0,z1)) -> False() checkConstrExp(T(),F()) -> False() checkConstrExp(T(),Fun(z0,z1)) -> False() checkConstrExp(T(),ITE(z0,z1,z2)) -> False() checkConstrExp(T(),T()) -> True() checkConstrExp(T(),Var(z0)) -> False() checkConstrExp(Var(z0),Bsf(z1,z2,z3)) -> False() checkConstrExp(Var(z0),Eq(z1,z2)) -> False() checkConstrExp(Var(z0),Error(z1,z2)) -> False() checkConstrExp(Var(z0),F()) -> False() checkConstrExp(Var(z0),Fun(z1,z2)) -> False() checkConstrExp(Var(z0),ITE(z1,z2,z3)) -> False() checkConstrExp(Var(z0),T()) -> False() checkConstrExp(Var(z0),Var(z1)) -> True() eeval(Bsf(z0,z1,z2),z3,z4,z5) -> eeval[Let](Bsf(z0,z1,z2),z3,z4,z5,eeval(z1,z3,z4,z5)) eeval(Eq(z0,z1),z2,z3,z4) -> eeval[True][Ite](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) eeval(Error(z0,z1),z2,z3,z4) -> eeval[False][Ite](False(),Error(z0,z1),z2,z3,z4) eeval(F(),z0,z1,z2) -> F() eeval(Fun(z0,z1),z2,z3,z4) -> eeval[False][Let](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) eeval(ITE(z0,z1,z2),z3,z4,z5) -> eeval[Ite](checkConstrExp(eeval(z0,z3,z4,z5),T()),ITE(z0,z1,z2),z3,z4,z5) eeval(T(),z0,z1,z2) -> T() eeval(Var(z0),z1,z2,z3) -> lookvar(z0,z1,z2) eeval[False][Ite](False(),Fun(z0,z1),z2,z3,z4) -> eeval[False][Let](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) eeval[False][Ite](True(),Eq(z0,z1),z2,z3,z4) -> eeval[True][Ite](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) eeval[False][Let](Fun(z0,z1),z2,z3,z4,z5) -> eeval[False][Let][Let](Fun(z0,z1),z2,z3,z4,z5,lookname(z0,z4)) eeval[False][Let][Let](Fun(z0,z1),z2,z3,z4,z5,z6) -> eeval[Let][Let][Let](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,z6 ,eeval(z1,z2,z3,z4)) eeval[Ite](False(),ITE(z0,z1,z2),z3,z4,z5) -> eeval(z2,z3,z4,z5) eeval[Ite](True(),ITE(z0,z1,z2),z3,z4,z5) -> eeval(z1,z3,z4,z5) eeval[Let](Bsf(z0,z1,z2),z3,z4,z5,z6) -> eeval[Let][Let](Bsf(z0,z1,z2),z3,z4,z5,z6,eeval(z2,z3,z4,z5)) eeval[Let][Let](Bsf(z0,z1,z2),z3,z4,z5,z6,z7) -> apply(z0,z6,z7) eeval[Let][Let][Let](z0,z1,z2,z3,z4,z5,z6) -> eeval(z4,Cons(z5,Nil()),Cons(z6,Nil()),z3) eeval[True][Ite](False(),z0,z1,z2,z3) -> F() eeval[True][Ite](True(),z0,z1,z2,z3) -> T() eqExp(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> and(True(),and(eqExp(z1,z4),eqExp(z2,z5))) eqExp(Bsf(z0,z1,z2),Eq(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),Error(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),F()) -> False() eqExp(Bsf(z0,z1,z2),Fun(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> False() eqExp(Bsf(z0,z1,z2),T()) -> False() eqExp(Bsf(z0,z1,z2),Var(z3)) -> False() eqExp(Eq(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Eq(z0,z1),Eq(z2,z3)) -> and(eqExp(z0,z2),eqExp(z1,z3)) eqExp(Eq(z0,z1),Error(z2,z3)) -> False() eqExp(Eq(z0,z1),F()) -> False() eqExp(Eq(z0,z1),Fun(z2,z3)) -> False() eqExp(Eq(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Eq(z0,z1),T()) -> False() eqExp(Eq(z0,z1),Var(z2)) -> False() eqExp(Error(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Error(z0,z1),Eq(z2,z3)) -> False() eqExp(Error(z0,z1),Error(z2,z3)) -> and(eqExp(z0,z2),eqExp(z1,z3)) eqExp(Error(z0,z1),F()) -> False() eqExp(Error(z0,z1),Fun(z2,z3)) -> False() eqExp(Error(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Error(z0,z1),T()) -> False() eqExp(Error(z0,z1),Var(z2)) -> False() eqExp(F(),Bsf(z0,z1,z2)) -> False() eqExp(F(),Eq(z0,z1)) -> False() eqExp(F(),Error(z0,z1)) -> False() eqExp(F(),F()) -> True() eqExp(F(),Fun(z0,z1)) -> False() eqExp(F(),ITE(z0,z1,z2)) -> False() eqExp(F(),T()) -> False() eqExp(F(),Var(z0)) -> False() eqExp(Fun(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Fun(z0,z1),Eq(z2,z3)) -> False() eqExp(Fun(z0,z1),Error(z2,z3)) -> False() eqExp(Fun(z0,z1),F()) -> False() eqExp(Fun(z0,z1),Fun(z2,z3)) -> and(!EQ(z0,z2),eqExp(z1,z3)) eqExp(Fun(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Fun(z0,z1),T()) -> False() eqExp(Fun(z0,z1),Var(z2)) -> False() eqExp(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> False() eqExp(ITE(z0,z1,z2),Eq(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),Error(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),F()) -> False() eqExp(ITE(z0,z1,z2),Fun(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> and(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) eqExp(ITE(z0,z1,z2),T()) -> False() eqExp(ITE(z0,z1,z2),Var(z3)) -> False() eqExp(T(),Bsf(z0,z1,z2)) -> False() eqExp(T(),Eq(z0,z1)) -> False() eqExp(T(),Error(z0,z1)) -> False() eqExp(T(),F()) -> False() eqExp(T(),Fun(z0,z1)) -> False() eqExp(T(),ITE(z0,z1,z2)) -> False() eqExp(T(),T()) -> True() eqExp(T(),Var(z0)) -> False() eqExp(Var(z0),Bsf(z1,z2,z3)) -> False() eqExp(Var(z0),Eq(z1,z2)) -> False() eqExp(Var(z0),Error(z1,z2)) -> False() eqExp(Var(z0),F()) -> False() eqExp(Var(z0),Fun(z1,z2)) -> False() eqExp(Var(z0),ITE(z1,z2,z3)) -> False() eqExp(Var(z0),T()) -> False() eqExp(Var(z0),Var(z1)) -> !EQ(z0,z1) eqOps(z0,z1) -> True() getBsfFirstTerm(Bsf(z0,z1,z2)) -> z1 getBsfOp(Bsf(z0,z1,z2)) -> z0 getBsfSecondTerm(Bsf(z0,z1,z2)) -> z2 getConst(Cst(z0)) -> z0 getEqFirst(Eq(z0,z1)) -> z0 getEqSecond(Eq(z0,z1)) -> z1 getFuncExp(Fun(z0,z1)) -> z1 getFuncName(Fun(z0,z1)) -> z0 getIfFalse(ITE(z0,z1,z2)) -> z2 getIfGuard(ITE(z0,z1,z2)) -> z0 getIfTrue(ITE(z0,z1,z2)) -> z1 getVar(Var(z0)) -> z0 lookbody(z0,Cons(Fun(z1,z2),z3)) -> lookbody[Ite](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)) lookbody[Ite](False(),z0,Cons(z1,z2)) -> lookbody(z0,z2) lookbody[Ite](True(),z0,Cons(Fun(z1,z2),z3)) -> z2 lookname(z0,Cons(Fun(z1,z2),z3)) -> lookname[Ite](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)) lookname[Ite](False(),z0,Cons(z1,z2)) -> lookname(z0,z2) lookname[Ite](True(),z0,Cons(Fun(z1,z2),z3)) -> z1 lookvar(z0,Cons(z1,z2),z3) -> lookvar[Ite](!EQ(z0,z1),z0,Cons(z1,z2),z3) lookvar[Ite](False(),z0,Cons(z1,z2),Cons(z3,z4)) -> lookvar(z0,z2,z4) lookvar[Ite](True(),z0,z1,Cons(z2,z3)) -> z2 run(Cons(Fun(z0,z1),z2),z3) -> run[Let][Let](Cons(Fun(z0,z1),z2),z3,z0,lookbody(z0,Cons(Fun(z0,z1),z2))) run[Let](z0,z1,z2,z3,z4) -> eeval(z3,Cons(z4,Nil()),Cons(z1,Nil()),z0) run[Let][Let](z0,z1,z2,z3) -> run[Let](z0,z1,z2,z3,lookname(z2,z0)) - Signature: {!EQ/2,!EQ'/2,AND/2,APPLY/3,APPLY[ITE]/4,CHECKCONSTREXP/2,EEVAL/4,EEVAL[FALSE][ITE]/5,EEVAL[FALSE][LET]/5 ,EEVAL[FALSE][LET][LET]/6,EEVAL[ITE]/5,EEVAL[LET]/5,EEVAL[LET][LET]/6,EEVAL[LET][LET][LET]/7 ,EEVAL[TRUE][ITE]/5,EQEXP/2,EQOPS/2,GETBSFFIRSTTERM/1,GETBSFOP/1,GETBSFSECONDTERM/1,GETCONST/1,GETEQFIRST/1 ,GETEQSECOND/1,GETFUNCEXP/1,GETFUNCNAME/1,GETIFFALSE/1,GETIFGUARD/1,GETIFTRUE/1,GETVAR/1,LOOKBODY/2 ,LOOKBODY[ITE]/3,LOOKNAME/2,LOOKNAME[ITE]/3,LOOKVAR/3,LOOKVAR[ITE]/4,RUN/2,RUN[LET]/5,RUN[LET][LET]/4,and/2 ,apply/3,apply[Ite]/4,checkConstrExp/2,eeval/4,eeval[False][Ite]/5,eeval[False][Let]/5 ,eeval[False][Let][Let]/6,eeval[Ite]/5,eeval[Let]/5,eeval[Let][Let]/6,eeval[Let][Let][Let]/7 ,eeval[True][Ite]/5,eqExp/2,eqOps/2,getBsfFirstTerm/1,getBsfOp/1,getBsfSecondTerm/1,getConst/1,getEqFirst/1 ,getEqSecond/1,getFuncExp/1,getFuncName/1,getIfFalse/1,getIfGuard/1,getIfTrue/1,getVar/1,lookbody/2 ,lookbody[Ite]/3,lookname/2,lookname[Ite]/3,lookvar/3,lookvar[Ite]/4,run/2,run[Let]/5 ,run[Let][Let]/4} / {0/0,Bsf/3,Cons/2,Cst/1,Eq/2,Error/2,F/0,False/0,Fun/2,ITE/3,Nil/0,S/1,T/0,True/0,Var/1 ,c/1,c1/0,c10/2,c100/3,c101/0,c102/0,c103/0,c104/0,c105/0,c106/0,c107/0,c108/0,c109/1,c11/1,c110/0,c111/0 ,c112/0,c113/0,c114/0,c115/0,c116/0,c117/0,c118/0,c119/0,c12/0,c120/0,c121/0,c122/0,c123/0,c124/0,c125/0 ,c126/0,c127/0,c128/0,c129/0,c13/0,c130/0,c131/0,c132/0,c133/0,c134/0,c135/0,c136/0,c137/0,c138/0,c139/0 ,c14/1,c140/0,c141/0,c142/0,c143/0,c144/0,c145/0,c146/0,c147/0,c148/0,c149/0,c15/0,c150/0,c151/0,c152/0 ,c153/0,c154/0,c155/0,c156/0,c157/0,c158/0,c159/0,c16/1,c160/0,c161/0,c162/0,c163/0,c164/0,c165/0,c166/0 ,c167/0,c168/0,c169/0,c17/1,c170/0,c171/0,c172/0,c173/0,c174/2,c175/2,c176/0,c177/0,c178/0,c179/0,c18/1 ,c180/0,c181/0,c182/0,c183/0,c184/0,c185/0,c186/0,c187/0,c188/2,c189/2,c19/2,c190/0,c2/0,c20/2,c21/2,c22/1 ,c23/0,c24/0,c25/0,c26/0,c27/2,c28/1,c29/1,c3/0,c30/2,c31/3,c32/3,c33/1,c34/0,c35/0,c36/3,c37/2,c38/1,c39/2 ,c4/0,c40/2,c41/2,c42/0,c43/0,c44/0,c45/0,c46/0,c47/0,c48/0,c49/0,c5/0,c50/0,c51/0,c52/0,c53/0,c54/0,c55/0 ,c56/0,c57/0,c58/0,c59/0,c6/0,c60/0,c61/0,c62/0,c63/0,c64/0,c65/0,c66/0,c67/0,c68/2,c69/2,c7/0,c70/0,c71/0 ,c72/0,c73/0,c74/0,c75/0,c76/0,c77/0,c78/2,c79/2,c8/3,c80/0,c81/0,c82/0,c83/0,c84/0,c85/0,c86/0,c87/0,c88/2 ,c89/3,c9/3,c90/3,c91/0,c92/0,c93/0,c94/0,c95/0,c96/0,c97/0,c98/0,c99/3} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,APPLY,APPLY[ITE],CHECKCONSTREXP,EEVAL ,EEVAL[FALSE][ITE],EEVAL[FALSE][LET],EEVAL[FALSE][LET][LET],EEVAL[ITE],EEVAL[LET],EEVAL[LET][LET] ,EEVAL[LET][LET][LET],EEVAL[TRUE][ITE],EQEXP,EQOPS,GETBSFFIRSTTERM,GETBSFOP,GETBSFSECONDTERM,GETCONST ,GETEQFIRST,GETEQSECOND,GETFUNCEXP,GETFUNCNAME,GETIFFALSE,GETIFGUARD,GETIFTRUE,GETVAR,LOOKBODY,LOOKBODY[ITE] ,LOOKNAME,LOOKNAME[ITE],LOOKVAR,LOOKVAR[ITE],RUN,RUN[LET],RUN[LET][LET],and,apply,apply[Ite],checkConstrExp ,eeval,eeval[False][Ite],eeval[False][Let],eeval[False][Let][Let],eeval[Ite],eeval[Let],eeval[Let][Let] ,eeval[Let][Let][Let],eeval[True][Ite],eqExp,eqOps,getBsfFirstTerm,getBsfOp,getBsfSecondTerm,getConst ,getEqFirst,getEqSecond,getFuncExp,getFuncName,getIfFalse,getIfGuard,getIfTrue,getVar,lookbody,lookbody[Ite] ,lookname,lookname[Ite],lookvar,lookvar[Ite],run,run[Let],run[Let][Let]} and constructors {0,Bsf,Cons,Cst,Eq ,Error,F,False,Fun,ITE,Nil,S,T,True,Var,c,c1,c10,c100,c101,c102,c103,c104,c105,c106,c107,c108,c109,c11,c110 ,c111,c112,c113,c114,c115,c116,c117,c118,c119,c12,c120,c121,c122,c123,c124,c125,c126,c127,c128,c129,c13,c130 ,c131,c132,c133,c134,c135,c136,c137,c138,c139,c14,c140,c141,c142,c143,c144,c145,c146,c147,c148,c149,c15,c150 ,c151,c152,c153,c154,c155,c156,c157,c158,c159,c16,c160,c161,c162,c163,c164,c165,c166,c167,c168,c169,c17,c170 ,c171,c172,c173,c174,c175,c176,c177,c178,c179,c18,c180,c181,c182,c183,c184,c185,c186,c187,c188,c189,c19,c190 ,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43 ,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68 ,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83,c84,c85,c86,c87,c88,c89,c9,c90,c91,c92 ,c93,c94,c95,c96,c97,c98,c99} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPLY(z0,z1,z2) -> c188(APPLY[ITE](eqExp(z1,z2),z0,z1,z2),EQEXP(z1,z2)) CHECKCONSTREXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c164() CHECKCONSTREXP(Bsf(z0,z1,z2),Eq(z3,z4)) -> c162() CHECKCONSTREXP(Bsf(z0,z1,z2),Error(z3,z4)) -> c158() CHECKCONSTREXP(Bsf(z0,z1,z2),F()) -> c159() CHECKCONSTREXP(Bsf(z0,z1,z2),Fun(z3,z4)) -> c161() CHECKCONSTREXP(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> c163() CHECKCONSTREXP(Bsf(z0,z1,z2),T()) -> c160() CHECKCONSTREXP(Bsf(z0,z1,z2),Var(z3)) -> c165() CHECKCONSTREXP(Eq(z0,z1),Bsf(z2,z3,z4)) -> c148() CHECKCONSTREXP(Eq(z0,z1),Eq(z2,z3)) -> c146() CHECKCONSTREXP(Eq(z0,z1),Error(z2,z3)) -> c142() CHECKCONSTREXP(Eq(z0,z1),F()) -> c143() CHECKCONSTREXP(Eq(z0,z1),Fun(z2,z3)) -> c145() CHECKCONSTREXP(Eq(z0,z1),ITE(z2,z3,z4)) -> c147() CHECKCONSTREXP(Eq(z0,z1),T()) -> c144() CHECKCONSTREXP(Eq(z0,z1),Var(z2)) -> c149() CHECKCONSTREXP(Error(z0,z1),Bsf(z2,z3,z4)) -> c116() CHECKCONSTREXP(Error(z0,z1),Eq(z2,z3)) -> c114() CHECKCONSTREXP(Error(z0,z1),Error(z2,z3)) -> c110() CHECKCONSTREXP(Error(z0,z1),F()) -> c111() CHECKCONSTREXP(Error(z0,z1),Fun(z2,z3)) -> c113() CHECKCONSTREXP(Error(z0,z1),ITE(z2,z3,z4)) -> c115() CHECKCONSTREXP(Error(z0,z1),T()) -> c112() CHECKCONSTREXP(Error(z0,z1),Var(z2)) -> c117() CHECKCONSTREXP(F(),Bsf(z0,z1,z2)) -> c124() CHECKCONSTREXP(F(),Eq(z0,z1)) -> c122() CHECKCONSTREXP(F(),Error(z0,z1)) -> c118() CHECKCONSTREXP(F(),F()) -> c119() CHECKCONSTREXP(F(),Fun(z0,z1)) -> c121() CHECKCONSTREXP(F(),ITE(z0,z1,z2)) -> c123() CHECKCONSTREXP(F(),T()) -> c120() CHECKCONSTREXP(F(),Var(z0)) -> c125() CHECKCONSTREXP(Fun(z0,z1),Bsf(z2,z3,z4)) -> c140() CHECKCONSTREXP(Fun(z0,z1),Eq(z2,z3)) -> c138() CHECKCONSTREXP(Fun(z0,z1),Error(z2,z3)) -> c134() CHECKCONSTREXP(Fun(z0,z1),F()) -> c135() CHECKCONSTREXP(Fun(z0,z1),Fun(z2,z3)) -> c137() CHECKCONSTREXP(Fun(z0,z1),ITE(z2,z3,z4)) -> c139() CHECKCONSTREXP(Fun(z0,z1),T()) -> c136() CHECKCONSTREXP(Fun(z0,z1),Var(z2)) -> c141() CHECKCONSTREXP(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> c156() CHECKCONSTREXP(ITE(z0,z1,z2),Eq(z3,z4)) -> c154() CHECKCONSTREXP(ITE(z0,z1,z2),Error(z3,z4)) -> c150() CHECKCONSTREXP(ITE(z0,z1,z2),F()) -> c151() CHECKCONSTREXP(ITE(z0,z1,z2),Fun(z3,z4)) -> c153() CHECKCONSTREXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c155() CHECKCONSTREXP(ITE(z0,z1,z2),T()) -> c152() CHECKCONSTREXP(ITE(z0,z1,z2),Var(z3)) -> c157() CHECKCONSTREXP(T(),Bsf(z0,z1,z2)) -> c132() CHECKCONSTREXP(T(),Eq(z0,z1)) -> c130() CHECKCONSTREXP(T(),Error(z0,z1)) -> c126() CHECKCONSTREXP(T(),F()) -> c127() CHECKCONSTREXP(T(),Fun(z0,z1)) -> c129() CHECKCONSTREXP(T(),ITE(z0,z1,z2)) -> c131() CHECKCONSTREXP(T(),T()) -> c128() CHECKCONSTREXP(T(),Var(z0)) -> c133() CHECKCONSTREXP(Var(z0),Bsf(z1,z2,z3)) -> c172() CHECKCONSTREXP(Var(z0),Eq(z1,z2)) -> c170() CHECKCONSTREXP(Var(z0),Error(z1,z2)) -> c166() CHECKCONSTREXP(Var(z0),F()) -> c167() CHECKCONSTREXP(Var(z0),Fun(z1,z2)) -> c169() CHECKCONSTREXP(Var(z0),ITE(z1,z2,z3)) -> c171() CHECKCONSTREXP(Var(z0),T()) -> c168() CHECKCONSTREXP(Var(z0),Var(z1)) -> c173() EEVAL(Bsf(z0,z1,z2),z3,z4,z5) -> c37(EEVAL[LET](Bsf(z0,z1,z2),z3,z4,z5,eeval(z1,z3,z4,z5)) ,EEVAL(z1,z3,z4,z5)) EEVAL(Eq(z0,z1),z2,z3,z4) -> c31(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z0,z2,z3,z4)) EEVAL(Eq(z0,z1),z2,z3,z4) -> c32(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL(Error(z0,z1),z2,z3,z4) -> c33(EEVAL[FALSE][ITE](False(),Error(z0,z1),z2,z3,z4)) EEVAL(F(),z0,z1,z2) -> c34() EEVAL(Fun(z0,z1),z2,z3,z4) -> c30(EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)),LOOKBODY(z0,z4)) EEVAL(ITE(z0,z1,z2),z3,z4,z5) -> c36(EEVAL[ITE](checkConstrExp(eeval(z0,z3,z4,z5),T()) ,ITE(z0,z1,z2) ,z3 ,z4 ,z5) ,CHECKCONSTREXP(eeval(z0,z3,z4,z5),T()) ,EEVAL(z0,z3,z4,z5)) EEVAL(T(),z0,z1,z2) -> c35() EEVAL(Var(z0),z1,z2,z3) -> c38(LOOKVAR(z0,z1,z2)) EQEXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c100(AND(True(),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z2,z5)) EQEXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c99(AND(True(),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z1,z4)) EQEXP(Bsf(z0,z1,z2),Eq(z3,z4)) -> c97() EQEXP(Bsf(z0,z1,z2),Error(z3,z4)) -> c93() EQEXP(Bsf(z0,z1,z2),F()) -> c94() EQEXP(Bsf(z0,z1,z2),Fun(z3,z4)) -> c96() EQEXP(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> c98() EQEXP(Bsf(z0,z1,z2),T()) -> c95() EQEXP(Bsf(z0,z1,z2),Var(z3)) -> c101() EQEXP(Eq(z0,z1),Bsf(z2,z3,z4)) -> c81() EQEXP(Eq(z0,z1),Eq(z2,z3)) -> c78(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z0,z2)) EQEXP(Eq(z0,z1),Eq(z2,z3)) -> c79(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Eq(z0,z1),Error(z2,z3)) -> c74() EQEXP(Eq(z0,z1),F()) -> c75() EQEXP(Eq(z0,z1),Fun(z2,z3)) -> c77() EQEXP(Eq(z0,z1),ITE(z2,z3,z4)) -> c80() EQEXP(Eq(z0,z1),T()) -> c76() EQEXP(Eq(z0,z1),Var(z2)) -> c82() EQEXP(Error(z0,z1),Bsf(z2,z3,z4)) -> c47() EQEXP(Error(z0,z1),Eq(z2,z3)) -> c45() EQEXP(Error(z0,z1),Error(z2,z3)) -> c40(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z0,z2)) EQEXP(Error(z0,z1),Error(z2,z3)) -> c41(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Error(z0,z1),F()) -> c42() EQEXP(Error(z0,z1),Fun(z2,z3)) -> c44() EQEXP(Error(z0,z1),ITE(z2,z3,z4)) -> c46() EQEXP(Error(z0,z1),T()) -> c43() EQEXP(Error(z0,z1),Var(z2)) -> c48() EQEXP(F(),Bsf(z0,z1,z2)) -> c55() EQEXP(F(),Eq(z0,z1)) -> c53() EQEXP(F(),Error(z0,z1)) -> c49() EQEXP(F(),F()) -> c50() EQEXP(F(),Fun(z0,z1)) -> c52() EQEXP(F(),ITE(z0,z1,z2)) -> c54() EQEXP(F(),T()) -> c51() EQEXP(F(),Var(z0)) -> c56() EQEXP(Fun(z0,z1),Bsf(z2,z3,z4)) -> c72() EQEXP(Fun(z0,z1),Eq(z2,z3)) -> c70() EQEXP(Fun(z0,z1),Error(z2,z3)) -> c65() EQEXP(Fun(z0,z1),F()) -> c66() EQEXP(Fun(z0,z1),Fun(z2,z3)) -> c68(AND(!EQ(z0,z2),eqExp(z1,z3)),!EQ'(z0,z2)) EQEXP(Fun(z0,z1),Fun(z2,z3)) -> c69(AND(!EQ(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Fun(z0,z1),ITE(z2,z3,z4)) -> c71() EQEXP(Fun(z0,z1),T()) -> c67() EQEXP(Fun(z0,z1),Var(z2)) -> c73() EQEXP(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> c91() EQEXP(ITE(z0,z1,z2),Eq(z3,z4)) -> c87() EQEXP(ITE(z0,z1,z2),Error(z3,z4)) -> c83() EQEXP(ITE(z0,z1,z2),F()) -> c84() EQEXP(ITE(z0,z1,z2),Fun(z3,z4)) -> c86() EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c88(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))),EQEXP(z0,z3)) EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c89(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z1,z4)) EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c90(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z2,z5)) EQEXP(ITE(z0,z1,z2),T()) -> c85() EQEXP(ITE(z0,z1,z2),Var(z3)) -> c92() EQEXP(T(),Bsf(z0,z1,z2)) -> c63() EQEXP(T(),Eq(z0,z1)) -> c61() EQEXP(T(),Error(z0,z1)) -> c57() EQEXP(T(),F()) -> c58() EQEXP(T(),Fun(z0,z1)) -> c60() EQEXP(T(),ITE(z0,z1,z2)) -> c62() EQEXP(T(),T()) -> c59() EQEXP(T(),Var(z0)) -> c64() EQEXP(Var(z0),Bsf(z1,z2,z3)) -> c108() EQEXP(Var(z0),Eq(z1,z2)) -> c106() EQEXP(Var(z0),Error(z1,z2)) -> c102() EQEXP(Var(z0),F()) -> c103() EQEXP(Var(z0),Fun(z1,z2)) -> c105() EQEXP(Var(z0),ITE(z1,z2,z3)) -> c107() EQEXP(Var(z0),T()) -> c104() EQEXP(Var(z0),Var(z1)) -> c109(!EQ'(z0,z1)) EQOPS(z0,z1) -> c190() GETBSFFIRSTTERM(Bsf(z0,z1,z2)) -> c187() GETBSFOP(Bsf(z0,z1,z2)) -> c186() GETBSFSECONDTERM(Bsf(z0,z1,z2)) -> c185() GETCONST(Cst(z0)) -> c184() GETEQFIRST(Eq(z0,z1)) -> c183() GETEQSECOND(Eq(z0,z1)) -> c182() GETFUNCEXP(Fun(z0,z1)) -> c181() GETFUNCNAME(Fun(z0,z1)) -> c180() GETIFFALSE(ITE(z0,z1,z2)) -> c179() GETIFGUARD(ITE(z0,z1,z2)) -> c178() GETIFTRUE(ITE(z0,z1,z2)) -> c177() GETVAR(Var(z0)) -> c176() LOOKBODY(z0,Cons(Fun(z1,z2),z3)) -> c175(LOOKBODY[ITE](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)),!EQ'(z0,z1)) LOOKNAME(z0,Cons(Fun(z1,z2),z3)) -> c174(LOOKNAME[ITE](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)),!EQ'(z0,z1)) LOOKVAR(z0,Cons(z1,z2),z3) -> c189(LOOKVAR[ITE](!EQ(z0,z1),z0,Cons(z1,z2),z3),!EQ'(z0,z1)) RUN(Cons(Fun(z0,z1),z2),z3) -> c39(RUN[LET][LET](Cons(Fun(z0,z1),z2),z3,z0,lookbody(z0,Cons(Fun(z0,z1),z2))) ,LOOKBODY(z0,Cons(Fun(z0,z1),z2))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c3() !EQ'(0(),S(z0)) -> c1() !EQ'(S(z0),0()) -> c2() !EQ'(S(z0),S(z1)) -> c(!EQ'(z0,z1)) AND(False(),False()) -> c4() AND(False(),True()) -> c6() AND(True(),False()) -> c5() AND(True(),True()) -> c7() APPLY[ITE](False(),z0,z1,z2) -> c25() APPLY[ITE](True(),z0,z1,z2) -> c26() EEVAL[FALSE][ITE](False(),Fun(z0,z1),z2,z3,z4) -> c10(EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) ,LOOKBODY(z0,z4)) EEVAL[FALSE][ITE](True(),Eq(z0,z1),z2,z3,z4) -> c8(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z0,z2,z3,z4)) EEVAL[FALSE][ITE](True(),Eq(z0,z1),z2,z3,z4) -> c9(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,z5) -> c19(EEVAL[FALSE][LET][LET](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,lookname(z0,z4)) ,LOOKNAME(z0,z4)) EEVAL[FALSE][LET][LET](Fun(z0,z1),z2,z3,z4,z5,z6) -> c20(EEVAL[LET][LET][LET](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,z6 ,eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL[ITE](False(),ITE(z0,z1,z2),z3,z4,z5) -> c17(EEVAL(z2,z3,z4,z5)) EEVAL[ITE](True(),ITE(z0,z1,z2),z3,z4,z5) -> c18(EEVAL(z1,z3,z4,z5)) EEVAL[LET](Bsf(z0,z1,z2),z3,z4,z5,z6) -> c21(EEVAL[LET][LET](Bsf(z0,z1,z2),z3,z4,z5,z6,eeval(z2,z3,z4,z5)) ,EEVAL(z2,z3,z4,z5)) EEVAL[LET][LET](Bsf(z0,z1,z2),z3,z4,z5,z6,z7) -> c22(APPLY(z0,z6,z7)) EEVAL[LET][LET][LET](z0,z1,z2,z3,z4,z5,z6) -> c29(EEVAL(z4,Cons(z5,Nil()),Cons(z6,Nil()),z3)) EEVAL[TRUE][ITE](False(),z0,z1,z2,z3) -> c23() EEVAL[TRUE][ITE](True(),z0,z1,z2,z3) -> c24() LOOKBODY[ITE](False(),z0,Cons(z1,z2)) -> c16(LOOKBODY(z0,z2)) LOOKBODY[ITE](True(),z0,Cons(Fun(z1,z2),z3)) -> c15() LOOKNAME[ITE](False(),z0,Cons(z1,z2)) -> c14(LOOKNAME(z0,z2)) LOOKNAME[ITE](True(),z0,Cons(Fun(z1,z2),z3)) -> c13() LOOKVAR[ITE](False(),z0,Cons(z1,z2),Cons(z3,z4)) -> c11(LOOKVAR(z0,z2,z4)) LOOKVAR[ITE](True(),z0,z1,Cons(z2,z3)) -> c12() RUN[LET](z0,z1,z2,z3,z4) -> c28(EEVAL(z3,Cons(z4,Nil()),Cons(z1,Nil()),z0)) RUN[LET][LET](z0,z1,z2,z3) -> c27(RUN[LET](z0,z1,z2,z3,lookname(z2,z0)),LOOKNAME(z2,z0)) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() apply(z0,z1,z2) -> apply[Ite](eqExp(z1,z2),z0,z1,z2) apply[Ite](False(),z0,z1,z2) -> F() apply[Ite](True(),z0,z1,z2) -> T() checkConstrExp(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> True() checkConstrExp(Bsf(z0,z1,z2),Eq(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),Error(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),F()) -> False() checkConstrExp(Bsf(z0,z1,z2),Fun(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> False() checkConstrExp(Bsf(z0,z1,z2),T()) -> False() checkConstrExp(Bsf(z0,z1,z2),Var(z3)) -> False() checkConstrExp(Eq(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Eq(z0,z1),Eq(z2,z3)) -> True() checkConstrExp(Eq(z0,z1),Error(z2,z3)) -> False() checkConstrExp(Eq(z0,z1),F()) -> False() checkConstrExp(Eq(z0,z1),Fun(z2,z3)) -> False() checkConstrExp(Eq(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Eq(z0,z1),T()) -> False() checkConstrExp(Eq(z0,z1),Var(z2)) -> False() checkConstrExp(Error(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Error(z0,z1),Eq(z2,z3)) -> False() checkConstrExp(Error(z0,z1),Error(z2,z3)) -> True() checkConstrExp(Error(z0,z1),F()) -> False() checkConstrExp(Error(z0,z1),Fun(z2,z3)) -> False() checkConstrExp(Error(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Error(z0,z1),T()) -> False() checkConstrExp(Error(z0,z1),Var(z2)) -> False() checkConstrExp(F(),Bsf(z0,z1,z2)) -> False() checkConstrExp(F(),Eq(z0,z1)) -> False() checkConstrExp(F(),Error(z0,z1)) -> False() checkConstrExp(F(),F()) -> True() checkConstrExp(F(),Fun(z0,z1)) -> False() checkConstrExp(F(),ITE(z0,z1,z2)) -> False() checkConstrExp(F(),T()) -> False() checkConstrExp(F(),Var(z0)) -> False() checkConstrExp(Fun(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Fun(z0,z1),Eq(z2,z3)) -> False() checkConstrExp(Fun(z0,z1),Error(z2,z3)) -> False() checkConstrExp(Fun(z0,z1),F()) -> False() checkConstrExp(Fun(z0,z1),Fun(z2,z3)) -> True() checkConstrExp(Fun(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Fun(z0,z1),T()) -> False() checkConstrExp(Fun(z0,z1),Var(z2)) -> False() checkConstrExp(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> False() checkConstrExp(ITE(z0,z1,z2),Eq(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),Error(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),F()) -> False() checkConstrExp(ITE(z0,z1,z2),Fun(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> True() checkConstrExp(ITE(z0,z1,z2),T()) -> False() checkConstrExp(ITE(z0,z1,z2),Var(z3)) -> False() checkConstrExp(T(),Bsf(z0,z1,z2)) -> False() checkConstrExp(T(),Eq(z0,z1)) -> False() checkConstrExp(T(),Error(z0,z1)) -> False() checkConstrExp(T(),F()) -> False() checkConstrExp(T(),Fun(z0,z1)) -> False() checkConstrExp(T(),ITE(z0,z1,z2)) -> False() checkConstrExp(T(),T()) -> True() checkConstrExp(T(),Var(z0)) -> False() checkConstrExp(Var(z0),Bsf(z1,z2,z3)) -> False() checkConstrExp(Var(z0),Eq(z1,z2)) -> False() checkConstrExp(Var(z0),Error(z1,z2)) -> False() checkConstrExp(Var(z0),F()) -> False() checkConstrExp(Var(z0),Fun(z1,z2)) -> False() checkConstrExp(Var(z0),ITE(z1,z2,z3)) -> False() checkConstrExp(Var(z0),T()) -> False() checkConstrExp(Var(z0),Var(z1)) -> True() eeval(Bsf(z0,z1,z2),z3,z4,z5) -> eeval[Let](Bsf(z0,z1,z2),z3,z4,z5,eeval(z1,z3,z4,z5)) eeval(Eq(z0,z1),z2,z3,z4) -> eeval[True][Ite](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) eeval(Error(z0,z1),z2,z3,z4) -> eeval[False][Ite](False(),Error(z0,z1),z2,z3,z4) eeval(F(),z0,z1,z2) -> F() eeval(Fun(z0,z1),z2,z3,z4) -> eeval[False][Let](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) eeval(ITE(z0,z1,z2),z3,z4,z5) -> eeval[Ite](checkConstrExp(eeval(z0,z3,z4,z5),T()),ITE(z0,z1,z2),z3,z4,z5) eeval(T(),z0,z1,z2) -> T() eeval(Var(z0),z1,z2,z3) -> lookvar(z0,z1,z2) eeval[False][Ite](False(),Fun(z0,z1),z2,z3,z4) -> eeval[False][Let](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) eeval[False][Ite](True(),Eq(z0,z1),z2,z3,z4) -> eeval[True][Ite](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) eeval[False][Let](Fun(z0,z1),z2,z3,z4,z5) -> eeval[False][Let][Let](Fun(z0,z1),z2,z3,z4,z5,lookname(z0,z4)) eeval[False][Let][Let](Fun(z0,z1),z2,z3,z4,z5,z6) -> eeval[Let][Let][Let](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,z6 ,eeval(z1,z2,z3,z4)) eeval[Ite](False(),ITE(z0,z1,z2),z3,z4,z5) -> eeval(z2,z3,z4,z5) eeval[Ite](True(),ITE(z0,z1,z2),z3,z4,z5) -> eeval(z1,z3,z4,z5) eeval[Let](Bsf(z0,z1,z2),z3,z4,z5,z6) -> eeval[Let][Let](Bsf(z0,z1,z2),z3,z4,z5,z6,eeval(z2,z3,z4,z5)) eeval[Let][Let](Bsf(z0,z1,z2),z3,z4,z5,z6,z7) -> apply(z0,z6,z7) eeval[Let][Let][Let](z0,z1,z2,z3,z4,z5,z6) -> eeval(z4,Cons(z5,Nil()),Cons(z6,Nil()),z3) eeval[True][Ite](False(),z0,z1,z2,z3) -> F() eeval[True][Ite](True(),z0,z1,z2,z3) -> T() eqExp(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> and(True(),and(eqExp(z1,z4),eqExp(z2,z5))) eqExp(Bsf(z0,z1,z2),Eq(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),Error(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),F()) -> False() eqExp(Bsf(z0,z1,z2),Fun(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> False() eqExp(Bsf(z0,z1,z2),T()) -> False() eqExp(Bsf(z0,z1,z2),Var(z3)) -> False() eqExp(Eq(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Eq(z0,z1),Eq(z2,z3)) -> and(eqExp(z0,z2),eqExp(z1,z3)) eqExp(Eq(z0,z1),Error(z2,z3)) -> False() eqExp(Eq(z0,z1),F()) -> False() eqExp(Eq(z0,z1),Fun(z2,z3)) -> False() eqExp(Eq(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Eq(z0,z1),T()) -> False() eqExp(Eq(z0,z1),Var(z2)) -> False() eqExp(Error(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Error(z0,z1),Eq(z2,z3)) -> False() eqExp(Error(z0,z1),Error(z2,z3)) -> and(eqExp(z0,z2),eqExp(z1,z3)) eqExp(Error(z0,z1),F()) -> False() eqExp(Error(z0,z1),Fun(z2,z3)) -> False() eqExp(Error(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Error(z0,z1),T()) -> False() eqExp(Error(z0,z1),Var(z2)) -> False() eqExp(F(),Bsf(z0,z1,z2)) -> False() eqExp(F(),Eq(z0,z1)) -> False() eqExp(F(),Error(z0,z1)) -> False() eqExp(F(),F()) -> True() eqExp(F(),Fun(z0,z1)) -> False() eqExp(F(),ITE(z0,z1,z2)) -> False() eqExp(F(),T()) -> False() eqExp(F(),Var(z0)) -> False() eqExp(Fun(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Fun(z0,z1),Eq(z2,z3)) -> False() eqExp(Fun(z0,z1),Error(z2,z3)) -> False() eqExp(Fun(z0,z1),F()) -> False() eqExp(Fun(z0,z1),Fun(z2,z3)) -> and(!EQ(z0,z2),eqExp(z1,z3)) eqExp(Fun(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Fun(z0,z1),T()) -> False() eqExp(Fun(z0,z1),Var(z2)) -> False() eqExp(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> False() eqExp(ITE(z0,z1,z2),Eq(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),Error(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),F()) -> False() eqExp(ITE(z0,z1,z2),Fun(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> and(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) eqExp(ITE(z0,z1,z2),T()) -> False() eqExp(ITE(z0,z1,z2),Var(z3)) -> False() eqExp(T(),Bsf(z0,z1,z2)) -> False() eqExp(T(),Eq(z0,z1)) -> False() eqExp(T(),Error(z0,z1)) -> False() eqExp(T(),F()) -> False() eqExp(T(),Fun(z0,z1)) -> False() eqExp(T(),ITE(z0,z1,z2)) -> False() eqExp(T(),T()) -> True() eqExp(T(),Var(z0)) -> False() eqExp(Var(z0),Bsf(z1,z2,z3)) -> False() eqExp(Var(z0),Eq(z1,z2)) -> False() eqExp(Var(z0),Error(z1,z2)) -> False() eqExp(Var(z0),F()) -> False() eqExp(Var(z0),Fun(z1,z2)) -> False() eqExp(Var(z0),ITE(z1,z2,z3)) -> False() eqExp(Var(z0),T()) -> False() eqExp(Var(z0),Var(z1)) -> !EQ(z0,z1) eqOps(z0,z1) -> True() getBsfFirstTerm(Bsf(z0,z1,z2)) -> z1 getBsfOp(Bsf(z0,z1,z2)) -> z0 getBsfSecondTerm(Bsf(z0,z1,z2)) -> z2 getConst(Cst(z0)) -> z0 getEqFirst(Eq(z0,z1)) -> z0 getEqSecond(Eq(z0,z1)) -> z1 getFuncExp(Fun(z0,z1)) -> z1 getFuncName(Fun(z0,z1)) -> z0 getIfFalse(ITE(z0,z1,z2)) -> z2 getIfGuard(ITE(z0,z1,z2)) -> z0 getIfTrue(ITE(z0,z1,z2)) -> z1 getVar(Var(z0)) -> z0 lookbody(z0,Cons(Fun(z1,z2),z3)) -> lookbody[Ite](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)) lookbody[Ite](False(),z0,Cons(z1,z2)) -> lookbody(z0,z2) lookbody[Ite](True(),z0,Cons(Fun(z1,z2),z3)) -> z2 lookname(z0,Cons(Fun(z1,z2),z3)) -> lookname[Ite](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)) lookname[Ite](False(),z0,Cons(z1,z2)) -> lookname(z0,z2) lookname[Ite](True(),z0,Cons(Fun(z1,z2),z3)) -> z1 lookvar(z0,Cons(z1,z2),z3) -> lookvar[Ite](!EQ(z0,z1),z0,Cons(z1,z2),z3) lookvar[Ite](False(),z0,Cons(z1,z2),Cons(z3,z4)) -> lookvar(z0,z2,z4) lookvar[Ite](True(),z0,z1,Cons(z2,z3)) -> z2 run(Cons(Fun(z0,z1),z2),z3) -> run[Let][Let](Cons(Fun(z0,z1),z2),z3,z0,lookbody(z0,Cons(Fun(z0,z1),z2))) run[Let](z0,z1,z2,z3,z4) -> eeval(z3,Cons(z4,Nil()),Cons(z1,Nil()),z0) run[Let][Let](z0,z1,z2,z3) -> run[Let](z0,z1,z2,z3,lookname(z2,z0)) - Signature: {!EQ/2,!EQ'/2,AND/2,APPLY/3,APPLY[ITE]/4,CHECKCONSTREXP/2,EEVAL/4,EEVAL[FALSE][ITE]/5,EEVAL[FALSE][LET]/5 ,EEVAL[FALSE][LET][LET]/6,EEVAL[ITE]/5,EEVAL[LET]/5,EEVAL[LET][LET]/6,EEVAL[LET][LET][LET]/7 ,EEVAL[TRUE][ITE]/5,EQEXP/2,EQOPS/2,GETBSFFIRSTTERM/1,GETBSFOP/1,GETBSFSECONDTERM/1,GETCONST/1,GETEQFIRST/1 ,GETEQSECOND/1,GETFUNCEXP/1,GETFUNCNAME/1,GETIFFALSE/1,GETIFGUARD/1,GETIFTRUE/1,GETVAR/1,LOOKBODY/2 ,LOOKBODY[ITE]/3,LOOKNAME/2,LOOKNAME[ITE]/3,LOOKVAR/3,LOOKVAR[ITE]/4,RUN/2,RUN[LET]/5,RUN[LET][LET]/4,and/2 ,apply/3,apply[Ite]/4,checkConstrExp/2,eeval/4,eeval[False][Ite]/5,eeval[False][Let]/5 ,eeval[False][Let][Let]/6,eeval[Ite]/5,eeval[Let]/5,eeval[Let][Let]/6,eeval[Let][Let][Let]/7 ,eeval[True][Ite]/5,eqExp/2,eqOps/2,getBsfFirstTerm/1,getBsfOp/1,getBsfSecondTerm/1,getConst/1,getEqFirst/1 ,getEqSecond/1,getFuncExp/1,getFuncName/1,getIfFalse/1,getIfGuard/1,getIfTrue/1,getVar/1,lookbody/2 ,lookbody[Ite]/3,lookname/2,lookname[Ite]/3,lookvar/3,lookvar[Ite]/4,run/2,run[Let]/5 ,run[Let][Let]/4} / {0/0,Bsf/3,Cons/2,Cst/1,Eq/2,Error/2,F/0,False/0,Fun/2,ITE/3,Nil/0,S/1,T/0,True/0,Var/1 ,c/1,c1/0,c10/2,c100/3,c101/0,c102/0,c103/0,c104/0,c105/0,c106/0,c107/0,c108/0,c109/1,c11/1,c110/0,c111/0 ,c112/0,c113/0,c114/0,c115/0,c116/0,c117/0,c118/0,c119/0,c12/0,c120/0,c121/0,c122/0,c123/0,c124/0,c125/0 ,c126/0,c127/0,c128/0,c129/0,c13/0,c130/0,c131/0,c132/0,c133/0,c134/0,c135/0,c136/0,c137/0,c138/0,c139/0 ,c14/1,c140/0,c141/0,c142/0,c143/0,c144/0,c145/0,c146/0,c147/0,c148/0,c149/0,c15/0,c150/0,c151/0,c152/0 ,c153/0,c154/0,c155/0,c156/0,c157/0,c158/0,c159/0,c16/1,c160/0,c161/0,c162/0,c163/0,c164/0,c165/0,c166/0 ,c167/0,c168/0,c169/0,c17/1,c170/0,c171/0,c172/0,c173/0,c174/2,c175/2,c176/0,c177/0,c178/0,c179/0,c18/1 ,c180/0,c181/0,c182/0,c183/0,c184/0,c185/0,c186/0,c187/0,c188/2,c189/2,c19/2,c190/0,c2/0,c20/2,c21/2,c22/1 ,c23/0,c24/0,c25/0,c26/0,c27/2,c28/1,c29/1,c3/0,c30/2,c31/3,c32/3,c33/1,c34/0,c35/0,c36/3,c37/2,c38/1,c39/2 ,c4/0,c40/2,c41/2,c42/0,c43/0,c44/0,c45/0,c46/0,c47/0,c48/0,c49/0,c5/0,c50/0,c51/0,c52/0,c53/0,c54/0,c55/0 ,c56/0,c57/0,c58/0,c59/0,c6/0,c60/0,c61/0,c62/0,c63/0,c64/0,c65/0,c66/0,c67/0,c68/2,c69/2,c7/0,c70/0,c71/0 ,c72/0,c73/0,c74/0,c75/0,c76/0,c77/0,c78/2,c79/2,c8/3,c80/0,c81/0,c82/0,c83/0,c84/0,c85/0,c86/0,c87/0,c88/2 ,c89/3,c9/3,c90/3,c91/0,c92/0,c93/0,c94/0,c95/0,c96/0,c97/0,c98/0,c99/3} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,APPLY,APPLY[ITE],CHECKCONSTREXP,EEVAL ,EEVAL[FALSE][ITE],EEVAL[FALSE][LET],EEVAL[FALSE][LET][LET],EEVAL[ITE],EEVAL[LET],EEVAL[LET][LET] ,EEVAL[LET][LET][LET],EEVAL[TRUE][ITE],EQEXP,EQOPS,GETBSFFIRSTTERM,GETBSFOP,GETBSFSECONDTERM,GETCONST ,GETEQFIRST,GETEQSECOND,GETFUNCEXP,GETFUNCNAME,GETIFFALSE,GETIFGUARD,GETIFTRUE,GETVAR,LOOKBODY,LOOKBODY[ITE] ,LOOKNAME,LOOKNAME[ITE],LOOKVAR,LOOKVAR[ITE],RUN,RUN[LET],RUN[LET][LET],and,apply,apply[Ite],checkConstrExp ,eeval,eeval[False][Ite],eeval[False][Let],eeval[False][Let][Let],eeval[Ite],eeval[Let],eeval[Let][Let] ,eeval[Let][Let][Let],eeval[True][Ite],eqExp,eqOps,getBsfFirstTerm,getBsfOp,getBsfSecondTerm,getConst ,getEqFirst,getEqSecond,getFuncExp,getFuncName,getIfFalse,getIfGuard,getIfTrue,getVar,lookbody,lookbody[Ite] ,lookname,lookname[Ite],lookvar,lookvar[Ite],run,run[Let],run[Let][Let]} and constructors {0,Bsf,Cons,Cst,Eq ,Error,F,False,Fun,ITE,Nil,S,T,True,Var,c,c1,c10,c100,c101,c102,c103,c104,c105,c106,c107,c108,c109,c11,c110 ,c111,c112,c113,c114,c115,c116,c117,c118,c119,c12,c120,c121,c122,c123,c124,c125,c126,c127,c128,c129,c13,c130 ,c131,c132,c133,c134,c135,c136,c137,c138,c139,c14,c140,c141,c142,c143,c144,c145,c146,c147,c148,c149,c15,c150 ,c151,c152,c153,c154,c155,c156,c157,c158,c159,c16,c160,c161,c162,c163,c164,c165,c166,c167,c168,c169,c17,c170 ,c171,c172,c173,c174,c175,c176,c177,c178,c179,c18,c180,c181,c182,c183,c184,c185,c186,c187,c188,c189,c19,c190 ,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43 ,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68 ,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83,c84,c85,c86,c87,c88,c89,c9,c90,c91,c92 ,c93,c94,c95,c96,c97,c98,c99} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPLY(z0,z1,z2) -> c188(APPLY[ITE](eqExp(z1,z2),z0,z1,z2),EQEXP(z1,z2)) CHECKCONSTREXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c164() CHECKCONSTREXP(Bsf(z0,z1,z2),Eq(z3,z4)) -> c162() CHECKCONSTREXP(Bsf(z0,z1,z2),Error(z3,z4)) -> c158() CHECKCONSTREXP(Bsf(z0,z1,z2),F()) -> c159() CHECKCONSTREXP(Bsf(z0,z1,z2),Fun(z3,z4)) -> c161() CHECKCONSTREXP(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> c163() CHECKCONSTREXP(Bsf(z0,z1,z2),T()) -> c160() CHECKCONSTREXP(Bsf(z0,z1,z2),Var(z3)) -> c165() CHECKCONSTREXP(Eq(z0,z1),Bsf(z2,z3,z4)) -> c148() CHECKCONSTREXP(Eq(z0,z1),Eq(z2,z3)) -> c146() CHECKCONSTREXP(Eq(z0,z1),Error(z2,z3)) -> c142() CHECKCONSTREXP(Eq(z0,z1),F()) -> c143() CHECKCONSTREXP(Eq(z0,z1),Fun(z2,z3)) -> c145() CHECKCONSTREXP(Eq(z0,z1),ITE(z2,z3,z4)) -> c147() CHECKCONSTREXP(Eq(z0,z1),T()) -> c144() CHECKCONSTREXP(Eq(z0,z1),Var(z2)) -> c149() CHECKCONSTREXP(Error(z0,z1),Bsf(z2,z3,z4)) -> c116() CHECKCONSTREXP(Error(z0,z1),Eq(z2,z3)) -> c114() CHECKCONSTREXP(Error(z0,z1),Error(z2,z3)) -> c110() CHECKCONSTREXP(Error(z0,z1),F()) -> c111() CHECKCONSTREXP(Error(z0,z1),Fun(z2,z3)) -> c113() CHECKCONSTREXP(Error(z0,z1),ITE(z2,z3,z4)) -> c115() CHECKCONSTREXP(Error(z0,z1),T()) -> c112() CHECKCONSTREXP(Error(z0,z1),Var(z2)) -> c117() CHECKCONSTREXP(F(),Bsf(z0,z1,z2)) -> c124() CHECKCONSTREXP(F(),Eq(z0,z1)) -> c122() CHECKCONSTREXP(F(),Error(z0,z1)) -> c118() CHECKCONSTREXP(F(),F()) -> c119() CHECKCONSTREXP(F(),Fun(z0,z1)) -> c121() CHECKCONSTREXP(F(),ITE(z0,z1,z2)) -> c123() CHECKCONSTREXP(F(),T()) -> c120() CHECKCONSTREXP(F(),Var(z0)) -> c125() CHECKCONSTREXP(Fun(z0,z1),Bsf(z2,z3,z4)) -> c140() CHECKCONSTREXP(Fun(z0,z1),Eq(z2,z3)) -> c138() CHECKCONSTREXP(Fun(z0,z1),Error(z2,z3)) -> c134() CHECKCONSTREXP(Fun(z0,z1),F()) -> c135() CHECKCONSTREXP(Fun(z0,z1),Fun(z2,z3)) -> c137() CHECKCONSTREXP(Fun(z0,z1),ITE(z2,z3,z4)) -> c139() CHECKCONSTREXP(Fun(z0,z1),T()) -> c136() CHECKCONSTREXP(Fun(z0,z1),Var(z2)) -> c141() CHECKCONSTREXP(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> c156() CHECKCONSTREXP(ITE(z0,z1,z2),Eq(z3,z4)) -> c154() CHECKCONSTREXP(ITE(z0,z1,z2),Error(z3,z4)) -> c150() CHECKCONSTREXP(ITE(z0,z1,z2),F()) -> c151() CHECKCONSTREXP(ITE(z0,z1,z2),Fun(z3,z4)) -> c153() CHECKCONSTREXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c155() CHECKCONSTREXP(ITE(z0,z1,z2),T()) -> c152() CHECKCONSTREXP(ITE(z0,z1,z2),Var(z3)) -> c157() CHECKCONSTREXP(T(),Bsf(z0,z1,z2)) -> c132() CHECKCONSTREXP(T(),Eq(z0,z1)) -> c130() CHECKCONSTREXP(T(),Error(z0,z1)) -> c126() CHECKCONSTREXP(T(),F()) -> c127() CHECKCONSTREXP(T(),Fun(z0,z1)) -> c129() CHECKCONSTREXP(T(),ITE(z0,z1,z2)) -> c131() CHECKCONSTREXP(T(),T()) -> c128() CHECKCONSTREXP(T(),Var(z0)) -> c133() CHECKCONSTREXP(Var(z0),Bsf(z1,z2,z3)) -> c172() CHECKCONSTREXP(Var(z0),Eq(z1,z2)) -> c170() CHECKCONSTREXP(Var(z0),Error(z1,z2)) -> c166() CHECKCONSTREXP(Var(z0),F()) -> c167() CHECKCONSTREXP(Var(z0),Fun(z1,z2)) -> c169() CHECKCONSTREXP(Var(z0),ITE(z1,z2,z3)) -> c171() CHECKCONSTREXP(Var(z0),T()) -> c168() CHECKCONSTREXP(Var(z0),Var(z1)) -> c173() EEVAL(Bsf(z0,z1,z2),z3,z4,z5) -> c37(EEVAL[LET](Bsf(z0,z1,z2),z3,z4,z5,eeval(z1,z3,z4,z5)) ,EEVAL(z1,z3,z4,z5)) EEVAL(Eq(z0,z1),z2,z3,z4) -> c31(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z0,z2,z3,z4)) EEVAL(Eq(z0,z1),z2,z3,z4) -> c32(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL(Error(z0,z1),z2,z3,z4) -> c33(EEVAL[FALSE][ITE](False(),Error(z0,z1),z2,z3,z4)) EEVAL(F(),z0,z1,z2) -> c34() EEVAL(Fun(z0,z1),z2,z3,z4) -> c30(EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)),LOOKBODY(z0,z4)) EEVAL(ITE(z0,z1,z2),z3,z4,z5) -> c36(EEVAL[ITE](checkConstrExp(eeval(z0,z3,z4,z5),T()) ,ITE(z0,z1,z2) ,z3 ,z4 ,z5) ,CHECKCONSTREXP(eeval(z0,z3,z4,z5),T()) ,EEVAL(z0,z3,z4,z5)) EEVAL(T(),z0,z1,z2) -> c35() EEVAL(Var(z0),z1,z2,z3) -> c38(LOOKVAR(z0,z1,z2)) EQEXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c100(AND(True(),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z2,z5)) EQEXP(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> c99(AND(True(),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z1,z4)) EQEXP(Bsf(z0,z1,z2),Eq(z3,z4)) -> c97() EQEXP(Bsf(z0,z1,z2),Error(z3,z4)) -> c93() EQEXP(Bsf(z0,z1,z2),F()) -> c94() EQEXP(Bsf(z0,z1,z2),Fun(z3,z4)) -> c96() EQEXP(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> c98() EQEXP(Bsf(z0,z1,z2),T()) -> c95() EQEXP(Bsf(z0,z1,z2),Var(z3)) -> c101() EQEXP(Eq(z0,z1),Bsf(z2,z3,z4)) -> c81() EQEXP(Eq(z0,z1),Eq(z2,z3)) -> c78(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z0,z2)) EQEXP(Eq(z0,z1),Eq(z2,z3)) -> c79(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Eq(z0,z1),Error(z2,z3)) -> c74() EQEXP(Eq(z0,z1),F()) -> c75() EQEXP(Eq(z0,z1),Fun(z2,z3)) -> c77() EQEXP(Eq(z0,z1),ITE(z2,z3,z4)) -> c80() EQEXP(Eq(z0,z1),T()) -> c76() EQEXP(Eq(z0,z1),Var(z2)) -> c82() EQEXP(Error(z0,z1),Bsf(z2,z3,z4)) -> c47() EQEXP(Error(z0,z1),Eq(z2,z3)) -> c45() EQEXP(Error(z0,z1),Error(z2,z3)) -> c40(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z0,z2)) EQEXP(Error(z0,z1),Error(z2,z3)) -> c41(AND(eqExp(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Error(z0,z1),F()) -> c42() EQEXP(Error(z0,z1),Fun(z2,z3)) -> c44() EQEXP(Error(z0,z1),ITE(z2,z3,z4)) -> c46() EQEXP(Error(z0,z1),T()) -> c43() EQEXP(Error(z0,z1),Var(z2)) -> c48() EQEXP(F(),Bsf(z0,z1,z2)) -> c55() EQEXP(F(),Eq(z0,z1)) -> c53() EQEXP(F(),Error(z0,z1)) -> c49() EQEXP(F(),F()) -> c50() EQEXP(F(),Fun(z0,z1)) -> c52() EQEXP(F(),ITE(z0,z1,z2)) -> c54() EQEXP(F(),T()) -> c51() EQEXP(F(),Var(z0)) -> c56() EQEXP(Fun(z0,z1),Bsf(z2,z3,z4)) -> c72() EQEXP(Fun(z0,z1),Eq(z2,z3)) -> c70() EQEXP(Fun(z0,z1),Error(z2,z3)) -> c65() EQEXP(Fun(z0,z1),F()) -> c66() EQEXP(Fun(z0,z1),Fun(z2,z3)) -> c68(AND(!EQ(z0,z2),eqExp(z1,z3)),!EQ'(z0,z2)) EQEXP(Fun(z0,z1),Fun(z2,z3)) -> c69(AND(!EQ(z0,z2),eqExp(z1,z3)),EQEXP(z1,z3)) EQEXP(Fun(z0,z1),ITE(z2,z3,z4)) -> c71() EQEXP(Fun(z0,z1),T()) -> c67() EQEXP(Fun(z0,z1),Var(z2)) -> c73() EQEXP(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> c91() EQEXP(ITE(z0,z1,z2),Eq(z3,z4)) -> c87() EQEXP(ITE(z0,z1,z2),Error(z3,z4)) -> c83() EQEXP(ITE(z0,z1,z2),F()) -> c84() EQEXP(ITE(z0,z1,z2),Fun(z3,z4)) -> c86() EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c88(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))),EQEXP(z0,z3)) EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c89(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z1,z4)) EQEXP(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> c90(AND(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) ,AND(eqExp(z1,z4),eqExp(z2,z5)) ,EQEXP(z2,z5)) EQEXP(ITE(z0,z1,z2),T()) -> c85() EQEXP(ITE(z0,z1,z2),Var(z3)) -> c92() EQEXP(T(),Bsf(z0,z1,z2)) -> c63() EQEXP(T(),Eq(z0,z1)) -> c61() EQEXP(T(),Error(z0,z1)) -> c57() EQEXP(T(),F()) -> c58() EQEXP(T(),Fun(z0,z1)) -> c60() EQEXP(T(),ITE(z0,z1,z2)) -> c62() EQEXP(T(),T()) -> c59() EQEXP(T(),Var(z0)) -> c64() EQEXP(Var(z0),Bsf(z1,z2,z3)) -> c108() EQEXP(Var(z0),Eq(z1,z2)) -> c106() EQEXP(Var(z0),Error(z1,z2)) -> c102() EQEXP(Var(z0),F()) -> c103() EQEXP(Var(z0),Fun(z1,z2)) -> c105() EQEXP(Var(z0),ITE(z1,z2,z3)) -> c107() EQEXP(Var(z0),T()) -> c104() EQEXP(Var(z0),Var(z1)) -> c109(!EQ'(z0,z1)) EQOPS(z0,z1) -> c190() GETBSFFIRSTTERM(Bsf(z0,z1,z2)) -> c187() GETBSFOP(Bsf(z0,z1,z2)) -> c186() GETBSFSECONDTERM(Bsf(z0,z1,z2)) -> c185() GETCONST(Cst(z0)) -> c184() GETEQFIRST(Eq(z0,z1)) -> c183() GETEQSECOND(Eq(z0,z1)) -> c182() GETFUNCEXP(Fun(z0,z1)) -> c181() GETFUNCNAME(Fun(z0,z1)) -> c180() GETIFFALSE(ITE(z0,z1,z2)) -> c179() GETIFGUARD(ITE(z0,z1,z2)) -> c178() GETIFTRUE(ITE(z0,z1,z2)) -> c177() GETVAR(Var(z0)) -> c176() LOOKBODY(z0,Cons(Fun(z1,z2),z3)) -> c175(LOOKBODY[ITE](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)),!EQ'(z0,z1)) LOOKNAME(z0,Cons(Fun(z1,z2),z3)) -> c174(LOOKNAME[ITE](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)),!EQ'(z0,z1)) LOOKVAR(z0,Cons(z1,z2),z3) -> c189(LOOKVAR[ITE](!EQ(z0,z1),z0,Cons(z1,z2),z3),!EQ'(z0,z1)) RUN(Cons(Fun(z0,z1),z2),z3) -> c39(RUN[LET][LET](Cons(Fun(z0,z1),z2),z3,z0,lookbody(z0,Cons(Fun(z0,z1),z2))) ,LOOKBODY(z0,Cons(Fun(z0,z1),z2))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(z0)) -> False() !EQ(S(z0),0()) -> False() !EQ(S(z0),S(z1)) -> !EQ(z0,z1) !EQ'(0(),0()) -> c3() !EQ'(0(),S(z0)) -> c1() !EQ'(S(z0),0()) -> c2() !EQ'(S(z0),S(z1)) -> c(!EQ'(z0,z1)) AND(False(),False()) -> c4() AND(False(),True()) -> c6() AND(True(),False()) -> c5() AND(True(),True()) -> c7() APPLY[ITE](False(),z0,z1,z2) -> c25() APPLY[ITE](True(),z0,z1,z2) -> c26() EEVAL[FALSE][ITE](False(),Fun(z0,z1),z2,z3,z4) -> c10(EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) ,LOOKBODY(z0,z4)) EEVAL[FALSE][ITE](True(),Eq(z0,z1),z2,z3,z4) -> c8(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z0,z2,z3,z4)) EEVAL[FALSE][ITE](True(),Eq(z0,z1),z2,z3,z4) -> c9(EEVAL[TRUE][ITE](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) ,EQEXP(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL[FALSE][LET](Fun(z0,z1),z2,z3,z4,z5) -> c19(EEVAL[FALSE][LET][LET](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,lookname(z0,z4)) ,LOOKNAME(z0,z4)) EEVAL[FALSE][LET][LET](Fun(z0,z1),z2,z3,z4,z5,z6) -> c20(EEVAL[LET][LET][LET](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,z6 ,eeval(z1,z2,z3,z4)) ,EEVAL(z1,z2,z3,z4)) EEVAL[ITE](False(),ITE(z0,z1,z2),z3,z4,z5) -> c17(EEVAL(z2,z3,z4,z5)) EEVAL[ITE](True(),ITE(z0,z1,z2),z3,z4,z5) -> c18(EEVAL(z1,z3,z4,z5)) EEVAL[LET](Bsf(z0,z1,z2),z3,z4,z5,z6) -> c21(EEVAL[LET][LET](Bsf(z0,z1,z2),z3,z4,z5,z6,eeval(z2,z3,z4,z5)) ,EEVAL(z2,z3,z4,z5)) EEVAL[LET][LET](Bsf(z0,z1,z2),z3,z4,z5,z6,z7) -> c22(APPLY(z0,z6,z7)) EEVAL[LET][LET][LET](z0,z1,z2,z3,z4,z5,z6) -> c29(EEVAL(z4,Cons(z5,Nil()),Cons(z6,Nil()),z3)) EEVAL[TRUE][ITE](False(),z0,z1,z2,z3) -> c23() EEVAL[TRUE][ITE](True(),z0,z1,z2,z3) -> c24() LOOKBODY[ITE](False(),z0,Cons(z1,z2)) -> c16(LOOKBODY(z0,z2)) LOOKBODY[ITE](True(),z0,Cons(Fun(z1,z2),z3)) -> c15() LOOKNAME[ITE](False(),z0,Cons(z1,z2)) -> c14(LOOKNAME(z0,z2)) LOOKNAME[ITE](True(),z0,Cons(Fun(z1,z2),z3)) -> c13() LOOKVAR[ITE](False(),z0,Cons(z1,z2),Cons(z3,z4)) -> c11(LOOKVAR(z0,z2,z4)) LOOKVAR[ITE](True(),z0,z1,Cons(z2,z3)) -> c12() RUN[LET](z0,z1,z2,z3,z4) -> c28(EEVAL(z3,Cons(z4,Nil()),Cons(z1,Nil()),z0)) RUN[LET][LET](z0,z1,z2,z3) -> c27(RUN[LET](z0,z1,z2,z3,lookname(z2,z0)),LOOKNAME(z2,z0)) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() apply(z0,z1,z2) -> apply[Ite](eqExp(z1,z2),z0,z1,z2) apply[Ite](False(),z0,z1,z2) -> F() apply[Ite](True(),z0,z1,z2) -> T() checkConstrExp(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> True() checkConstrExp(Bsf(z0,z1,z2),Eq(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),Error(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),F()) -> False() checkConstrExp(Bsf(z0,z1,z2),Fun(z3,z4)) -> False() checkConstrExp(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> False() checkConstrExp(Bsf(z0,z1,z2),T()) -> False() checkConstrExp(Bsf(z0,z1,z2),Var(z3)) -> False() checkConstrExp(Eq(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Eq(z0,z1),Eq(z2,z3)) -> True() checkConstrExp(Eq(z0,z1),Error(z2,z3)) -> False() checkConstrExp(Eq(z0,z1),F()) -> False() checkConstrExp(Eq(z0,z1),Fun(z2,z3)) -> False() checkConstrExp(Eq(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Eq(z0,z1),T()) -> False() checkConstrExp(Eq(z0,z1),Var(z2)) -> False() checkConstrExp(Error(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Error(z0,z1),Eq(z2,z3)) -> False() checkConstrExp(Error(z0,z1),Error(z2,z3)) -> True() checkConstrExp(Error(z0,z1),F()) -> False() checkConstrExp(Error(z0,z1),Fun(z2,z3)) -> False() checkConstrExp(Error(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Error(z0,z1),T()) -> False() checkConstrExp(Error(z0,z1),Var(z2)) -> False() checkConstrExp(F(),Bsf(z0,z1,z2)) -> False() checkConstrExp(F(),Eq(z0,z1)) -> False() checkConstrExp(F(),Error(z0,z1)) -> False() checkConstrExp(F(),F()) -> True() checkConstrExp(F(),Fun(z0,z1)) -> False() checkConstrExp(F(),ITE(z0,z1,z2)) -> False() checkConstrExp(F(),T()) -> False() checkConstrExp(F(),Var(z0)) -> False() checkConstrExp(Fun(z0,z1),Bsf(z2,z3,z4)) -> False() checkConstrExp(Fun(z0,z1),Eq(z2,z3)) -> False() checkConstrExp(Fun(z0,z1),Error(z2,z3)) -> False() checkConstrExp(Fun(z0,z1),F()) -> False() checkConstrExp(Fun(z0,z1),Fun(z2,z3)) -> True() checkConstrExp(Fun(z0,z1),ITE(z2,z3,z4)) -> False() checkConstrExp(Fun(z0,z1),T()) -> False() checkConstrExp(Fun(z0,z1),Var(z2)) -> False() checkConstrExp(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> False() checkConstrExp(ITE(z0,z1,z2),Eq(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),Error(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),F()) -> False() checkConstrExp(ITE(z0,z1,z2),Fun(z3,z4)) -> False() checkConstrExp(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> True() checkConstrExp(ITE(z0,z1,z2),T()) -> False() checkConstrExp(ITE(z0,z1,z2),Var(z3)) -> False() checkConstrExp(T(),Bsf(z0,z1,z2)) -> False() checkConstrExp(T(),Eq(z0,z1)) -> False() checkConstrExp(T(),Error(z0,z1)) -> False() checkConstrExp(T(),F()) -> False() checkConstrExp(T(),Fun(z0,z1)) -> False() checkConstrExp(T(),ITE(z0,z1,z2)) -> False() checkConstrExp(T(),T()) -> True() checkConstrExp(T(),Var(z0)) -> False() checkConstrExp(Var(z0),Bsf(z1,z2,z3)) -> False() checkConstrExp(Var(z0),Eq(z1,z2)) -> False() checkConstrExp(Var(z0),Error(z1,z2)) -> False() checkConstrExp(Var(z0),F()) -> False() checkConstrExp(Var(z0),Fun(z1,z2)) -> False() checkConstrExp(Var(z0),ITE(z1,z2,z3)) -> False() checkConstrExp(Var(z0),T()) -> False() checkConstrExp(Var(z0),Var(z1)) -> True() eeval(Bsf(z0,z1,z2),z3,z4,z5) -> eeval[Let](Bsf(z0,z1,z2),z3,z4,z5,eeval(z1,z3,z4,z5)) eeval(Eq(z0,z1),z2,z3,z4) -> eeval[True][Ite](eqExp(eeval(z0,z2,z3,z4),eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) eeval(Error(z0,z1),z2,z3,z4) -> eeval[False][Ite](False(),Error(z0,z1),z2,z3,z4) eeval(F(),z0,z1,z2) -> F() eeval(Fun(z0,z1),z2,z3,z4) -> eeval[False][Let](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) eeval(ITE(z0,z1,z2),z3,z4,z5) -> eeval[Ite](checkConstrExp(eeval(z0,z3,z4,z5),T()),ITE(z0,z1,z2),z3,z4,z5) eeval(T(),z0,z1,z2) -> T() eeval(Var(z0),z1,z2,z3) -> lookvar(z0,z1,z2) eeval[False][Ite](False(),Fun(z0,z1),z2,z3,z4) -> eeval[False][Let](Fun(z0,z1),z2,z3,z4,lookbody(z0,z4)) eeval[False][Ite](True(),Eq(z0,z1),z2,z3,z4) -> eeval[True][Ite](eqExp(eeval(z0,z2,z3,z4) ,eeval(z1,z2,z3,z4)) ,Eq(z0,z1) ,z2 ,z3 ,z4) eeval[False][Let](Fun(z0,z1),z2,z3,z4,z5) -> eeval[False][Let][Let](Fun(z0,z1),z2,z3,z4,z5,lookname(z0,z4)) eeval[False][Let][Let](Fun(z0,z1),z2,z3,z4,z5,z6) -> eeval[Let][Let][Let](Fun(z0,z1) ,z2 ,z3 ,z4 ,z5 ,z6 ,eeval(z1,z2,z3,z4)) eeval[Ite](False(),ITE(z0,z1,z2),z3,z4,z5) -> eeval(z2,z3,z4,z5) eeval[Ite](True(),ITE(z0,z1,z2),z3,z4,z5) -> eeval(z1,z3,z4,z5) eeval[Let](Bsf(z0,z1,z2),z3,z4,z5,z6) -> eeval[Let][Let](Bsf(z0,z1,z2),z3,z4,z5,z6,eeval(z2,z3,z4,z5)) eeval[Let][Let](Bsf(z0,z1,z2),z3,z4,z5,z6,z7) -> apply(z0,z6,z7) eeval[Let][Let][Let](z0,z1,z2,z3,z4,z5,z6) -> eeval(z4,Cons(z5,Nil()),Cons(z6,Nil()),z3) eeval[True][Ite](False(),z0,z1,z2,z3) -> F() eeval[True][Ite](True(),z0,z1,z2,z3) -> T() eqExp(Bsf(z0,z1,z2),Bsf(z3,z4,z5)) -> and(True(),and(eqExp(z1,z4),eqExp(z2,z5))) eqExp(Bsf(z0,z1,z2),Eq(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),Error(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),F()) -> False() eqExp(Bsf(z0,z1,z2),Fun(z3,z4)) -> False() eqExp(Bsf(z0,z1,z2),ITE(z3,z4,z5)) -> False() eqExp(Bsf(z0,z1,z2),T()) -> False() eqExp(Bsf(z0,z1,z2),Var(z3)) -> False() eqExp(Eq(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Eq(z0,z1),Eq(z2,z3)) -> and(eqExp(z0,z2),eqExp(z1,z3)) eqExp(Eq(z0,z1),Error(z2,z3)) -> False() eqExp(Eq(z0,z1),F()) -> False() eqExp(Eq(z0,z1),Fun(z2,z3)) -> False() eqExp(Eq(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Eq(z0,z1),T()) -> False() eqExp(Eq(z0,z1),Var(z2)) -> False() eqExp(Error(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Error(z0,z1),Eq(z2,z3)) -> False() eqExp(Error(z0,z1),Error(z2,z3)) -> and(eqExp(z0,z2),eqExp(z1,z3)) eqExp(Error(z0,z1),F()) -> False() eqExp(Error(z0,z1),Fun(z2,z3)) -> False() eqExp(Error(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Error(z0,z1),T()) -> False() eqExp(Error(z0,z1),Var(z2)) -> False() eqExp(F(),Bsf(z0,z1,z2)) -> False() eqExp(F(),Eq(z0,z1)) -> False() eqExp(F(),Error(z0,z1)) -> False() eqExp(F(),F()) -> True() eqExp(F(),Fun(z0,z1)) -> False() eqExp(F(),ITE(z0,z1,z2)) -> False() eqExp(F(),T()) -> False() eqExp(F(),Var(z0)) -> False() eqExp(Fun(z0,z1),Bsf(z2,z3,z4)) -> False() eqExp(Fun(z0,z1),Eq(z2,z3)) -> False() eqExp(Fun(z0,z1),Error(z2,z3)) -> False() eqExp(Fun(z0,z1),F()) -> False() eqExp(Fun(z0,z1),Fun(z2,z3)) -> and(!EQ(z0,z2),eqExp(z1,z3)) eqExp(Fun(z0,z1),ITE(z2,z3,z4)) -> False() eqExp(Fun(z0,z1),T()) -> False() eqExp(Fun(z0,z1),Var(z2)) -> False() eqExp(ITE(z0,z1,z2),Bsf(z3,z4,z5)) -> False() eqExp(ITE(z0,z1,z2),Eq(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),Error(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),F()) -> False() eqExp(ITE(z0,z1,z2),Fun(z3,z4)) -> False() eqExp(ITE(z0,z1,z2),ITE(z3,z4,z5)) -> and(eqExp(z0,z3),and(eqExp(z1,z4),eqExp(z2,z5))) eqExp(ITE(z0,z1,z2),T()) -> False() eqExp(ITE(z0,z1,z2),Var(z3)) -> False() eqExp(T(),Bsf(z0,z1,z2)) -> False() eqExp(T(),Eq(z0,z1)) -> False() eqExp(T(),Error(z0,z1)) -> False() eqExp(T(),F()) -> False() eqExp(T(),Fun(z0,z1)) -> False() eqExp(T(),ITE(z0,z1,z2)) -> False() eqExp(T(),T()) -> True() eqExp(T(),Var(z0)) -> False() eqExp(Var(z0),Bsf(z1,z2,z3)) -> False() eqExp(Var(z0),Eq(z1,z2)) -> False() eqExp(Var(z0),Error(z1,z2)) -> False() eqExp(Var(z0),F()) -> False() eqExp(Var(z0),Fun(z1,z2)) -> False() eqExp(Var(z0),ITE(z1,z2,z3)) -> False() eqExp(Var(z0),T()) -> False() eqExp(Var(z0),Var(z1)) -> !EQ(z0,z1) eqOps(z0,z1) -> True() getBsfFirstTerm(Bsf(z0,z1,z2)) -> z1 getBsfOp(Bsf(z0,z1,z2)) -> z0 getBsfSecondTerm(Bsf(z0,z1,z2)) -> z2 getConst(Cst(z0)) -> z0 getEqFirst(Eq(z0,z1)) -> z0 getEqSecond(Eq(z0,z1)) -> z1 getFuncExp(Fun(z0,z1)) -> z1 getFuncName(Fun(z0,z1)) -> z0 getIfFalse(ITE(z0,z1,z2)) -> z2 getIfGuard(ITE(z0,z1,z2)) -> z0 getIfTrue(ITE(z0,z1,z2)) -> z1 getVar(Var(z0)) -> z0 lookbody(z0,Cons(Fun(z1,z2),z3)) -> lookbody[Ite](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)) lookbody[Ite](False(),z0,Cons(z1,z2)) -> lookbody(z0,z2) lookbody[Ite](True(),z0,Cons(Fun(z1,z2),z3)) -> z2 lookname(z0,Cons(Fun(z1,z2),z3)) -> lookname[Ite](!EQ(z0,z1),z0,Cons(Fun(z1,z2),z3)) lookname[Ite](False(),z0,Cons(z1,z2)) -> lookname(z0,z2) lookname[Ite](True(),z0,Cons(Fun(z1,z2),z3)) -> z1 lookvar(z0,Cons(z1,z2),z3) -> lookvar[Ite](!EQ(z0,z1),z0,Cons(z1,z2),z3) lookvar[Ite](False(),z0,Cons(z1,z2),Cons(z3,z4)) -> lookvar(z0,z2,z4) lookvar[Ite](True(),z0,z1,Cons(z2,z3)) -> z2 run(Cons(Fun(z0,z1),z2),z3) -> run[Let][Let](Cons(Fun(z0,z1),z2),z3,z0,lookbody(z0,Cons(Fun(z0,z1),z2))) run[Let](z0,z1,z2,z3,z4) -> eeval(z3,Cons(z4,Nil()),Cons(z1,Nil()),z0) run[Let][Let](z0,z1,z2,z3) -> run[Let](z0,z1,z2,z3,lookname(z2,z0)) - Signature: {!EQ/2,!EQ'/2,AND/2,APPLY/3,APPLY[ITE]/4,CHECKCONSTREXP/2,EEVAL/4,EEVAL[FALSE][ITE]/5,EEVAL[FALSE][LET]/5 ,EEVAL[FALSE][LET][LET]/6,EEVAL[ITE]/5,EEVAL[LET]/5,EEVAL[LET][LET]/6,EEVAL[LET][LET][LET]/7 ,EEVAL[TRUE][ITE]/5,EQEXP/2,EQOPS/2,GETBSFFIRSTTERM/1,GETBSFOP/1,GETBSFSECONDTERM/1,GETCONST/1,GETEQFIRST/1 ,GETEQSECOND/1,GETFUNCEXP/1,GETFUNCNAME/1,GETIFFALSE/1,GETIFGUARD/1,GETIFTRUE/1,GETVAR/1,LOOKBODY/2 ,LOOKBODY[ITE]/3,LOOKNAME/2,LOOKNAME[ITE]/3,LOOKVAR/3,LOOKVAR[ITE]/4,RUN/2,RUN[LET]/5,RUN[LET][LET]/4,and/2 ,apply/3,apply[Ite]/4,checkConstrExp/2,eeval/4,eeval[False][Ite]/5,eeval[False][Let]/5 ,eeval[False][Let][Let]/6,eeval[Ite]/5,eeval[Let]/5,eeval[Let][Let]/6,eeval[Let][Let][Let]/7 ,eeval[True][Ite]/5,eqExp/2,eqOps/2,getBsfFirstTerm/1,getBsfOp/1,getBsfSecondTerm/1,getConst/1,getEqFirst/1 ,getEqSecond/1,getFuncExp/1,getFuncName/1,getIfFalse/1,getIfGuard/1,getIfTrue/1,getVar/1,lookbody/2 ,lookbody[Ite]/3,lookname/2,lookname[Ite]/3,lookvar/3,lookvar[Ite]/4,run/2,run[Let]/5 ,run[Let][Let]/4} / {0/0,Bsf/3,Cons/2,Cst/1,Eq/2,Error/2,F/0,False/0,Fun/2,ITE/3,Nil/0,S/1,T/0,True/0,Var/1 ,c/1,c1/0,c10/2,c100/3,c101/0,c102/0,c103/0,c104/0,c105/0,c106/0,c107/0,c108/0,c109/1,c11/1,c110/0,c111/0 ,c112/0,c113/0,c114/0,c115/0,c116/0,c117/0,c118/0,c119/0,c12/0,c120/0,c121/0,c122/0,c123/0,c124/0,c125/0 ,c126/0,c127/0,c128/0,c129/0,c13/0,c130/0,c131/0,c132/0,c133/0,c134/0,c135/0,c136/0,c137/0,c138/0,c139/0 ,c14/1,c140/0,c141/0,c142/0,c143/0,c144/0,c145/0,c146/0,c147/0,c148/0,c149/0,c15/0,c150/0,c151/0,c152/0 ,c153/0,c154/0,c155/0,c156/0,c157/0,c158/0,c159/0,c16/1,c160/0,c161/0,c162/0,c163/0,c164/0,c165/0,c166/0 ,c167/0,c168/0,c169/0,c17/1,c170/0,c171/0,c172/0,c173/0,c174/2,c175/2,c176/0,c177/0,c178/0,c179/0,c18/1 ,c180/0,c181/0,c182/0,c183/0,c184/0,c185/0,c186/0,c187/0,c188/2,c189/2,c19/2,c190/0,c2/0,c20/2,c21/2,c22/1 ,c23/0,c24/0,c25/0,c26/0,c27/2,c28/1,c29/1,c3/0,c30/2,c31/3,c32/3,c33/1,c34/0,c35/0,c36/3,c37/2,c38/1,c39/2 ,c4/0,c40/2,c41/2,c42/0,c43/0,c44/0,c45/0,c46/0,c47/0,c48/0,c49/0,c5/0,c50/0,c51/0,c52/0,c53/0,c54/0,c55/0 ,c56/0,c57/0,c58/0,c59/0,c6/0,c60/0,c61/0,c62/0,c63/0,c64/0,c65/0,c66/0,c67/0,c68/2,c69/2,c7/0,c70/0,c71/0 ,c72/0,c73/0,c74/0,c75/0,c76/0,c77/0,c78/2,c79/2,c8/3,c80/0,c81/0,c82/0,c83/0,c84/0,c85/0,c86/0,c87/0,c88/2 ,c89/3,c9/3,c90/3,c91/0,c92/0,c93/0,c94/0,c95/0,c96/0,c97/0,c98/0,c99/3} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,APPLY,APPLY[ITE],CHECKCONSTREXP,EEVAL ,EEVAL[FALSE][ITE],EEVAL[FALSE][LET],EEVAL[FALSE][LET][LET],EEVAL[ITE],EEVAL[LET],EEVAL[LET][LET] ,EEVAL[LET][LET][LET],EEVAL[TRUE][ITE],EQEXP,EQOPS,GETBSFFIRSTTERM,GETBSFOP,GETBSFSECONDTERM,GETCONST ,GETEQFIRST,GETEQSECOND,GETFUNCEXP,GETFUNCNAME,GETIFFALSE,GETIFGUARD,GETIFTRUE,GETVAR,LOOKBODY,LOOKBODY[ITE] ,LOOKNAME,LOOKNAME[ITE],LOOKVAR,LOOKVAR[ITE],RUN,RUN[LET],RUN[LET][LET],and,apply,apply[Ite],checkConstrExp ,eeval,eeval[False][Ite],eeval[False][Let],eeval[False][Let][Let],eeval[Ite],eeval[Let],eeval[Let][Let] ,eeval[Let][Let][Let],eeval[True][Ite],eqExp,eqOps,getBsfFirstTerm,getBsfOp,getBsfSecondTerm,getConst ,getEqFirst,getEqSecond,getFuncExp,getFuncName,getIfFalse,getIfGuard,getIfTrue,getVar,lookbody,lookbody[Ite] ,lookname,lookname[Ite],lookvar,lookvar[Ite],run,run[Let],run[Let][Let]} and constructors {0,Bsf,Cons,Cst,Eq ,Error,F,False,Fun,ITE,Nil,S,T,True,Var,c,c1,c10,c100,c101,c102,c103,c104,c105,c106,c107,c108,c109,c11,c110 ,c111,c112,c113,c114,c115,c116,c117,c118,c119,c12,c120,c121,c122,c123,c124,c125,c126,c127,c128,c129,c13,c130 ,c131,c132,c133,c134,c135,c136,c137,c138,c139,c14,c140,c141,c142,c143,c144,c145,c146,c147,c148,c149,c15,c150 ,c151,c152,c153,c154,c155,c156,c157,c158,c159,c16,c160,c161,c162,c163,c164,c165,c166,c167,c168,c169,c17,c170 ,c171,c172,c173,c174,c175,c176,c177,c178,c179,c18,c180,c181,c182,c183,c184,c185,c186,c187,c188,c189,c19,c190 ,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43 ,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68 ,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83,c84,c85,c86,c87,c88,c89,c9,c90,c91,c92 ,c93,c94,c95,c96,c97,c98,c99} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: EEVAL(y,u,v,w){y -> Bsf(x,y,z)} = EEVAL(Bsf(x,y,z),u,v,w) ->^+ c37(EEVAL[LET](Bsf(x,y,z),u,v,w,eeval(y,u,v,w)),EEVAL(y,u,v,w)) = C[EEVAL(y,u,v,w) = EEVAL(y,u,v,w){}] WORST_CASE(Omega(n^1),?)