YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { mkapp(e1, e2) -> App(e1, e2) , subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) , subst(x, a, V(int)) -> subst[Ite][True][Ite](eqTerm(x, V(int)), x, a, V(int)) , subst(x, a, Lam(var, exp)) -> subst[Ite][False][Ite][True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) , lambody(Lam(var, exp)) -> exp , isvar(App(t1, t2)) -> False() , isvar(V(int)) -> True() , isvar(Lam(int, term)) -> False() , appe2(App(e1, e2)) -> e2 , lamvar(Lam(var, exp)) -> V(var) , appe1(App(e1, e2)) -> e1 , lambdaint(e) -> red(e) , eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) , eqTerm(App(t11, t12), V(v2)) -> False() , eqTerm(App(t11, t12), Lam(i2, l2)) -> False() , eqTerm(V(v1), App(t21, t22)) -> False() , eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) , eqTerm(V(v1), Lam(i2, l2)) -> False() , eqTerm(Lam(i1, l1), App(t21, t22)) -> False() , eqTerm(Lam(i1, l1), V(v2)) -> False() , eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) , red(App(e1, e2)) -> red[Ite][False][Ite][False][Let](App(e1, e2), red(e1)) , red(V(int)) -> V(int) , red(Lam(int, term)) -> Lam(int, term) , mklam(V(name), e) -> Lam(name, e) , islam(App(t1, t2)) -> False() , islam(V(int)) -> False() , islam(Lam(int, term)) -> True() } Weak Trs: { subst[Ite][True][Ite](True(), x, a, e) -> a , subst[Ite][True][Ite](False(), x, a, e) -> e , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following dependency tuples: Strict DPs: { mkapp^#(e1, e2) -> c_1() , subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , subst^#(x, a, V(int)) -> c_3(subst[Ite][True][Ite]^#(eqTerm(x, V(int)), x, a, V(int)), eqTerm^#(x, V(int))) , subst^#(x, a, Lam(var, exp)) -> c_4(eqTerm^#(x, V(var))) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(App(t11, t12), V(v2)) -> c_14() , eqTerm^#(App(t11, t12), Lam(i2, l2)) -> c_15() , eqTerm^#(V(v1), App(t21, t22)) -> c_16() , eqTerm^#(V(v1), V(v2)) -> c_17(!EQ^#(v1, v2)) , eqTerm^#(V(v1), Lam(i2, l2)) -> c_18() , eqTerm^#(Lam(i1, l1), App(t21, t22)) -> c_19() , eqTerm^#(Lam(i1, l1), V(v2)) -> c_20() , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) , lambody^#(Lam(var, exp)) -> c_5() , isvar^#(App(t1, t2)) -> c_6() , isvar^#(V(int)) -> c_7() , isvar^#(Lam(int, term)) -> c_8() , appe2^#(App(e1, e2)) -> c_9() , lamvar^#(Lam(var, exp)) -> c_10() , appe1^#(App(e1, e2)) -> c_11() , lambdaint^#(e) -> c_12(red^#(e)) , red^#(App(e1, e2)) -> c_22(red^#(e1)) , red^#(V(int)) -> c_23() , red^#(Lam(int, term)) -> c_24() , mklam^#(V(name), e) -> c_25() , islam^#(App(t1, t2)) -> c_26() , islam^#(V(int)) -> c_27() , islam^#(Lam(int, term)) -> c_28() } Weak DPs: { subst[Ite][True][Ite]^#(True(), x, a, e) -> c_29() , subst[Ite][True][Ite]^#(False(), x, a, e) -> c_30() , and^#(True(), True()) -> c_31() , and^#(True(), False()) -> c_32() , and^#(False(), True()) -> c_33() , and^#(False(), False()) -> c_34() , !EQ^#(S(x), S(y)) -> c_35(!EQ^#(x, y)) , !EQ^#(S(x), 0()) -> c_36() , !EQ^#(0(), S(y)) -> c_37() , !EQ^#(0(), 0()) -> c_38() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { mkapp^#(e1, e2) -> c_1() , subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , subst^#(x, a, V(int)) -> c_3(subst[Ite][True][Ite]^#(eqTerm(x, V(int)), x, a, V(int)), eqTerm^#(x, V(int))) , subst^#(x, a, Lam(var, exp)) -> c_4(eqTerm^#(x, V(var))) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(App(t11, t12), V(v2)) -> c_14() , eqTerm^#(App(t11, t12), Lam(i2, l2)) -> c_15() , eqTerm^#(V(v1), App(t21, t22)) -> c_16() , eqTerm^#(V(v1), V(v2)) -> c_17(!EQ^#(v1, v2)) , eqTerm^#(V(v1), Lam(i2, l2)) -> c_18() , eqTerm^#(Lam(i1, l1), App(t21, t22)) -> c_19() , eqTerm^#(Lam(i1, l1), V(v2)) -> c_20() , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) , lambody^#(Lam(var, exp)) -> c_5() , isvar^#(App(t1, t2)) -> c_6() , isvar^#(V(int)) -> c_7() , isvar^#(Lam(int, term)) -> c_8() , appe2^#(App(e1, e2)) -> c_9() , lamvar^#(Lam(var, exp)) -> c_10() , appe1^#(App(e1, e2)) -> c_11() , lambdaint^#(e) -> c_12(red^#(e)) , red^#(App(e1, e2)) -> c_22(red^#(e1)) , red^#(V(int)) -> c_23() , red^#(Lam(int, term)) -> c_24() , mklam^#(V(name), e) -> c_25() , islam^#(App(t1, t2)) -> c_26() , islam^#(V(int)) -> c_27() , islam^#(Lam(int, term)) -> c_28() } Weak DPs: { subst[Ite][True][Ite]^#(True(), x, a, e) -> c_29() , subst[Ite][True][Ite]^#(False(), x, a, e) -> c_30() , and^#(True(), True()) -> c_31() , and^#(True(), False()) -> c_32() , and^#(False(), True()) -> c_33() , and^#(False(), False()) -> c_34() , !EQ^#(S(x), S(y)) -> c_35(!EQ^#(x, y)) , !EQ^#(S(x), 0()) -> c_36() , !EQ^#(0(), S(y)) -> c_37() , !EQ^#(0(), 0()) -> c_38() } Weak Trs: { mkapp(e1, e2) -> App(e1, e2) , subst[Ite][True][Ite](True(), x, a, e) -> a , subst[Ite][True][Ite](False(), x, a, e) -> e , subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) , subst(x, a, V(int)) -> subst[Ite][True][Ite](eqTerm(x, V(int)), x, a, V(int)) , subst(x, a, Lam(var, exp)) -> subst[Ite][False][Ite][True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , lambody(Lam(var, exp)) -> exp , isvar(App(t1, t2)) -> False() , isvar(V(int)) -> True() , isvar(Lam(int, term)) -> False() , appe2(App(e1, e2)) -> e2 , lamvar(Lam(var, exp)) -> V(var) , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() , appe1(App(e1, e2)) -> e1 , lambdaint(e) -> red(e) , eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) , eqTerm(App(t11, t12), V(v2)) -> False() , eqTerm(App(t11, t12), Lam(i2, l2)) -> False() , eqTerm(V(v1), App(t21, t22)) -> False() , eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) , eqTerm(V(v1), Lam(i2, l2)) -> False() , eqTerm(Lam(i1, l1), App(t21, t22)) -> False() , eqTerm(Lam(i1, l1), V(v2)) -> False() , eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) , red(App(e1, e2)) -> red[Ite][False][Ite][False][Let](App(e1, e2), red(e1)) , red(V(int)) -> V(int) , red(Lam(int, term)) -> Lam(int, term) , mklam(V(name), e) -> Lam(name, e) , islam(App(t1, t2)) -> False() , islam(V(int)) -> False() , islam(Lam(int, term)) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {1,6,7,8,9,10,11,12,14,15,16,17,18,19,20,23,24,25,26,27,28} by applications of Pre({1,6,7,8,9,10,11,12,14,15,16,17,18,19,20,23,24,25,26,27,28}) = {2,3,4,5,13,21,22}. Here rules are labeled as follows: DPs: { 1: mkapp^#(e1, e2) -> c_1() , 2: subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , 3: subst^#(x, a, V(int)) -> c_3(subst[Ite][True][Ite]^#(eqTerm(x, V(int)), x, a, V(int)), eqTerm^#(x, V(int))) , 4: subst^#(x, a, Lam(var, exp)) -> c_4(eqTerm^#(x, V(var))) , 5: eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , 6: eqTerm^#(App(t11, t12), V(v2)) -> c_14() , 7: eqTerm^#(App(t11, t12), Lam(i2, l2)) -> c_15() , 8: eqTerm^#(V(v1), App(t21, t22)) -> c_16() , 9: eqTerm^#(V(v1), V(v2)) -> c_17(!EQ^#(v1, v2)) , 10: eqTerm^#(V(v1), Lam(i2, l2)) -> c_18() , 11: eqTerm^#(Lam(i1, l1), App(t21, t22)) -> c_19() , 12: eqTerm^#(Lam(i1, l1), V(v2)) -> c_20() , 13: eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) , 14: lambody^#(Lam(var, exp)) -> c_5() , 15: isvar^#(App(t1, t2)) -> c_6() , 16: isvar^#(V(int)) -> c_7() , 17: isvar^#(Lam(int, term)) -> c_8() , 18: appe2^#(App(e1, e2)) -> c_9() , 19: lamvar^#(Lam(var, exp)) -> c_10() , 20: appe1^#(App(e1, e2)) -> c_11() , 21: lambdaint^#(e) -> c_12(red^#(e)) , 22: red^#(App(e1, e2)) -> c_22(red^#(e1)) , 23: red^#(V(int)) -> c_23() , 24: red^#(Lam(int, term)) -> c_24() , 25: mklam^#(V(name), e) -> c_25() , 26: islam^#(App(t1, t2)) -> c_26() , 27: islam^#(V(int)) -> c_27() , 28: islam^#(Lam(int, term)) -> c_28() , 29: subst[Ite][True][Ite]^#(True(), x, a, e) -> c_29() , 30: subst[Ite][True][Ite]^#(False(), x, a, e) -> c_30() , 31: and^#(True(), True()) -> c_31() , 32: and^#(True(), False()) -> c_32() , 33: and^#(False(), True()) -> c_33() , 34: and^#(False(), False()) -> c_34() , 35: !EQ^#(S(x), S(y)) -> c_35(!EQ^#(x, y)) , 36: !EQ^#(S(x), 0()) -> c_36() , 37: !EQ^#(0(), S(y)) -> c_37() , 38: !EQ^#(0(), 0()) -> c_38() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , subst^#(x, a, V(int)) -> c_3(subst[Ite][True][Ite]^#(eqTerm(x, V(int)), x, a, V(int)), eqTerm^#(x, V(int))) , subst^#(x, a, Lam(var, exp)) -> c_4(eqTerm^#(x, V(var))) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) , lambdaint^#(e) -> c_12(red^#(e)) , red^#(App(e1, e2)) -> c_22(red^#(e1)) } Weak DPs: { mkapp^#(e1, e2) -> c_1() , subst[Ite][True][Ite]^#(True(), x, a, e) -> c_29() , subst[Ite][True][Ite]^#(False(), x, a, e) -> c_30() , eqTerm^#(App(t11, t12), V(v2)) -> c_14() , eqTerm^#(App(t11, t12), Lam(i2, l2)) -> c_15() , eqTerm^#(V(v1), App(t21, t22)) -> c_16() , eqTerm^#(V(v1), V(v2)) -> c_17(!EQ^#(v1, v2)) , eqTerm^#(V(v1), Lam(i2, l2)) -> c_18() , eqTerm^#(Lam(i1, l1), App(t21, t22)) -> c_19() , eqTerm^#(Lam(i1, l1), V(v2)) -> c_20() , lambody^#(Lam(var, exp)) -> c_5() , isvar^#(App(t1, t2)) -> c_6() , isvar^#(V(int)) -> c_7() , isvar^#(Lam(int, term)) -> c_8() , appe2^#(App(e1, e2)) -> c_9() , lamvar^#(Lam(var, exp)) -> c_10() , appe1^#(App(e1, e2)) -> c_11() , red^#(V(int)) -> c_23() , red^#(Lam(int, term)) -> c_24() , and^#(True(), True()) -> c_31() , and^#(True(), False()) -> c_32() , and^#(False(), True()) -> c_33() , and^#(False(), False()) -> c_34() , !EQ^#(S(x), S(y)) -> c_35(!EQ^#(x, y)) , !EQ^#(S(x), 0()) -> c_36() , !EQ^#(0(), S(y)) -> c_37() , !EQ^#(0(), 0()) -> c_38() , mklam^#(V(name), e) -> c_25() , islam^#(App(t1, t2)) -> c_26() , islam^#(V(int)) -> c_27() , islam^#(Lam(int, term)) -> c_28() } Weak Trs: { mkapp(e1, e2) -> App(e1, e2) , subst[Ite][True][Ite](True(), x, a, e) -> a , subst[Ite][True][Ite](False(), x, a, e) -> e , subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) , subst(x, a, V(int)) -> subst[Ite][True][Ite](eqTerm(x, V(int)), x, a, V(int)) , subst(x, a, Lam(var, exp)) -> subst[Ite][False][Ite][True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , lambody(Lam(var, exp)) -> exp , isvar(App(t1, t2)) -> False() , isvar(V(int)) -> True() , isvar(Lam(int, term)) -> False() , appe2(App(e1, e2)) -> e2 , lamvar(Lam(var, exp)) -> V(var) , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() , appe1(App(e1, e2)) -> e1 , lambdaint(e) -> red(e) , eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) , eqTerm(App(t11, t12), V(v2)) -> False() , eqTerm(App(t11, t12), Lam(i2, l2)) -> False() , eqTerm(V(v1), App(t21, t22)) -> False() , eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) , eqTerm(V(v1), Lam(i2, l2)) -> False() , eqTerm(Lam(i1, l1), App(t21, t22)) -> False() , eqTerm(Lam(i1, l1), V(v2)) -> False() , eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) , red(App(e1, e2)) -> red[Ite][False][Ite][False][Let](App(e1, e2), red(e1)) , red(V(int)) -> V(int) , red(Lam(int, term)) -> Lam(int, term) , mklam(V(name), e) -> Lam(name, e) , islam(App(t1, t2)) -> False() , islam(V(int)) -> False() , islam(Lam(int, term)) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {2,3} by applications of Pre({2,3}) = {1}. Here rules are labeled as follows: DPs: { 1: subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , 2: subst^#(x, a, V(int)) -> c_3(subst[Ite][True][Ite]^#(eqTerm(x, V(int)), x, a, V(int)), eqTerm^#(x, V(int))) , 3: subst^#(x, a, Lam(var, exp)) -> c_4(eqTerm^#(x, V(var))) , 4: eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , 5: eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) , 6: lambdaint^#(e) -> c_12(red^#(e)) , 7: red^#(App(e1, e2)) -> c_22(red^#(e1)) , 8: mkapp^#(e1, e2) -> c_1() , 9: subst[Ite][True][Ite]^#(True(), x, a, e) -> c_29() , 10: subst[Ite][True][Ite]^#(False(), x, a, e) -> c_30() , 11: eqTerm^#(App(t11, t12), V(v2)) -> c_14() , 12: eqTerm^#(App(t11, t12), Lam(i2, l2)) -> c_15() , 13: eqTerm^#(V(v1), App(t21, t22)) -> c_16() , 14: eqTerm^#(V(v1), V(v2)) -> c_17(!EQ^#(v1, v2)) , 15: eqTerm^#(V(v1), Lam(i2, l2)) -> c_18() , 16: eqTerm^#(Lam(i1, l1), App(t21, t22)) -> c_19() , 17: eqTerm^#(Lam(i1, l1), V(v2)) -> c_20() , 18: lambody^#(Lam(var, exp)) -> c_5() , 19: isvar^#(App(t1, t2)) -> c_6() , 20: isvar^#(V(int)) -> c_7() , 21: isvar^#(Lam(int, term)) -> c_8() , 22: appe2^#(App(e1, e2)) -> c_9() , 23: lamvar^#(Lam(var, exp)) -> c_10() , 24: appe1^#(App(e1, e2)) -> c_11() , 25: red^#(V(int)) -> c_23() , 26: red^#(Lam(int, term)) -> c_24() , 27: and^#(True(), True()) -> c_31() , 28: and^#(True(), False()) -> c_32() , 29: and^#(False(), True()) -> c_33() , 30: and^#(False(), False()) -> c_34() , 31: !EQ^#(S(x), S(y)) -> c_35(!EQ^#(x, y)) , 32: !EQ^#(S(x), 0()) -> c_36() , 33: !EQ^#(0(), S(y)) -> c_37() , 34: !EQ^#(0(), 0()) -> c_38() , 35: mklam^#(V(name), e) -> c_25() , 36: islam^#(App(t1, t2)) -> c_26() , 37: islam^#(V(int)) -> c_27() , 38: islam^#(Lam(int, term)) -> c_28() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) , lambdaint^#(e) -> c_12(red^#(e)) , red^#(App(e1, e2)) -> c_22(red^#(e1)) } Weak DPs: { mkapp^#(e1, e2) -> c_1() , subst^#(x, a, V(int)) -> c_3(subst[Ite][True][Ite]^#(eqTerm(x, V(int)), x, a, V(int)), eqTerm^#(x, V(int))) , subst^#(x, a, Lam(var, exp)) -> c_4(eqTerm^#(x, V(var))) , subst[Ite][True][Ite]^#(True(), x, a, e) -> c_29() , subst[Ite][True][Ite]^#(False(), x, a, e) -> c_30() , eqTerm^#(App(t11, t12), V(v2)) -> c_14() , eqTerm^#(App(t11, t12), Lam(i2, l2)) -> c_15() , eqTerm^#(V(v1), App(t21, t22)) -> c_16() , eqTerm^#(V(v1), V(v2)) -> c_17(!EQ^#(v1, v2)) , eqTerm^#(V(v1), Lam(i2, l2)) -> c_18() , eqTerm^#(Lam(i1, l1), App(t21, t22)) -> c_19() , eqTerm^#(Lam(i1, l1), V(v2)) -> c_20() , lambody^#(Lam(var, exp)) -> c_5() , isvar^#(App(t1, t2)) -> c_6() , isvar^#(V(int)) -> c_7() , isvar^#(Lam(int, term)) -> c_8() , appe2^#(App(e1, e2)) -> c_9() , lamvar^#(Lam(var, exp)) -> c_10() , appe1^#(App(e1, e2)) -> c_11() , red^#(V(int)) -> c_23() , red^#(Lam(int, term)) -> c_24() , and^#(True(), True()) -> c_31() , and^#(True(), False()) -> c_32() , and^#(False(), True()) -> c_33() , and^#(False(), False()) -> c_34() , !EQ^#(S(x), S(y)) -> c_35(!EQ^#(x, y)) , !EQ^#(S(x), 0()) -> c_36() , !EQ^#(0(), S(y)) -> c_37() , !EQ^#(0(), 0()) -> c_38() , mklam^#(V(name), e) -> c_25() , islam^#(App(t1, t2)) -> c_26() , islam^#(V(int)) -> c_27() , islam^#(Lam(int, term)) -> c_28() } Weak Trs: { mkapp(e1, e2) -> App(e1, e2) , subst[Ite][True][Ite](True(), x, a, e) -> a , subst[Ite][True][Ite](False(), x, a, e) -> e , subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) , subst(x, a, V(int)) -> subst[Ite][True][Ite](eqTerm(x, V(int)), x, a, V(int)) , subst(x, a, Lam(var, exp)) -> subst[Ite][False][Ite][True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , lambody(Lam(var, exp)) -> exp , isvar(App(t1, t2)) -> False() , isvar(V(int)) -> True() , isvar(Lam(int, term)) -> False() , appe2(App(e1, e2)) -> e2 , lamvar(Lam(var, exp)) -> V(var) , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() , appe1(App(e1, e2)) -> e1 , lambdaint(e) -> red(e) , eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) , eqTerm(App(t11, t12), V(v2)) -> False() , eqTerm(App(t11, t12), Lam(i2, l2)) -> False() , eqTerm(V(v1), App(t21, t22)) -> False() , eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) , eqTerm(V(v1), Lam(i2, l2)) -> False() , eqTerm(Lam(i1, l1), App(t21, t22)) -> False() , eqTerm(Lam(i1, l1), V(v2)) -> False() , eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) , red(App(e1, e2)) -> red[Ite][False][Ite][False][Let](App(e1, e2), red(e1)) , red(V(int)) -> V(int) , red(Lam(int, term)) -> Lam(int, term) , mklam(V(name), e) -> Lam(name, e) , islam(App(t1, t2)) -> False() , islam(V(int)) -> False() , islam(Lam(int, term)) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { mkapp^#(e1, e2) -> c_1() , subst^#(x, a, V(int)) -> c_3(subst[Ite][True][Ite]^#(eqTerm(x, V(int)), x, a, V(int)), eqTerm^#(x, V(int))) , subst^#(x, a, Lam(var, exp)) -> c_4(eqTerm^#(x, V(var))) , subst[Ite][True][Ite]^#(True(), x, a, e) -> c_29() , subst[Ite][True][Ite]^#(False(), x, a, e) -> c_30() , eqTerm^#(App(t11, t12), V(v2)) -> c_14() , eqTerm^#(App(t11, t12), Lam(i2, l2)) -> c_15() , eqTerm^#(V(v1), App(t21, t22)) -> c_16() , eqTerm^#(V(v1), V(v2)) -> c_17(!EQ^#(v1, v2)) , eqTerm^#(V(v1), Lam(i2, l2)) -> c_18() , eqTerm^#(Lam(i1, l1), App(t21, t22)) -> c_19() , eqTerm^#(Lam(i1, l1), V(v2)) -> c_20() , lambody^#(Lam(var, exp)) -> c_5() , isvar^#(App(t1, t2)) -> c_6() , isvar^#(V(int)) -> c_7() , isvar^#(Lam(int, term)) -> c_8() , appe2^#(App(e1, e2)) -> c_9() , lamvar^#(Lam(var, exp)) -> c_10() , appe1^#(App(e1, e2)) -> c_11() , red^#(V(int)) -> c_23() , red^#(Lam(int, term)) -> c_24() , and^#(True(), True()) -> c_31() , and^#(True(), False()) -> c_32() , and^#(False(), True()) -> c_33() , and^#(False(), False()) -> c_34() , !EQ^#(S(x), S(y)) -> c_35(!EQ^#(x, y)) , !EQ^#(S(x), 0()) -> c_36() , !EQ^#(0(), S(y)) -> c_37() , !EQ^#(0(), 0()) -> c_38() , mklam^#(V(name), e) -> c_25() , islam^#(App(t1, t2)) -> c_26() , islam^#(V(int)) -> c_27() , islam^#(Lam(int, term)) -> c_28() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) , lambdaint^#(e) -> c_12(red^#(e)) , red^#(App(e1, e2)) -> c_22(red^#(e1)) } Weak Trs: { mkapp(e1, e2) -> App(e1, e2) , subst[Ite][True][Ite](True(), x, a, e) -> a , subst[Ite][True][Ite](False(), x, a, e) -> e , subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) , subst(x, a, V(int)) -> subst[Ite][True][Ite](eqTerm(x, V(int)), x, a, V(int)) , subst(x, a, Lam(var, exp)) -> subst[Ite][False][Ite][True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , lambody(Lam(var, exp)) -> exp , isvar(App(t1, t2)) -> False() , isvar(V(int)) -> True() , isvar(Lam(int, term)) -> False() , appe2(App(e1, e2)) -> e2 , lamvar(Lam(var, exp)) -> V(var) , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() , appe1(App(e1, e2)) -> e1 , lambdaint(e) -> red(e) , eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) , eqTerm(App(t11, t12), V(v2)) -> False() , eqTerm(App(t11, t12), Lam(i2, l2)) -> False() , eqTerm(V(v1), App(t21, t22)) -> False() , eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) , eqTerm(V(v1), Lam(i2, l2)) -> False() , eqTerm(Lam(i1, l1), App(t21, t22)) -> False() , eqTerm(Lam(i1, l1), V(v2)) -> False() , eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) , red(App(e1, e2)) -> red[Ite][False][Ite][False][Let](App(e1, e2), red(e1)) , red(V(int)) -> V(int) , red(Lam(int, term)) -> Lam(int, term) , mklam(V(name), e) -> Lam(name, e) , islam(App(t1, t2)) -> False() , islam(V(int)) -> False() , islam(Lam(int, term)) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { subst^#(x, a, App(e1, e2)) -> c_2(mkapp^#(subst(x, a, e1), subst(x, a, e2)), subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_13(and^#(eqTerm(t11, t21), eqTerm(t12, t22)), eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_21(and^#(!EQ(i1, i2), eqTerm(l1, l2)), !EQ^#(i1, i2), eqTerm^#(l1, l2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) , lambdaint^#(e) -> c_4(red^#(e)) , red^#(App(e1, e2)) -> c_5(red^#(e1)) } Weak Trs: { mkapp(e1, e2) -> App(e1, e2) , subst[Ite][True][Ite](True(), x, a, e) -> a , subst[Ite][True][Ite](False(), x, a, e) -> e , subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) , subst(x, a, V(int)) -> subst[Ite][True][Ite](eqTerm(x, V(int)), x, a, V(int)) , subst(x, a, Lam(var, exp)) -> subst[Ite][False][Ite][True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , lambody(Lam(var, exp)) -> exp , isvar(App(t1, t2)) -> False() , isvar(V(int)) -> True() , isvar(Lam(int, term)) -> False() , appe2(App(e1, e2)) -> e2 , lamvar(Lam(var, exp)) -> V(var) , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() , appe1(App(e1, e2)) -> e1 , lambdaint(e) -> red(e) , eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) , eqTerm(App(t11, t12), V(v2)) -> False() , eqTerm(App(t11, t12), Lam(i2, l2)) -> False() , eqTerm(V(v1), App(t21, t22)) -> False() , eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) , eqTerm(V(v1), Lam(i2, l2)) -> False() , eqTerm(Lam(i1, l1), App(t21, t22)) -> False() , eqTerm(Lam(i1, l1), V(v2)) -> False() , eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) , red(App(e1, e2)) -> red[Ite][False][Ite][False][Let](App(e1, e2), red(e1)) , red(V(int)) -> V(int) , red(Lam(int, term)) -> Lam(int, term) , mklam(V(name), e) -> Lam(name, e) , islam(App(t1, t2)) -> False() , islam(V(int)) -> False() , islam(Lam(int, term)) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) , lambdaint^#(e) -> c_4(red^#(e)) , red^#(App(e1, e2)) -> c_5(red^#(e1)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Consider the dependency graph 1: subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) -->_2 subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) :1 -->_1 subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) :1 2: eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) -->_2 eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) :3 -->_1 eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) :3 -->_2 eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) :2 -->_1 eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) :2 3: eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) -->_1 eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) :3 -->_1 eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) :2 4: lambdaint^#(e) -> c_4(red^#(e)) -->_1 red^#(App(e1, e2)) -> c_5(red^#(e1)) :5 5: red^#(App(e1, e2)) -> c_5(red^#(e1)) -->_1 red^#(App(e1, e2)) -> c_5(red^#(e1)) :5 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { lambdaint^#(e) -> c_4(red^#(e)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) , red^#(App(e1, e2)) -> c_5(red^#(e1)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [App](x1, x2) = [1] x1 + [1] x2 + [4] [True] = [0] [mkapp](x1, x2) = [7] x1 + [7] x2 + [0] [V](x1) = [1] x1 + [0] [subst[Ite][True][Ite]](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [subst](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and](x1, x2) = [7] x1 + [7] x2 + [0] [lambody](x1) = [7] x1 + [0] [isvar](x1) = [7] x1 + [0] [appe2](x1) = [7] x1 + [0] [lamvar](x1) = [7] x1 + [0] [!EQ](x1, x2) = [7] x1 + [7] x2 + [0] [appe1](x1) = [7] x1 + [0] [Lam](x1, x2) = [1] x1 + [1] x2 + [0] [lambdaint](x1) = [7] x1 + [0] [S](x1) = [1] x1 + [0] [eqTerm](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [subst[Ite][False][Ite][True][Ite]](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] [red[Ite][False][Ite][False][Let]](x1, x2) = [1] x1 + [1] x2 + [0] [red](x1) = [7] x1 + [0] [mklam](x1, x2) = [7] x1 + [7] x2 + [0] [False] = [0] [islam](x1) = [7] x1 + [0] [mkapp^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [subst^#](x1, x2, x3) = [0] [c_2](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_3](x1, x2) = [7] x1 + [7] x2 + [0] [subst[Ite][True][Ite]^#](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [eqTerm^#](x1, x2) = [2] x2 + [0] [c_4](x1) = [7] x1 + [0] [lambody^#](x1) = [7] x1 + [0] [c_5] = [0] [isvar^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7] = [0] [c_8] = [0] [appe2^#](x1) = [7] x1 + [0] [c_9] = [0] [lamvar^#](x1) = [7] x1 + [0] [c_10] = [0] [appe1^#](x1) = [7] x1 + [0] [c_11] = [0] [lambdaint^#](x1) = [7] x1 + [0] [c_12](x1) = [7] x1 + [0] [red^#](x1) = [0] [c_13](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_14] = [0] [c_15] = [0] [c_16] = [0] [c_17](x1) = [7] x1 + [0] [!EQ^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_18] = [0] [c_19] = [0] [c_20] = [0] [c_21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_22](x1) = [7] x1 + [0] [c_23] = [0] [c_24] = [0] [mklam^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_25] = [0] [islam^#](x1) = [7] x1 + [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](x1) = [7] x1 + [0] [c_36] = [0] [c_37] = [0] [c_38] = [0] [c] = [0] [c_1](x1, x2) = [4] x1 + [2] x2 + [0] [c_2](x1, x2) = [1] x1 + [1] x2 + [1] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [7] x1 + [0] [c_5](x1) = [2] x1 + [0] The following symbols are considered usable {subst^#, eqTerm^#, red^#} The order satisfies the following ordering constraints: [subst^#(x, a, App(e1, e2))] = [0] >= [0] = [c_1(subst^#(x, a, e1), subst^#(x, a, e2))] [eqTerm^#(App(t11, t12), App(t21, t22))] = [2] t21 + [2] t22 + [8] > [2] t21 + [2] t22 + [1] = [c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22))] [eqTerm^#(Lam(i1, l1), Lam(i2, l2))] = [2] i2 + [2] l2 + [0] >= [2] l2 + [0] = [c_3(eqTerm^#(l1, l2))] [red^#(App(e1, e2))] = [0] >= [0] = [c_5(red^#(e1))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) , red^#(App(e1, e2)) -> c_5(red^#(e1)) } Weak DPs: { eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) , 4: eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [App](x1, x2) = [1] x1 + [1] x2 + [4] [True] = [0] [mkapp](x1, x2) = [7] x1 + [7] x2 + [0] [V](x1) = [1] x1 + [0] [subst[Ite][True][Ite]](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [subst](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and](x1, x2) = [7] x1 + [7] x2 + [0] [lambody](x1) = [7] x1 + [0] [isvar](x1) = [7] x1 + [0] [appe2](x1) = [7] x1 + [0] [lamvar](x1) = [7] x1 + [0] [!EQ](x1, x2) = [7] x1 + [7] x2 + [0] [appe1](x1) = [7] x1 + [0] [Lam](x1, x2) = [1] x1 + [1] x2 + [0] [lambdaint](x1) = [7] x1 + [0] [S](x1) = [1] x1 + [0] [eqTerm](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [subst[Ite][False][Ite][True][Ite]](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] [red[Ite][False][Ite][False][Let]](x1, x2) = [1] x1 + [1] x2 + [0] [red](x1) = [7] x1 + [0] [mklam](x1, x2) = [7] x1 + [7] x2 + [0] [False] = [0] [islam](x1) = [7] x1 + [0] [mkapp^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [subst^#](x1, x2, x3) = [2] x3 + [0] [c_2](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_3](x1, x2) = [7] x1 + [7] x2 + [0] [subst[Ite][True][Ite]^#](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [eqTerm^#](x1, x2) = [2] x1 + [0] [c_4](x1) = [7] x1 + [0] [lambody^#](x1) = [7] x1 + [0] [c_5] = [0] [isvar^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7] = [0] [c_8] = [0] [appe2^#](x1) = [7] x1 + [0] [c_9] = [0] [lamvar^#](x1) = [7] x1 + [0] [c_10] = [0] [appe1^#](x1) = [7] x1 + [0] [c_11] = [0] [lambdaint^#](x1) = [7] x1 + [0] [c_12](x1) = [7] x1 + [0] [red^#](x1) = [0] [c_13](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_14] = [0] [c_15] = [0] [c_16] = [0] [c_17](x1) = [7] x1 + [0] [!EQ^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_18] = [0] [c_19] = [0] [c_20] = [0] [c_21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_22](x1) = [7] x1 + [0] [c_23] = [0] [c_24] = [0] [mklam^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_25] = [0] [islam^#](x1) = [7] x1 + [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](x1) = [7] x1 + [0] [c_36] = [0] [c_37] = [0] [c_38] = [0] [c] = [0] [c_1](x1, x2) = [1] x1 + [1] x2 + [1] [c_2](x1, x2) = [1] x1 + [1] x2 + [7] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [7] x1 + [0] [c_5](x1) = [2] x1 + [0] The following symbols are considered usable {subst^#, eqTerm^#, red^#} The order satisfies the following ordering constraints: [subst^#(x, a, App(e1, e2))] = [2] e1 + [2] e2 + [8] > [2] e1 + [2] e2 + [1] = [c_1(subst^#(x, a, e1), subst^#(x, a, e2))] [eqTerm^#(App(t11, t12), App(t21, t22))] = [2] t11 + [2] t12 + [8] > [2] t11 + [2] t12 + [7] = [c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22))] [eqTerm^#(Lam(i1, l1), Lam(i2, l2))] = [2] i1 + [2] l1 + [0] >= [2] l1 + [0] = [c_3(eqTerm^#(l1, l2))] [red^#(App(e1, e2))] = [0] >= [0] = [c_5(red^#(e1))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) , red^#(App(e1, e2)) -> c_5(red^#(e1)) } Weak DPs: { subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) , eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { subst^#(x, a, App(e1, e2)) -> c_1(subst^#(x, a, e1), subst^#(x, a, e2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) , red^#(App(e1, e2)) -> c_5(red^#(e1)) } Weak DPs: { eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: red^#(App(e1, e2)) -> c_5(red^#(e1)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [App](x1, x2) = [1] x1 + [1] x2 + [4] [True] = [0] [mkapp](x1, x2) = [7] x1 + [7] x2 + [0] [V](x1) = [1] x1 + [0] [subst[Ite][True][Ite]](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [subst](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and](x1, x2) = [7] x1 + [7] x2 + [0] [lambody](x1) = [7] x1 + [0] [isvar](x1) = [7] x1 + [0] [appe2](x1) = [7] x1 + [0] [lamvar](x1) = [7] x1 + [0] [!EQ](x1, x2) = [7] x1 + [7] x2 + [0] [appe1](x1) = [7] x1 + [0] [Lam](x1, x2) = [1] x1 + [1] x2 + [0] [lambdaint](x1) = [7] x1 + [0] [S](x1) = [1] x1 + [0] [eqTerm](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [subst[Ite][False][Ite][True][Ite]](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] [red[Ite][False][Ite][False][Let]](x1, x2) = [1] x1 + [1] x2 + [0] [red](x1) = [7] x1 + [0] [mklam](x1, x2) = [7] x1 + [7] x2 + [0] [False] = [0] [islam](x1) = [7] x1 + [0] [mkapp^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [subst^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_2](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_3](x1, x2) = [7] x1 + [7] x2 + [0] [subst[Ite][True][Ite]^#](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [eqTerm^#](x1, x2) = [0] [c_4](x1) = [7] x1 + [0] [lambody^#](x1) = [7] x1 + [0] [c_5] = [0] [isvar^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7] = [0] [c_8] = [0] [appe2^#](x1) = [7] x1 + [0] [c_9] = [0] [lamvar^#](x1) = [7] x1 + [0] [c_10] = [0] [appe1^#](x1) = [7] x1 + [0] [c_11] = [0] [lambdaint^#](x1) = [7] x1 + [0] [c_12](x1) = [7] x1 + [0] [red^#](x1) = [2] x1 + [0] [c_13](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_14] = [0] [c_15] = [0] [c_16] = [0] [c_17](x1) = [7] x1 + [0] [!EQ^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_18] = [0] [c_19] = [0] [c_20] = [0] [c_21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_22](x1) = [7] x1 + [0] [c_23] = [0] [c_24] = [0] [mklam^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_25] = [0] [islam^#](x1) = [7] x1 + [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](x1) = [7] x1 + [0] [c_36] = [0] [c_37] = [0] [c_38] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [1] x1 + [4] x2 + [0] [c_3](x1) = [2] x1 + [0] [c_4](x1) = [7] x1 + [0] [c_5](x1) = [1] x1 + [1] The following symbols are considered usable {eqTerm^#, red^#} The order satisfies the following ordering constraints: [eqTerm^#(App(t11, t12), App(t21, t22))] = [0] >= [0] = [c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22))] [eqTerm^#(Lam(i1, l1), Lam(i2, l2))] = [0] >= [0] = [c_3(eqTerm^#(l1, l2))] [red^#(App(e1, e2))] = [2] e1 + [2] e2 + [8] > [2] e1 + [1] = [c_5(red^#(e1))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) } Weak DPs: { eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , red^#(App(e1, e2)) -> c_5(red^#(e1)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { red^#(App(e1, e2)) -> c_5(red^#(e1)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) } Weak DPs: { eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_2) = {1, 2}, Uargs(c_3) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [App](x1, x2) = [1] x1 + [1] x2 + [0] [True] = [0] [mkapp](x1, x2) = [7] x1 + [7] x2 + [0] [V](x1) = [1] x1 + [0] [subst[Ite][True][Ite]](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [subst](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and](x1, x2) = [7] x1 + [7] x2 + [0] [lambody](x1) = [7] x1 + [0] [isvar](x1) = [7] x1 + [0] [appe2](x1) = [7] x1 + [0] [lamvar](x1) = [7] x1 + [0] [!EQ](x1, x2) = [7] x1 + [7] x2 + [0] [appe1](x1) = [7] x1 + [0] [Lam](x1, x2) = [1] x1 + [1] x2 + [4] [lambdaint](x1) = [7] x1 + [0] [S](x1) = [1] x1 + [0] [eqTerm](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [subst[Ite][False][Ite][True][Ite]](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] [red[Ite][False][Ite][False][Let]](x1, x2) = [1] x1 + [1] x2 + [0] [red](x1) = [7] x1 + [0] [mklam](x1, x2) = [7] x1 + [7] x2 + [0] [False] = [0] [islam](x1) = [7] x1 + [0] [mkapp^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [subst^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_2](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_3](x1, x2) = [7] x1 + [7] x2 + [0] [subst[Ite][True][Ite]^#](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [eqTerm^#](x1, x2) = [2] x1 + [0] [c_4](x1) = [7] x1 + [0] [lambody^#](x1) = [7] x1 + [0] [c_5] = [0] [isvar^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7] = [0] [c_8] = [0] [appe2^#](x1) = [7] x1 + [0] [c_9] = [0] [lamvar^#](x1) = [7] x1 + [0] [c_10] = [0] [appe1^#](x1) = [7] x1 + [0] [c_11] = [0] [lambdaint^#](x1) = [7] x1 + [0] [c_12](x1) = [7] x1 + [0] [red^#](x1) = [7] x1 + [0] [c_13](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [and^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_14] = [0] [c_15] = [0] [c_16] = [0] [c_17](x1) = [7] x1 + [0] [!EQ^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_18] = [0] [c_19] = [0] [c_20] = [0] [c_21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_22](x1) = [7] x1 + [0] [c_23] = [0] [c_24] = [0] [mklam^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_25] = [0] [islam^#](x1) = [7] x1 + [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](x1) = [7] x1 + [0] [c_36] = [0] [c_37] = [0] [c_38] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [1] x1 + [1] x2 + [0] [c_3](x1) = [1] x1 + [5] [c_4](x1) = [7] x1 + [0] [c_5](x1) = [7] x1 + [0] The following symbols are considered usable {eqTerm^#} The order satisfies the following ordering constraints: [eqTerm^#(App(t11, t12), App(t21, t22))] = [2] t11 + [2] t12 + [0] >= [2] t11 + [2] t12 + [0] = [c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22))] [eqTerm^#(Lam(i1, l1), Lam(i2, l2))] = [2] i1 + [2] l1 + [8] > [2] l1 + [5] = [c_3(eqTerm^#(l1, l2))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { eqTerm^#(App(t11, t12), App(t21, t22)) -> c_2(eqTerm^#(t11, t21), eqTerm^#(t12, t22)) , eqTerm^#(Lam(i1, l1), Lam(i2, l2)) -> c_3(eqTerm^#(l1, l2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))