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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 19 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 300 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 31 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 635 ms]
        (20) typed CpxTrs


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

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


The TRS R consists of the following rules:

   rev(nil) -> nil
   rev(++(x, y)) -> ++(rev1(x, y), rev2(x, y))
   rev1(x, nil) -> x
   rev1(x, ++(y, z)) -> rev1(y, z)
   rev2(x, nil) -> nil
   rev2(x, ++(y, z)) -> rev(++(x, rev(rev2(y, z))))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev(nil) -> nil
   rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
   rev1(z0, nil) -> z0
   rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
   rev2(z0, nil) -> nil
   rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))
Tuples:
   REV(nil) -> c
   REV(++(z0, z1)) -> c1(REV1(z0, z1))
   REV(++(z0, z1)) -> c2(REV2(z0, z1))
   REV1(z0, nil) -> c3
   REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
   REV2(z0, nil) -> c5
   REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
S tuples:
   REV(nil) -> c
   REV(++(z0, z1)) -> c1(REV1(z0, z1))
   REV(++(z0, z1)) -> c2(REV2(z0, z1))
   REV1(z0, nil) -> c3
   REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
   REV2(z0, nil) -> c5
   REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
K tuples:none
Defined Rule Symbols:   rev_1, rev1_2, rev2_2

Defined Pair Symbols:   REV_1, REV1_2, REV2_2

Compound Symbols:   c, c1_1, c2_1, c3, c4_1, c5, c6_3


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

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

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

   REV(nil) -> c
   REV(++(z0, z1)) -> c1(REV1(z0, z1))
   REV(++(z0, z1)) -> c2(REV2(z0, z1))
   REV1(z0, nil) -> c3
   REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
   REV2(z0, nil) -> c5
   REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))

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

   rev(nil) -> nil
   rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
   rev1(z0, nil) -> z0
   rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
   rev2(z0, nil) -> nil
   rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

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

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

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

   REV(nil) -> c
   REV(++(z0, z1)) -> c1(REV1(z0, z1))
   REV(++(z0, z1)) -> c2(REV2(z0, z1))
   REV1(z0, nil) -> c3
   REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
   REV2(z0, nil) -> c5
   REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))

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

   rev(nil) -> nil
   rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
   rev1(z0, nil) -> z0
   rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
   rev2(z0, nil) -> nil
   rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(++(z0, z1)) -> c1(REV1(z0, z1))
REV(++(z0, z1)) -> c2(REV2(z0, z1))
REV1(z0, nil) -> c3
REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
REV2(z0, nil) -> c5
REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
rev(nil) -> nil
rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
rev1(z0, nil) -> z0
rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
rev2(z0, nil) -> nil
rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

Types:
REV :: nil:++ -> c:c1:c2
nil :: nil:++
c :: c:c1:c2
++ :: rev1 -> nil:++ -> nil:++
c1 :: c3:c4 -> c:c1:c2
REV1 :: rev1 -> nil:++ -> c3:c4
c2 :: c5:c6 -> c:c1:c2
REV2 :: rev1 -> nil:++ -> c5:c6
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
c5 :: c5:c6
c6 :: c:c1:c2 -> c:c1:c2 -> c5:c6 -> c5:c6
rev :: nil:++ -> nil:++
rev2 :: rev1 -> nil:++ -> nil:++
rev1 :: rev1 -> nil:++ -> rev1
hole_c:c1:c21_7 :: c:c1:c2
hole_nil:++2_7 :: nil:++
hole_rev13_7 :: rev1
hole_c3:c44_7 :: c3:c4
hole_c5:c65_7 :: c5:c6
gen_nil:++6_7 :: Nat -> nil:++
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
REV, REV1, REV2, rev, rev2, rev1

They will be analysed ascendingly in the following order:
REV1 < REV
REV = REV2
rev < REV2
rev2 < REV2
rev = rev2
rev1 < rev

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

(10)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(++(z0, z1)) -> c1(REV1(z0, z1))
REV(++(z0, z1)) -> c2(REV2(z0, z1))
REV1(z0, nil) -> c3
REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
REV2(z0, nil) -> c5
REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
rev(nil) -> nil
rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
rev1(z0, nil) -> z0
rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
rev2(z0, nil) -> nil
rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

Types:
REV :: nil:++ -> c:c1:c2
nil :: nil:++
c :: c:c1:c2
++ :: rev1 -> nil:++ -> nil:++
c1 :: c3:c4 -> c:c1:c2
REV1 :: rev1 -> nil:++ -> c3:c4
c2 :: c5:c6 -> c:c1:c2
REV2 :: rev1 -> nil:++ -> c5:c6
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
c5 :: c5:c6
c6 :: c:c1:c2 -> c:c1:c2 -> c5:c6 -> c5:c6
rev :: nil:++ -> nil:++
rev2 :: rev1 -> nil:++ -> nil:++
rev1 :: rev1 -> nil:++ -> rev1
hole_c:c1:c21_7 :: c:c1:c2
hole_nil:++2_7 :: nil:++
hole_rev13_7 :: rev1
hole_c3:c44_7 :: c3:c4
hole_c5:c65_7 :: c5:c6
gen_nil:++6_7 :: Nat -> nil:++
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Generator Equations:
gen_nil:++6_7(0) <=> nil
gen_nil:++6_7(+(x, 1)) <=> ++(hole_rev13_7, gen_nil:++6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
REV1, REV, REV2, rev, rev2, rev1

They will be analysed ascendingly in the following order:
REV1 < REV
REV = REV2
rev < REV2
rev2 < REV2
rev = rev2
rev1 < rev

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REV1(hole_rev13_7, gen_nil:++6_7(n10_7)) -> gen_c3:c47_7(n10_7), rt in Omega(1 + n10_7)

Induction Base:
REV1(hole_rev13_7, gen_nil:++6_7(0)) ->_R^Omega(1)
c3

Induction Step:
REV1(hole_rev13_7, gen_nil:++6_7(+(n10_7, 1))) ->_R^Omega(1)
c4(REV1(hole_rev13_7, gen_nil:++6_7(n10_7))) ->_IH
c4(gen_c3:c47_7(c11_7))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
REV(nil) -> c
REV(++(z0, z1)) -> c1(REV1(z0, z1))
REV(++(z0, z1)) -> c2(REV2(z0, z1))
REV1(z0, nil) -> c3
REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
REV2(z0, nil) -> c5
REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
rev(nil) -> nil
rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
rev1(z0, nil) -> z0
rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
rev2(z0, nil) -> nil
rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

Types:
REV :: nil:++ -> c:c1:c2
nil :: nil:++
c :: c:c1:c2
++ :: rev1 -> nil:++ -> nil:++
c1 :: c3:c4 -> c:c1:c2
REV1 :: rev1 -> nil:++ -> c3:c4
c2 :: c5:c6 -> c:c1:c2
REV2 :: rev1 -> nil:++ -> c5:c6
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
c5 :: c5:c6
c6 :: c:c1:c2 -> c:c1:c2 -> c5:c6 -> c5:c6
rev :: nil:++ -> nil:++
rev2 :: rev1 -> nil:++ -> nil:++
rev1 :: rev1 -> nil:++ -> rev1
hole_c:c1:c21_7 :: c:c1:c2
hole_nil:++2_7 :: nil:++
hole_rev13_7 :: rev1
hole_c3:c44_7 :: c3:c4
hole_c5:c65_7 :: c5:c6
gen_nil:++6_7 :: Nat -> nil:++
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Generator Equations:
gen_nil:++6_7(0) <=> nil
gen_nil:++6_7(+(x, 1)) <=> ++(hole_rev13_7, gen_nil:++6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
REV1, REV, REV2, rev, rev2, rev1

They will be analysed ascendingly in the following order:
REV1 < REV
REV = REV2
rev < REV2
rev2 < REV2
rev = rev2
rev1 < rev

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(++(z0, z1)) -> c1(REV1(z0, z1))
REV(++(z0, z1)) -> c2(REV2(z0, z1))
REV1(z0, nil) -> c3
REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
REV2(z0, nil) -> c5
REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
rev(nil) -> nil
rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
rev1(z0, nil) -> z0
rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
rev2(z0, nil) -> nil
rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

Types:
REV :: nil:++ -> c:c1:c2
nil :: nil:++
c :: c:c1:c2
++ :: rev1 -> nil:++ -> nil:++
c1 :: c3:c4 -> c:c1:c2
REV1 :: rev1 -> nil:++ -> c3:c4
c2 :: c5:c6 -> c:c1:c2
REV2 :: rev1 -> nil:++ -> c5:c6
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
c5 :: c5:c6
c6 :: c:c1:c2 -> c:c1:c2 -> c5:c6 -> c5:c6
rev :: nil:++ -> nil:++
rev2 :: rev1 -> nil:++ -> nil:++
rev1 :: rev1 -> nil:++ -> rev1
hole_c:c1:c21_7 :: c:c1:c2
hole_nil:++2_7 :: nil:++
hole_rev13_7 :: rev1
hole_c3:c44_7 :: c3:c4
hole_c5:c65_7 :: c5:c6
gen_nil:++6_7 :: Nat -> nil:++
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
REV1(hole_rev13_7, gen_nil:++6_7(n10_7)) -> gen_c3:c47_7(n10_7), rt in Omega(1 + n10_7)


Generator Equations:
gen_nil:++6_7(0) <=> nil
gen_nil:++6_7(+(x, 1)) <=> ++(hole_rev13_7, gen_nil:++6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
rev1, REV, REV2, rev, rev2

They will be analysed ascendingly in the following order:
REV = REV2
rev < REV2
rev2 < REV2
rev = rev2
rev1 < rev

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rev1(hole_rev13_7, gen_nil:++6_7(n317_7)) -> hole_rev13_7, rt in Omega(0)

Induction Base:
rev1(hole_rev13_7, gen_nil:++6_7(0)) ->_R^Omega(0)
hole_rev13_7

Induction Step:
rev1(hole_rev13_7, gen_nil:++6_7(+(n317_7, 1))) ->_R^Omega(0)
rev1(hole_rev13_7, gen_nil:++6_7(n317_7)) ->_IH
hole_rev13_7

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

(18)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(++(z0, z1)) -> c1(REV1(z0, z1))
REV(++(z0, z1)) -> c2(REV2(z0, z1))
REV1(z0, nil) -> c3
REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
REV2(z0, nil) -> c5
REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
rev(nil) -> nil
rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
rev1(z0, nil) -> z0
rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
rev2(z0, nil) -> nil
rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

Types:
REV :: nil:++ -> c:c1:c2
nil :: nil:++
c :: c:c1:c2
++ :: rev1 -> nil:++ -> nil:++
c1 :: c3:c4 -> c:c1:c2
REV1 :: rev1 -> nil:++ -> c3:c4
c2 :: c5:c6 -> c:c1:c2
REV2 :: rev1 -> nil:++ -> c5:c6
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
c5 :: c5:c6
c6 :: c:c1:c2 -> c:c1:c2 -> c5:c6 -> c5:c6
rev :: nil:++ -> nil:++
rev2 :: rev1 -> nil:++ -> nil:++
rev1 :: rev1 -> nil:++ -> rev1
hole_c:c1:c21_7 :: c:c1:c2
hole_nil:++2_7 :: nil:++
hole_rev13_7 :: rev1
hole_c3:c44_7 :: c3:c4
hole_c5:c65_7 :: c5:c6
gen_nil:++6_7 :: Nat -> nil:++
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
REV1(hole_rev13_7, gen_nil:++6_7(n10_7)) -> gen_c3:c47_7(n10_7), rt in Omega(1 + n10_7)
rev1(hole_rev13_7, gen_nil:++6_7(n317_7)) -> hole_rev13_7, rt in Omega(0)


Generator Equations:
gen_nil:++6_7(0) <=> nil
gen_nil:++6_7(+(x, 1)) <=> ++(hole_rev13_7, gen_nil:++6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
rev2, REV, REV2, rev

They will be analysed ascendingly in the following order:
REV = REV2
rev < REV2
rev2 < REV2
rev = rev2

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rev2(hole_rev13_7, gen_nil:++6_7(+(1, n468_7))) -> *9_7, rt in Omega(0)

Induction Base:
rev2(hole_rev13_7, gen_nil:++6_7(+(1, 0)))

Induction Step:
rev2(hole_rev13_7, gen_nil:++6_7(+(1, +(n468_7, 1)))) ->_R^Omega(0)
rev(++(hole_rev13_7, rev(rev2(hole_rev13_7, gen_nil:++6_7(+(1, n468_7)))))) ->_IH
rev(++(hole_rev13_7, rev(*9_7)))

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

(20)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(++(z0, z1)) -> c1(REV1(z0, z1))
REV(++(z0, z1)) -> c2(REV2(z0, z1))
REV1(z0, nil) -> c3
REV1(z0, ++(z1, z2)) -> c4(REV1(z1, z2))
REV2(z0, nil) -> c5
REV2(z0, ++(z1, z2)) -> c6(REV(++(z0, rev(rev2(z1, z2)))), REV(rev2(z1, z2)), REV2(z1, z2))
rev(nil) -> nil
rev(++(z0, z1)) -> ++(rev1(z0, z1), rev2(z0, z1))
rev1(z0, nil) -> z0
rev1(z0, ++(z1, z2)) -> rev1(z1, z2)
rev2(z0, nil) -> nil
rev2(z0, ++(z1, z2)) -> rev(++(z0, rev(rev2(z1, z2))))

Types:
REV :: nil:++ -> c:c1:c2
nil :: nil:++
c :: c:c1:c2
++ :: rev1 -> nil:++ -> nil:++
c1 :: c3:c4 -> c:c1:c2
REV1 :: rev1 -> nil:++ -> c3:c4
c2 :: c5:c6 -> c:c1:c2
REV2 :: rev1 -> nil:++ -> c5:c6
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
c5 :: c5:c6
c6 :: c:c1:c2 -> c:c1:c2 -> c5:c6 -> c5:c6
rev :: nil:++ -> nil:++
rev2 :: rev1 -> nil:++ -> nil:++
rev1 :: rev1 -> nil:++ -> rev1
hole_c:c1:c21_7 :: c:c1:c2
hole_nil:++2_7 :: nil:++
hole_rev13_7 :: rev1
hole_c3:c44_7 :: c3:c4
hole_c5:c65_7 :: c5:c6
gen_nil:++6_7 :: Nat -> nil:++
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
REV1(hole_rev13_7, gen_nil:++6_7(n10_7)) -> gen_c3:c47_7(n10_7), rt in Omega(1 + n10_7)
rev1(hole_rev13_7, gen_nil:++6_7(n317_7)) -> hole_rev13_7, rt in Omega(0)
rev2(hole_rev13_7, gen_nil:++6_7(+(1, n468_7))) -> *9_7, rt in Omega(0)


Generator Equations:
gen_nil:++6_7(0) <=> nil
gen_nil:++6_7(+(x, 1)) <=> ++(hole_rev13_7, gen_nil:++6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
rev, REV, REV2

They will be analysed ascendingly in the following order:
REV = REV2
rev < REV2
rev2 < REV2
rev = rev2