WORST_CASE(Omega(n^2),O(n^2))
proof of input_75i3ggErew.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 2 ms]
    (6) CdtProblem
    (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 60 ms]
    (8) CdtProblem
    (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 44 ms]
    (10) CdtProblem
    (11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) BOUNDS(1, 1)
(13) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CdtProblem
    (15) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxRelTRS
    (17) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) CpxRelTRS
    (19) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (20) typed CpxTrs
    (21) OrderProof [LOWER BOUND(ID), 9 ms]
    (22) typed CpxTrs
    (23) RewriteLemmaProof [LOWER BOUND(ID), 308 ms]
    (24) BEST
        (25) proven lower bound
            (26) LowerBoundPropagationProof [FINISHED, 0 ms]
            (27) BOUNDS(n^1, INF)
        (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 64 ms]
            (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 10 ms]
            (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 702 ms]
            (34) proven lower bound
            (35) LowerBoundPropagationProof [FINISHED, 0 ms]
            (36) BOUNDS(n^2, INF)


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

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


The TRS R consists of the following rules:

   rev(nil) -> nil
   rev(.(x, y)) -> ++(rev(y), .(x, nil))
   car(.(x, y)) -> x
   cdr(.(x, y)) -> y
   null(nil) -> true
   null(.(x, y)) -> false
   ++(nil, y) -> y
   ++(.(x, y), z) -> .(x, ++(y, z))

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

(1) CpxTrsToCdtProof (UPPER BOUND(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)) -> ++(rev(z1), .(z0, nil))
   car(.(z0, z1)) -> z0
   cdr(.(z0, z1)) -> z1
   null(nil) -> true
   null(.(z0, z1)) -> false
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
Tuples:
   REV(nil) -> c
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   CAR(.(z0, z1)) -> c2
   CDR(.(z0, z1)) -> c3
   NULL(nil) -> c4
   NULL(.(z0, z1)) -> c5
   ++'(nil, z0) -> c6
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
S tuples:
   REV(nil) -> c
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   CAR(.(z0, z1)) -> c2
   CDR(.(z0, z1)) -> c3
   NULL(nil) -> c4
   NULL(.(z0, z1)) -> c5
   ++'(nil, z0) -> c6
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
K tuples:none
Defined Rule Symbols:   rev_1, car_1, cdr_1, null_1, ++_2

Defined Pair Symbols:   REV_1, CAR_1, CDR_1, NULL_1, ++'_2

Compound Symbols:   c, c1_2, c2, c3, c4, c5, c6, c7_1


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 6 trailing nodes:
   NULL(.(z0, z1)) -> c5
   REV(nil) -> c
   CAR(.(z0, z1)) -> c2
   ++'(nil, z0) -> c6
   CDR(.(z0, z1)) -> c3
   NULL(nil) -> c4

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev(nil) -> nil
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   car(.(z0, z1)) -> z0
   cdr(.(z0, z1)) -> z1
   null(nil) -> true
   null(.(z0, z1)) -> false
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
Tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
S tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
K tuples:none
Defined Rule Symbols:   rev_1, car_1, cdr_1, null_1, ++_2

Defined Pair Symbols:   REV_1, ++'_2

Compound Symbols:   c1_2, c7_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   car(.(z0, z1)) -> z0
   cdr(.(z0, z1)) -> z1
   null(nil) -> true
   null(.(z0, z1)) -> false

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev(nil) -> nil
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
Tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
S tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
K tuples:none
Defined Rule Symbols:   rev_1, ++_2

Defined Pair Symbols:   REV_1, ++'_2

Compound Symbols:   c1_2, c7_1


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

(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
We considered the (Usable) Rules:none
And the Tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(++(x_1, x_2)) = x_1 + x_2
   POL(++'(x_1, x_2)) = 0
   POL(.(x_1, x_2)) = [1] + x_1 + x_2
   POL(REV(x_1)) = x_1
   POL(c1(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   POL(nil) = 0
   POL(rev(x_1)) = [1] + x_1

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev(nil) -> nil
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
Tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
S tuples:
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
K tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
Defined Rule Symbols:   rev_1, ++_2

Defined Pair Symbols:   REV_1, ++'_2

Compound Symbols:   c1_2, c7_1


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
We considered the (Usable) Rules:
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   rev(nil) -> nil
   ++(nil, z0) -> z0
And the Tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(++(x_1, x_2)) = x_1 + [2]x_2
   POL(++'(x_1, x_2)) = [2]x_1
   POL(.(x_1, x_2)) = [2] + x_2
   POL(REV(x_1)) = x_1^2
   POL(c1(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   POL(nil) = 0
   POL(rev(x_1)) = [2]x_1

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev(nil) -> nil
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
Tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
S tuples:none
K tuples:
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
Defined Rule Symbols:   rev_1, ++_2

Defined Pair Symbols:   REV_1, ++'_2

Compound Symbols:   c1_2, c7_1


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

(11) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(12)
BOUNDS(1, 1)

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

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev(nil) -> nil
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   car(.(z0, z1)) -> z0
   cdr(.(z0, z1)) -> z1
   null(nil) -> true
   null(.(z0, z1)) -> false
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
Tuples:
   REV(nil) -> c
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   CAR(.(z0, z1)) -> c2
   CDR(.(z0, z1)) -> c3
   NULL(nil) -> c4
   NULL(.(z0, z1)) -> c5
   ++'(nil, z0) -> c6
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
S tuples:
   REV(nil) -> c
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   CAR(.(z0, z1)) -> c2
   CDR(.(z0, z1)) -> c3
   NULL(nil) -> c4
   NULL(.(z0, z1)) -> c5
   ++'(nil, z0) -> c6
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))
K tuples:none
Defined Rule Symbols:   rev_1, car_1, cdr_1, null_1, ++_2

Defined Pair Symbols:   REV_1, CAR_1, CDR_1, NULL_1, ++'_2

Compound Symbols:   c, c1_2, c2, c3, c4, c5, c6, c7_1


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

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

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


The TRS R consists of the following rules:

   REV(nil) -> c
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   CAR(.(z0, z1)) -> c2
   CDR(.(z0, z1)) -> c3
   NULL(nil) -> c4
   NULL(.(z0, z1)) -> c5
   ++'(nil, z0) -> c6
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))

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

   rev(nil) -> nil
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   car(.(z0, z1)) -> z0
   cdr(.(z0, z1)) -> z1
   null(nil) -> true
   null(.(z0, z1)) -> false
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

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

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

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


The TRS R consists of the following rules:

   REV(nil) -> c
   REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
   CAR(.(z0, z1)) -> c2
   CDR(.(z0, z1)) -> c3
   NULL(nil) -> c4
   NULL(.(z0, z1)) -> c5
   ++'(nil, z0) -> c6
   ++'(.(z0, z1), z2) -> c7(++'(z1, z2))

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

   rev(nil) -> nil
   rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
   car(.(z0, z1)) -> z0
   cdr(.(z0, z1)) -> z1
   null(nil) -> true
   null(.(z0, z1)) -> false
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

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

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

(20)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) -> c2
CDR(.(z0, z1)) -> c3
NULL(nil) -> c4
NULL(.(z0, z1)) -> c5
++'(nil, z0) -> c6
++'(.(z0, z1), z2) -> c7(++'(z1, z2))
rev(nil) -> nil
rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
car(.(z0, z1)) -> z0
cdr(.(z0, z1)) -> z1
null(nil) -> true
null(.(z0, z1)) -> false
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

Types:
REV :: nil:. -> c:c1
nil :: nil:.
c :: c:c1
. :: car -> nil:. -> nil:.
c1 :: c6:c7 -> c:c1 -> c:c1
++' :: nil:. -> nil:. -> c6:c7
rev :: nil:. -> nil:.
CAR :: nil:. -> c2
c2 :: c2
CDR :: nil:. -> c3
c3 :: c3
NULL :: nil:. -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
hole_c:c11_8 :: c:c1
hole_nil:.2_8 :: nil:.
hole_car3_8 :: car
hole_c6:c74_8 :: c6:c7
hole_c25_8 :: c2
hole_c36_8 :: c3
hole_c4:c57_8 :: c4:c5
hole_true:false8_8 :: true:false
gen_c:c19_8 :: Nat -> c:c1
gen_nil:.10_8 :: Nat -> nil:.
gen_c6:c711_8 :: Nat -> c6:c7

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

(21) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
REV, ++', rev, ++

They will be analysed ascendingly in the following order:
++' < REV
rev < REV
++ < rev

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

(22)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) -> c2
CDR(.(z0, z1)) -> c3
NULL(nil) -> c4
NULL(.(z0, z1)) -> c5
++'(nil, z0) -> c6
++'(.(z0, z1), z2) -> c7(++'(z1, z2))
rev(nil) -> nil
rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
car(.(z0, z1)) -> z0
cdr(.(z0, z1)) -> z1
null(nil) -> true
null(.(z0, z1)) -> false
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

Types:
REV :: nil:. -> c:c1
nil :: nil:.
c :: c:c1
. :: car -> nil:. -> nil:.
c1 :: c6:c7 -> c:c1 -> c:c1
++' :: nil:. -> nil:. -> c6:c7
rev :: nil:. -> nil:.
CAR :: nil:. -> c2
c2 :: c2
CDR :: nil:. -> c3
c3 :: c3
NULL :: nil:. -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
hole_c:c11_8 :: c:c1
hole_nil:.2_8 :: nil:.
hole_car3_8 :: car
hole_c6:c74_8 :: c6:c7
hole_c25_8 :: c2
hole_c36_8 :: c3
hole_c4:c57_8 :: c4:c5
hole_true:false8_8 :: true:false
gen_c:c19_8 :: Nat -> c:c1
gen_nil:.10_8 :: Nat -> nil:.
gen_c6:c711_8 :: Nat -> c6:c7


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(c6, gen_c:c19_8(x))
gen_nil:.10_8(0) <=> nil
gen_nil:.10_8(+(x, 1)) <=> .(hole_car3_8, gen_nil:.10_8(x))
gen_c6:c711_8(0) <=> c6
gen_c6:c711_8(+(x, 1)) <=> c7(gen_c6:c711_8(x))


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

They will be analysed ascendingly in the following order:
++' < REV
rev < REV
++ < rev

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
++'(gen_nil:.10_8(n13_8), gen_nil:.10_8(b)) -> gen_c6:c711_8(n13_8), rt in Omega(1 + n13_8)

Induction Base:
++'(gen_nil:.10_8(0), gen_nil:.10_8(b)) ->_R^Omega(1)
c6

Induction Step:
++'(gen_nil:.10_8(+(n13_8, 1)), gen_nil:.10_8(b)) ->_R^Omega(1)
c7(++'(gen_nil:.10_8(n13_8), gen_nil:.10_8(b))) ->_IH
c7(gen_c6:c711_8(c14_8))

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

(24)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
REV(nil) -> c
REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) -> c2
CDR(.(z0, z1)) -> c3
NULL(nil) -> c4
NULL(.(z0, z1)) -> c5
++'(nil, z0) -> c6
++'(.(z0, z1), z2) -> c7(++'(z1, z2))
rev(nil) -> nil
rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
car(.(z0, z1)) -> z0
cdr(.(z0, z1)) -> z1
null(nil) -> true
null(.(z0, z1)) -> false
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

Types:
REV :: nil:. -> c:c1
nil :: nil:.
c :: c:c1
. :: car -> nil:. -> nil:.
c1 :: c6:c7 -> c:c1 -> c:c1
++' :: nil:. -> nil:. -> c6:c7
rev :: nil:. -> nil:.
CAR :: nil:. -> c2
c2 :: c2
CDR :: nil:. -> c3
c3 :: c3
NULL :: nil:. -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
hole_c:c11_8 :: c:c1
hole_nil:.2_8 :: nil:.
hole_car3_8 :: car
hole_c6:c74_8 :: c6:c7
hole_c25_8 :: c2
hole_c36_8 :: c3
hole_c4:c57_8 :: c4:c5
hole_true:false8_8 :: true:false
gen_c:c19_8 :: Nat -> c:c1
gen_nil:.10_8 :: Nat -> nil:.
gen_c6:c711_8 :: Nat -> c6:c7


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(c6, gen_c:c19_8(x))
gen_nil:.10_8(0) <=> nil
gen_nil:.10_8(+(x, 1)) <=> .(hole_car3_8, gen_nil:.10_8(x))
gen_c6:c711_8(0) <=> c6
gen_c6:c711_8(+(x, 1)) <=> c7(gen_c6:c711_8(x))


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

They will be analysed ascendingly in the following order:
++' < REV
rev < REV
++ < rev

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

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

(27)
BOUNDS(n^1, INF)

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

(28)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) -> c2
CDR(.(z0, z1)) -> c3
NULL(nil) -> c4
NULL(.(z0, z1)) -> c5
++'(nil, z0) -> c6
++'(.(z0, z1), z2) -> c7(++'(z1, z2))
rev(nil) -> nil
rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
car(.(z0, z1)) -> z0
cdr(.(z0, z1)) -> z1
null(nil) -> true
null(.(z0, z1)) -> false
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

Types:
REV :: nil:. -> c:c1
nil :: nil:.
c :: c:c1
. :: car -> nil:. -> nil:.
c1 :: c6:c7 -> c:c1 -> c:c1
++' :: nil:. -> nil:. -> c6:c7
rev :: nil:. -> nil:.
CAR :: nil:. -> c2
c2 :: c2
CDR :: nil:. -> c3
c3 :: c3
NULL :: nil:. -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
hole_c:c11_8 :: c:c1
hole_nil:.2_8 :: nil:.
hole_car3_8 :: car
hole_c6:c74_8 :: c6:c7
hole_c25_8 :: c2
hole_c36_8 :: c3
hole_c4:c57_8 :: c4:c5
hole_true:false8_8 :: true:false
gen_c:c19_8 :: Nat -> c:c1
gen_nil:.10_8 :: Nat -> nil:.
gen_c6:c711_8 :: Nat -> c6:c7


Lemmas:
++'(gen_nil:.10_8(n13_8), gen_nil:.10_8(b)) -> gen_c6:c711_8(n13_8), rt in Omega(1 + n13_8)


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(c6, gen_c:c19_8(x))
gen_nil:.10_8(0) <=> nil
gen_nil:.10_8(+(x, 1)) <=> .(hole_car3_8, gen_nil:.10_8(x))
gen_c6:c711_8(0) <=> c6
gen_c6:c711_8(+(x, 1)) <=> c7(gen_c6:c711_8(x))


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

They will be analysed ascendingly in the following order:
rev < REV
++ < rev

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
++(gen_nil:.10_8(n558_8), gen_nil:.10_8(b)) -> gen_nil:.10_8(+(n558_8, b)), rt in Omega(0)

Induction Base:
++(gen_nil:.10_8(0), gen_nil:.10_8(b)) ->_R^Omega(0)
gen_nil:.10_8(b)

Induction Step:
++(gen_nil:.10_8(+(n558_8, 1)), gen_nil:.10_8(b)) ->_R^Omega(0)
.(hole_car3_8, ++(gen_nil:.10_8(n558_8), gen_nil:.10_8(b))) ->_IH
.(hole_car3_8, gen_nil:.10_8(+(b, c559_8)))

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

(30)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) -> c2
CDR(.(z0, z1)) -> c3
NULL(nil) -> c4
NULL(.(z0, z1)) -> c5
++'(nil, z0) -> c6
++'(.(z0, z1), z2) -> c7(++'(z1, z2))
rev(nil) -> nil
rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
car(.(z0, z1)) -> z0
cdr(.(z0, z1)) -> z1
null(nil) -> true
null(.(z0, z1)) -> false
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

Types:
REV :: nil:. -> c:c1
nil :: nil:.
c :: c:c1
. :: car -> nil:. -> nil:.
c1 :: c6:c7 -> c:c1 -> c:c1
++' :: nil:. -> nil:. -> c6:c7
rev :: nil:. -> nil:.
CAR :: nil:. -> c2
c2 :: c2
CDR :: nil:. -> c3
c3 :: c3
NULL :: nil:. -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
hole_c:c11_8 :: c:c1
hole_nil:.2_8 :: nil:.
hole_car3_8 :: car
hole_c6:c74_8 :: c6:c7
hole_c25_8 :: c2
hole_c36_8 :: c3
hole_c4:c57_8 :: c4:c5
hole_true:false8_8 :: true:false
gen_c:c19_8 :: Nat -> c:c1
gen_nil:.10_8 :: Nat -> nil:.
gen_c6:c711_8 :: Nat -> c6:c7


Lemmas:
++'(gen_nil:.10_8(n13_8), gen_nil:.10_8(b)) -> gen_c6:c711_8(n13_8), rt in Omega(1 + n13_8)
++(gen_nil:.10_8(n558_8), gen_nil:.10_8(b)) -> gen_nil:.10_8(+(n558_8, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(c6, gen_c:c19_8(x))
gen_nil:.10_8(0) <=> nil
gen_nil:.10_8(+(x, 1)) <=> .(hole_car3_8, gen_nil:.10_8(x))
gen_c6:c711_8(0) <=> c6
gen_c6:c711_8(+(x, 1)) <=> c7(gen_c6:c711_8(x))


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

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

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rev(gen_nil:.10_8(n1553_8)) -> gen_nil:.10_8(n1553_8), rt in Omega(0)

Induction Base:
rev(gen_nil:.10_8(0)) ->_R^Omega(0)
nil

Induction Step:
rev(gen_nil:.10_8(+(n1553_8, 1))) ->_R^Omega(0)
++(rev(gen_nil:.10_8(n1553_8)), .(hole_car3_8, nil)) ->_IH
++(gen_nil:.10_8(c1554_8), .(hole_car3_8, nil)) ->_L^Omega(0)
gen_nil:.10_8(+(n1553_8, +(0, 1)))

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

(32)
Obligation:
Innermost TRS:
Rules:
REV(nil) -> c
REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) -> c2
CDR(.(z0, z1)) -> c3
NULL(nil) -> c4
NULL(.(z0, z1)) -> c5
++'(nil, z0) -> c6
++'(.(z0, z1), z2) -> c7(++'(z1, z2))
rev(nil) -> nil
rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
car(.(z0, z1)) -> z0
cdr(.(z0, z1)) -> z1
null(nil) -> true
null(.(z0, z1)) -> false
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

Types:
REV :: nil:. -> c:c1
nil :: nil:.
c :: c:c1
. :: car -> nil:. -> nil:.
c1 :: c6:c7 -> c:c1 -> c:c1
++' :: nil:. -> nil:. -> c6:c7
rev :: nil:. -> nil:.
CAR :: nil:. -> c2
c2 :: c2
CDR :: nil:. -> c3
c3 :: c3
NULL :: nil:. -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
hole_c:c11_8 :: c:c1
hole_nil:.2_8 :: nil:.
hole_car3_8 :: car
hole_c6:c74_8 :: c6:c7
hole_c25_8 :: c2
hole_c36_8 :: c3
hole_c4:c57_8 :: c4:c5
hole_true:false8_8 :: true:false
gen_c:c19_8 :: Nat -> c:c1
gen_nil:.10_8 :: Nat -> nil:.
gen_c6:c711_8 :: Nat -> c6:c7


Lemmas:
++'(gen_nil:.10_8(n13_8), gen_nil:.10_8(b)) -> gen_c6:c711_8(n13_8), rt in Omega(1 + n13_8)
++(gen_nil:.10_8(n558_8), gen_nil:.10_8(b)) -> gen_nil:.10_8(+(n558_8, b)), rt in Omega(0)
rev(gen_nil:.10_8(n1553_8)) -> gen_nil:.10_8(n1553_8), rt in Omega(0)


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(c6, gen_c:c19_8(x))
gen_nil:.10_8(0) <=> nil
gen_nil:.10_8(+(x, 1)) <=> .(hole_car3_8, gen_nil:.10_8(x))
gen_c6:c711_8(0) <=> c6
gen_c6:c711_8(+(x, 1)) <=> c7(gen_c6:c711_8(x))


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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REV(gen_nil:.10_8(n1869_8)) -> *12_8, rt in Omega(n1869_8 + n1869_8^2)

Induction Base:
REV(gen_nil:.10_8(0))

Induction Step:
REV(gen_nil:.10_8(+(n1869_8, 1))) ->_R^Omega(1)
c1(++'(rev(gen_nil:.10_8(n1869_8)), .(hole_car3_8, nil)), REV(gen_nil:.10_8(n1869_8))) ->_L^Omega(0)
c1(++'(gen_nil:.10_8(n1869_8), .(hole_car3_8, nil)), REV(gen_nil:.10_8(n1869_8))) ->_L^Omega(1 + n1869_8)
c1(gen_c6:c711_8(n1869_8), REV(gen_nil:.10_8(n1869_8))) ->_IH
c1(gen_c6:c711_8(n1869_8), *12_8)

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

(34)
Obligation:
Proved the lower bound n^2 for the following obligation:

Innermost TRS:
Rules:
REV(nil) -> c
REV(.(z0, z1)) -> c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) -> c2
CDR(.(z0, z1)) -> c3
NULL(nil) -> c4
NULL(.(z0, z1)) -> c5
++'(nil, z0) -> c6
++'(.(z0, z1), z2) -> c7(++'(z1, z2))
rev(nil) -> nil
rev(.(z0, z1)) -> ++(rev(z1), .(z0, nil))
car(.(z0, z1)) -> z0
cdr(.(z0, z1)) -> z1
null(nil) -> true
null(.(z0, z1)) -> false
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))

Types:
REV :: nil:. -> c:c1
nil :: nil:.
c :: c:c1
. :: car -> nil:. -> nil:.
c1 :: c6:c7 -> c:c1 -> c:c1
++' :: nil:. -> nil:. -> c6:c7
rev :: nil:. -> nil:.
CAR :: nil:. -> c2
c2 :: c2
CDR :: nil:. -> c3
c3 :: c3
NULL :: nil:. -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
hole_c:c11_8 :: c:c1
hole_nil:.2_8 :: nil:.
hole_car3_8 :: car
hole_c6:c74_8 :: c6:c7
hole_c25_8 :: c2
hole_c36_8 :: c3
hole_c4:c57_8 :: c4:c5
hole_true:false8_8 :: true:false
gen_c:c19_8 :: Nat -> c:c1
gen_nil:.10_8 :: Nat -> nil:.
gen_c6:c711_8 :: Nat -> c6:c7


Lemmas:
++'(gen_nil:.10_8(n13_8), gen_nil:.10_8(b)) -> gen_c6:c711_8(n13_8), rt in Omega(1 + n13_8)
++(gen_nil:.10_8(n558_8), gen_nil:.10_8(b)) -> gen_nil:.10_8(+(n558_8, b)), rt in Omega(0)
rev(gen_nil:.10_8(n1553_8)) -> gen_nil:.10_8(n1553_8), rt in Omega(0)


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(c6, gen_c:c19_8(x))
gen_nil:.10_8(0) <=> nil
gen_nil:.10_8(+(x, 1)) <=> .(hole_car3_8, gen_nil:.10_8(x))
gen_c6:c711_8(0) <=> c6
gen_c6:c711_8(+(x, 1)) <=> c7(gen_c6:c711_8(x))


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

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

(36)
BOUNDS(n^2, INF)