WORST_CASE(Omega(n^1),O(n^1))
proof of input_oFqxD5zOsN.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, n^1).

(0) CpxTRS
(1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(2) CpxTRS
    (3) CpxTrsMatchBoundsTAProof [FINISHED, 73 ms]
    (4) BOUNDS(1, n^1)
(5) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 2 ms]
    (12) typed CpxTrs
    (13) OrderProof [LOWER BOUND(ID), 0 ms]
    (14) typed CpxTrs
    (15) RewriteLemmaProof [LOWER BOUND(ID), 2780 ms]
    (16) typed CpxTrs
    (17) RewriteLemmaProof [LOWER BOUND(ID), 1922 ms]
    (18) typed CpxTrs
    (19) RewriteLemmaProof [LOWER BOUND(ID), 1765 ms]
    (20) typed CpxTrs
    (21) RewriteLemmaProof [LOWER BOUND(ID), 1691 ms]
    (22) typed CpxTrs
    (23) RewriteLemmaProof [LOWER BOUND(ID), 1602 ms]
    (24) typed CpxTrs
    (25) RewriteLemmaProof [LOWER BOUND(ID), 1689 ms]
    (26) typed CpxTrs
    (27) RewriteLemmaProof [LOWER BOUND(ID), 531 ms]
    (28) BEST
        (29) proven lower bound
            (30) LowerBoundPropagationProof [FINISHED, 0 ms]
            (31) BOUNDS(n^1, INF)
        (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 677 ms]
            (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 590 ms]
            (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 621 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 646 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 656 ms]
            (42) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   group3(@l) -> group3#1(@l)
   group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
   group3#1(nil) -> nil
   group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
   group3#2(nil, @x) -> nil
   group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs))
   group3#3(nil, @x, @y) -> nil
   zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
   zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
   zip3#1(nil, @l2, @l3) -> nil
   zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys)
   zip3#2(nil, @l3, @x, @xs) -> nil
   zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
   zip3#3(nil, @x, @xs, @y, @ys) -> nil

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

(1) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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


The TRS R consists of the following rules:

   group3(@l) -> group3#1(@l)
   group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
   group3#1(nil) -> nil
   group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
   group3#2(nil, @x) -> nil
   group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs))
   group3#3(nil, @x, @y) -> nil
   zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
   zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
   zip3#1(nil, @l2, @l3) -> nil
   zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys)
   zip3#2(nil, @l3, @x, @xs) -> nil
   zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
   zip3#3(nil, @x, @xs, @y, @ys) -> nil

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

(3) CpxTrsMatchBoundsTAProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2. 

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1, 2, 3, 4, 5, 6, 7, 8]
transitions: 
::0(0, 0) -> 0
nil0() -> 0
tuple#30(0, 0, 0) -> 0
group30(0) -> 1
group3#10(0) -> 2
group3#20(0, 0) -> 3
group3#30(0, 0, 0) -> 4
zip30(0, 0, 0) -> 5
zip3#10(0, 0, 0) -> 6
zip3#20(0, 0, 0, 0) -> 7
zip3#30(0, 0, 0, 0, 0) -> 8
group3#11(0) -> 1
group3#21(0, 0) -> 2
nil1() -> 2
group3#31(0, 0, 0) -> 3
nil1() -> 3
tuple#31(0, 0, 0) -> 9
group31(0) -> 10
::1(9, 10) -> 4
nil1() -> 4
zip3#11(0, 0, 0) -> 5
zip3#21(0, 0, 0, 0) -> 6
nil1() -> 6
zip3#31(0, 0, 0, 0, 0) -> 7
nil1() -> 7
zip31(0, 0, 0) -> 11
::1(9, 11) -> 8
nil1() -> 8
group3#12(0) -> 10
group3#21(0, 0) -> 1
nil1() -> 1
group3#31(0, 0, 0) -> 2
::1(9, 10) -> 3
zip3#12(0, 0, 0) -> 11
zip3#21(0, 0, 0, 0) -> 5
nil1() -> 5
zip3#31(0, 0, 0, 0, 0) -> 6
::1(9, 11) -> 7
group3#31(0, 0, 0) -> 1
::1(9, 10) -> 2
zip3#31(0, 0, 0, 0, 0) -> 5
::1(9, 11) -> 6
group3#21(0, 0) -> 10
nil1() -> 10
zip3#21(0, 0, 0, 0) -> 11
nil1() -> 11
group3#31(0, 0, 0) -> 10
::1(9, 10) -> 1
zip3#31(0, 0, 0, 0, 0) -> 11
::1(9, 11) -> 5
::1(9, 10) -> 10
::1(9, 11) -> 11

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

(4)
BOUNDS(1, n^1)

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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   group3(z0) -> group3#1(z0)
   group3#1(::(z0, z1)) -> group3#2(z1, z0)
   group3#1(nil) -> nil
   group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
   group3#2(nil, z0) -> nil
   group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
   group3#3(nil, z0, z1) -> nil
   zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
   zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
   zip3#1(nil, z0, z1) -> nil
   zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
   zip3#2(nil, z0, z1, z2) -> nil
   zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
   zip3#3(nil, z0, z1, z2, z3) -> nil
Tuples:
   GROUP3(z0) -> c(GROUP3#1(z0))
   GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
   GROUP3#1(nil) -> c2
   GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
   GROUP3#2(nil, z0) -> c4
   GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
   GROUP3#3(nil, z0, z1) -> c6
   ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
   ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
   ZIP3#1(nil, z0, z1) -> c9
   ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
   ZIP3#2(nil, z0, z1, z2) -> c11
   ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
   ZIP3#3(nil, z0, z1, z2, z3) -> c13
S tuples:
   GROUP3(z0) -> c(GROUP3#1(z0))
   GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
   GROUP3#1(nil) -> c2
   GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
   GROUP3#2(nil, z0) -> c4
   GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
   GROUP3#3(nil, z0, z1) -> c6
   ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
   ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
   ZIP3#1(nil, z0, z1) -> c9
   ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
   ZIP3#2(nil, z0, z1, z2) -> c11
   ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
   ZIP3#3(nil, z0, z1, z2, z3) -> c13
K tuples:none
Defined Rule Symbols:   group3_1, group3#1_1, group3#2_2, group3#3_3, zip3_3, zip3#1_3, zip3#2_4, zip3#3_5

Defined Pair Symbols:   GROUP3_1, GROUP3#1_1, GROUP3#2_2, GROUP3#3_3, ZIP3_3, ZIP3#1_3, ZIP3#2_4, ZIP3#3_5

Compound Symbols:   c_1, c1_1, c2, c3_1, c4, c5_1, c6, c7_1, c8_1, c9, c10_1, c11, c12_1, c13


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

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

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

   GROUP3(z0) -> c(GROUP3#1(z0))
   GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
   GROUP3#1(nil) -> c2
   GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
   GROUP3#2(nil, z0) -> c4
   GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
   GROUP3#3(nil, z0, z1) -> c6
   ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
   ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
   ZIP3#1(nil, z0, z1) -> c9
   ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
   ZIP3#2(nil, z0, z1, z2) -> c11
   ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
   ZIP3#3(nil, z0, z1, z2, z3) -> c13

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

   group3(z0) -> group3#1(z0)
   group3#1(::(z0, z1)) -> group3#2(z1, z0)
   group3#1(nil) -> nil
   group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
   group3#2(nil, z0) -> nil
   group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
   group3#3(nil, z0, z1) -> nil
   zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
   zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
   zip3#1(nil, z0, z1) -> nil
   zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
   zip3#2(nil, z0, z1, z2) -> nil
   zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
   zip3#3(nil, z0, z1, z2, z3) -> nil

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

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

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

   GROUP3(z0) -> c(GROUP3#1(z0))
   GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
   GROUP3#1(nil) -> c2
   GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
   GROUP3#2(nil, z0) -> c4
   GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
   GROUP3#3(nil, z0, z1) -> c6
   ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
   ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
   ZIP3#1(nil, z0, z1) -> c9
   ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
   ZIP3#2(nil, z0, z1, z2) -> c11
   ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
   ZIP3#3(nil, z0, z1, z2, z3) -> c13

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

   group3(z0) -> group3#1(z0)
   group3#1(::(z0, z1)) -> group3#2(z1, z0)
   group3#1(nil) -> nil
   group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
   group3#2(nil, z0) -> nil
   group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
   group3#3(nil, z0, z1) -> nil
   zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
   zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
   zip3#1(nil, z0, z1) -> nil
   zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
   zip3#2(nil, z0, z1, z2) -> nil
   zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
   zip3#3(nil, z0, z1, z2, z3) -> nil

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

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

(12)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3

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

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
GROUP3, GROUP3#1, ZIP3, ZIP3#1, group3, group3#1, zip3, zip3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1
group3 = group3#1
zip3 = zip3#1

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

(14)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
zip3#1, GROUP3, GROUP3#1, ZIP3, ZIP3#1, group3, group3#1, zip3

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1
group3 = group3#1
zip3 = zip3#1

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
zip3#1(gen_:::nil11_14(+(1, n14_14)), gen_:::nil11_14(n14_14), gen_:::nil11_14(n14_14)) -> *13_14, rt in Omega(0)

Induction Base:
zip3#1(gen_:::nil11_14(+(1, 0)), gen_:::nil11_14(0), gen_:::nil11_14(0))

Induction Step:
zip3#1(gen_:::nil11_14(+(1, +(n14_14, 1))), gen_:::nil11_14(+(n14_14, 1)), gen_:::nil11_14(+(n14_14, 1))) ->_R^Omega(0)
zip3#2(gen_:::nil11_14(+(n14_14, 1)), gen_:::nil11_14(+(n14_14, 1)), hole_tuple#34_14, gen_:::nil11_14(+(1, n14_14))) ->_R^Omega(0)
zip3#3(gen_:::nil11_14(+(1, n14_14)), hole_tuple#34_14, gen_:::nil11_14(+(1, n14_14)), hole_tuple#34_14, gen_:::nil11_14(n14_14)) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), zip3(gen_:::nil11_14(+(1, n14_14)), gen_:::nil11_14(n14_14), gen_:::nil11_14(n14_14))) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), zip3#1(gen_:::nil11_14(+(1, n14_14)), gen_:::nil11_14(n14_14), gen_:::nil11_14(n14_14))) ->_IH
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), *13_14)

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

(16)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n14_14)), gen_:::nil11_14(n14_14), gen_:::nil11_14(n14_14)) -> *13_14, rt in Omega(0)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
zip3, GROUP3, GROUP3#1, ZIP3, ZIP3#1, group3, group3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1
group3 = group3#1
zip3 = zip3#1

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)

Induction Base:
zip3(gen_:::nil11_14(0), gen_:::nil11_14(0), gen_:::nil11_14(0))

Induction Step:
zip3(gen_:::nil11_14(+(n24386_14, 1)), gen_:::nil11_14(+(n24386_14, 1)), gen_:::nil11_14(+(n24386_14, 1))) ->_R^Omega(0)
zip3#1(gen_:::nil11_14(+(n24386_14, 1)), gen_:::nil11_14(+(n24386_14, 1)), gen_:::nil11_14(+(n24386_14, 1))) ->_R^Omega(0)
zip3#2(gen_:::nil11_14(+(1, n24386_14)), gen_:::nil11_14(+(1, n24386_14)), hole_tuple#34_14, gen_:::nil11_14(n24386_14)) ->_R^Omega(0)
zip3#3(gen_:::nil11_14(+(1, n24386_14)), hole_tuple#34_14, gen_:::nil11_14(n24386_14), hole_tuple#34_14, gen_:::nil11_14(n24386_14)) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14))) ->_IH
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), *13_14)

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:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n14_14)), gen_:::nil11_14(n14_14), gen_:::nil11_14(n14_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
zip3#1, GROUP3, GROUP3#1, ZIP3, ZIP3#1, group3, group3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1
group3 = group3#1
zip3 = zip3#1

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)

Induction Base:
zip3#1(gen_:::nil11_14(+(1, 0)), gen_:::nil11_14(0), gen_:::nil11_14(0))

Induction Step:
zip3#1(gen_:::nil11_14(+(1, +(n50127_14, 1))), gen_:::nil11_14(+(n50127_14, 1)), gen_:::nil11_14(+(n50127_14, 1))) ->_R^Omega(0)
zip3#2(gen_:::nil11_14(+(n50127_14, 1)), gen_:::nil11_14(+(n50127_14, 1)), hole_tuple#34_14, gen_:::nil11_14(+(1, n50127_14))) ->_R^Omega(0)
zip3#3(gen_:::nil11_14(+(1, n50127_14)), hole_tuple#34_14, gen_:::nil11_14(+(1, n50127_14)), hole_tuple#34_14, gen_:::nil11_14(n50127_14)) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), zip3(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14))) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14))) ->_IH
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), *13_14)

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:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
group3#1, GROUP3, GROUP3#1, ZIP3, ZIP3#1, group3

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1
group3 = group3#1

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
group3#1(gen_:::nil11_14(+(1, *(3, n79551_14)))) -> *13_14, rt in Omega(0)

Induction Base:
group3#1(gen_:::nil11_14(+(1, *(3, 0))))

Induction Step:
group3#1(gen_:::nil11_14(+(1, *(3, +(n79551_14, 1))))) ->_R^Omega(0)
group3#2(gen_:::nil11_14(+(3, *(3, n79551_14))), hole_tuple#34_14) ->_R^Omega(0)
group3#3(gen_:::nil11_14(+(2, *(3, n79551_14))), hole_tuple#34_14, hole_tuple#34_14) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), group3(gen_:::nil11_14(+(1, *(3, n79551_14))))) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), group3#1(gen_:::nil11_14(+(1, *(3, n79551_14))))) ->_IH
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), *13_14)

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

(22)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n79551_14)))) -> *13_14, rt in Omega(0)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
group3, GROUP3, GROUP3#1, ZIP3, ZIP3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1
group3 = group3#1

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)

Induction Base:
group3(gen_:::nil11_14(*(3, 0)))

Induction Step:
group3(gen_:::nil11_14(*(3, +(n107637_14, 1)))) ->_R^Omega(0)
group3#1(gen_:::nil11_14(*(3, +(n107637_14, 1)))) ->_R^Omega(0)
group3#2(gen_:::nil11_14(+(2, *(3, n107637_14))), hole_tuple#34_14) ->_R^Omega(0)
group3#3(gen_:::nil11_14(+(1, *(3, n107637_14))), hole_tuple#34_14, hole_tuple#34_14) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), group3(gen_:::nil11_14(*(3, n107637_14)))) ->_IH
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), *13_14)

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

(24)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n79551_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
group3#1, GROUP3, GROUP3#1, ZIP3, ZIP3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1
group3 = group3#1

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)

Induction Base:
group3#1(gen_:::nil11_14(+(1, *(3, 0))))

Induction Step:
group3#1(gen_:::nil11_14(+(1, *(3, +(n136840_14, 1))))) ->_R^Omega(0)
group3#2(gen_:::nil11_14(+(3, *(3, n136840_14))), hole_tuple#34_14) ->_R^Omega(0)
group3#3(gen_:::nil11_14(+(2, *(3, n136840_14))), hole_tuple#34_14, hole_tuple#34_14) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), group3(gen_:::nil11_14(+(1, *(3, n136840_14))))) ->_R^Omega(0)
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), group3#1(gen_:::nil11_14(+(1, *(3, n136840_14))))) ->_IH
::(tuple#3(hole_tuple#34_14, hole_tuple#34_14, hole_tuple#34_14), *13_14)

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

(26)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
ZIP3#1, GROUP3, GROUP3#1, ZIP3

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ZIP3#1(gen_:::nil11_14(+(1, n169562_14)), gen_:::nil11_14(n169562_14), gen_:::nil11_14(n169562_14)) -> *13_14, rt in Omega(n169562_14)

Induction Base:
ZIP3#1(gen_:::nil11_14(+(1, 0)), gen_:::nil11_14(0), gen_:::nil11_14(0))

Induction Step:
ZIP3#1(gen_:::nil11_14(+(1, +(n169562_14, 1))), gen_:::nil11_14(+(n169562_14, 1)), gen_:::nil11_14(+(n169562_14, 1))) ->_R^Omega(1)
c8(ZIP3#2(gen_:::nil11_14(+(n169562_14, 1)), gen_:::nil11_14(+(n169562_14, 1)), hole_tuple#34_14, gen_:::nil11_14(+(1, n169562_14)))) ->_R^Omega(1)
c8(c10(ZIP3#3(gen_:::nil11_14(+(1, n169562_14)), hole_tuple#34_14, gen_:::nil11_14(+(1, n169562_14)), hole_tuple#34_14, gen_:::nil11_14(n169562_14)))) ->_R^Omega(1)
c8(c10(c12(ZIP3(gen_:::nil11_14(+(1, n169562_14)), gen_:::nil11_14(n169562_14), gen_:::nil11_14(n169562_14))))) ->_R^Omega(1)
c8(c10(c12(c7(ZIP3#1(gen_:::nil11_14(+(1, n169562_14)), gen_:::nil11_14(n169562_14), gen_:::nil11_14(n169562_14)))))) ->_IH
c8(c10(c12(c7(*13_14))))

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

(28)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
ZIP3#1, GROUP3, GROUP3#1, ZIP3

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1

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

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

(31)
BOUNDS(n^1, INF)

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

(32)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)
ZIP3#1(gen_:::nil11_14(+(1, n169562_14)), gen_:::nil11_14(n169562_14), gen_:::nil11_14(n169562_14)) -> *13_14, rt in Omega(n169562_14)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
ZIP3, GROUP3, GROUP3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ZIP3(gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14)) -> *13_14, rt in Omega(n176008_14)

Induction Base:
ZIP3(gen_:::nil11_14(0), gen_:::nil11_14(0), gen_:::nil11_14(0))

Induction Step:
ZIP3(gen_:::nil11_14(+(n176008_14, 1)), gen_:::nil11_14(+(n176008_14, 1)), gen_:::nil11_14(+(n176008_14, 1))) ->_R^Omega(1)
c7(ZIP3#1(gen_:::nil11_14(+(n176008_14, 1)), gen_:::nil11_14(+(n176008_14, 1)), gen_:::nil11_14(+(n176008_14, 1)))) ->_R^Omega(1)
c7(c8(ZIP3#2(gen_:::nil11_14(+(1, n176008_14)), gen_:::nil11_14(+(1, n176008_14)), hole_tuple#34_14, gen_:::nil11_14(n176008_14)))) ->_R^Omega(1)
c7(c8(c10(ZIP3#3(gen_:::nil11_14(+(1, n176008_14)), hole_tuple#34_14, gen_:::nil11_14(n176008_14), hole_tuple#34_14, gen_:::nil11_14(n176008_14))))) ->_R^Omega(1)
c7(c8(c10(c12(ZIP3(gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14)))))) ->_IH
c7(c8(c10(c12(*13_14))))

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

(34)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)
ZIP3#1(gen_:::nil11_14(+(1, n169562_14)), gen_:::nil11_14(n169562_14), gen_:::nil11_14(n169562_14)) -> *13_14, rt in Omega(n169562_14)
ZIP3(gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14)) -> *13_14, rt in Omega(n176008_14)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
ZIP3#1, GROUP3, GROUP3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1
ZIP3 = ZIP3#1

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ZIP3#1(gen_:::nil11_14(+(1, n183709_14)), gen_:::nil11_14(n183709_14), gen_:::nil11_14(n183709_14)) -> *13_14, rt in Omega(n183709_14)

Induction Base:
ZIP3#1(gen_:::nil11_14(+(1, 0)), gen_:::nil11_14(0), gen_:::nil11_14(0))

Induction Step:
ZIP3#1(gen_:::nil11_14(+(1, +(n183709_14, 1))), gen_:::nil11_14(+(n183709_14, 1)), gen_:::nil11_14(+(n183709_14, 1))) ->_R^Omega(1)
c8(ZIP3#2(gen_:::nil11_14(+(n183709_14, 1)), gen_:::nil11_14(+(n183709_14, 1)), hole_tuple#34_14, gen_:::nil11_14(+(1, n183709_14)))) ->_R^Omega(1)
c8(c10(ZIP3#3(gen_:::nil11_14(+(1, n183709_14)), hole_tuple#34_14, gen_:::nil11_14(+(1, n183709_14)), hole_tuple#34_14, gen_:::nil11_14(n183709_14)))) ->_R^Omega(1)
c8(c10(c12(ZIP3(gen_:::nil11_14(+(1, n183709_14)), gen_:::nil11_14(n183709_14), gen_:::nil11_14(n183709_14))))) ->_R^Omega(1)
c8(c10(c12(c7(ZIP3#1(gen_:::nil11_14(+(1, n183709_14)), gen_:::nil11_14(n183709_14), gen_:::nil11_14(n183709_14)))))) ->_IH
c8(c10(c12(c7(*13_14))))

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

(36)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)
ZIP3#1(gen_:::nil11_14(+(1, n183709_14)), gen_:::nil11_14(n183709_14), gen_:::nil11_14(n183709_14)) -> *13_14, rt in Omega(n183709_14)
ZIP3(gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14)) -> *13_14, rt in Omega(n176008_14)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
GROUP3#1, GROUP3

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GROUP3#1(gen_:::nil11_14(+(1, *(3, n192579_14)))) -> *13_14, rt in Omega(n192579_14)

Induction Base:
GROUP3#1(gen_:::nil11_14(+(1, *(3, 0))))

Induction Step:
GROUP3#1(gen_:::nil11_14(+(1, *(3, +(n192579_14, 1))))) ->_R^Omega(1)
c1(GROUP3#2(gen_:::nil11_14(+(3, *(3, n192579_14))), hole_tuple#34_14)) ->_R^Omega(1)
c1(c3(GROUP3#3(gen_:::nil11_14(+(2, *(3, n192579_14))), hole_tuple#34_14, hole_tuple#34_14))) ->_R^Omega(1)
c1(c3(c5(GROUP3(gen_:::nil11_14(+(1, *(3, n192579_14))))))) ->_R^Omega(1)
c1(c3(c5(c(GROUP3#1(gen_:::nil11_14(+(1, *(3, n192579_14)))))))) ->_IH
c1(c3(c5(c(*13_14))))

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

(38)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)
ZIP3#1(gen_:::nil11_14(+(1, n183709_14)), gen_:::nil11_14(n183709_14), gen_:::nil11_14(n183709_14)) -> *13_14, rt in Omega(n183709_14)
ZIP3(gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14)) -> *13_14, rt in Omega(n176008_14)
GROUP3#1(gen_:::nil11_14(+(1, *(3, n192579_14)))) -> *13_14, rt in Omega(n192579_14)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
GROUP3

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GROUP3(gen_:::nil11_14(*(3, n199239_14))) -> *13_14, rt in Omega(n199239_14)

Induction Base:
GROUP3(gen_:::nil11_14(*(3, 0)))

Induction Step:
GROUP3(gen_:::nil11_14(*(3, +(n199239_14, 1)))) ->_R^Omega(1)
c(GROUP3#1(gen_:::nil11_14(*(3, +(n199239_14, 1))))) ->_R^Omega(1)
c(c1(GROUP3#2(gen_:::nil11_14(+(2, *(3, n199239_14))), hole_tuple#34_14))) ->_R^Omega(1)
c(c1(c3(GROUP3#3(gen_:::nil11_14(+(1, *(3, n199239_14))), hole_tuple#34_14, hole_tuple#34_14)))) ->_R^Omega(1)
c(c1(c3(c5(GROUP3(gen_:::nil11_14(*(3, n199239_14))))))) ->_IH
c(c1(c3(c5(*13_14))))

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

(40)
Obligation:
Innermost TRS:
Rules:
GROUP3(z0) -> c(GROUP3#1(z0))
GROUP3#1(::(z0, z1)) -> c1(GROUP3#2(z1, z0))
GROUP3#1(nil) -> c2
GROUP3#2(::(z0, z1), z2) -> c3(GROUP3#3(z1, z2, z0))
GROUP3#2(nil, z0) -> c4
GROUP3#3(::(z0, z1), z2, z3) -> c5(GROUP3(z1))
GROUP3#3(nil, z0, z1) -> c6
ZIP3(z0, z1, z2) -> c7(ZIP3#1(z0, z1, z2))
ZIP3#1(::(z0, z1), z2, z3) -> c8(ZIP3#2(z2, z3, z0, z1))
ZIP3#1(nil, z0, z1) -> c9
ZIP3#2(::(z0, z1), z2, z3, z4) -> c10(ZIP3#3(z2, z3, z4, z0, z1))
ZIP3#2(nil, z0, z1, z2) -> c11
ZIP3#3(::(z0, z1), z2, z3, z4, z5) -> c12(ZIP3(z3, z5, z1))
ZIP3#3(nil, z0, z1, z2, z3) -> c13
group3(z0) -> group3#1(z0)
group3#1(::(z0, z1)) -> group3#2(z1, z0)
group3#1(nil) -> nil
group3#2(::(z0, z1), z2) -> group3#3(z1, z2, z0)
group3#2(nil, z0) -> nil
group3#3(::(z0, z1), z2, z3) -> ::(tuple#3(z2, z3, z0), group3(z1))
group3#3(nil, z0, z1) -> nil
zip3(z0, z1, z2) -> zip3#1(z0, z1, z2)
zip3#1(::(z0, z1), z2, z3) -> zip3#2(z2, z3, z0, z1)
zip3#1(nil, z0, z1) -> nil
zip3#2(::(z0, z1), z2, z3, z4) -> zip3#3(z2, z3, z4, z0, z1)
zip3#2(nil, z0, z1, z2) -> nil
zip3#3(::(z0, z1), z2, z3, z4, z5) -> ::(tuple#3(z2, z4, z0), zip3(z3, z5, z1))
zip3#3(nil, z0, z1, z2, z3) -> nil

Types:
GROUP3 :: :::nil -> c
c :: c1:c2 -> c
GROUP3#1 :: :::nil -> c1:c2
:: :: tuple#3 -> :::nil -> :::nil
c1 :: c3:c4 -> c1:c2
GROUP3#2 :: :::nil -> tuple#3 -> c3:c4
nil :: :::nil
c2 :: c1:c2
c3 :: c5:c6 -> c3:c4
GROUP3#3 :: :::nil -> tuple#3 -> tuple#3 -> c5:c6
c4 :: c3:c4
c5 :: c -> c5:c6
c6 :: c5:c6
ZIP3 :: :::nil -> :::nil -> :::nil -> c7
c7 :: c8:c9 -> c7
ZIP3#1 :: :::nil -> :::nil -> :::nil -> c8:c9
c8 :: c10:c11 -> c8:c9
ZIP3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> c10:c11
c9 :: c8:c9
c10 :: c12:c13 -> c10:c11
ZIP3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> c12:c13
c11 :: c10:c11
c12 :: c7 -> c12:c13
c13 :: c12:c13
group3 :: :::nil -> :::nil
group3#1 :: :::nil -> :::nil
group3#2 :: :::nil -> tuple#3 -> :::nil
group3#3 :: :::nil -> tuple#3 -> tuple#3 -> :::nil
tuple#3 :: tuple#3 -> tuple#3 -> tuple#3 -> tuple#3
zip3 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#1 :: :::nil -> :::nil -> :::nil -> :::nil
zip3#2 :: :::nil -> :::nil -> tuple#3 -> :::nil -> :::nil
zip3#3 :: :::nil -> tuple#3 -> :::nil -> tuple#3 -> :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_tuple#34_14 :: tuple#3
hole_c3:c45_14 :: c3:c4
hole_c5:c66_14 :: c5:c6
hole_c77_14 :: c7
hole_c8:c98_14 :: c8:c9
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_:::nil11_14 :: Nat -> :::nil
gen_tuple#312_14 :: Nat -> tuple#3


Lemmas:
zip3#1(gen_:::nil11_14(+(1, n50127_14)), gen_:::nil11_14(n50127_14), gen_:::nil11_14(n50127_14)) -> *13_14, rt in Omega(0)
zip3(gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14), gen_:::nil11_14(n24386_14)) -> *13_14, rt in Omega(0)
group3#1(gen_:::nil11_14(+(1, *(3, n136840_14)))) -> *13_14, rt in Omega(0)
group3(gen_:::nil11_14(*(3, n107637_14))) -> *13_14, rt in Omega(0)
ZIP3#1(gen_:::nil11_14(+(1, n183709_14)), gen_:::nil11_14(n183709_14), gen_:::nil11_14(n183709_14)) -> *13_14, rt in Omega(n183709_14)
ZIP3(gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14), gen_:::nil11_14(n176008_14)) -> *13_14, rt in Omega(n176008_14)
GROUP3#1(gen_:::nil11_14(+(1, *(3, n192579_14)))) -> *13_14, rt in Omega(n192579_14)
GROUP3(gen_:::nil11_14(*(3, n199239_14))) -> *13_14, rt in Omega(n199239_14)


Generator Equations:
gen_:::nil11_14(0) <=> nil
gen_:::nil11_14(+(x, 1)) <=> ::(hole_tuple#34_14, gen_:::nil11_14(x))
gen_tuple#312_14(0) <=> hole_tuple#34_14
gen_tuple#312_14(+(x, 1)) <=> tuple#3(hole_tuple#34_14, hole_tuple#34_14, gen_tuple#312_14(x))


The following defined symbols remain to be analysed:
GROUP3#1

They will be analysed ascendingly in the following order:
GROUP3 = GROUP3#1

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

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GROUP3#1(gen_:::nil11_14(+(1, *(3, n207110_14)))) -> *13_14, rt in Omega(n207110_14)

Induction Base:
GROUP3#1(gen_:::nil11_14(+(1, *(3, 0))))

Induction Step:
GROUP3#1(gen_:::nil11_14(+(1, *(3, +(n207110_14, 1))))) ->_R^Omega(1)
c1(GROUP3#2(gen_:::nil11_14(+(3, *(3, n207110_14))), hole_tuple#34_14)) ->_R^Omega(1)
c1(c3(GROUP3#3(gen_:::nil11_14(+(2, *(3, n207110_14))), hole_tuple#34_14, hole_tuple#34_14))) ->_R^Omega(1)
c1(c3(c5(GROUP3(gen_:::nil11_14(+(1, *(3, n207110_14))))))) ->_R^Omega(1)
c1(c3(c5(c(GROUP3#1(gen_:::nil11_14(+(1, *(3, n207110_14)))))))) ->_IH
c1(c3(c5(c(*13_14))))

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

(42)
BOUNDS(1, INF)