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