Problem HirokawaMiddeldorp 04 t011

YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { g(f(x), y) -> f(h(x, y))
  , h(x, y) -> g(x, f(y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(g) = {}, Uargs(f) = {1}, Uargs(h) = {}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

  [g](x1, x2) = [2] x1 + [0]
                            
      [f](x1) = [1] x1 + [2]
                            
  [h](x1, x2) = [2] x1 + [1]

This order satisfies following ordering constraints

  [g(f(x), y)] = [2] x + [4] 
               > [2] x + [3] 
               = [f(h(x, y))]
                             
     [h(x, y)] = [2] x + [1] 
               > [2] x + [0] 
               = [g(x, f(y))]
                             

Hurray, we answered YES(?,O(n^1))

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { g(f(x), y) -> f(h(x, y))
  , h(x, y) -> g(x, f(y)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { g(f(x), y) -> f(h(x, y))
  , h(x, y) -> g(x, f(y)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { g(f(x), y) -> f(h(x, y))
  , h(x, y) -> g(x, f(y)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { g(f(x), y) -> f(h(x, y))
  , h(x, y) -> g(x, f(y)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..