Problem Waldmann 06 jwmatchb1

YES(?,O(n^3))

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

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

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

                [1 3 0]      [3]
      [h](x1) = [0 0 1] x1 + [0]
                [0 3 0]      [0]
                                
                [1 0 0]      [1 0 0]      [3]
  [f](x1, x2) = [0 1 1] x1 + [0 0 0] x2 + [3]
                [0 0 0]      [0 1 1]      [3]
                                             
                [0]
          [a] = [0]
                [0]

This order satisfies following ordering constraints

  [h(f(x, y))] = [1 3 3]     [1 0 0]     [15]
                 [0 0 0] x + [0 1 1] y + [3] 
                 [0 3 3]     [0 0 0]     [9] 
               > [1 3 3]     [1 0 0]     [12]
                 [0 0 0] x + [0 1 1] y + [3] 
                 [0 3 3]     [0 0 0]     [9] 
               = [f(y, f(h(h(x)), a()))]     
                                             

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

MAYBE

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

Strict Trs: { h(f(x, y)) -> f(y, f(h(h(x)), a())) }
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: { h(f(x, y)) -> f(y, f(h(h(x)), a())) }
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: { h(f(x, y)) -> f(y, f(h(h(x)), a())) }
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: { h(f(x, y)) -> f(y, f(h(h(x)), a())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..