Problem Transformed CSR 04 Ex1 Zan97 GM

YES(?,O(n^1))

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

Strict Trs:
  { a__g(X) -> a__h(X)
  , a__g(X) -> g(X)
  , a__h(X) -> h(X)
  , a__h(d()) -> a__g(c())
  , a__c() -> d()
  , a__c() -> c()
  , mark(d()) -> d()
  , mark(c()) -> a__c()
  , mark(g(X)) -> a__g(X)
  , mark(h(X)) -> a__h(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(a__g) = {}, Uargs(a__h) = {}, Uargs(mark) = {},
  Uargs(g) = {}, Uargs(h) = {}

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

  [a__g](x1) = [2] x1 + [2]
                           
  [a__h](x1) = [2] x1 + [1]
                           
      [a__c] = [3]
                  
         [d] = [2]
                  
         [c] = [1]
                  
  [mark](x1) = [3] x1 + [2]
                           
     [g](x1) = [1] x1 + [1]
                           
     [h](x1) = [1] x1 + [0]

This order satisfies following ordering constraints

     [a__g(X)] = [2] X + [2]
               > [2] X + [1]
               = [a__h(X)]  
                            
     [a__g(X)] = [2] X + [2]
               > [1] X + [1]
               = [g(X)]     
                            
     [a__h(X)] = [2] X + [1]
               > [1] X + [0]
               = [h(X)]     
                            
   [a__h(d())] = [5]        
               > [4]        
               = [a__g(c())]
                            
      [a__c()] = [3]        
               > [2]        
               = [d()]      
                            
      [a__c()] = [3]        
               > [1]        
               = [c()]      
                            
   [mark(d())] = [8]        
               > [2]        
               = [d()]      
                            
   [mark(c())] = [5]        
               > [3]        
               = [a__c()]   
                            
  [mark(g(X))] = [3] X + [5]
               > [2] X + [2]
               = [a__g(X)]  
                            
  [mark(h(X))] = [3] X + [2]
               > [2] X + [1]
               = [a__h(X)]  
                            

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

MAYBE

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

Strict Trs:
  { a__g(X) -> a__h(X)
  , a__c() -> d()
  , a__h(d()) -> a__g(c())
  , mark(g(X)) -> a__g(X)
  , mark(h(X)) -> a__h(X)
  , mark(c()) -> a__c()
  , mark(d()) -> d()
  , a__g(X) -> g(X)
  , a__h(X) -> h(X)
  , a__c() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

YES(?,PRIMREC)

We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).

Strict Trs:
  { a__g(X) -> a__h(X)
  , a__c() -> d()
  , a__h(d()) -> a__g(c())
  , mark(g(X)) -> a__g(X)
  , mark(h(X)) -> a__h(X)
  , mark(c()) -> a__c()
  , mark(d()) -> d()
  , a__g(X) -> g(X)
  , a__h(X) -> h(X)
  , a__c() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

The input was oriented with the instance of'multiset path orders'
as induced by the precedence

 a__g > a__h, a__g > g, a__h > h, a__c > d, a__c > c, d > a__g,
 d > c, mark > a__g, mark > a__h, a__c ~ mark .

Hurray, we answered YES(?,PRIMREC)

MAYBE

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

Strict Trs:
  { a__g(X) -> a__h(X)
  , a__c() -> d()
  , a__h(d()) -> a__g(c())
  , mark(g(X)) -> a__g(X)
  , mark(h(X)) -> a__h(X)
  , mark(c()) -> a__c()
  , mark(d()) -> d()
  , a__g(X) -> g(X)
  , a__h(X) -> h(X)
  , a__c() -> c() }
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:
  { a__g(X) -> a__h(X)
  , a__c() -> d()
  , a__h(d()) -> a__g(c())
  , mark(g(X)) -> a__g(X)
  , mark(h(X)) -> a__h(X)
  , mark(c()) -> a__c()
  , mark(d()) -> d()
  , a__g(X) -> g(X)
  , a__h(X) -> h(X)
  , a__c() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..