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))