We consider the following Problem:
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, appendAll(@l) -> appendAll#1(@l)
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll#1(nil()) -> nil()
, appendAll2(@l) -> appendAll2#1(@l)
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll2#1(nil()) -> nil()
, appendAll3(@l) -> appendAll3#1(@l)
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))
, appendAll3#1(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, appendAll(@l) -> appendAll#1(@l)
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll#1(nil()) -> nil()
, appendAll2(@l) -> appendAll2#1(@l)
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll2#1(nil()) -> nil()
, appendAll3(@l) -> appendAll3#1(@l)
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))
, appendAll3#1(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(append) = {1, 2}, Uargs(append#1) = {}, Uargs(::) = {2},
Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
append(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
append#1(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 1] [0 1] [1]
nil() = [0]
[0]
appendAll(x1) = [0 1] x1 + [0]
[0 0] [0]
appendAll#1(x1) = [0 1] x1 + [0]
[0 0] [1]
appendAll2(x1) = [0 1] x1 + [0]
[0 0] [0]
appendAll2#1(x1) = [0 1] x1 + [0]
[0 0] [1]
appendAll3(x1) = [0 1] x1 + [0]
[0 0] [0]
appendAll3#1(x1) = [0 1] x1 + [0]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, appendAll(@l) -> appendAll#1(@l)
, appendAll#1(nil()) -> nil()
, appendAll2(@l) -> appendAll2#1(@l)
, appendAll2#1(nil()) -> nil()
, appendAll3(@l) -> appendAll3#1(@l)
, appendAll3#1(nil()) -> nil()}
Weak Trs:
{ append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ appendAll#1(nil()) -> nil()
, appendAll2#1(nil()) -> nil()
, appendAll3#1(nil()) -> nil()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(append) = {1, 2}, Uargs(append#1) = {}, Uargs(::) = {2},
Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
append(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
append#1(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
::(x1, x2) = [0 1] x1 + [1 0] x2 + [0]
[1 0] [0 1] [1]
nil() = [0]
[0]
appendAll(x1) = [0 1] x1 + [0]
[0 0] [0]
appendAll#1(x1) = [0 1] x1 + [1]
[0 0] [1]
appendAll2(x1) = [1 0] x1 + [0]
[0 0] [0]
appendAll2#1(x1) = [1 0] x1 + [1]
[0 0] [1]
appendAll3(x1) = [0 1] x1 + [0]
[0 0] [0]
appendAll3#1(x1) = [0 1] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, appendAll(@l) -> appendAll#1(@l)
, appendAll2(@l) -> appendAll2#1(@l)
, appendAll3(@l) -> appendAll3#1(@l)}
Weak Trs:
{ appendAll#1(nil()) -> nil()
, appendAll2#1(nil()) -> nil()
, appendAll3#1(nil()) -> nil()
, append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {appendAll3(@l) -> appendAll3#1(@l)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(append) = {1, 2}, Uargs(append#1) = {}, Uargs(::) = {2},
Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
append(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
append#1(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
::(x1, x2) = [0 1] x1 + [1 0] x2 + [0]
[1 0] [0 1] [1]
nil() = [0]
[0]
appendAll(x1) = [0 1] x1 + [0]
[0 0] [0]
appendAll#1(x1) = [0 1] x1 + [1]
[0 0] [1]
appendAll2(x1) = [1 0] x1 + [0]
[0 0] [0]
appendAll2#1(x1) = [1 0] x1 + [1]
[0 0] [1]
appendAll3(x1) = [0 1] x1 + [2]
[0 0] [2]
appendAll3#1(x1) = [0 1] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, appendAll(@l) -> appendAll#1(@l)
, appendAll2(@l) -> appendAll2#1(@l)}
Weak Trs:
{ appendAll3(@l) -> appendAll3#1(@l)
, appendAll#1(nil()) -> nil()
, appendAll2#1(nil()) -> nil()
, appendAll3#1(nil()) -> nil()
, append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(append) = {1, 2}, Uargs(append#1) = {}, Uargs(::) = {2},
Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
append(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
append#1(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
::(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
nil() = [0]
[0]
appendAll(x1) = [1 0] x1 + [0]
[0 0] [0]
appendAll#1(x1) = [1 0] x1 + [1]
[0 0] [1]
appendAll2(x1) = [1 0] x1 + [0]
[0 0] [0]
appendAll2#1(x1) = [1 0] x1 + [1]
[0 0] [1]
appendAll3(x1) = [1 0] x1 + [1]
[0 0] [2]
appendAll3#1(x1) = [1 0] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, appendAll(@l) -> appendAll#1(@l)
, appendAll2(@l) -> appendAll2#1(@l)}
Weak Trs:
{ append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, appendAll3(@l) -> appendAll3#1(@l)
, appendAll#1(nil()) -> nil()
, appendAll2#1(nil()) -> nil()
, appendAll3#1(nil()) -> nil()
, append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {appendAll(@l) -> appendAll#1(@l)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(append) = {1, 2}, Uargs(append#1) = {}, Uargs(::) = {2},
Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
append(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
append#1(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [1 1] [1]
::(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [1 0] [0]
nil() = [0]
[0]
appendAll(x1) = [1 0] x1 + [1]
[0 0] [1]
appendAll#1(x1) = [1 0] x1 + [0]
[0 0] [1]
appendAll2(x1) = [1 0] x1 + [0]
[0 0] [0]
appendAll2#1(x1) = [1 0] x1 + [2]
[0 0] [1]
appendAll3(x1) = [1 0] x1 + [2]
[0 0] [2]
appendAll3#1(x1) = [1 0] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, appendAll2(@l) -> appendAll2#1(@l)}
Weak Trs:
{ appendAll(@l) -> appendAll#1(@l)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, appendAll3(@l) -> appendAll3#1(@l)
, appendAll#1(nil()) -> nil()
, appendAll2#1(nil()) -> nil()
, appendAll3#1(nil()) -> nil()
, append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {appendAll2(@l) -> appendAll2#1(@l)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(append) = {1, 2}, Uargs(append#1) = {}, Uargs(::) = {2},
Uargs(appendAll) = {}, Uargs(appendAll#1) = {},
Uargs(appendAll2) = {}, Uargs(appendAll2#1) = {},
Uargs(appendAll3) = {}, Uargs(appendAll3#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
append(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
append#1(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [1 1] [0]
::(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [1 0] [0]
nil() = [3]
[1]
appendAll(x1) = [1 0] x1 + [0]
[1 1] [2]
appendAll#1(x1) = [1 0] x1 + [0]
[1 1] [1]
appendAll2(x1) = [1 0] x1 + [1]
[0 0] [2]
appendAll2#1(x1) = [1 0] x1 + [0]
[0 0] [1]
appendAll3(x1) = [1 0] x1 + [0]
[0 0] [2]
appendAll3#1(x1) = [1 0] x1 + [0]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {append(@l1, @l2) -> append#1(@l1, @l2)}
Weak Trs:
{ appendAll2(@l) -> appendAll2#1(@l)
, appendAll(@l) -> appendAll#1(@l)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, appendAll3(@l) -> appendAll3#1(@l)
, appendAll#1(nil()) -> nil()
, appendAll2#1(nil()) -> nil()
, appendAll3#1(nil()) -> nil()
, append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs: {append(@l1, @l2) -> append#1(@l1, @l2)}
Weak Trs:
{ appendAll2(@l) -> appendAll2#1(@l)
, appendAll(@l) -> appendAll#1(@l)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, appendAll3(@l) -> appendAll3#1(@l)
, appendAll#1(nil()) -> nil()
, appendAll2#1(nil()) -> nil()
, appendAll3#1(nil()) -> nil()
, append#1(nil(), @l2) -> @l2
, appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
, appendAll2#1(::(@l1, @ls)) ->
append(appendAll(@l1), appendAll2(@ls))
, appendAll3#1(::(@l1, @ls)) ->
append(appendAll2(@l1), appendAll3(@ls))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ append_0(3, 3) -> 1
, append_0(3, 4) -> 1
, append_0(3, 5) -> 5
, append_0(3, 5) -> 6
, append_0(3, 5) -> 12
, append_0(4, 3) -> 1
, append_0(4, 4) -> 1
, append_0(4, 5) -> 5
, append_0(4, 5) -> 6
, append_0(4, 5) -> 12
, append_0(5, 7) -> 7
, append_0(5, 7) -> 8
, append_0(5, 7) -> 16
, append_0(5, 7) -> 18
, append_0(7, 9) -> 9
, append_0(7, 9) -> 10
, append_0(7, 9) -> 17
, append_0(7, 9) -> 20
, append_0(7, 9) -> 21
, append_0(7, 9) -> 22
, append_1(3, 3) -> 11
, append_1(3, 4) -> 11
, append_1(3, 5) -> 12
, append_1(3, 13) -> 13
, append_1(4, 3) -> 11
, append_1(4, 4) -> 11
, append_1(4, 5) -> 12
, append_1(4, 13) -> 13
, append_1(12, 7) -> 16
, append_1(13, 14) -> 7
, append_1(13, 14) -> 8
, append_1(13, 14) -> 14
, append_1(13, 14) -> 16
, append_1(13, 14) -> 18
, append_1(13, 14) -> 19
, append_1(14, 15) -> 9
, append_1(14, 15) -> 10
, append_1(14, 15) -> 15
, append_1(14, 15) -> 17
, append_1(14, 15) -> 20
, append_1(14, 15) -> 21
, append_1(14, 15) -> 22
, append_1(16, 9) -> 17
, append_2(12, 7) -> 18
, append_2(13, 14) -> 19
, append_2(16, 9) -> 20
, append_2(18, 9) -> 20
, append_2(19, 9) -> 21
, append_2(19, 15) -> 21
, append_3(18, 9) -> 22
, append_3(19, 9) -> 22
, append_3(19, 15) -> 22
, append#1_0(3, 3) -> 2
, append#1_0(3, 4) -> 2
, append#1_0(4, 3) -> 2
, append#1_0(4, 4) -> 2
, append#1_1(3, 3) -> 1
, append#1_1(3, 4) -> 1
, append#1_1(3, 5) -> 5
, append#1_1(3, 5) -> 6
, append#1_1(3, 5) -> 12
, append#1_1(4, 3) -> 1
, append#1_1(4, 4) -> 1
, append#1_1(4, 5) -> 5
, append#1_1(4, 5) -> 6
, append#1_1(4, 5) -> 12
, append#1_1(5, 7) -> 7
, append#1_1(5, 7) -> 8
, append#1_1(5, 7) -> 16
, append#1_1(5, 7) -> 18
, append#1_1(7, 9) -> 9
, append#1_1(7, 9) -> 10
, append#1_1(7, 9) -> 17
, append#1_1(7, 9) -> 20
, append#1_1(7, 9) -> 21
, append#1_1(7, 9) -> 22
, append#1_2(3, 3) -> 11
, append#1_2(3, 4) -> 11
, append#1_2(3, 5) -> 12
, append#1_2(3, 13) -> 13
, append#1_2(4, 3) -> 11
, append#1_2(4, 4) -> 11
, append#1_2(4, 5) -> 12
, append#1_2(4, 13) -> 13
, append#1_2(12, 7) -> 16
, append#1_2(13, 14) -> 7
, append#1_2(13, 14) -> 8
, append#1_2(13, 14) -> 14
, append#1_2(13, 14) -> 16
, append#1_2(13, 14) -> 18
, append#1_2(13, 14) -> 19
, append#1_2(14, 15) -> 9
, append#1_2(14, 15) -> 10
, append#1_2(14, 15) -> 15
, append#1_2(14, 15) -> 17
, append#1_2(14, 15) -> 20
, append#1_2(14, 15) -> 21
, append#1_2(14, 15) -> 22
, append#1_2(16, 9) -> 17
, append#1_3(12, 7) -> 18
, append#1_3(13, 14) -> 19
, append#1_3(16, 9) -> 20
, append#1_3(18, 9) -> 20
, append#1_3(19, 9) -> 21
, append#1_3(19, 15) -> 21
, append#1_4(18, 9) -> 22
, append#1_4(19, 9) -> 22
, append#1_4(19, 15) -> 22
, ::_0(3, 1) -> 2
, ::_0(3, 3) -> 1
, ::_0(3, 3) -> 2
, ::_0(3, 3) -> 3
, ::_0(3, 3) -> 11
, ::_0(3, 4) -> 1
, ::_0(3, 4) -> 2
, ::_0(3, 4) -> 3
, ::_0(3, 4) -> 11
, ::_0(4, 1) -> 2
, ::_0(4, 3) -> 1
, ::_0(4, 3) -> 2
, ::_0(4, 3) -> 3
, ::_0(4, 3) -> 11
, ::_0(4, 4) -> 1
, ::_0(4, 4) -> 2
, ::_0(4, 4) -> 3
, ::_0(4, 4) -> 11
, ::_1(3, 11) -> 1
, ::_1(3, 11) -> 11
, ::_1(3, 12) -> 5
, ::_1(3, 12) -> 6
, ::_1(3, 12) -> 12
, ::_1(3, 13) -> 13
, ::_1(3, 16) -> 7
, ::_1(3, 16) -> 8
, ::_1(3, 16) -> 16
, ::_1(3, 16) -> 18
, ::_1(3, 17) -> 9
, ::_1(3, 17) -> 10
, ::_1(3, 17) -> 17
, ::_1(3, 17) -> 20
, ::_1(3, 17) -> 21
, ::_1(3, 17) -> 22
, ::_1(4, 11) -> 1
, ::_1(4, 11) -> 11
, ::_1(4, 12) -> 5
, ::_1(4, 12) -> 6
, ::_1(4, 12) -> 12
, ::_1(4, 13) -> 13
, ::_1(4, 16) -> 7
, ::_1(4, 16) -> 8
, ::_1(4, 16) -> 16
, ::_1(4, 16) -> 18
, ::_1(4, 17) -> 9
, ::_1(4, 17) -> 10
, ::_1(4, 17) -> 17
, ::_1(4, 17) -> 20
, ::_1(4, 17) -> 21
, ::_1(4, 17) -> 22
, ::_2(3, 18) -> 16
, ::_2(3, 18) -> 18
, ::_2(3, 19) -> 7
, ::_2(3, 19) -> 8
, ::_2(3, 19) -> 14
, ::_2(3, 19) -> 16
, ::_2(3, 19) -> 18
, ::_2(3, 19) -> 19
, ::_2(3, 20) -> 17
, ::_2(3, 20) -> 20
, ::_2(3, 20) -> 22
, ::_2(3, 21) -> 9
, ::_2(3, 21) -> 10
, ::_2(3, 21) -> 15
, ::_2(3, 21) -> 17
, ::_2(3, 21) -> 20
, ::_2(3, 21) -> 21
, ::_2(3, 21) -> 22
, ::_2(4, 18) -> 16
, ::_2(4, 18) -> 18
, ::_2(4, 19) -> 7
, ::_2(4, 19) -> 8
, ::_2(4, 19) -> 14
, ::_2(4, 19) -> 16
, ::_2(4, 19) -> 18
, ::_2(4, 19) -> 19
, ::_2(4, 20) -> 17
, ::_2(4, 20) -> 20
, ::_2(4, 20) -> 22
, ::_2(4, 21) -> 9
, ::_2(4, 21) -> 10
, ::_2(4, 21) -> 15
, ::_2(4, 21) -> 17
, ::_2(4, 21) -> 20
, ::_2(4, 21) -> 21
, ::_2(4, 21) -> 22
, ::_3(3, 22) -> 20
, ::_3(3, 22) -> 21
, ::_3(3, 22) -> 22
, ::_3(4, 22) -> 20
, ::_3(4, 22) -> 21
, ::_3(4, 22) -> 22
, nil_0() -> 1
, nil_0() -> 2
, nil_0() -> 4
, nil_0() -> 5
, nil_0() -> 6
, nil_0() -> 7
, nil_0() -> 8
, nil_0() -> 9
, nil_0() -> 10
, nil_0() -> 11
, nil_0() -> 12
, nil_0() -> 16
, nil_0() -> 17
, nil_0() -> 18
, nil_0() -> 20
, nil_0() -> 21
, nil_0() -> 22
, nil_1() -> 7
, nil_1() -> 8
, nil_1() -> 9
, nil_1() -> 10
, nil_1() -> 13
, nil_1() -> 14
, nil_1() -> 15
, nil_1() -> 16
, nil_1() -> 17
, nil_1() -> 18
, nil_1() -> 19
, nil_1() -> 20
, nil_1() -> 21
, nil_1() -> 22
, appendAll_0(3) -> 5
, appendAll_0(3) -> 6
, appendAll_0(3) -> 12
, appendAll_0(4) -> 5
, appendAll_0(4) -> 6
, appendAll_0(4) -> 12
, appendAll_1(3) -> 13
, appendAll_1(4) -> 13
, appendAll#1_0(3) -> 5
, appendAll#1_0(3) -> 6
, appendAll#1_0(3) -> 12
, appendAll#1_0(4) -> 5
, appendAll#1_0(4) -> 6
, appendAll#1_0(4) -> 12
, appendAll#1_1(3) -> 13
, appendAll#1_1(4) -> 13
, appendAll2_0(3) -> 7
, appendAll2_0(3) -> 8
, appendAll2_0(3) -> 16
, appendAll2_0(3) -> 18
, appendAll2_0(4) -> 7
, appendAll2_0(4) -> 8
, appendAll2_0(4) -> 16
, appendAll2_0(4) -> 18
, appendAll2_1(3) -> 7
, appendAll2_1(3) -> 8
, appendAll2_1(3) -> 14
, appendAll2_1(3) -> 16
, appendAll2_1(3) -> 18
, appendAll2_1(3) -> 19
, appendAll2_1(4) -> 7
, appendAll2_1(4) -> 8
, appendAll2_1(4) -> 14
, appendAll2_1(4) -> 16
, appendAll2_1(4) -> 18
, appendAll2_1(4) -> 19
, appendAll2#1_0(3) -> 7
, appendAll2#1_0(3) -> 8
, appendAll2#1_0(3) -> 16
, appendAll2#1_0(3) -> 18
, appendAll2#1_0(4) -> 7
, appendAll2#1_0(4) -> 8
, appendAll2#1_0(4) -> 16
, appendAll2#1_0(4) -> 18
, appendAll2#1_1(3) -> 7
, appendAll2#1_1(3) -> 8
, appendAll2#1_1(3) -> 14
, appendAll2#1_1(3) -> 16
, appendAll2#1_1(3) -> 18
, appendAll2#1_1(3) -> 19
, appendAll2#1_1(4) -> 7
, appendAll2#1_1(4) -> 8
, appendAll2#1_1(4) -> 14
, appendAll2#1_1(4) -> 16
, appendAll2#1_1(4) -> 18
, appendAll2#1_1(4) -> 19
, appendAll3_0(3) -> 9
, appendAll3_0(3) -> 10
, appendAll3_0(3) -> 17
, appendAll3_0(3) -> 20
, appendAll3_0(3) -> 21
, appendAll3_0(3) -> 22
, appendAll3_0(4) -> 9
, appendAll3_0(4) -> 10
, appendAll3_0(4) -> 17
, appendAll3_0(4) -> 20
, appendAll3_0(4) -> 21
, appendAll3_0(4) -> 22
, appendAll3_1(3) -> 9
, appendAll3_1(3) -> 10
, appendAll3_1(3) -> 15
, appendAll3_1(3) -> 17
, appendAll3_1(3) -> 20
, appendAll3_1(3) -> 21
, appendAll3_1(3) -> 22
, appendAll3_1(4) -> 9
, appendAll3_1(4) -> 10
, appendAll3_1(4) -> 15
, appendAll3_1(4) -> 17
, appendAll3_1(4) -> 20
, appendAll3_1(4) -> 21
, appendAll3_1(4) -> 22
, appendAll3#1_0(3) -> 9
, appendAll3#1_0(3) -> 10
, appendAll3#1_0(3) -> 17
, appendAll3#1_0(3) -> 20
, appendAll3#1_0(3) -> 21
, appendAll3#1_0(3) -> 22
, appendAll3#1_0(4) -> 9
, appendAll3#1_0(4) -> 10
, appendAll3#1_0(4) -> 17
, appendAll3#1_0(4) -> 20
, appendAll3#1_0(4) -> 21
, appendAll3#1_0(4) -> 22
, appendAll3#1_1(3) -> 9
, appendAll3#1_1(3) -> 10
, appendAll3#1_1(3) -> 15
, appendAll3#1_1(3) -> 17
, appendAll3#1_1(3) -> 20
, appendAll3#1_1(3) -> 21
, appendAll3#1_1(3) -> 22
, appendAll3#1_1(4) -> 9
, appendAll3#1_1(4) -> 10
, appendAll3#1_1(4) -> 15
, appendAll3#1_1(4) -> 17
, appendAll3#1_1(4) -> 20
, appendAll3#1_1(4) -> 21
, appendAll3#1_1(4) -> 22}
Hurray, we answered YES(?,O(n^1))