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
Renamed function symbols to avoid clashes with predefined symbol.
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'
Sliced the following arguments:
::'/0
group3#2'/1
group3#3'/1
group3#3'/2
tuple#3'/0
tuple#3'/1
tuple#3'/2
zip3#2'/2
zip3#3'/1
zip3#3'/3
Runtime Complexity TRS:
The TRS R consists of the following rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Infered types.
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Heuristically decided to analyse the following defined symbols:
group3', group3#1', group3#2', group3#3', zip3', zip3#1', zip3#2', zip3#3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
zip3' = zip3#1'
zip3' = zip3#2'
zip3' = zip3#3'
zip3#1' = zip3#2'
zip3#1' = zip3#3'
zip3#2' = zip3#3'
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
zip3#1', group3', group3#1', group3#2', group3#3', zip3', zip3#2', zip3#3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
zip3' = zip3#1'
zip3' = zip3#2'
zip3' = zip3#3'
zip3#1' = zip3#2'
zip3#1' = zip3#3'
zip3#2' = zip3#3'
Proved the following rewrite lemma:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
Induction Base:
zip3#1'(_gen_::':nil'2(0), _gen_::':nil'2(0), _gen_::':nil'2(0)) →RΩ(1)
nil'
Induction Step:
zip3#1'(_gen_::':nil'2(+(_$n5, 1)), _gen_::':nil'2(+(_$n5, 1)), _gen_::':nil'2(+(_$n5, 1))) →RΩ(1)
zip3#2'(_gen_::':nil'2(+(_$n5, 1)), _gen_::':nil'2(+(_$n5, 1)), _gen_::':nil'2(_$n5)) →RΩ(1)
zip3#3'(_gen_::':nil'2(+(1, _$n5)), _gen_::':nil'2(_$n5), _gen_::':nil'2(_$n5)) →RΩ(1)
::'(zip3'(_gen_::':nil'2(_$n5), _gen_::':nil'2(_$n5), _gen_::':nil'2(_$n5))) →RΩ(1)
::'(zip3#1'(_gen_::':nil'2(_$n5), _gen_::':nil'2(_$n5), _gen_::':nil'2(_$n5))) →IH
::'(_gen_::':nil'2(_$n5))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
zip3#2', group3', group3#1', group3#2', group3#3', zip3', zip3#3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
zip3' = zip3#1'
zip3' = zip3#2'
zip3' = zip3#3'
zip3#1' = zip3#2'
zip3#1' = zip3#3'
zip3#2' = zip3#3'
Could not prove a rewrite lemma for the defined symbol zip3#2'.
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
zip3#3', group3', group3#1', group3#2', group3#3', zip3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
zip3' = zip3#1'
zip3' = zip3#2'
zip3' = zip3#3'
zip3#1' = zip3#2'
zip3#1' = zip3#3'
zip3#2' = zip3#3'
Could not prove a rewrite lemma for the defined symbol zip3#3'.
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
zip3', group3', group3#1', group3#2', group3#3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
zip3' = zip3#1'
zip3' = zip3#2'
zip3' = zip3#3'
zip3#1' = zip3#2'
zip3#1' = zip3#3'
zip3#2' = zip3#3'
Could not prove a rewrite lemma for the defined symbol zip3'.
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
group3#1', group3', group3#2', group3#3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
Proved the following rewrite lemma:
group3#1'(_gen_::':nil'2(*(3, _n2782))) → _gen_::':nil'2(_n2782), rt ∈ Ω(1 + n2782)
Induction Base:
group3#1'(_gen_::':nil'2(*(3, 0))) →RΩ(1)
nil'
Induction Step:
group3#1'(_gen_::':nil'2(*(3, +(_$n2783, 1)))) →RΩ(1)
group3#2'(_gen_::':nil'2(+(2, *(3, _$n2783)))) →RΩ(1)
group3#3'(_gen_::':nil'2(+(1, *(3, _$n2783)))) →RΩ(1)
::'(group3'(_gen_::':nil'2(*(3, _$n2783)))) →RΩ(1)
::'(group3#1'(_gen_::':nil'2(*(3, _$n2783)))) →IH
::'(_gen_::':nil'2(_$n2783))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
group3#1'(_gen_::':nil'2(*(3, _n2782))) → _gen_::':nil'2(_n2782), rt ∈ Ω(1 + n2782)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
group3#2', group3', group3#3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
Could not prove a rewrite lemma for the defined symbol group3#2'.
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
group3#1'(_gen_::':nil'2(*(3, _n2782))) → _gen_::':nil'2(_n2782), rt ∈ Ω(1 + n2782)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
group3#3', group3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
Could not prove a rewrite lemma for the defined symbol group3#3'.
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
group3#1'(_gen_::':nil'2(*(3, _n2782))) → _gen_::':nil'2(_n2782), rt ∈ Ω(1 + n2782)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
The following defined symbols remain to be analysed:
group3'
They will be analysed ascendingly in the following order:
group3' = group3#1'
group3' = group3#2'
group3' = group3#3'
group3#1' = group3#2'
group3#1' = group3#3'
group3#2' = group3#3'
Could not prove a rewrite lemma for the defined symbol group3'.
Rules:
group3'(@l) → group3#1'(@l)
group3#1'(::'(@xs)) → group3#2'(@xs)
group3#1'(nil') → nil'
group3#2'(::'(@ys)) → group3#3'(@ys)
group3#2'(nil') → nil'
group3#3'(::'(@zs)) → ::'(group3'(@zs))
group3#3'(nil') → nil'
zip3'(@l1, @l2, @l3) → zip3#1'(@l1, @l2, @l3)
zip3#1'(::'(@xs), @l2, @l3) → zip3#2'(@l2, @l3, @xs)
zip3#1'(nil', @l2, @l3) → nil'
zip3#2'(::'(@ys), @l3, @xs) → zip3#3'(@l3, @xs, @ys)
zip3#2'(nil', @l3, @xs) → nil'
zip3#3'(::'(@zs), @xs, @ys) → ::'(zip3'(@xs, @ys, @zs))
zip3#3'(nil', @xs, @ys) → nil'
Types:
group3' :: ::':nil' → ::':nil'
group3#1' :: ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
group3#2' :: ::':nil' → ::':nil'
nil' :: ::':nil'
group3#3' :: ::':nil' → ::':nil'
zip3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#1' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#2' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
zip3#3' :: ::':nil' → ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'
Lemmas:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)
group3#1'(_gen_::':nil'2(*(3, _n2782))) → _gen_::':nil'2(_n2782), rt ∈ Ω(1 + n2782)
Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(_gen_::':nil'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
zip3#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(_n4), _gen_::':nil'2(_n4)) → _gen_::':nil'2(_n4), rt ∈ Ω(1 + n4)