We consider the following Problem:
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, f2() -> g1()
, f2() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
Arguments of following rules are not normal-forms:
{ e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)}
All above mentioned rules can be savely removed.
We consider the following Problem:
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, f2() -> g1()
, f2() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ f1() -> g1()
, f1() -> g2()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(e1) = {}, Uargs(e2) = {}, Uargs(e3) = {}, Uargs(e4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f1() = [2]
[0]
g1() = [0]
[0]
g2() = [0]
[0]
f2() = [0]
[0]
h1() = [0]
[0]
h2() = [0]
[0]
e1(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1 1] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
e2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 1] x4 + [0 0] x5 + [0]
[1 0] [0 0] [0 0] [0 0] [1 0] [0]
e3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 1] x7 + [0 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
e4(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 0] x7 + [0 1] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f2() -> g1()
, f2() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)}
Weak Trs:
{ f1() -> g1()
, f1() -> g2()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ f2() -> g1()
, f2() -> g2()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(e1) = {}, Uargs(e2) = {}, Uargs(e3) = {}, Uargs(e4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f1() = [0]
[0]
g1() = [0]
[0]
g2() = [0]
[0]
f2() = [2]
[0]
h1() = [0]
[0]
h2() = [0]
[0]
e1(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1 1] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
e2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 1] x4 + [0 0] x5 + [0]
[1 0] [0 0] [0 0] [0 0] [1 0] [0]
e3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 1] x7 + [0 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
e4(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 1] x7 + [0 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)}
Weak Trs:
{ f2() -> g1()
, f2() -> g2()
, f1() -> g1()
, f1() -> g2()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ g1() -> h1()
, g1() -> h2()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(e1) = {}, Uargs(e2) = {}, Uargs(e3) = {}, Uargs(e4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f1() = [2]
[0]
g1() = [1]
[0]
g2() = [0]
[0]
f2() = [1]
[0]
h1() = [0]
[0]
h2() = [0]
[0]
e1(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1 1] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
e2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 1] x4 + [1 0] x5 + [0]
[1 0] [0 0] [0 0] [1 0] [0 0] [0]
e3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 1] x7 + [0 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
e4(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 1] x7 + [0 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ g2() -> h1()
, g2() -> h2()
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)}
Weak Trs:
{ g1() -> h1()
, g1() -> h2()
, f2() -> g1()
, f2() -> g2()
, f1() -> g1()
, f1() -> g2()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ g2() -> h1()
, g2() -> h2()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(e1) = {}, Uargs(e2) = {}, Uargs(e3) = {}, Uargs(e4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f1() = [2]
[0]
g1() = [0]
[0]
g2() = [2]
[0]
f2() = [2]
[0]
h1() = [0]
[0]
h2() = [0]
[0]
e1(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1 1] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
e2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1 1] x5 + [0]
[1 0] [0 0] [0 0] [1 0] [0 0] [0]
e3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 1] x7 + [0 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
e4(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 0] x7 + [0 1] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)}
Weak Trs:
{ g2() -> h1()
, g2() -> h2()
, g1() -> h1()
, g1() -> h2()
, f2() -> g1()
, f2() -> g2()
, f1() -> g1()
, f1() -> g2()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(e1) = {}, Uargs(e2) = {}, Uargs(e3) = {}, Uargs(e4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f1() = [0]
[0]
g1() = [0]
[0]
g2() = [0]
[0]
f2() = [0]
[0]
h1() = [0]
[0]
h2() = [0]
[0]
e1(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1 1] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
e2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 1] x4 + [0 0] x5 + [0]
[1 0] [0 0] [0 0] [0 0] [1 0] [0]
e3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [0 1] x7 + [1 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [2]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [1 0] [0 0] [0 0] [0 0] [0 0] [0]
e4(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0 0] x4 + [1 1] x5 + [0 0] x6 + [1 1] x7 + [0 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [1 0] [0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)}
Weak Trs:
{ e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, g2() -> h1()
, g2() -> h2()
, g1() -> h1()
, g1() -> h2()
, f2() -> g1()
, f2() -> g2()
, f1() -> g1()
, f1() -> g2()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(e1) = {}, Uargs(e2) = {}, Uargs(e3) = {}, Uargs(e4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f1() = [2]
[0]
g1() = [1]
[0]
g2() = [1]
[0]
f2() = [1]
[0]
h1() = [1]
[0]
h2() = [0]
[0]
e1(x1, x2, x3, x4, x5) = [1 0] x1 + [1 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [0]
[0 0] [1 0] [1 0] [0 0] [0 1] [1]
e2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0 0] x5 + [0]
[1 0] [0 0] [0 0] [0 1] [0 0] [0]
e3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [1 0] x4 + [0 0] x5 + [1 0] x6 + [0 0] x7 + [1 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 1] [1 0] [0 1] [1 0] [0 1] [1 0] [0 1] [1 0] [0 0] [0 0] [0 0] [0]
e4(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [1 0] x4 + [1 0] x5 + [0 0] x6 + [0 0] x7 + [1 0] x8 + [0 0] x9 + [0 0] x10 + [0 0] x11 + [0]
[0 1] [1 0] [0 1] [1 0] [1 0] [0 1] [0 1] [1 0] [0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, g2() -> h1()
, g2() -> h2()
, g1() -> h1()
, g1() -> h2()
, f2() -> g1()
, f2() -> g2()
, f1() -> g1()
, f1() -> g2()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, g2() -> h1()
, g2() -> h2()
, g1() -> h1()
, g1() -> h2()
, f2() -> g1()
, f2() -> g2()
, f1() -> g1()
, f1() -> g2()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))