KILLED
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(1, INF).

(0) CpxRelTRS


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

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


The TRS R consists of the following rules:

   SUBST(z0, z1, App(z2, z3)) -> c16(MKAPP(subst(z0, z1, z2), subst(z0, z1, z3)), SUBST(z0, z1, z2))
   SUBST(z0, z1, App(z2, z3)) -> c17(MKAPP(subst(z0, z1, z2), subst(z0, z1, z3)), SUBST(z0, z1, z3))
   SUBST(z0, z1, Lam(z2, z3)) -> c18(SUBST[TRUE][ITE](eqTerm(z0, V(z2)), z0, z1, Lam(z2, z3)), EQTERM(z0, V(z2)))
   SUBST(z0, z1, V(z2)) -> c19(SUBST[ITE](eqTerm(z0, V(z2)), z0, z1, V(z2)), EQTERM(z0, V(z2)))
   RED(App(z0, z1)) -> c20(RED[LET](App(z0, z1), red(z0)), RED(z0))
   RED(Lam(z0, z1)) -> c21
   RED(V(z0)) -> c22
   EQTERM(App(z0, z1), App(z2, z3)) -> c23(AND(eqTerm(z0, z2), eqTerm(z1, z3)), EQTERM(z0, z2))
   EQTERM(App(z0, z1), App(z2, z3)) -> c24(AND(eqTerm(z0, z2), eqTerm(z1, z3)), EQTERM(z1, z3))
   EQTERM(App(z0, z1), Lam(z2, z3)) -> c25
   EQTERM(App(z0, z1), V(z2)) -> c26
   EQTERM(Lam(z0, z1), App(z2, z3)) -> c27
   EQTERM(Lam(z0, z1), Lam(z2, z3)) -> c28(AND(!EQ(z0, z2), eqTerm(z1, z3)), !EQ'(z0, z2))
   EQTERM(Lam(z0, z1), Lam(z2, z3)) -> c29(AND(!EQ(z0, z2), eqTerm(z1, z3)), EQTERM(z1, z3))
   EQTERM(Lam(z0, z1), V(z2)) -> c30
   EQTERM(V(z0), App(z1, z2)) -> c31
   EQTERM(V(z0), Lam(z1, z2)) -> c32
   EQTERM(V(z0), V(z1)) -> c33(!EQ'(z0, z1))
   MKLAM(V(z0), z1) -> c34
   LAMVAR(Lam(z0, z1)) -> c35
   LAMBODY(Lam(z0, z1)) -> c36
   ISVAR(App(z0, z1)) -> c37
   ISVAR(Lam(z0, z1)) -> c38
   ISVAR(V(z0)) -> c39
   ISLAM(App(z0, z1)) -> c40
   ISLAM(Lam(z0, z1)) -> c41
   ISLAM(V(z0)) -> c42
   APPE2(App(z0, z1)) -> c43
   APPE1(App(z0, z1)) -> c44
   MKAPP(z0, z1) -> c45
   LAMBDAINT(z0) -> c46(RED(z0))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c5
   !EQ'(S(z0), 0) -> c6
   !EQ'(0, 0) -> c7
   RED[LET][LET](z0, Lam(z1, z2), z3) -> c8(RED(subst(V(z1), z3, z2)), SUBST(V(z1), z3, z2))
   RED[LET][LET](z0, App(z1, z2), z3) -> c9
   RED[LET][LET](z0, V(z1), z2) -> c10
   SUBST[TRUE][ITE](False, z0, z1, Lam(z2, z3)) -> c11(MKLAM(V(z2), subst(z0, z1, z3)), SUBST(z0, z1, z3))
   SUBST[TRUE][ITE](True, z0, z1, z2) -> c12
   RED[LET](App(z0, z1), z2) -> c13(RED[LET][LET](App(z0, z1), z2, red(z1)), RED(z1))
   SUBST[ITE](False, z0, z1, z2) -> c14
   SUBST[ITE](True, z0, z1, z2) -> c15
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   red[Let][Let](z0, Lam(z1, z2), z3) -> red(subst(V(z1), z3, z2))
   red[Let][Let](z0, App(z1, z2), z3) -> App(App(z1, z2), z3)
   red[Let][Let](z0, V(z1), z2) -> App(V(z1), z2)
   subst[True][Ite](False, z0, z1, Lam(z2, z3)) -> mklam(V(z2), subst(z0, z1, z3))
   subst[True][Ite](True, z0, z1, z2) -> z2
   red[Let](App(z0, z1), z2) -> red[Let][Let](App(z0, z1), z2, red(z1))
   subst[Ite](False, z0, z1, z2) -> z2
   subst[Ite](True, z0, z1, z2) -> z1
   subst(z0, z1, App(z2, z3)) -> mkapp(subst(z0, z1, z2), subst(z0, z1, z3))
   subst(z0, z1, Lam(z2, z3)) -> subst[True][Ite](eqTerm(z0, V(z2)), z0, z1, Lam(z2, z3))
   subst(z0, z1, V(z2)) -> subst[Ite](eqTerm(z0, V(z2)), z0, z1, V(z2))
   red(App(z0, z1)) -> red[Let](App(z0, z1), red(z0))
   red(Lam(z0, z1)) -> Lam(z0, z1)
   red(V(z0)) -> V(z0)
   eqTerm(App(z0, z1), App(z2, z3)) -> and(eqTerm(z0, z2), eqTerm(z1, z3))
   eqTerm(App(z0, z1), Lam(z2, z3)) -> False
   eqTerm(App(z0, z1), V(z2)) -> False
   eqTerm(Lam(z0, z1), App(z2, z3)) -> False
   eqTerm(Lam(z0, z1), Lam(z2, z3)) -> and(!EQ(z0, z2), eqTerm(z1, z3))
   eqTerm(Lam(z0, z1), V(z2)) -> False
   eqTerm(V(z0), App(z1, z2)) -> False
   eqTerm(V(z0), Lam(z1, z2)) -> False
   eqTerm(V(z0), V(z1)) -> !EQ(z0, z1)
   mklam(V(z0), z1) -> Lam(z0, z1)
   lamvar(Lam(z0, z1)) -> V(z0)
   lambody(Lam(z0, z1)) -> z1
   isvar(App(z0, z1)) -> False
   isvar(Lam(z0, z1)) -> False
   isvar(V(z0)) -> True
   islam(App(z0, z1)) -> False
   islam(Lam(z0, z1)) -> True
   islam(V(z0)) -> False
   appe2(App(z0, z1)) -> z1
   appe1(App(z0, z1)) -> z0
   mkapp(z0, z1) -> App(z0, z1)
   lambdaint(z0) -> red(z0)

Rewrite Strategy: INNERMOST