WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPE1(App(z0,z1)) -> c44() APPE2(App(z0,z1)) -> c43() EQTERM(App(z0,z1),App(z2,z3)) -> c23(AND(eqTerm(z0,z2),eqTerm(z1,z3)),EQTERM(z0,z2)) EQTERM(App(z0,z1),App(z2,z3)) -> c24(AND(eqTerm(z0,z2),eqTerm(z1,z3)),EQTERM(z1,z3)) EQTERM(App(z0,z1),Lam(z2,z3)) -> c25() EQTERM(App(z0,z1),V(z2)) -> c26() EQTERM(Lam(z0,z1),App(z2,z3)) -> c27() EQTERM(Lam(z0,z1),Lam(z2,z3)) -> c28(AND(!EQ(z0,z2),eqTerm(z1,z3)),!EQ'(z0,z2)) EQTERM(Lam(z0,z1),Lam(z2,z3)) -> c29(AND(!EQ(z0,z2),eqTerm(z1,z3)),EQTERM(z1,z3)) EQTERM(Lam(z0,z1),V(z2)) -> c30() EQTERM(V(z0),App(z1,z2)) -> c31() EQTERM(V(z0),Lam(z1,z2)) -> c32() EQTERM(V(z0),V(z1)) -> c33(!EQ'(z0,z1)) ISLAM(App(z0,z1)) -> c40() ISLAM(Lam(z0,z1)) -> c41() ISLAM(V(z0)) -> c42() ISVAR(App(z0,z1)) -> c37() ISVAR(Lam(z0,z1)) -> c38() ISVAR(V(z0)) -> c39() LAMBDAINT(z0) -> c46(RED(z0)) LAMBODY(Lam(z0,z1)) -> c36() LAMVAR(Lam(z0,z1)) -> c35() MKAPP(z0,z1) -> c45() MKLAM(V(z0),z1) -> c34() RED(App(z0,z1)) -> c20(RED[LET](App(z0,z1),red(z0)),RED(z0)) RED(Lam(z0,z1)) -> c21() RED(V(z0)) -> c22() SUBST(z0,z1,App(z2,z3)) -> c16(MKAPP(subst(z0,z1,z2),subst(z0,z1,z3)),SUBST(z0,z1,z2)) SUBST(z0,z1,App(z2,z3)) -> c17(MKAPP(subst(z0,z1,z2),subst(z0,z1,z3)),SUBST(z0,z1,z3)) SUBST(z0,z1,Lam(z2,z3)) -> c18(SUBST[TRUE][ITE](eqTerm(z0,V(z2)),z0,z1,Lam(z2,z3)),EQTERM(z0,V(z2))) SUBST(z0,z1,V(z2)) -> c19(SUBST[ITE](eqTerm(z0,V(z2)),z0,z1,V(z2)),EQTERM(z0,V(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()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() RED[LET](App(z0,z1),z2) -> c13(RED[LET][LET](App(z0,z1),z2,red(z1)),RED(z1)) RED[LET][LET](z0,App(z1,z2),z3) -> c9() RED[LET][LET](z0,Lam(z1,z2),z3) -> c8(RED(subst(V(z1),z3,z2)),SUBST(V(z1),z3,z2)) RED[LET][LET](z0,V(z1),z2) -> c10() SUBST[ITE](False(),z0,z1,z2) -> c14() SUBST[ITE](True(),z0,z1,z2) -> c15() SUBST[TRUE][ITE](False(),z0,z1,Lam(z2,z3)) -> c11(MKLAM(V(z2),subst(z0,z1,z3)),SUBST(z0,z1,z3)) SUBST[TRUE][ITE](True(),z0,z1,z2) -> c12() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() appe1(App(z0,z1)) -> z0 appe2(App(z0,z1)) -> z1 eqTerm(App(z0,z1),App(z2,z3)) -> and(eqTerm(z0,z2),eqTerm(z1,z3)) eqTerm(App(z0,z1),Lam(z2,z3)) -> False() eqTerm(App(z0,z1),V(z2)) -> False() eqTerm(Lam(z0,z1),App(z2,z3)) -> False() eqTerm(Lam(z0,z1),Lam(z2,z3)) -> and(!EQ(z0,z2),eqTerm(z1,z3)) eqTerm(Lam(z0,z1),V(z2)) -> False() eqTerm(V(z0),App(z1,z2)) -> False() eqTerm(V(z0),Lam(z1,z2)) -> False() eqTerm(V(z0),V(z1)) -> !EQ(z0,z1) islam(App(z0,z1)) -> False() islam(Lam(z0,z1)) -> True() islam(V(z0)) -> False() isvar(App(z0,z1)) -> False() isvar(Lam(z0,z1)) -> False() isvar(V(z0)) -> True() lambdaint(z0) -> red(z0) lambody(Lam(z0,z1)) -> z1 lamvar(Lam(z0,z1)) -> V(z0) mkapp(z0,z1) -> App(z0,z1) mklam(V(z0),z1) -> Lam(z0,z1) red(App(z0,z1)) -> red[Let](App(z0,z1),red(z0)) red(Lam(z0,z1)) -> Lam(z0,z1) red(V(z0)) -> V(z0) red[Let](App(z0,z1),z2) -> red[Let][Let](App(z0,z1),z2,red(z1)) red[Let][Let](z0,App(z1,z2),z3) -> App(App(z1,z2),z3) red[Let][Let](z0,Lam(z1,z2),z3) -> red(subst(V(z1),z3,z2)) red[Let][Let](z0,V(z1),z2) -> App(V(z1),z2) subst(z0,z1,App(z2,z3)) -> mkapp(subst(z0,z1,z2),subst(z0,z1,z3)) subst(z0,z1,Lam(z2,z3)) -> subst[True][Ite](eqTerm(z0,V(z2)),z0,z1,Lam(z2,z3)) subst(z0,z1,V(z2)) -> subst[Ite](eqTerm(z0,V(z2)),z0,z1,V(z2)) subst[Ite](False(),z0,z1,z2) -> z2 subst[Ite](True(),z0,z1,z2) -> z1 subst[True][Ite](False(),z0,z1,Lam(z2,z3)) -> mklam(V(z2),subst(z0,z1,z3)) subst[True][Ite](True(),z0,z1,z2) -> z2 - Signature: {!EQ/2,!EQ'/2,AND/2,APPE1/1,APPE2/1,EQTERM/2,ISLAM/1,ISVAR/1,LAMBDAINT/1,LAMBODY/1,LAMVAR/1,MKAPP/2,MKLAM/2 ,RED/1,RED[LET]/2,RED[LET][LET]/3,SUBST/3,SUBST[ITE]/4,SUBST[TRUE][ITE]/4,and/2,appe1/1,appe2/1,eqTerm/2 ,islam/1,isvar/1,lambdaint/1,lambody/1,lamvar/1,mkapp/2,mklam/2,red/1,red[Let]/2,red[Let][Let]/3,subst/3 ,subst[Ite]/4,subst[True][Ite]/4} / {0/0,App/2,False/0,Lam/2,S/1,True/0,V/1,c/0,c1/0,c10/0,c11/2,c12/0,c13/2 ,c14/0,c15/0,c16/2,c17/2,c18/2,c19/2,c2/0,c20/2,c21/0,c22/0,c23/2,c24/2,c25/0,c26/0,c27/0,c28/2,c29/2,c3/0 ,c30/0,c31/0,c32/0,c33/1,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/1,c40/0,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1 ,c5/0,c6/0,c7/0,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,APPE1,APPE2,EQTERM,ISLAM,ISVAR,LAMBDAINT ,LAMBODY,LAMVAR,MKAPP,MKLAM,RED,RED[LET],RED[LET][LET],SUBST,SUBST[ITE],SUBST[TRUE][ITE],and,appe1,appe2 ,eqTerm,islam,isvar,lambdaint,lambody,lamvar,mkapp,mklam,red,red[Let],red[Let][Let],subst,subst[Ite] ,subst[True][Ite]} and constructors {0,App,False,Lam,S,True,V,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19 ,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,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPE1(App(z0,z1)) -> c44() APPE2(App(z0,z1)) -> c43() EQTERM(App(z0,z1),App(z2,z3)) -> c23(AND(eqTerm(z0,z2),eqTerm(z1,z3)),EQTERM(z0,z2)) EQTERM(App(z0,z1),App(z2,z3)) -> c24(AND(eqTerm(z0,z2),eqTerm(z1,z3)),EQTERM(z1,z3)) EQTERM(App(z0,z1),Lam(z2,z3)) -> c25() EQTERM(App(z0,z1),V(z2)) -> c26() EQTERM(Lam(z0,z1),App(z2,z3)) -> c27() EQTERM(Lam(z0,z1),Lam(z2,z3)) -> c28(AND(!EQ(z0,z2),eqTerm(z1,z3)),!EQ'(z0,z2)) EQTERM(Lam(z0,z1),Lam(z2,z3)) -> c29(AND(!EQ(z0,z2),eqTerm(z1,z3)),EQTERM(z1,z3)) EQTERM(Lam(z0,z1),V(z2)) -> c30() EQTERM(V(z0),App(z1,z2)) -> c31() EQTERM(V(z0),Lam(z1,z2)) -> c32() EQTERM(V(z0),V(z1)) -> c33(!EQ'(z0,z1)) ISLAM(App(z0,z1)) -> c40() ISLAM(Lam(z0,z1)) -> c41() ISLAM(V(z0)) -> c42() ISVAR(App(z0,z1)) -> c37() ISVAR(Lam(z0,z1)) -> c38() ISVAR(V(z0)) -> c39() LAMBDAINT(z0) -> c46(RED(z0)) LAMBODY(Lam(z0,z1)) -> c36() LAMVAR(Lam(z0,z1)) -> c35() MKAPP(z0,z1) -> c45() MKLAM(V(z0),z1) -> c34() RED(App(z0,z1)) -> c20(RED[LET](App(z0,z1),red(z0)),RED(z0)) RED(Lam(z0,z1)) -> c21() RED(V(z0)) -> c22() SUBST(z0,z1,App(z2,z3)) -> c16(MKAPP(subst(z0,z1,z2),subst(z0,z1,z3)),SUBST(z0,z1,z2)) SUBST(z0,z1,App(z2,z3)) -> c17(MKAPP(subst(z0,z1,z2),subst(z0,z1,z3)),SUBST(z0,z1,z3)) SUBST(z0,z1,Lam(z2,z3)) -> c18(SUBST[TRUE][ITE](eqTerm(z0,V(z2)),z0,z1,Lam(z2,z3)),EQTERM(z0,V(z2))) SUBST(z0,z1,V(z2)) -> c19(SUBST[ITE](eqTerm(z0,V(z2)),z0,z1,V(z2)),EQTERM(z0,V(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()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() RED[LET](App(z0,z1),z2) -> c13(RED[LET][LET](App(z0,z1),z2,red(z1)),RED(z1)) RED[LET][LET](z0,App(z1,z2),z3) -> c9() RED[LET][LET](z0,Lam(z1,z2),z3) -> c8(RED(subst(V(z1),z3,z2)),SUBST(V(z1),z3,z2)) RED[LET][LET](z0,V(z1),z2) -> c10() SUBST[ITE](False(),z0,z1,z2) -> c14() SUBST[ITE](True(),z0,z1,z2) -> c15() SUBST[TRUE][ITE](False(),z0,z1,Lam(z2,z3)) -> c11(MKLAM(V(z2),subst(z0,z1,z3)),SUBST(z0,z1,z3)) SUBST[TRUE][ITE](True(),z0,z1,z2) -> c12() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() appe1(App(z0,z1)) -> z0 appe2(App(z0,z1)) -> z1 eqTerm(App(z0,z1),App(z2,z3)) -> and(eqTerm(z0,z2),eqTerm(z1,z3)) eqTerm(App(z0,z1),Lam(z2,z3)) -> False() eqTerm(App(z0,z1),V(z2)) -> False() eqTerm(Lam(z0,z1),App(z2,z3)) -> False() eqTerm(Lam(z0,z1),Lam(z2,z3)) -> and(!EQ(z0,z2),eqTerm(z1,z3)) eqTerm(Lam(z0,z1),V(z2)) -> False() eqTerm(V(z0),App(z1,z2)) -> False() eqTerm(V(z0),Lam(z1,z2)) -> False() eqTerm(V(z0),V(z1)) -> !EQ(z0,z1) islam(App(z0,z1)) -> False() islam(Lam(z0,z1)) -> True() islam(V(z0)) -> False() isvar(App(z0,z1)) -> False() isvar(Lam(z0,z1)) -> False() isvar(V(z0)) -> True() lambdaint(z0) -> red(z0) lambody(Lam(z0,z1)) -> z1 lamvar(Lam(z0,z1)) -> V(z0) mkapp(z0,z1) -> App(z0,z1) mklam(V(z0),z1) -> Lam(z0,z1) red(App(z0,z1)) -> red[Let](App(z0,z1),red(z0)) red(Lam(z0,z1)) -> Lam(z0,z1) red(V(z0)) -> V(z0) red[Let](App(z0,z1),z2) -> red[Let][Let](App(z0,z1),z2,red(z1)) red[Let][Let](z0,App(z1,z2),z3) -> App(App(z1,z2),z3) red[Let][Let](z0,Lam(z1,z2),z3) -> red(subst(V(z1),z3,z2)) red[Let][Let](z0,V(z1),z2) -> App(V(z1),z2) subst(z0,z1,App(z2,z3)) -> mkapp(subst(z0,z1,z2),subst(z0,z1,z3)) subst(z0,z1,Lam(z2,z3)) -> subst[True][Ite](eqTerm(z0,V(z2)),z0,z1,Lam(z2,z3)) subst(z0,z1,V(z2)) -> subst[Ite](eqTerm(z0,V(z2)),z0,z1,V(z2)) subst[Ite](False(),z0,z1,z2) -> z2 subst[Ite](True(),z0,z1,z2) -> z1 subst[True][Ite](False(),z0,z1,Lam(z2,z3)) -> mklam(V(z2),subst(z0,z1,z3)) subst[True][Ite](True(),z0,z1,z2) -> z2 - Signature: {!EQ/2,!EQ'/2,AND/2,APPE1/1,APPE2/1,EQTERM/2,ISLAM/1,ISVAR/1,LAMBDAINT/1,LAMBODY/1,LAMVAR/1,MKAPP/2,MKLAM/2 ,RED/1,RED[LET]/2,RED[LET][LET]/3,SUBST/3,SUBST[ITE]/4,SUBST[TRUE][ITE]/4,and/2,appe1/1,appe2/1,eqTerm/2 ,islam/1,isvar/1,lambdaint/1,lambody/1,lamvar/1,mkapp/2,mklam/2,red/1,red[Let]/2,red[Let][Let]/3,subst/3 ,subst[Ite]/4,subst[True][Ite]/4} / {0/0,App/2,False/0,Lam/2,S/1,True/0,V/1,c/0,c1/0,c10/0,c11/2,c12/0,c13/2 ,c14/0,c15/0,c16/2,c17/2,c18/2,c19/2,c2/0,c20/2,c21/0,c22/0,c23/2,c24/2,c25/0,c26/0,c27/0,c28/2,c29/2,c3/0 ,c30/0,c31/0,c32/0,c33/1,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/1,c40/0,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1 ,c5/0,c6/0,c7/0,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,APPE1,APPE2,EQTERM,ISLAM,ISVAR,LAMBDAINT ,LAMBODY,LAMVAR,MKAPP,MKLAM,RED,RED[LET],RED[LET][LET],SUBST,SUBST[ITE],SUBST[TRUE][ITE],and,appe1,appe2 ,eqTerm,islam,isvar,lambdaint,lambody,lamvar,mkapp,mklam,red,red[Let],red[Let][Let],subst,subst[Ite] ,subst[True][Ite]} and constructors {0,App,False,Lam,S,True,V,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19 ,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,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPE1(App(z0,z1)) -> c44() APPE2(App(z0,z1)) -> c43() EQTERM(App(z0,z1),App(z2,z3)) -> c23(AND(eqTerm(z0,z2),eqTerm(z1,z3)),EQTERM(z0,z2)) EQTERM(App(z0,z1),App(z2,z3)) -> c24(AND(eqTerm(z0,z2),eqTerm(z1,z3)),EQTERM(z1,z3)) EQTERM(App(z0,z1),Lam(z2,z3)) -> c25() EQTERM(App(z0,z1),V(z2)) -> c26() EQTERM(Lam(z0,z1),App(z2,z3)) -> c27() EQTERM(Lam(z0,z1),Lam(z2,z3)) -> c28(AND(!EQ(z0,z2),eqTerm(z1,z3)),!EQ'(z0,z2)) EQTERM(Lam(z0,z1),Lam(z2,z3)) -> c29(AND(!EQ(z0,z2),eqTerm(z1,z3)),EQTERM(z1,z3)) EQTERM(Lam(z0,z1),V(z2)) -> c30() EQTERM(V(z0),App(z1,z2)) -> c31() EQTERM(V(z0),Lam(z1,z2)) -> c32() EQTERM(V(z0),V(z1)) -> c33(!EQ'(z0,z1)) ISLAM(App(z0,z1)) -> c40() ISLAM(Lam(z0,z1)) -> c41() ISLAM(V(z0)) -> c42() ISVAR(App(z0,z1)) -> c37() ISVAR(Lam(z0,z1)) -> c38() ISVAR(V(z0)) -> c39() LAMBDAINT(z0) -> c46(RED(z0)) LAMBODY(Lam(z0,z1)) -> c36() LAMVAR(Lam(z0,z1)) -> c35() MKAPP(z0,z1) -> c45() MKLAM(V(z0),z1) -> c34() RED(App(z0,z1)) -> c20(RED[LET](App(z0,z1),red(z0)),RED(z0)) RED(Lam(z0,z1)) -> c21() RED(V(z0)) -> c22() SUBST(z0,z1,App(z2,z3)) -> c16(MKAPP(subst(z0,z1,z2),subst(z0,z1,z3)),SUBST(z0,z1,z2)) SUBST(z0,z1,App(z2,z3)) -> c17(MKAPP(subst(z0,z1,z2),subst(z0,z1,z3)),SUBST(z0,z1,z3)) SUBST(z0,z1,Lam(z2,z3)) -> c18(SUBST[TRUE][ITE](eqTerm(z0,V(z2)),z0,z1,Lam(z2,z3)),EQTERM(z0,V(z2))) SUBST(z0,z1,V(z2)) -> c19(SUBST[ITE](eqTerm(z0,V(z2)),z0,z1,V(z2)),EQTERM(z0,V(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()) -> c7() !EQ'(0(),S(z0)) -> c5() !EQ'(S(z0),0()) -> c6() !EQ'(S(z0),S(z1)) -> c4(!EQ'(z0,z1)) AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() RED[LET](App(z0,z1),z2) -> c13(RED[LET][LET](App(z0,z1),z2,red(z1)),RED(z1)) RED[LET][LET](z0,App(z1,z2),z3) -> c9() RED[LET][LET](z0,Lam(z1,z2),z3) -> c8(RED(subst(V(z1),z3,z2)),SUBST(V(z1),z3,z2)) RED[LET][LET](z0,V(z1),z2) -> c10() SUBST[ITE](False(),z0,z1,z2) -> c14() SUBST[ITE](True(),z0,z1,z2) -> c15() SUBST[TRUE][ITE](False(),z0,z1,Lam(z2,z3)) -> c11(MKLAM(V(z2),subst(z0,z1,z3)),SUBST(z0,z1,z3)) SUBST[TRUE][ITE](True(),z0,z1,z2) -> c12() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() appe1(App(z0,z1)) -> z0 appe2(App(z0,z1)) -> z1 eqTerm(App(z0,z1),App(z2,z3)) -> and(eqTerm(z0,z2),eqTerm(z1,z3)) eqTerm(App(z0,z1),Lam(z2,z3)) -> False() eqTerm(App(z0,z1),V(z2)) -> False() eqTerm(Lam(z0,z1),App(z2,z3)) -> False() eqTerm(Lam(z0,z1),Lam(z2,z3)) -> and(!EQ(z0,z2),eqTerm(z1,z3)) eqTerm(Lam(z0,z1),V(z2)) -> False() eqTerm(V(z0),App(z1,z2)) -> False() eqTerm(V(z0),Lam(z1,z2)) -> False() eqTerm(V(z0),V(z1)) -> !EQ(z0,z1) islam(App(z0,z1)) -> False() islam(Lam(z0,z1)) -> True() islam(V(z0)) -> False() isvar(App(z0,z1)) -> False() isvar(Lam(z0,z1)) -> False() isvar(V(z0)) -> True() lambdaint(z0) -> red(z0) lambody(Lam(z0,z1)) -> z1 lamvar(Lam(z0,z1)) -> V(z0) mkapp(z0,z1) -> App(z0,z1) mklam(V(z0),z1) -> Lam(z0,z1) red(App(z0,z1)) -> red[Let](App(z0,z1),red(z0)) red(Lam(z0,z1)) -> Lam(z0,z1) red(V(z0)) -> V(z0) red[Let](App(z0,z1),z2) -> red[Let][Let](App(z0,z1),z2,red(z1)) red[Let][Let](z0,App(z1,z2),z3) -> App(App(z1,z2),z3) red[Let][Let](z0,Lam(z1,z2),z3) -> red(subst(V(z1),z3,z2)) red[Let][Let](z0,V(z1),z2) -> App(V(z1),z2) subst(z0,z1,App(z2,z3)) -> mkapp(subst(z0,z1,z2),subst(z0,z1,z3)) subst(z0,z1,Lam(z2,z3)) -> subst[True][Ite](eqTerm(z0,V(z2)),z0,z1,Lam(z2,z3)) subst(z0,z1,V(z2)) -> subst[Ite](eqTerm(z0,V(z2)),z0,z1,V(z2)) subst[Ite](False(),z0,z1,z2) -> z2 subst[Ite](True(),z0,z1,z2) -> z1 subst[True][Ite](False(),z0,z1,Lam(z2,z3)) -> mklam(V(z2),subst(z0,z1,z3)) subst[True][Ite](True(),z0,z1,z2) -> z2 - Signature: {!EQ/2,!EQ'/2,AND/2,APPE1/1,APPE2/1,EQTERM/2,ISLAM/1,ISVAR/1,LAMBDAINT/1,LAMBODY/1,LAMVAR/1,MKAPP/2,MKLAM/2 ,RED/1,RED[LET]/2,RED[LET][LET]/3,SUBST/3,SUBST[ITE]/4,SUBST[TRUE][ITE]/4,and/2,appe1/1,appe2/1,eqTerm/2 ,islam/1,isvar/1,lambdaint/1,lambody/1,lamvar/1,mkapp/2,mklam/2,red/1,red[Let]/2,red[Let][Let]/3,subst/3 ,subst[Ite]/4,subst[True][Ite]/4} / {0/0,App/2,False/0,Lam/2,S/1,True/0,V/1,c/0,c1/0,c10/0,c11/2,c12/0,c13/2 ,c14/0,c15/0,c16/2,c17/2,c18/2,c19/2,c2/0,c20/2,c21/0,c22/0,c23/2,c24/2,c25/0,c26/0,c27/0,c28/2,c29/2,c3/0 ,c30/0,c31/0,c32/0,c33/1,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/1,c40/0,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1 ,c5/0,c6/0,c7/0,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,APPE1,APPE2,EQTERM,ISLAM,ISVAR,LAMBDAINT ,LAMBODY,LAMVAR,MKAPP,MKLAM,RED,RED[LET],RED[LET][LET],SUBST,SUBST[ITE],SUBST[TRUE][ITE],and,appe1,appe2 ,eqTerm,islam,isvar,lambdaint,lambody,lamvar,mkapp,mklam,red,red[Let],red[Let][Let],subst,subst[Ite] ,subst[True][Ite]} and constructors {0,App,False,Lam,S,True,V,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19 ,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,c5,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: EQTERM(x,z){x -> App(x,y),z -> App(z,u)} = EQTERM(App(x,y),App(z,u)) ->^+ c23(AND(eqTerm(x,z),eqTerm(y,u)),EQTERM(x,z)) = C[EQTERM(x,z) = EQTERM(x,z){}] WORST_CASE(Omega(n^1),?)