WORST_CASE(Omega(n^1),?)
proof of input_ox0sBdIh7u.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), 338 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 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), 1 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 0 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 19.4 s]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 12 ms]
(16) proven lower bound
(17) LowerBoundPropagationProof [FINISHED, 0 ms]
(18) BOUNDS(n^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:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n))
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), 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:

   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(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:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n))
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), 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:

   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(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:
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   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:
   REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
   REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   SECOND(Op(z0, z1)) -> c6
   ISOP(Val(z0)) -> c7
   ISOP(Op(z0, z1)) -> c8
   FIRST(Val(z0)) -> c9
   FIRST(Op(z0, z1)) -> c10
   ASSREWRITE(z0) -> c11(REWRITE(z0))
S tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   SECOND(Op(z0, z1)) -> c6
   ISOP(Val(z0)) -> c7
   ISOP(Op(z0, z1)) -> c8
   FIRST(Val(z0)) -> c9
   FIRST(Op(z0, z1)) -> c10
   ASSREWRITE(z0) -> c11(REWRITE(z0))
K tuples:none
Defined Rule Symbols:   rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

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

Compound Symbols:   c_2, c1_2, c2_2, c3_1, c4_2, c5, c6, c7, c8, c9, c10, c11_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:

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

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

   REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
   REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   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:

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

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

   REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
   REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   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:
REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
REWRITE(Val(z0)) -> c5
SECOND(Op(z0, z1)) -> c6
ISOP(Val(z0)) -> c7
ISOP(Op(z0, z1)) -> c8
FIRST(Val(z0)) -> c9
FIRST(Op(z0, z1)) -> c10
ASSREWRITE(z0) -> c11(REWRITE(z0))
REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
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:
REWRITE :: Val:Op -> c3:c4:c5
Op :: Val:Op -> Val:Op -> Val:Op
Val :: a -> Val:Op
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c -> c3:c4:c5 -> c3:c4:c5
REWRITE[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4:c5
SECOND :: Val:Op -> c6
c6 :: c6
ISOP :: Val:Op -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
FIRST :: Val:Op -> c9:c10
c9 :: c9:c10
c10 :: c9:c10
ASSREWRITE :: Val:Op -> c11
c11 :: c3:c4:c5 -> c11
c :: c1 -> c3:c4:c5 -> c
REWRITE[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c3:c4:c5 -> c1
REWRITE[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4:c5 -> c3:c4:c5 -> c2
rewrite[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let][Let] :: Val:Op -> Val:Op -> 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:c4:c51_12 :: c3:c4:c5
hole_Val:Op2_12 :: Val:Op
hole_a3_12 :: a
hole_c4_12 :: c
hole_c65_12 :: c6
hole_c7:c86_12 :: c7:c8
hole_c9:c107_12 :: c9:c10
hole_c118_12 :: c11
hole_c19_12 :: c1
hole_c210_12 :: c2
hole_False:True11_12 :: False:True
gen_c3:c4:c512_12 :: Nat -> c3:c4:c5
gen_Val:Op13_12 :: Nat -> Val:Op

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

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

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

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

(12)
Obligation:
Innermost TRS:
Rules:
REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
REWRITE(Val(z0)) -> c5
SECOND(Op(z0, z1)) -> c6
ISOP(Val(z0)) -> c7
ISOP(Op(z0, z1)) -> c8
FIRST(Val(z0)) -> c9
FIRST(Op(z0, z1)) -> c10
ASSREWRITE(z0) -> c11(REWRITE(z0))
REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
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:
REWRITE :: Val:Op -> c3:c4:c5
Op :: Val:Op -> Val:Op -> Val:Op
Val :: a -> Val:Op
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c -> c3:c4:c5 -> c3:c4:c5
REWRITE[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4:c5
SECOND :: Val:Op -> c6
c6 :: c6
ISOP :: Val:Op -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
FIRST :: Val:Op -> c9:c10
c9 :: c9:c10
c10 :: c9:c10
ASSREWRITE :: Val:Op -> c11
c11 :: c3:c4:c5 -> c11
c :: c1 -> c3:c4:c5 -> c
REWRITE[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c3:c4:c5 -> c1
REWRITE[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4:c5 -> c3:c4:c5 -> c2
rewrite[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let][Let] :: Val:Op -> Val:Op -> 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:c4:c51_12 :: c3:c4:c5
hole_Val:Op2_12 :: Val:Op
hole_a3_12 :: a
hole_c4_12 :: c
hole_c65_12 :: c6
hole_c7:c86_12 :: c7:c8
hole_c9:c107_12 :: c9:c10
hole_c118_12 :: c11
hole_c19_12 :: c1
hole_c210_12 :: c2
hole_False:True11_12 :: False:True
gen_c3:c4:c512_12 :: Nat -> c3:c4:c5
gen_Val:Op13_12 :: Nat -> Val:Op


Generator Equations:
gen_c3:c4:c512_12(0) <=> c5
gen_c3:c4:c512_12(+(x, 1)) <=> c3(gen_c3:c4:c512_12(x))
gen_Val:Op13_12(0) <=> Val(hole_a3_12)
gen_Val:Op13_12(+(x, 1)) <=> Op(Val(hole_a3_12), gen_Val:Op13_12(x))


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

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

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rewrite(gen_Val:Op13_12(+(1, n15_12))) -> *14_12, rt in Omega(0)

Induction Base:
rewrite(gen_Val:Op13_12(+(1, 0)))

Induction Step:
rewrite(gen_Val:Op13_12(+(1, +(n15_12, 1)))) ->_R^Omega(0)
Op(rewrite(gen_Val:Op13_12(+(1, n15_12))), Val(hole_a3_12)) ->_IH
Op(*14_12, Val(hole_a3_12))

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:
REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
REWRITE(Val(z0)) -> c5
SECOND(Op(z0, z1)) -> c6
ISOP(Val(z0)) -> c7
ISOP(Op(z0, z1)) -> c8
FIRST(Val(z0)) -> c9
FIRST(Op(z0, z1)) -> c10
ASSREWRITE(z0) -> c11(REWRITE(z0))
REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
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:
REWRITE :: Val:Op -> c3:c4:c5
Op :: Val:Op -> Val:Op -> Val:Op
Val :: a -> Val:Op
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c -> c3:c4:c5 -> c3:c4:c5
REWRITE[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4:c5
SECOND :: Val:Op -> c6
c6 :: c6
ISOP :: Val:Op -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
FIRST :: Val:Op -> c9:c10
c9 :: c9:c10
c10 :: c9:c10
ASSREWRITE :: Val:Op -> c11
c11 :: c3:c4:c5 -> c11
c :: c1 -> c3:c4:c5 -> c
REWRITE[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c3:c4:c5 -> c1
REWRITE[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4:c5 -> c3:c4:c5 -> c2
rewrite[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let][Let] :: Val:Op -> Val:Op -> 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:c4:c51_12 :: c3:c4:c5
hole_Val:Op2_12 :: Val:Op
hole_a3_12 :: a
hole_c4_12 :: c
hole_c65_12 :: c6
hole_c7:c86_12 :: c7:c8
hole_c9:c107_12 :: c9:c10
hole_c118_12 :: c11
hole_c19_12 :: c1
hole_c210_12 :: c2
hole_False:True11_12 :: False:True
gen_c3:c4:c512_12 :: Nat -> c3:c4:c5
gen_Val:Op13_12 :: Nat -> Val:Op


Lemmas:
rewrite(gen_Val:Op13_12(+(1, n15_12))) -> *14_12, rt in Omega(0)


Generator Equations:
gen_c3:c4:c512_12(0) <=> c5
gen_c3:c4:c512_12(+(x, 1)) <=> c3(gen_c3:c4:c512_12(x))
gen_Val:Op13_12(0) <=> Val(hole_a3_12)
gen_Val:Op13_12(+(x, 1)) <=> Op(Val(hole_a3_12), gen_Val:Op13_12(x))


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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REWRITE(gen_Val:Op13_12(n290780_12)) -> gen_c3:c4:c512_12(n290780_12), rt in Omega(1 + n290780_12)

Induction Base:
REWRITE(gen_Val:Op13_12(0)) ->_R^Omega(1)
c5

Induction Step:
REWRITE(gen_Val:Op13_12(+(n290780_12, 1))) ->_R^Omega(1)
c3(REWRITE(gen_Val:Op13_12(n290780_12))) ->_IH
c3(gen_c3:c4:c512_12(c290781_12))

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

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

Innermost TRS:
Rules:
REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
REWRITE(Val(z0)) -> c5
SECOND(Op(z0, z1)) -> c6
ISOP(Val(z0)) -> c7
ISOP(Op(z0, z1)) -> c8
FIRST(Val(z0)) -> c9
FIRST(Op(z0, z1)) -> c10
ASSREWRITE(z0) -> c11(REWRITE(z0))
REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
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:
REWRITE :: Val:Op -> c3:c4:c5
Op :: Val:Op -> Val:Op -> Val:Op
Val :: a -> Val:Op
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c -> c3:c4:c5 -> c3:c4:c5
REWRITE[LET] :: Val:Op -> Val:Op -> Val:Op -> c
rewrite :: Val:Op -> Val:Op
c5 :: c3:c4:c5
SECOND :: Val:Op -> c6
c6 :: c6
ISOP :: Val:Op -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
FIRST :: Val:Op -> c9:c10
c9 :: c9:c10
c10 :: c9:c10
ASSREWRITE :: Val:Op -> c11
c11 :: c3:c4:c5 -> c11
c :: c1 -> c3:c4:c5 -> c
REWRITE[LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c1
c1 :: c2 -> c3:c4:c5 -> c1
REWRITE[LET][LET][LET] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> c2
c2 :: c3:c4:c5 -> c3:c4:c5 -> c2
rewrite[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let][Let] :: Val:Op -> Val:Op -> 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:c4:c51_12 :: c3:c4:c5
hole_Val:Op2_12 :: Val:Op
hole_a3_12 :: a
hole_c4_12 :: c
hole_c65_12 :: c6
hole_c7:c86_12 :: c7:c8
hole_c9:c107_12 :: c9:c10
hole_c118_12 :: c11
hole_c19_12 :: c1
hole_c210_12 :: c2
hole_False:True11_12 :: False:True
gen_c3:c4:c512_12 :: Nat -> c3:c4:c5
gen_Val:Op13_12 :: Nat -> Val:Op


Lemmas:
rewrite(gen_Val:Op13_12(+(1, n15_12))) -> *14_12, rt in Omega(0)


Generator Equations:
gen_c3:c4:c512_12(0) <=> c5
gen_c3:c4:c512_12(+(x, 1)) <=> c3(gen_c3:c4:c512_12(x))
gen_Val:Op13_12(0) <=> Val(hole_a3_12)
gen_Val:Op13_12(+(x, 1)) <=> Op(Val(hole_a3_12), gen_Val:Op13_12(x))


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

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

(18)
BOUNDS(n^1, INF)