WORST_CASE(Omega(n^1),?)
proof of input_3Egct3haEo.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 314 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 13 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxRelTRS
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 0 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 277 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 520 ms]
(16) BEST
    (17) proven lower bound
        (18) LowerBoundPropagationProof [FINISHED, 0 ms]
        (19) BOUNDS(n^1, INF)
    (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 418 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 374 ms]
        (24) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   rw(Val(n), c) -> Op(Val(n), rewrite(c))
   rewrite(Op(x, y)) -> rw(x, y)
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x))
   rewrite(Val(n)) -> Val(n)
   second(Op(x, y)) -> y
   isOp(Val(n)) -> False
   isOp(Op(x, y)) -> True
   first(Val(n)) -> Val(n)
   first(Op(x, y)) -> x
   assrewrite(exp) -> rewrite(exp)

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

   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y))
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c))
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1))

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

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


The TRS R consists of the following rules:

   rw(Val(n), c) -> Op(Val(n), rewrite(c))
   rewrite(Op(x, y)) -> rw(x, y)
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x))
   rewrite(Val(n)) -> Val(n)
   second(Op(x, y)) -> y
   isOp(Val(n)) -> False
   isOp(Op(x, y)) -> True
   first(Val(n)) -> Val(n)
   first(Op(x, y)) -> x
   assrewrite(exp) -> rewrite(exp)

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

   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y))
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c))
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1))

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
   rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
   rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
   rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
   rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
   rewrite(Op(z0, z1)) -> rw(z0, z1)
   rewrite(Val(z0)) -> Val(z0)
   second(Op(z0, z1)) -> z1
   isOp(Val(z0)) -> False
   isOp(Op(z0, z1)) -> True
   first(Val(z0)) -> Val(z0)
   first(Op(z0, z1)) -> z0
   assrewrite(z0) -> rewrite(z0)
Tuples:
   RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
   SECOND(Op(z0, z1)) -> c7
   ISOP(Val(z0)) -> c8
   ISOP(Op(z0, z1)) -> c9
   FIRST(Val(z0)) -> c10
   FIRST(Op(z0, z1)) -> c11
   ASSREWRITE(z0) -> c12(REWRITE(z0))
S tuples:
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
   SECOND(Op(z0, z1)) -> c7
   ISOP(Val(z0)) -> c8
   ISOP(Op(z0, z1)) -> c9
   FIRST(Val(z0)) -> c10
   FIRST(Op(z0, z1)) -> c11
   ASSREWRITE(z0) -> c12(REWRITE(z0))
K tuples:none
Defined Rule Symbols:   rw_2, rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rw[Let]_3, rw[Let][Let]_4, rw[Let][Let][Let]_4

Defined Pair Symbols:   RW[LET]_3, RW[LET][LET]_4, RW[LET][LET][LET]_4, RW_2, REWRITE_1, SECOND_1, ISOP_1, FIRST_1, ASSREWRITE_1

Compound Symbols:   c_2, c1_2, c2_1, c3_1, c4_2, c5_1, c6, c7, c8, c9, c10, c11, c12_1


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

(5) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(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:

   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
   SECOND(Op(z0, z1)) -> c7
   ISOP(Val(z0)) -> c8
   ISOP(Op(z0, z1)) -> c9
   FIRST(Val(z0)) -> c10
   FIRST(Op(z0, z1)) -> c11
   ASSREWRITE(z0) -> c12(REWRITE(z0))

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

   RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
   rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
   rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
   rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
   rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
   rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
   rewrite(Op(z0, z1)) -> rw(z0, z1)
   rewrite(Val(z0)) -> Val(z0)
   second(Op(z0, z1)) -> z1
   isOp(Val(z0)) -> False
   isOp(Op(z0, z1)) -> True
   first(Val(z0)) -> Val(z0)
   first(Op(z0, z1)) -> z0
   assrewrite(z0) -> rewrite(z0)

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

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

(8)
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:

   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
   SECOND(Op(z0, z1)) -> c7
   ISOP(Val(z0)) -> c8
   ISOP(Op(z0, z1)) -> c9
   FIRST(Val(z0)) -> c10
   FIRST(Op(z0, z1)) -> c11
   ASSREWRITE(z0) -> c12(REWRITE(z0))

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

   RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
   rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
   rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
   rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
   rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
   rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
   rewrite(Op(z0, z1)) -> rw(z0, z1)
   rewrite(Val(z0)) -> Val(z0)
   second(Op(z0, z1)) -> z1
   isOp(Val(z0)) -> False
   isOp(Op(z0, z1)) -> True
   first(Val(z0)) -> Val(z0)
   first(Op(z0, z1)) -> z0
   assrewrite(z0) -> rewrite(z0)

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

(9) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
RW(Val(z0), z1) -> c3(REWRITE(z1))
RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
REWRITE(Val(z0)) -> c6
SECOND(Op(z0, z1)) -> c7
ISOP(Val(z0)) -> c8
ISOP(Op(z0, z1)) -> c9
FIRST(Val(z0)) -> c10
FIRST(Op(z0, z1)) -> c11
ASSREWRITE(z0) -> c12(REWRITE(z0))
RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
rewrite(Op(z0, z1)) -> rw(z0, z1)
rewrite(Val(z0)) -> Val(z0)
second(Op(z0, z1)) -> z1
isOp(Val(z0)) -> False
isOp(Op(z0, z1)) -> True
first(Val(z0)) -> Val(z0)
first(Op(z0, z1)) -> z0
assrewrite(z0) -> rewrite(z0)

Types:
RW :: Val:Op -> Val:Op -> c3:c4
Val :: a -> Val:Op
c3 :: c5:c6 -> c3:c4
REWRITE :: Val:Op -> c5:c6
Op :: Val:Op -> Val:Op -> Val:Op
c4 :: c -> c5:c6 -> c3:c4
RW[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4 -> c5:c6
c6 :: c5:c6
SECOND :: Val:Op -> c7
c7 :: c7
ISOP :: Val:Op -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FIRST :: Val:Op -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
ASSREWRITE :: Val:Op -> c12
c12 :: c5:c6 -> c12
c :: c1 -> c5:c6 -> c
RW[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c5:c6 -> c1
RW[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4 -> c2
rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw :: Val:Op -> Val:Op -> Val:Op
second :: Val:Op -> Val:Op
isOp :: Val:Op -> False:True
False :: False:True
True :: False:True
first :: Val:Op -> Val:Op
assrewrite :: Val:Op -> Val:Op
hole_c3:c41_13 :: c3:c4
hole_Val:Op2_13 :: Val:Op
hole_a3_13 :: a
hole_c5:c64_13 :: c5:c6
hole_c5_13 :: c
hole_c76_13 :: c7
hole_c8:c97_13 :: c8:c9
hole_c10:c118_13 :: c10:c11
hole_c129_13 :: c12
hole_c110_13 :: c1
hole_c211_13 :: c2
hole_False:True12_13 :: False:True
gen_Val:Op13_13 :: Nat -> Val:Op

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

(11) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
RW, REWRITE, rewrite, rw

They will be analysed ascendingly in the following order:
RW = REWRITE
rewrite < RW
rewrite = rw

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

(12)
Obligation:
Innermost TRS:
Rules:
RW(Val(z0), z1) -> c3(REWRITE(z1))
RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
REWRITE(Val(z0)) -> c6
SECOND(Op(z0, z1)) -> c7
ISOP(Val(z0)) -> c8
ISOP(Op(z0, z1)) -> c9
FIRST(Val(z0)) -> c10
FIRST(Op(z0, z1)) -> c11
ASSREWRITE(z0) -> c12(REWRITE(z0))
RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
rewrite(Op(z0, z1)) -> rw(z0, z1)
rewrite(Val(z0)) -> Val(z0)
second(Op(z0, z1)) -> z1
isOp(Val(z0)) -> False
isOp(Op(z0, z1)) -> True
first(Val(z0)) -> Val(z0)
first(Op(z0, z1)) -> z0
assrewrite(z0) -> rewrite(z0)

Types:
RW :: Val:Op -> Val:Op -> c3:c4
Val :: a -> Val:Op
c3 :: c5:c6 -> c3:c4
REWRITE :: Val:Op -> c5:c6
Op :: Val:Op -> Val:Op -> Val:Op
c4 :: c -> c5:c6 -> c3:c4
RW[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4 -> c5:c6
c6 :: c5:c6
SECOND :: Val:Op -> c7
c7 :: c7
ISOP :: Val:Op -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FIRST :: Val:Op -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
ASSREWRITE :: Val:Op -> c12
c12 :: c5:c6 -> c12
c :: c1 -> c5:c6 -> c
RW[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c5:c6 -> c1
RW[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4 -> c2
rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw :: Val:Op -> Val:Op -> Val:Op
second :: Val:Op -> Val:Op
isOp :: Val:Op -> False:True
False :: False:True
True :: False:True
first :: Val:Op -> Val:Op
assrewrite :: Val:Op -> Val:Op
hole_c3:c41_13 :: c3:c4
hole_Val:Op2_13 :: Val:Op
hole_a3_13 :: a
hole_c5:c64_13 :: c5:c6
hole_c5_13 :: c
hole_c76_13 :: c7
hole_c8:c97_13 :: c8:c9
hole_c10:c118_13 :: c10:c11
hole_c129_13 :: c12
hole_c110_13 :: c1
hole_c211_13 :: c2
hole_False:True12_13 :: False:True
gen_Val:Op13_13 :: Nat -> Val:Op


Generator Equations:
gen_Val:Op13_13(0) <=> Val(hole_a3_13)
gen_Val:Op13_13(+(x, 1)) <=> Op(Val(hole_a3_13), gen_Val:Op13_13(x))


The following defined symbols remain to be analysed:
rw, RW, REWRITE, rewrite

They will be analysed ascendingly in the following order:
RW = REWRITE
rewrite < RW
rewrite = rw

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rw(gen_Val:Op13_13(0), gen_Val:Op13_13(n15_13)) -> gen_Val:Op13_13(+(1, n15_13)), rt in Omega(0)

Induction Base:
rw(gen_Val:Op13_13(0), gen_Val:Op13_13(0)) ->_R^Omega(0)
Op(Val(hole_a3_13), rewrite(gen_Val:Op13_13(0))) ->_R^Omega(0)
Op(Val(hole_a3_13), Val(hole_a3_13))

Induction Step:
rw(gen_Val:Op13_13(0), gen_Val:Op13_13(+(n15_13, 1))) ->_R^Omega(0)
Op(Val(hole_a3_13), rewrite(gen_Val:Op13_13(+(n15_13, 1)))) ->_R^Omega(0)
Op(Val(hole_a3_13), rw(Val(hole_a3_13), gen_Val:Op13_13(n15_13))) ->_IH
Op(Val(hole_a3_13), gen_Val:Op13_13(+(1, c16_13)))

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

(14)
Obligation:
Innermost TRS:
Rules:
RW(Val(z0), z1) -> c3(REWRITE(z1))
RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
REWRITE(Val(z0)) -> c6
SECOND(Op(z0, z1)) -> c7
ISOP(Val(z0)) -> c8
ISOP(Op(z0, z1)) -> c9
FIRST(Val(z0)) -> c10
FIRST(Op(z0, z1)) -> c11
ASSREWRITE(z0) -> c12(REWRITE(z0))
RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
rewrite(Op(z0, z1)) -> rw(z0, z1)
rewrite(Val(z0)) -> Val(z0)
second(Op(z0, z1)) -> z1
isOp(Val(z0)) -> False
isOp(Op(z0, z1)) -> True
first(Val(z0)) -> Val(z0)
first(Op(z0, z1)) -> z0
assrewrite(z0) -> rewrite(z0)

Types:
RW :: Val:Op -> Val:Op -> c3:c4
Val :: a -> Val:Op
c3 :: c5:c6 -> c3:c4
REWRITE :: Val:Op -> c5:c6
Op :: Val:Op -> Val:Op -> Val:Op
c4 :: c -> c5:c6 -> c3:c4
RW[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4 -> c5:c6
c6 :: c5:c6
SECOND :: Val:Op -> c7
c7 :: c7
ISOP :: Val:Op -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FIRST :: Val:Op -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
ASSREWRITE :: Val:Op -> c12
c12 :: c5:c6 -> c12
c :: c1 -> c5:c6 -> c
RW[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c5:c6 -> c1
RW[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4 -> c2
rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw :: Val:Op -> Val:Op -> Val:Op
second :: Val:Op -> Val:Op
isOp :: Val:Op -> False:True
False :: False:True
True :: False:True
first :: Val:Op -> Val:Op
assrewrite :: Val:Op -> Val:Op
hole_c3:c41_13 :: c3:c4
hole_Val:Op2_13 :: Val:Op
hole_a3_13 :: a
hole_c5:c64_13 :: c5:c6
hole_c5_13 :: c
hole_c76_13 :: c7
hole_c8:c97_13 :: c8:c9
hole_c10:c118_13 :: c10:c11
hole_c129_13 :: c12
hole_c110_13 :: c1
hole_c211_13 :: c2
hole_False:True12_13 :: False:True
gen_Val:Op13_13 :: Nat -> Val:Op


Lemmas:
rw(gen_Val:Op13_13(0), gen_Val:Op13_13(n15_13)) -> gen_Val:Op13_13(+(1, n15_13)), rt in Omega(0)


Generator Equations:
gen_Val:Op13_13(0) <=> Val(hole_a3_13)
gen_Val:Op13_13(+(x, 1)) <=> Op(Val(hole_a3_13), gen_Val:Op13_13(x))


The following defined symbols remain to be analysed:
rewrite, RW, REWRITE

They will be analysed ascendingly in the following order:
RW = REWRITE
rewrite < RW
rewrite = rw

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REWRITE(gen_Val:Op13_13(+(1, n686_13))) -> *14_13, rt in Omega(n686_13)

Induction Base:
REWRITE(gen_Val:Op13_13(+(1, 0)))

Induction Step:
REWRITE(gen_Val:Op13_13(+(1, +(n686_13, 1)))) ->_R^Omega(1)
c5(RW(Val(hole_a3_13), gen_Val:Op13_13(+(1, n686_13)))) ->_R^Omega(1)
c5(c3(REWRITE(gen_Val:Op13_13(+(1, n686_13))))) ->_IH
c5(c3(*14_13))

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

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
RW(Val(z0), z1) -> c3(REWRITE(z1))
RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
REWRITE(Val(z0)) -> c6
SECOND(Op(z0, z1)) -> c7
ISOP(Val(z0)) -> c8
ISOP(Op(z0, z1)) -> c9
FIRST(Val(z0)) -> c10
FIRST(Op(z0, z1)) -> c11
ASSREWRITE(z0) -> c12(REWRITE(z0))
RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
rewrite(Op(z0, z1)) -> rw(z0, z1)
rewrite(Val(z0)) -> Val(z0)
second(Op(z0, z1)) -> z1
isOp(Val(z0)) -> False
isOp(Op(z0, z1)) -> True
first(Val(z0)) -> Val(z0)
first(Op(z0, z1)) -> z0
assrewrite(z0) -> rewrite(z0)

Types:
RW :: Val:Op -> Val:Op -> c3:c4
Val :: a -> Val:Op
c3 :: c5:c6 -> c3:c4
REWRITE :: Val:Op -> c5:c6
Op :: Val:Op -> Val:Op -> Val:Op
c4 :: c -> c5:c6 -> c3:c4
RW[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4 -> c5:c6
c6 :: c5:c6
SECOND :: Val:Op -> c7
c7 :: c7
ISOP :: Val:Op -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FIRST :: Val:Op -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
ASSREWRITE :: Val:Op -> c12
c12 :: c5:c6 -> c12
c :: c1 -> c5:c6 -> c
RW[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c5:c6 -> c1
RW[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4 -> c2
rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw :: Val:Op -> Val:Op -> Val:Op
second :: Val:Op -> Val:Op
isOp :: Val:Op -> False:True
False :: False:True
True :: False:True
first :: Val:Op -> Val:Op
assrewrite :: Val:Op -> Val:Op
hole_c3:c41_13 :: c3:c4
hole_Val:Op2_13 :: Val:Op
hole_a3_13 :: a
hole_c5:c64_13 :: c5:c6
hole_c5_13 :: c
hole_c76_13 :: c7
hole_c8:c97_13 :: c8:c9
hole_c10:c118_13 :: c10:c11
hole_c129_13 :: c12
hole_c110_13 :: c1
hole_c211_13 :: c2
hole_False:True12_13 :: False:True
gen_Val:Op13_13 :: Nat -> Val:Op


Lemmas:
rw(gen_Val:Op13_13(0), gen_Val:Op13_13(n15_13)) -> gen_Val:Op13_13(+(1, n15_13)), rt in Omega(0)


Generator Equations:
gen_Val:Op13_13(0) <=> Val(hole_a3_13)
gen_Val:Op13_13(+(x, 1)) <=> Op(Val(hole_a3_13), gen_Val:Op13_13(x))


The following defined symbols remain to be analysed:
REWRITE, RW

They will be analysed ascendingly in the following order:
RW = REWRITE

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
RW(Val(z0), z1) -> c3(REWRITE(z1))
RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
REWRITE(Val(z0)) -> c6
SECOND(Op(z0, z1)) -> c7
ISOP(Val(z0)) -> c8
ISOP(Op(z0, z1)) -> c9
FIRST(Val(z0)) -> c10
FIRST(Op(z0, z1)) -> c11
ASSREWRITE(z0) -> c12(REWRITE(z0))
RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
rewrite(Op(z0, z1)) -> rw(z0, z1)
rewrite(Val(z0)) -> Val(z0)
second(Op(z0, z1)) -> z1
isOp(Val(z0)) -> False
isOp(Op(z0, z1)) -> True
first(Val(z0)) -> Val(z0)
first(Op(z0, z1)) -> z0
assrewrite(z0) -> rewrite(z0)

Types:
RW :: Val:Op -> Val:Op -> c3:c4
Val :: a -> Val:Op
c3 :: c5:c6 -> c3:c4
REWRITE :: Val:Op -> c5:c6
Op :: Val:Op -> Val:Op -> Val:Op
c4 :: c -> c5:c6 -> c3:c4
RW[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4 -> c5:c6
c6 :: c5:c6
SECOND :: Val:Op -> c7
c7 :: c7
ISOP :: Val:Op -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FIRST :: Val:Op -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
ASSREWRITE :: Val:Op -> c12
c12 :: c5:c6 -> c12
c :: c1 -> c5:c6 -> c
RW[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c5:c6 -> c1
RW[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4 -> c2
rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw :: Val:Op -> Val:Op -> Val:Op
second :: Val:Op -> Val:Op
isOp :: Val:Op -> False:True
False :: False:True
True :: False:True
first :: Val:Op -> Val:Op
assrewrite :: Val:Op -> Val:Op
hole_c3:c41_13 :: c3:c4
hole_Val:Op2_13 :: Val:Op
hole_a3_13 :: a
hole_c5:c64_13 :: c5:c6
hole_c5_13 :: c
hole_c76_13 :: c7
hole_c8:c97_13 :: c8:c9
hole_c10:c118_13 :: c10:c11
hole_c129_13 :: c12
hole_c110_13 :: c1
hole_c211_13 :: c2
hole_False:True12_13 :: False:True
gen_Val:Op13_13 :: Nat -> Val:Op


Lemmas:
rw(gen_Val:Op13_13(0), gen_Val:Op13_13(n15_13)) -> gen_Val:Op13_13(+(1, n15_13)), rt in Omega(0)
REWRITE(gen_Val:Op13_13(+(1, n686_13))) -> *14_13, rt in Omega(n686_13)


Generator Equations:
gen_Val:Op13_13(0) <=> Val(hole_a3_13)
gen_Val:Op13_13(+(x, 1)) <=> Op(Val(hole_a3_13), gen_Val:Op13_13(x))


The following defined symbols remain to be analysed:
RW

They will be analysed ascendingly in the following order:
RW = REWRITE

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
RW(gen_Val:Op13_13(0), gen_Val:Op13_13(n1285_13)) -> *14_13, rt in Omega(n1285_13)

Induction Base:
RW(gen_Val:Op13_13(0), gen_Val:Op13_13(0))

Induction Step:
RW(gen_Val:Op13_13(0), gen_Val:Op13_13(+(n1285_13, 1))) ->_R^Omega(1)
c3(REWRITE(gen_Val:Op13_13(+(n1285_13, 1)))) ->_R^Omega(1)
c3(c5(RW(Val(hole_a3_13), gen_Val:Op13_13(n1285_13)))) ->_IH
c3(c5(*14_13))

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

(22)
Obligation:
Innermost TRS:
Rules:
RW(Val(z0), z1) -> c3(REWRITE(z1))
RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
REWRITE(Val(z0)) -> c6
SECOND(Op(z0, z1)) -> c7
ISOP(Val(z0)) -> c8
ISOP(Op(z0, z1)) -> c9
FIRST(Val(z0)) -> c10
FIRST(Op(z0, z1)) -> c11
ASSREWRITE(z0) -> c12(REWRITE(z0))
RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
rewrite(Op(z0, z1)) -> rw(z0, z1)
rewrite(Val(z0)) -> Val(z0)
second(Op(z0, z1)) -> z1
isOp(Val(z0)) -> False
isOp(Op(z0, z1)) -> True
first(Val(z0)) -> Val(z0)
first(Op(z0, z1)) -> z0
assrewrite(z0) -> rewrite(z0)

Types:
RW :: Val:Op -> Val:Op -> c3:c4
Val :: a -> Val:Op
c3 :: c5:c6 -> c3:c4
REWRITE :: Val:Op -> c5:c6
Op :: Val:Op -> Val:Op -> Val:Op
c4 :: c -> c5:c6 -> c3:c4
RW[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4 -> c5:c6
c6 :: c5:c6
SECOND :: Val:Op -> c7
c7 :: c7
ISOP :: Val:Op -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FIRST :: Val:Op -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
ASSREWRITE :: Val:Op -> c12
c12 :: c5:c6 -> c12
c :: c1 -> c5:c6 -> c
RW[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c5:c6 -> c1
RW[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4 -> c2
rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw :: Val:Op -> Val:Op -> Val:Op
second :: Val:Op -> Val:Op
isOp :: Val:Op -> False:True
False :: False:True
True :: False:True
first :: Val:Op -> Val:Op
assrewrite :: Val:Op -> Val:Op
hole_c3:c41_13 :: c3:c4
hole_Val:Op2_13 :: Val:Op
hole_a3_13 :: a
hole_c5:c64_13 :: c5:c6
hole_c5_13 :: c
hole_c76_13 :: c7
hole_c8:c97_13 :: c8:c9
hole_c10:c118_13 :: c10:c11
hole_c129_13 :: c12
hole_c110_13 :: c1
hole_c211_13 :: c2
hole_False:True12_13 :: False:True
gen_Val:Op13_13 :: Nat -> Val:Op


Lemmas:
rw(gen_Val:Op13_13(0), gen_Val:Op13_13(n15_13)) -> gen_Val:Op13_13(+(1, n15_13)), rt in Omega(0)
REWRITE(gen_Val:Op13_13(+(1, n686_13))) -> *14_13, rt in Omega(n686_13)
RW(gen_Val:Op13_13(0), gen_Val:Op13_13(n1285_13)) -> *14_13, rt in Omega(n1285_13)


Generator Equations:
gen_Val:Op13_13(0) <=> Val(hole_a3_13)
gen_Val:Op13_13(+(x, 1)) <=> Op(Val(hole_a3_13), gen_Val:Op13_13(x))


The following defined symbols remain to be analysed:
REWRITE

They will be analysed ascendingly in the following order:
RW = REWRITE

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REWRITE(gen_Val:Op13_13(+(1, n5702_13))) -> *14_13, rt in Omega(n5702_13)

Induction Base:
REWRITE(gen_Val:Op13_13(+(1, 0)))

Induction Step:
REWRITE(gen_Val:Op13_13(+(1, +(n5702_13, 1)))) ->_R^Omega(1)
c5(RW(Val(hole_a3_13), gen_Val:Op13_13(+(1, n5702_13)))) ->_R^Omega(1)
c5(c3(REWRITE(gen_Val:Op13_13(+(1, n5702_13))))) ->_IH
c5(c3(*14_13))

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

(24)
BOUNDS(1, INF)