We consider the following Problem:
Strict Trs:
{ 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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ 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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [0]
[0 0] [0]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[1 0] [0 0] [0 0] [0]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))}
Weak Trs:
{ group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [0]
[0 0] [0]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[1 0] [0 0] [0 0] [0]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [2]
[0 0] [0 0] [0 0] [2]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))}
Weak Trs:
{ zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [0]
[0 0] [0]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[1 0] [0 0] [0 0] [0]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [2]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [3]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)}
Weak Trs:
{ zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [0]
[0 0] [0]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[1 0] [0 0] [0 0] [0]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [2]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [3]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [2]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)}
Weak Trs:
{ zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [0]
[0 0] [0]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[1 0] [0 0] [0 0] [0]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [2]
zip3#1(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))}
Weak Trs:
{ zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [0]
[0 0] [0]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[1 0] [0 0] [0 0] [1]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)}
Weak Trs:
{ group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {group3(@l) -> group3#1(@l)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [2]
[0 0] [1]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [3]
[1 0] [0 0] [0 0] [0]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [2]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)}
Weak Trs:
{ group3(@l) -> group3#1(@l)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 0] x1 + [1]
[0 0] [2]
group3#1(x1) = [0 0] x1 + [1]
[0 0] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
group3#2(x1, x2) = [0 0] x1 + [0 0] x2 + [3]
[0 0] [0 0] [1]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [2]
[0 0] [0 0] [0 0] [1]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [2]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
zip3#3(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {group3#1(::(@x, @xs)) -> group3#2(@xs, @x)}
Weak Trs:
{ group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3(@l) -> group3#1(@l)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {group3#1(::(@x, @xs)) -> group3#2(@xs, @x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(group3) = {}, Uargs(group3#1) = {}, Uargs(::) = {2},
Uargs(group3#2) = {}, Uargs(group3#3) = {}, Uargs(tuple#3) = {},
Uargs(zip3) = {}, Uargs(zip3#1) = {}, Uargs(zip3#2) = {},
Uargs(zip3#3) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
group3(x1) = [0 1] x1 + [3]
[1 0] [3]
group3#1(x1) = [0 1] x1 + [3]
[1 0] [3]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
group3#2(x1, x2) = [0 1] x1 + [0 0] x2 + [3]
[1 0] [0 0] [3]
nil() = [0]
[0]
group3#3(x1, x2, x3) = [0 1] x1 + [0 0] x2 + [0 0] x3 + [3]
[1 0] [0 0] [0 0] [3]
tuple#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
zip3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1]
[0 0] [0 1] [0 1] [1]
zip3#1(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1]
[0 0] [0 1] [0 1] [1]
zip3#2(x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 1] [0 1] [0 0] [0 0] [0]
zip3#3(x1, x2, x3, x4, x5) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [1]
[0 1] [0 0] [0 0] [0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3(@l) -> group3#1(@l)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3(@l) -> group3#1(@l)
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, group3#1(nil()) -> nil()
, group3#2(nil(), @x) -> nil()
, group3#3(nil(), @x, @y) -> nil()
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))