WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 420 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 309 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 1523 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 231 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 2394 ms]
        (22) BOUNDS(1, INF)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
   subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
   red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
   red(Lam(int, term)) -> Lam(int, term)
   subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), x, a, V(int))
   red(V(int)) -> V(int)
   eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
   eqTerm(App(t11, t12), Lam(i2, l2)) -> False
   eqTerm(App(t11, t12), V(v2)) -> False
   eqTerm(Lam(i1, l1), App(t21, t22)) -> False
   eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
   eqTerm(Lam(i1, l1), V(v2)) -> False
   eqTerm(V(v1), App(t21, t22)) -> False
   eqTerm(V(v1), Lam(i2, l2)) -> False
   eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
   mklam(V(name), e) -> Lam(name, e)
   lamvar(Lam(var, exp)) -> V(var)
   lambody(Lam(var, exp)) -> exp
   isvar(App(t1, t2)) -> False
   isvar(Lam(int, term)) -> False
   isvar(V(int)) -> True
   islam(App(t1, t2)) -> False
   islam(Lam(int, term)) -> True
   islam(V(int)) -> False
   appe2(App(e1, e2)) -> e2
   appe1(App(e1, e2)) -> e1
   mkapp(e1, e2) -> App(e1, e2)
   lambdaint(e) -> red(e)

The (relative) TRS S consists of the following rules:

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   red[Let][Let](e, Lam(var, exp), a) -> red(subst(V(var), a, exp))
   subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
   red[Let][Let](e, App(t1, t2), e2) -> App(App(t1, t2), e2)
   red[Let][Let](e, V(int), e2) -> App(V(int), e2)
   red[Let](App(e1, e2), f) -> red[Let][Let](App(e1, e2), f, red(e2))
   subst[True][Ite](True, x, a, e) -> e
   subst[Ite](False, x, a, e) -> e
   subst[Ite](True, x, a, e) -> a

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
   subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
   red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
   red(Lam(int, term)) -> Lam(int, term)
   subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), x, a, V(int))
   red(V(int)) -> V(int)
   eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
   eqTerm(App(t11, t12), Lam(i2, l2)) -> False
   eqTerm(App(t11, t12), V(v2)) -> False
   eqTerm(Lam(i1, l1), App(t21, t22)) -> False
   eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
   eqTerm(Lam(i1, l1), V(v2)) -> False
   eqTerm(V(v1), App(t21, t22)) -> False
   eqTerm(V(v1), Lam(i2, l2)) -> False
   eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
   mklam(V(name), e) -> Lam(name, e)
   lamvar(Lam(var, exp)) -> V(var)
   lambody(Lam(var, exp)) -> exp
   isvar(App(t1, t2)) -> False
   isvar(Lam(int, term)) -> False
   isvar(V(int)) -> True
   islam(App(t1, t2)) -> False
   islam(Lam(int, term)) -> True
   islam(V(int)) -> False
   appe2(App(e1, e2)) -> e2
   appe1(App(e1, e2)) -> e1
   mkapp(e1, e2) -> App(e1, e2)
   lambdaint(e) -> red(e)

The (relative) TRS S consists of the following rules:

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   red[Let][Let](e, Lam(var, exp), a) -> red(subst(V(var), a, exp))
   subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
   red[Let][Let](e, App(t1, t2), e2) -> App(App(t1, t2), e2)
   red[Let][Let](e, V(int), e2) -> App(V(int), e2)
   red[Let](App(e1, e2), f) -> red[Let][Let](App(e1, e2), f, red(e2))
   subst[True][Ite](True, x, a, e) -> e
   subst[Ite](False, x, a, e) -> e
   subst[Ite](True, x, a, e) -> a

Rewrite Strategy: INNERMOST
----------------------------------------

(3) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
   subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
   red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
   red(Lam(int, term)) -> Lam(int, term)
   subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), x, a, V(int))
   red(V(int)) -> V(int)
   eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
   eqTerm(App(t11, t12), Lam(i2, l2)) -> False
   eqTerm(App(t11, t12), V(v2)) -> False
   eqTerm(Lam(i1, l1), App(t21, t22)) -> False
   eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
   eqTerm(Lam(i1, l1), V(v2)) -> False
   eqTerm(V(v1), App(t21, t22)) -> False
   eqTerm(V(v1), Lam(i2, l2)) -> False
   eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
   mklam(V(name), e) -> Lam(name, e)
   lamvar(Lam(var, exp)) -> V(var)
   lambody(Lam(var, exp)) -> exp
   isvar(App(t1, t2)) -> False
   isvar(Lam(int, term)) -> False
   isvar(V(int)) -> True
   islam(App(t1, t2)) -> False
   islam(Lam(int, term)) -> True
   islam(V(int)) -> False
   appe2(App(e1, e2)) -> e2
   appe1(App(e1, e2)) -> e1
   mkapp(e1, e2) -> App(e1, e2)
   lambdaint(e) -> red(e)

The (relative) TRS S consists of the following rules:

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0', S(y)) -> False
   !EQ(S(x), 0') -> False
   !EQ(0', 0') -> True
   red[Let][Let](e, Lam(var, exp), a) -> red(subst(V(var), a, exp))
   subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
   red[Let][Let](e, App(t1, t2), e2) -> App(App(t1, t2), e2)
   red[Let][Let](e, V(int), e2) -> App(V(int), e2)
   red[Let](App(e1, e2), f) -> red[Let][Let](App(e1, e2), f, red(e2))
   subst[True][Ite](True, x, a, e) -> e
   subst[Ite](False, x, a, e) -> e
   subst[Ite](True, x, a, e) -> a

Rewrite Strategy: INNERMOST
----------------------------------------

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
subst[Ite]/1
red[Let][Let]/0

----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
   subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
   red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
   red(Lam(int, term)) -> Lam(int, term)
   subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int))
   red(V(int)) -> V(int)
   eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
   eqTerm(App(t11, t12), Lam(i2, l2)) -> False
   eqTerm(App(t11, t12), V(v2)) -> False
   eqTerm(Lam(i1, l1), App(t21, t22)) -> False
   eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
   eqTerm(Lam(i1, l1), V(v2)) -> False
   eqTerm(V(v1), App(t21, t22)) -> False
   eqTerm(V(v1), Lam(i2, l2)) -> False
   eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
   mklam(V(name), e) -> Lam(name, e)
   lamvar(Lam(var, exp)) -> V(var)
   lambody(Lam(var, exp)) -> exp
   isvar(App(t1, t2)) -> False
   isvar(Lam(int, term)) -> False
   isvar(V(int)) -> True
   islam(App(t1, t2)) -> False
   islam(Lam(int, term)) -> True
   islam(V(int)) -> False
   appe2(App(e1, e2)) -> e2
   appe1(App(e1, e2)) -> e1
   mkapp(e1, e2) -> App(e1, e2)
   lambdaint(e) -> red(e)

The (relative) TRS S consists of the following rules:

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0', S(y)) -> False
   !EQ(S(x), 0') -> False
   !EQ(0', 0') -> True
   red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp))
   subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
   red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2)
   red[Let][Let](V(int), e2) -> App(V(int), e2)
   red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2))
   subst[True][Ite](True, x, a, e) -> e
   subst[Ite](False, a, e) -> e
   subst[Ite](True, a, e) -> a

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) -> Lam(int, term)
subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) -> V(int)
eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) -> False
eqTerm(App(t11, t12), V(v2)) -> False
eqTerm(Lam(i1, l1), App(t21, t22)) -> False
eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) -> False
eqTerm(V(v1), App(t21, t22)) -> False
eqTerm(V(v1), Lam(i2, l2)) -> False
eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
mklam(V(name), e) -> Lam(name, e)
lamvar(Lam(var, exp)) -> V(var)
lambody(Lam(var, exp)) -> exp
isvar(App(t1, t2)) -> False
isvar(Lam(int, term)) -> False
isvar(V(int)) -> True
islam(App(t1, t2)) -> False
islam(Lam(int, term)) -> True
islam(V(int)) -> False
appe2(App(e1, e2)) -> e2
appe1(App(e1, e2)) -> e1
mkapp(e1, e2) -> App(e1, e2)
lambdaint(e) -> red(e)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2)
red[Let][Let](V(int), e2) -> App(V(int), e2)
red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) -> e
subst[Ite](False, a, e) -> e
subst[Ite](True, a, e) -> a

Types:
subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
App :: App:Lam:V -> App:Lam:V -> App:Lam:V
mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V
Lam :: S:0' -> App:Lam:V -> App:Lam:V
subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
eqTerm :: App:Lam:V -> App:Lam:V -> False:True
V :: S:0' -> App:Lam:V
red :: App:Lam:V -> App:Lam:V
red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V
and :: False:True -> False:True -> False:True
False :: False:True
!EQ :: S:0' -> S:0' -> False:True
mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V
lamvar :: App:Lam:V -> App:Lam:V
lambody :: App:Lam:V -> App:Lam:V
isvar :: App:Lam:V -> False:True
True :: False:True
islam :: App:Lam:V -> False:True
appe2 :: App:Lam:V -> App:Lam:V
appe1 :: App:Lam:V -> App:Lam:V
lambdaint :: App:Lam:V -> App:Lam:V
S :: S:0' -> S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat -> App:Lam:V
gen_S:0'5_0 :: Nat -> S:0'

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
subst, eqTerm, red, !EQ

They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red
!EQ < eqTerm

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) -> Lam(int, term)
subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) -> V(int)
eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) -> False
eqTerm(App(t11, t12), V(v2)) -> False
eqTerm(Lam(i1, l1), App(t21, t22)) -> False
eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) -> False
eqTerm(V(v1), App(t21, t22)) -> False
eqTerm(V(v1), Lam(i2, l2)) -> False
eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
mklam(V(name), e) -> Lam(name, e)
lamvar(Lam(var, exp)) -> V(var)
lambody(Lam(var, exp)) -> exp
isvar(App(t1, t2)) -> False
isvar(Lam(int, term)) -> False
isvar(V(int)) -> True
islam(App(t1, t2)) -> False
islam(Lam(int, term)) -> True
islam(V(int)) -> False
appe2(App(e1, e2)) -> e2
appe1(App(e1, e2)) -> e1
mkapp(e1, e2) -> App(e1, e2)
lambdaint(e) -> red(e)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2)
red[Let][Let](V(int), e2) -> App(V(int), e2)
red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) -> e
subst[Ite](False, a, e) -> e
subst[Ite](True, a, e) -> a

Types:
subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
App :: App:Lam:V -> App:Lam:V -> App:Lam:V
mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V
Lam :: S:0' -> App:Lam:V -> App:Lam:V
subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
eqTerm :: App:Lam:V -> App:Lam:V -> False:True
V :: S:0' -> App:Lam:V
red :: App:Lam:V -> App:Lam:V
red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V
and :: False:True -> False:True -> False:True
False :: False:True
!EQ :: S:0' -> S:0' -> False:True
mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V
lamvar :: App:Lam:V -> App:Lam:V
lambody :: App:Lam:V -> App:Lam:V
isvar :: App:Lam:V -> False:True
True :: False:True
islam :: App:Lam:V -> False:True
appe2 :: App:Lam:V -> App:Lam:V
appe1 :: App:Lam:V -> App:Lam:V
lambdaint :: App:Lam:V -> App:Lam:V
S :: S:0' -> S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat -> App:Lam:V
gen_S:0'5_0 :: Nat -> S:0'


Generator Equations:
gen_App:Lam:V4_0(0) <=> V(0')
gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))


The following defined symbols remain to be analysed:
!EQ, subst, eqTerm, red

They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red
!EQ < eqTerm

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0)

Induction Base:
!EQ(gen_S:0'5_0(0), gen_S:0'5_0(+(1, 0))) ->_R^Omega(0)
False

Induction Step:
!EQ(gen_S:0'5_0(+(n7_0, 1)), gen_S:0'5_0(+(1, +(n7_0, 1)))) ->_R^Omega(0)
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) ->_IH
False

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(12)
Obligation:
Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) -> Lam(int, term)
subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) -> V(int)
eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) -> False
eqTerm(App(t11, t12), V(v2)) -> False
eqTerm(Lam(i1, l1), App(t21, t22)) -> False
eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) -> False
eqTerm(V(v1), App(t21, t22)) -> False
eqTerm(V(v1), Lam(i2, l2)) -> False
eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
mklam(V(name), e) -> Lam(name, e)
lamvar(Lam(var, exp)) -> V(var)
lambody(Lam(var, exp)) -> exp
isvar(App(t1, t2)) -> False
isvar(Lam(int, term)) -> False
isvar(V(int)) -> True
islam(App(t1, t2)) -> False
islam(Lam(int, term)) -> True
islam(V(int)) -> False
appe2(App(e1, e2)) -> e2
appe1(App(e1, e2)) -> e1
mkapp(e1, e2) -> App(e1, e2)
lambdaint(e) -> red(e)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2)
red[Let][Let](V(int), e2) -> App(V(int), e2)
red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) -> e
subst[Ite](False, a, e) -> e
subst[Ite](True, a, e) -> a

Types:
subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
App :: App:Lam:V -> App:Lam:V -> App:Lam:V
mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V
Lam :: S:0' -> App:Lam:V -> App:Lam:V
subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
eqTerm :: App:Lam:V -> App:Lam:V -> False:True
V :: S:0' -> App:Lam:V
red :: App:Lam:V -> App:Lam:V
red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V
and :: False:True -> False:True -> False:True
False :: False:True
!EQ :: S:0' -> S:0' -> False:True
mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V
lamvar :: App:Lam:V -> App:Lam:V
lambody :: App:Lam:V -> App:Lam:V
isvar :: App:Lam:V -> False:True
True :: False:True
islam :: App:Lam:V -> False:True
appe2 :: App:Lam:V -> App:Lam:V
appe1 :: App:Lam:V -> App:Lam:V
lambdaint :: App:Lam:V -> App:Lam:V
S :: S:0' -> S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat -> App:Lam:V
gen_S:0'5_0 :: Nat -> S:0'


Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0)


Generator Equations:
gen_App:Lam:V4_0(0) <=> V(0')
gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))


The following defined symbols remain to be analysed:
eqTerm, subst, red

They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red

----------------------------------------

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)) -> False, rt in Omega(1 + n460_0)

Induction Base:
eqTerm(gen_App:Lam:V4_0(+(1, 0)), gen_App:Lam:V4_0(0)) ->_R^Omega(1)
False

Induction Step:
eqTerm(gen_App:Lam:V4_0(+(1, +(n460_0, 1))), gen_App:Lam:V4_0(+(n460_0, 1))) ->_R^Omega(1)
and(eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)), eqTerm(V(0'), V(0'))) ->_IH
and(False, eqTerm(V(0'), V(0'))) ->_R^Omega(1)
and(False, !EQ(0', 0')) ->_R^Omega(0)
and(False, True) ->_R^Omega(0)
False

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(14)
Complex Obligation (BEST)

----------------------------------------

(15)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) -> Lam(int, term)
subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) -> V(int)
eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) -> False
eqTerm(App(t11, t12), V(v2)) -> False
eqTerm(Lam(i1, l1), App(t21, t22)) -> False
eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) -> False
eqTerm(V(v1), App(t21, t22)) -> False
eqTerm(V(v1), Lam(i2, l2)) -> False
eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
mklam(V(name), e) -> Lam(name, e)
lamvar(Lam(var, exp)) -> V(var)
lambody(Lam(var, exp)) -> exp
isvar(App(t1, t2)) -> False
isvar(Lam(int, term)) -> False
isvar(V(int)) -> True
islam(App(t1, t2)) -> False
islam(Lam(int, term)) -> True
islam(V(int)) -> False
appe2(App(e1, e2)) -> e2
appe1(App(e1, e2)) -> e1
mkapp(e1, e2) -> App(e1, e2)
lambdaint(e) -> red(e)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2)
red[Let][Let](V(int), e2) -> App(V(int), e2)
red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) -> e
subst[Ite](False, a, e) -> e
subst[Ite](True, a, e) -> a

Types:
subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
App :: App:Lam:V -> App:Lam:V -> App:Lam:V
mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V
Lam :: S:0' -> App:Lam:V -> App:Lam:V
subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
eqTerm :: App:Lam:V -> App:Lam:V -> False:True
V :: S:0' -> App:Lam:V
red :: App:Lam:V -> App:Lam:V
red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V
and :: False:True -> False:True -> False:True
False :: False:True
!EQ :: S:0' -> S:0' -> False:True
mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V
lamvar :: App:Lam:V -> App:Lam:V
lambody :: App:Lam:V -> App:Lam:V
isvar :: App:Lam:V -> False:True
True :: False:True
islam :: App:Lam:V -> False:True
appe2 :: App:Lam:V -> App:Lam:V
appe1 :: App:Lam:V -> App:Lam:V
lambdaint :: App:Lam:V -> App:Lam:V
S :: S:0' -> S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat -> App:Lam:V
gen_S:0'5_0 :: Nat -> S:0'


Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0)


Generator Equations:
gen_App:Lam:V4_0(0) <=> V(0')
gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))


The following defined symbols remain to be analysed:
eqTerm, subst, red

They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red

----------------------------------------

(16) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(17)
BOUNDS(n^1, INF)

----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) -> Lam(int, term)
subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) -> V(int)
eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) -> False
eqTerm(App(t11, t12), V(v2)) -> False
eqTerm(Lam(i1, l1), App(t21, t22)) -> False
eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) -> False
eqTerm(V(v1), App(t21, t22)) -> False
eqTerm(V(v1), Lam(i2, l2)) -> False
eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
mklam(V(name), e) -> Lam(name, e)
lamvar(Lam(var, exp)) -> V(var)
lambody(Lam(var, exp)) -> exp
isvar(App(t1, t2)) -> False
isvar(Lam(int, term)) -> False
isvar(V(int)) -> True
islam(App(t1, t2)) -> False
islam(Lam(int, term)) -> True
islam(V(int)) -> False
appe2(App(e1, e2)) -> e2
appe1(App(e1, e2)) -> e1
mkapp(e1, e2) -> App(e1, e2)
lambdaint(e) -> red(e)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2)
red[Let][Let](V(int), e2) -> App(V(int), e2)
red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) -> e
subst[Ite](False, a, e) -> e
subst[Ite](True, a, e) -> a

Types:
subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
App :: App:Lam:V -> App:Lam:V -> App:Lam:V
mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V
Lam :: S:0' -> App:Lam:V -> App:Lam:V
subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
eqTerm :: App:Lam:V -> App:Lam:V -> False:True
V :: S:0' -> App:Lam:V
red :: App:Lam:V -> App:Lam:V
red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V
and :: False:True -> False:True -> False:True
False :: False:True
!EQ :: S:0' -> S:0' -> False:True
mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V
lamvar :: App:Lam:V -> App:Lam:V
lambody :: App:Lam:V -> App:Lam:V
isvar :: App:Lam:V -> False:True
True :: False:True
islam :: App:Lam:V -> False:True
appe2 :: App:Lam:V -> App:Lam:V
appe1 :: App:Lam:V -> App:Lam:V
lambdaint :: App:Lam:V -> App:Lam:V
S :: S:0' -> S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat -> App:Lam:V
gen_S:0'5_0 :: Nat -> S:0'


Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0)
eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)) -> False, rt in Omega(1 + n460_0)


Generator Equations:
gen_App:Lam:V4_0(0) <=> V(0')
gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))


The following defined symbols remain to be analysed:
subst, red

They will be analysed ascendingly in the following order:
subst < red

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369328_0)) -> gen_App:Lam:V4_0(n369328_0), rt in Omega(1 + n369328_0)

Induction Base:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(0)) ->_R^Omega(1)
subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(b), V(0')) ->_L^Omega(1)
subst[Ite](False, gen_App:Lam:V4_0(b), V(0')) ->_R^Omega(0)
V(0')

Induction Step:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(+(n369328_0, 1))) ->_R^Omega(1)
mkapp(subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369328_0)), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) ->_IH
mkapp(gen_App:Lam:V4_0(c369329_0), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) ->_R^Omega(1)
mkapp(gen_App:Lam:V4_0(n369328_0), subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(b), V(0'))) ->_L^Omega(1)
mkapp(gen_App:Lam:V4_0(n369328_0), subst[Ite](False, gen_App:Lam:V4_0(b), V(0'))) ->_R^Omega(0)
mkapp(gen_App:Lam:V4_0(n369328_0), V(0')) ->_R^Omega(1)
App(gen_App:Lam:V4_0(n369328_0), V(0'))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) -> Lam(int, term)
subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) -> V(int)
eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) -> False
eqTerm(App(t11, t12), V(v2)) -> False
eqTerm(Lam(i1, l1), App(t21, t22)) -> False
eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) -> False
eqTerm(V(v1), App(t21, t22)) -> False
eqTerm(V(v1), Lam(i2, l2)) -> False
eqTerm(V(v1), V(v2)) -> !EQ(v1, v2)
mklam(V(name), e) -> Lam(name, e)
lamvar(Lam(var, exp)) -> V(var)
lambody(Lam(var, exp)) -> exp
isvar(App(t1, t2)) -> False
isvar(Lam(int, term)) -> False
isvar(V(int)) -> True
islam(App(t1, t2)) -> False
islam(Lam(int, term)) -> True
islam(V(int)) -> False
appe2(App(e1, e2)) -> e2
appe1(App(e1, e2)) -> e1
mkapp(e1, e2) -> App(e1, e2)
lambdaint(e) -> red(e)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2)
red[Let][Let](V(int), e2) -> App(V(int), e2)
red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) -> e
subst[Ite](False, a, e) -> e
subst[Ite](True, a, e) -> a

Types:
subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
App :: App:Lam:V -> App:Lam:V -> App:Lam:V
mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V
Lam :: S:0' -> App:Lam:V -> App:Lam:V
subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V
eqTerm :: App:Lam:V -> App:Lam:V -> False:True
V :: S:0' -> App:Lam:V
red :: App:Lam:V -> App:Lam:V
red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V
and :: False:True -> False:True -> False:True
False :: False:True
!EQ :: S:0' -> S:0' -> False:True
mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V
lamvar :: App:Lam:V -> App:Lam:V
lambody :: App:Lam:V -> App:Lam:V
isvar :: App:Lam:V -> False:True
True :: False:True
islam :: App:Lam:V -> False:True
appe2 :: App:Lam:V -> App:Lam:V
appe1 :: App:Lam:V -> App:Lam:V
lambdaint :: App:Lam:V -> App:Lam:V
S :: S:0' -> S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat -> App:Lam:V
gen_S:0'5_0 :: Nat -> S:0'


Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0)
eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)) -> False, rt in Omega(1 + n460_0)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369328_0)) -> gen_App:Lam:V4_0(n369328_0), rt in Omega(1 + n369328_0)


Generator Equations:
gen_App:Lam:V4_0(0) <=> V(0')
gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))


The following defined symbols remain to be analysed:
red
----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
red(gen_App:Lam:V4_0(n374311_0)) -> *6_0, rt in Omega(n374311_0)

Induction Base:
red(gen_App:Lam:V4_0(0))

Induction Step:
red(gen_App:Lam:V4_0(+(n374311_0, 1))) ->_R^Omega(1)
red[Let](App(gen_App:Lam:V4_0(n374311_0), V(0')), red(gen_App:Lam:V4_0(n374311_0))) ->_IH
red[Let](App(gen_App:Lam:V4_0(n374311_0), V(0')), *6_0)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(22)
BOUNDS(1, INF)