We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, top(rec(up(x))) -> top(check(rec(x)))
, top(sent(up(x))) -> top(check(rec(x)))
, top(no(up(x))) -> top(check(rec(x)))
, check(rec(x)) -> rec(check(x))
, check(sent(x)) -> sent(check(x))
, check(no(x)) -> no(x)
, check(no(x)) -> no(check(x))
, check(up(x)) -> up(check(x)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Arguments of following rules are not normal-forms:
{ top(rec(up(x))) -> top(check(rec(x)))
, top(sent(up(x))) -> top(check(rec(x)))
, top(no(up(x))) -> top(check(rec(x))) }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, check(rec(x)) -> rec(check(x))
, check(sent(x)) -> sent(check(x))
, check(no(x)) -> no(x)
, check(no(x)) -> no(check(x))
, check(up(x)) -> up(check(x)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ rec^#(rec(x)) -> c_1(sent^#(rec(x)))
, rec^#(sent(x)) -> c_2(sent^#(rec(x)))
, rec^#(no(x)) -> c_3(sent^#(rec(x)))
, rec^#(bot()) -> c_4(sent^#(bot()))
, rec^#(up(x)) -> c_5(rec^#(x))
, sent^#(up(x)) -> c_6(sent^#(x))
, no^#(up(x)) -> c_7(no^#(x))
, check^#(rec(x)) -> c_8(rec^#(check(x)))
, check^#(sent(x)) -> c_9(sent^#(check(x)))
, check^#(no(x)) -> c_10(no^#(x))
, check^#(no(x)) -> c_11(no^#(check(x)))
, check^#(up(x)) -> c_12(check^#(x)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ rec^#(rec(x)) -> c_1(sent^#(rec(x)))
, rec^#(sent(x)) -> c_2(sent^#(rec(x)))
, rec^#(no(x)) -> c_3(sent^#(rec(x)))
, rec^#(bot()) -> c_4(sent^#(bot()))
, rec^#(up(x)) -> c_5(rec^#(x))
, sent^#(up(x)) -> c_6(sent^#(x))
, no^#(up(x)) -> c_7(no^#(x))
, check^#(rec(x)) -> c_8(rec^#(check(x)))
, check^#(sent(x)) -> c_9(sent^#(check(x)))
, check^#(no(x)) -> c_10(no^#(x))
, check^#(no(x)) -> c_11(no^#(check(x)))
, check^#(up(x)) -> c_12(check^#(x)) }
Strict Trs:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, check(rec(x)) -> rec(check(x))
, check(sent(x)) -> sent(check(x))
, check(no(x)) -> no(x)
, check(no(x)) -> no(check(x))
, check(up(x)) -> up(check(x)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(rec) = {1}, Uargs(sent) = {1}, Uargs(no) = {1},
Uargs(up) = {1}, Uargs(rec^#) = {1}, Uargs(sent^#) = {1},
Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1},
Uargs(c_6) = {1}, Uargs(no^#) = {1}, Uargs(c_7) = {1},
Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1},
Uargs(c_11) = {1}, Uargs(c_12) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[rec](x1) = [2 1] x1 + [1]
[1 2] [2]
[sent](x1) = [2 0] x1 + [0]
[0 2] [2]
[no](x1) = [2 0] x1 + [0]
[0 2] [2]
[bot] = [1]
[2]
[up](x1) = [1 0] x1 + [2]
[0 1] [1]
[check](x1) = [2 1] x1 + [1]
[1 2] [1]
[rec^#](x1) = [2 2] x1 + [0]
[0 0] [0]
[c_1](x1) = [0]
[0]
[sent^#](x1) = [2 0] x1 + [0]
[0 0] [0]
[c_2](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_3](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_4](x1) = [0]
[0]
[c_5](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_6](x1) = [1 0] x1 + [0]
[0 1] [0]
[no^#](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_7](x1) = [1 0] x1 + [0]
[0 1] [0]
[check^#](x1) = [2 2] x1 + [0]
[0 0] [0]
[c_8](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_9](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_10](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_11](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_12](x1) = [1 0] x1 + [0]
[0 1] [0]
The order satisfies the following ordering constraints:
[rec(rec(x))] = [5 4] x + [5]
[4 5] [7]
> [4 2] x + [2]
[2 4] [6]
= [sent(rec(x))]
[rec(sent(x))] = [4 2] x + [3]
[2 4] [6]
> [4 2] x + [2]
[2 4] [6]
= [sent(rec(x))]
[rec(no(x))] = [4 2] x + [3]
[2 4] [6]
> [4 2] x + [2]
[2 4] [6]
= [sent(rec(x))]
[rec(bot())] = [5]
[7]
> [4]
[7]
= [up(sent(bot()))]
[rec(up(x))] = [2 1] x + [6]
[1 2] [6]
> [2 1] x + [3]
[1 2] [3]
= [up(rec(x))]
[sent(up(x))] = [2 0] x + [4]
[0 2] [4]
> [2 0] x + [2]
[0 2] [3]
= [up(sent(x))]
[no(up(x))] = [2 0] x + [4]
[0 2] [4]
> [2 0] x + [2]
[0 2] [3]
= [up(no(x))]
[check(rec(x))] = [5 4] x + [5]
[4 5] [6]
> [5 4] x + [4]
[4 5] [5]
= [rec(check(x))]
[check(sent(x))] = [4 2] x + [3]
[2 4] [5]
> [4 2] x + [2]
[2 4] [4]
= [sent(check(x))]
[check(no(x))] = [4 2] x + [3]
[2 4] [5]
> [2 0] x + [0]
[0 2] [2]
= [no(x)]
[check(no(x))] = [4 2] x + [3]
[2 4] [5]
> [4 2] x + [2]
[2 4] [4]
= [no(check(x))]
[check(up(x))] = [2 1] x + [6]
[1 2] [5]
> [2 1] x + [3]
[1 2] [2]
= [up(check(x))]
[rec^#(rec(x))] = [6 6] x + [6]
[0 0] [0]
> [0]
[0]
= [c_1(sent^#(rec(x)))]
[rec^#(sent(x))] = [4 4] x + [4]
[0 0] [0]
> [4 2] x + [2]
[0 0] [0]
= [c_2(sent^#(rec(x)))]
[rec^#(no(x))] = [4 4] x + [4]
[0 0] [0]
> [4 2] x + [2]
[0 0] [0]
= [c_3(sent^#(rec(x)))]
[rec^#(bot())] = [6]
[0]
> [0]
[0]
= [c_4(sent^#(bot()))]
[rec^#(up(x))] = [2 2] x + [6]
[0 0] [0]
> [2 2] x + [0]
[0 0] [0]
= [c_5(rec^#(x))]
[sent^#(up(x))] = [2 0] x + [4]
[0 0] [0]
> [2 0] x + [0]
[0 0] [0]
= [c_6(sent^#(x))]
[no^#(up(x))] = [1 0] x + [2]
[0 0] [0]
> [1 0] x + [0]
[0 0] [0]
= [c_7(no^#(x))]
[check^#(rec(x))] = [6 6] x + [6]
[0 0] [0]
> [6 6] x + [4]
[0 0] [0]
= [c_8(rec^#(check(x)))]
[check^#(sent(x))] = [4 4] x + [4]
[0 0] [0]
> [4 2] x + [2]
[0 0] [0]
= [c_9(sent^#(check(x)))]
[check^#(no(x))] = [4 4] x + [4]
[0 0] [0]
> [1 0] x + [0]
[0 0] [0]
= [c_10(no^#(x))]
[check^#(no(x))] = [4 4] x + [4]
[0 0] [0]
> [2 1] x + [1]
[0 0] [0]
= [c_11(no^#(check(x)))]
[check^#(up(x))] = [2 2] x + [6]
[0 0] [0]
> [2 2] x + [0]
[0 0] [0]
= [c_12(check^#(x))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ rec^#(rec(x)) -> c_1(sent^#(rec(x)))
, rec^#(sent(x)) -> c_2(sent^#(rec(x)))
, rec^#(no(x)) -> c_3(sent^#(rec(x)))
, rec^#(bot()) -> c_4(sent^#(bot()))
, rec^#(up(x)) -> c_5(rec^#(x))
, sent^#(up(x)) -> c_6(sent^#(x))
, no^#(up(x)) -> c_7(no^#(x))
, check^#(rec(x)) -> c_8(rec^#(check(x)))
, check^#(sent(x)) -> c_9(sent^#(check(x)))
, check^#(no(x)) -> c_10(no^#(x))
, check^#(no(x)) -> c_11(no^#(check(x)))
, check^#(up(x)) -> c_12(check^#(x)) }
Weak Trs:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, check(rec(x)) -> rec(check(x))
, check(sent(x)) -> sent(check(x))
, check(no(x)) -> no(x)
, check(no(x)) -> no(check(x))
, check(up(x)) -> up(check(x)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ rec^#(rec(x)) -> c_1(sent^#(rec(x)))
, rec^#(sent(x)) -> c_2(sent^#(rec(x)))
, rec^#(no(x)) -> c_3(sent^#(rec(x)))
, rec^#(bot()) -> c_4(sent^#(bot()))
, rec^#(up(x)) -> c_5(rec^#(x))
, sent^#(up(x)) -> c_6(sent^#(x))
, no^#(up(x)) -> c_7(no^#(x))
, check^#(rec(x)) -> c_8(rec^#(check(x)))
, check^#(sent(x)) -> c_9(sent^#(check(x)))
, check^#(no(x)) -> c_10(no^#(x))
, check^#(no(x)) -> c_11(no^#(check(x)))
, check^#(up(x)) -> c_12(check^#(x)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, check(rec(x)) -> rec(check(x))
, check(sent(x)) -> sent(check(x))
, check(no(x)) -> no(x)
, check(no(x)) -> no(check(x))
, check(up(x)) -> up(check(x)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))