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

(0) Obligation:

Runtime Complexity TRS:
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

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
group3(::(@x2_0, ::(@y44_0, ::(@z128_0, @zs129_0)))) →⁺ ::(tuple#3(@x2_0, @y44_0, @z128_0), group3(@zs129_0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@zs129_0 / ::(@x2_0, ::(@y44_0, ::(@z128_0, @zs129_0)))].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
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: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
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

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: tuple#3 → :::nil → :::nil
group3#2 :: :::nil → tuple#3 → :::nil
nil :: :::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_:::nil1_0 :: :::nil
hole_tuple#32_0 :: tuple#3
gen_:::nil3_0 :: Nat → :::nil
gen_tuple#34_0 :: Nat → tuple#3

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
group3, group3#1, zip3, zip3#1

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

(8) Obligation:

Innermost TRS:
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

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: tuple#3 → :::nil → :::nil
group3#2 :: :::nil → tuple#3 → :::nil
nil :: :::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_:::nil1_0 :: :::nil
hole_tuple#32_0 :: tuple#3
gen_:::nil3_0 :: Nat → :::nil
gen_tuple#34_0 :: Nat → tuple#3

Generator Equations:
gen_:::nil3_0(0) ⇔ nil
gen_:::nil3_0(+(x, 1)) ⇔ ::(hole_tuple#32_0, gen_:::nil3_0(x))
gen_tuple#34_0(0) ⇔ hole_tuple#32_0
gen_tuple#34_0(+(x, 1)) ⇔ tuple#3(hole_tuple#32_0, hole_tuple#32_0, gen_tuple#34_0(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

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol zip3#1.

(10) Obligation:

Innermost TRS:
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

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: tuple#3 → :::nil → :::nil
group3#2 :: :::nil → tuple#3 → :::nil
nil :: :::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_:::nil1_0 :: :::nil
hole_tuple#32_0 :: tuple#3
gen_:::nil3_0 :: Nat → :::nil
gen_tuple#34_0 :: Nat → tuple#3

Generator Equations:
gen_:::nil3_0(0) ⇔ nil
gen_:::nil3_0(+(x, 1)) ⇔ ::(hole_tuple#32_0, gen_:::nil3_0(x))
gen_tuple#34_0(0) ⇔ hole_tuple#32_0
gen_tuple#34_0(+(x, 1)) ⇔ tuple#3(hole_tuple#32_0, hole_tuple#32_0, gen_tuple#34_0(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

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol zip3.

(12) Obligation:

Innermost TRS:
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

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: tuple#3 → :::nil → :::nil
group3#2 :: :::nil → tuple#3 → :::nil
nil :: :::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_:::nil1_0 :: :::nil
hole_tuple#32_0 :: tuple#3
gen_:::nil3_0 :: Nat → :::nil
gen_tuple#34_0 :: Nat → tuple#3

Generator Equations:
gen_:::nil3_0(0) ⇔ nil
gen_:::nil3_0(+(x, 1)) ⇔ ::(hole_tuple#32_0, gen_:::nil3_0(x))
gen_tuple#34_0(0) ⇔ hole_tuple#32_0
gen_tuple#34_0(+(x, 1)) ⇔ tuple#3(hole_tuple#32_0, hole_tuple#32_0, gen_tuple#34_0(x))

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

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

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol group3#1.

(14) Obligation:

Innermost TRS:
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

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: tuple#3 → :::nil → :::nil
group3#2 :: :::nil → tuple#3 → :::nil
nil :: :::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_:::nil1_0 :: :::nil
hole_tuple#32_0 :: tuple#3
gen_:::nil3_0 :: Nat → :::nil
gen_tuple#34_0 :: Nat → tuple#3

Generator Equations:
gen_:::nil3_0(0) ⇔ nil
gen_:::nil3_0(+(x, 1)) ⇔ ::(hole_tuple#32_0, gen_:::nil3_0(x))
gen_tuple#34_0(0) ⇔ hole_tuple#32_0
gen_tuple#34_0(+(x, 1)) ⇔ tuple#3(hole_tuple#32_0, hole_tuple#32_0, gen_tuple#34_0(x))

The following defined symbols remain to be analysed:
group3

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

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol group3.

(16) Obligation:

Innermost TRS:
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

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: tuple#3 → :::nil → :::nil
group3#2 :: :::nil → tuple#3 → :::nil
nil :: :::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_:::nil1_0 :: :::nil
hole_tuple#32_0 :: tuple#3
gen_:::nil3_0 :: Nat → :::nil
gen_tuple#34_0 :: Nat → tuple#3

Generator Equations:
gen_:::nil3_0(0) ⇔ nil
gen_:::nil3_0(+(x, 1)) ⇔ ::(hole_tuple#32_0, gen_:::nil3_0(x))
gen_tuple#34_0(0) ⇔ hole_tuple#32_0
gen_tuple#34_0(+(x, 1)) ⇔ tuple#3(hole_tuple#32_0, hole_tuple#32_0, gen_tuple#34_0(x))

No more defined symbols left to analyse.