We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ a__f(X1, X2, X3) -> f(X1, X2, X3)
, a__f(a(), X, X) -> a__f(X, a__b(), b())
, a__b() -> a()
, a__b() -> b()
, mark(a()) -> a()
, mark(b()) -> a__b()
, mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The input is overlay and right-linear. Switching to innermost
rewriting.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ a__f(X1, X2, X3) -> f(X1, X2, X3)
, a__f(a(), X, X) -> a__f(X, a__b(), b())
, a__b() -> a()
, a__b() -> b()
, mark(a()) -> a()
, mark(b()) -> a__b()
, mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ a__f(X1, X2, X3) -> f(X1, X2, X3)
, mark(a()) -> a()
, mark(b()) -> a__b()
, mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(a__f) = {2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[a__f](x1, x2, x3) = [1] x2 + [3] x3 + [5]
[a] = [0]
[a__b] = [0]
[b] = [0]
[mark](x1) = [3] x1 + [1]
[f](x1, x2, x3) = [1] x2 + [1] x3 + [4]
The order satisfies the following ordering constraints:
[a__f(X1, X2, X3)] = [1] X2 + [3] X3 + [5]
> [1] X2 + [1] X3 + [4]
= [f(X1, X2, X3)]
[a__f(a(), X, X)] = [4] X + [5]
>= [5]
= [a__f(X, a__b(), b())]
[a__b()] = [0]
>= [0]
= [a()]
[a__b()] = [0]
>= [0]
= [b()]
[mark(a())] = [1]
> [0]
= [a()]
[mark(b())] = [1]
> [0]
= [a__b()]
[mark(f(X1, X2, X3))] = [3] X2 + [3] X3 + [13]
> [3] X2 + [3] X3 + [6]
= [a__f(X1, mark(X2), X3)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ a__f(a(), X, X) -> a__f(X, a__b(), b())
, a__b() -> a()
, a__b() -> b() }
Weak Trs:
{ a__f(X1, X2, X3) -> f(X1, X2, X3)
, mark(a()) -> a()
, mark(b()) -> a__b()
, mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ a__f(a(), X, X) -> a__f(X, a__b(), b())
, a__b() -> a()
, a__b() -> b() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(a__f) = {2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[a__f](x1, x2, x3) = [4] x1 + [1] x2 + [4] x3 + [1]
[a] = [2]
[a__b] = [3]
[b] = [1]
[mark](x1) = [4] x1 + [1]
[f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
The order satisfies the following ordering constraints:
[a__f(X1, X2, X3)] = [4] X1 + [1] X2 + [4] X3 + [1]
>= [1] X1 + [1] X2 + [1] X3 + [1]
= [f(X1, X2, X3)]
[a__f(a(), X, X)] = [5] X + [9]
> [4] X + [8]
= [a__f(X, a__b(), b())]
[a__b()] = [3]
> [2]
= [a()]
[a__b()] = [3]
> [1]
= [b()]
[mark(a())] = [9]
> [2]
= [a()]
[mark(b())] = [5]
> [3]
= [a__b()]
[mark(f(X1, X2, X3))] = [4] X1 + [4] X2 + [4] X3 + [5]
> [4] X1 + [4] X2 + [4] X3 + [2]
= [a__f(X1, mark(X2), X3)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ a__f(X1, X2, X3) -> f(X1, X2, X3)
, a__f(a(), X, X) -> a__f(X, a__b(), b())
, a__b() -> a()
, a__b() -> b()
, mark(a()) -> a()
, mark(b()) -> a__b()
, mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))