We consider the following Problem:
Strict Trs:
{ app(nil(), YS) -> YS
, app(cons(X), YS) -> cons(X)
, from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, nil()) -> nil()
, zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
, prefix(L) -> cons(nil())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ app(nil(), YS) -> YS
, app(cons(X), YS) -> cons(X)
, from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, nil()) -> nil()
, zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
, prefix(L) -> cons(nil())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, nil()) -> nil()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(app) = {}, Uargs(cons) = {1}, Uargs(from) = {},
Uargs(zWadr) = {}, Uargs(prefix) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
app(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [1 0] [1]
nil() = [0]
[0]
cons(x1) = [1 0] x1 + [0]
[1 0] [0]
from(x1) = [1 0] x1 + [2]
[1 0] [0]
zWadr(x1, x2) = [0 1] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
prefix(x1) = [0 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ app(nil(), YS) -> YS
, app(cons(X), YS) -> cons(X)
, zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
, prefix(L) -> cons(nil())}
Weak Trs:
{ from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, 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: {prefix(L) -> cons(nil())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(app) = {}, Uargs(cons) = {1}, Uargs(from) = {},
Uargs(zWadr) = {}, Uargs(prefix) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
app(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [1 0] [1]
nil() = [0]
[0]
cons(x1) = [1 0] x1 + [0]
[1 0] [0]
from(x1) = [1 0] x1 + [0]
[1 0] [0]
zWadr(x1, x2) = [0 1] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
prefix(x1) = [0 0] x1 + [2]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ app(nil(), YS) -> YS
, app(cons(X), YS) -> cons(X)
, zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))}
Weak Trs:
{ prefix(L) -> cons(nil())
, from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, 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: {app(nil(), YS) -> YS}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(app) = {}, Uargs(cons) = {1}, Uargs(from) = {},
Uargs(zWadr) = {}, Uargs(prefix) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
app(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
nil() = [0]
[0]
cons(x1) = [1 0] x1 + [0]
[1 0] [0]
from(x1) = [1 0] x1 + [0]
[1 0] [0]
zWadr(x1, x2) = [0 1] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
prefix(x1) = [0 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ app(cons(X), YS) -> cons(X)
, zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))}
Weak Trs:
{ app(nil(), YS) -> YS
, prefix(L) -> cons(nil())
, from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, 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: {zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(app) = {}, Uargs(cons) = {1}, Uargs(from) = {},
Uargs(zWadr) = {}, Uargs(prefix) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
app(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
nil() = [0]
[0]
cons(x1) = [1 0] x1 + [0]
[1 0] [0]
from(x1) = [1 0] x1 + [0]
[1 0] [0]
zWadr(x1, x2) = [0 1] x1 + [0 0] x2 + [3]
[0 1] [0 0] [1]
prefix(x1) = [0 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {app(cons(X), YS) -> cons(X)}
Weak Trs:
{ zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
, app(nil(), YS) -> YS
, prefix(L) -> cons(nil())
, from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, 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: {app(cons(X), YS) -> cons(X)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(app) = {}, Uargs(cons) = {1}, Uargs(from) = {},
Uargs(zWadr) = {}, Uargs(prefix) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
app(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[1 0] [0 1] [1]
nil() = [0]
[0]
cons(x1) = [1 0] x1 + [0]
[0 0] [1]
from(x1) = [1 0] x1 + [0]
[0 0] [2]
zWadr(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
prefix(x1) = [0 0] x1 + [0]
[0 0] [2]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ app(cons(X), YS) -> cons(X)
, zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
, app(nil(), YS) -> YS
, prefix(L) -> cons(nil())
, from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ app(cons(X), YS) -> cons(X)
, zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
, app(nil(), YS) -> YS
, prefix(L) -> cons(nil())
, from(X) -> cons(X)
, zWadr(nil(), YS) -> nil()
, zWadr(XS, nil()) -> 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))