Problem AG01 3.7

Tool CaT

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputAG01 3.7

stdout:

YES(?,O(n^1))

Problem:
 half(0()) -> 0()
 half(s(s(x))) -> s(half(x))
 log(s(0())) -> 0()
 log(s(s(x))) -> s(log(s(half(x))))

Proof:
 Complexity Transformation Processor:
  strict:
   half(0()) -> 0()
   half(s(s(x))) -> s(half(x))
   log(s(0())) -> 0()
   log(s(s(x))) -> s(log(s(half(x))))
  weak:
   
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [log](x0) = 1x0,
    
    [s](x0) = x0,
    
    [half](x0) = x0,
    
    [0] = 6
   orientation:
    half(0()) = 6 >= 6 = 0()
    
    half(s(s(x))) = x >= x = s(half(x))
    
    log(s(0())) = 7 >= 6 = 0()
    
    log(s(s(x))) = 1x >= 1x = s(log(s(half(x))))
   problem:
    strict:
     half(0()) -> 0()
     half(s(s(x))) -> s(half(x))
     log(s(s(x))) -> s(log(s(half(x))))
    weak:
     log(s(0())) -> 0()
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [log](x0) = x0,
     
     [s](x0) = 1x0,
     
     [half](x0) = x0,
     
     [0] = 2
    orientation:
     half(0()) = 2 >= 2 = 0()
     
     half(s(s(x))) = 2x >= 1x = s(half(x))
     
     log(s(s(x))) = 2x >= 2x = s(log(s(half(x))))
     
     log(s(0())) = 3 >= 2 = 0()
    problem:
     strict:
      half(0()) -> 0()
      log(s(s(x))) -> s(log(s(half(x))))
     weak:
      half(s(s(x))) -> s(half(x))
      log(s(0())) -> 0()
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
                  [0  -&]  
      [log](x0) = [1  -&]x0,
      
                [0 0]  
      [s](x0) = [2 0]x0,
      
                   [0  -&]  
      [half](x0) = [0  -&]x0,
      
            [0]
      [0] = [0]
     orientation:
                  [0]    [0]      
      half(0()) = [0] >= [0] = 0()
      
                     [2 0]     [1  -&]                      
      log(s(s(x))) = [3 1]x >= [2  -&]x = s(log(s(half(x))))
      
                      [2 0]     [0  -&]              
      half(s(s(x))) = [2 0]x >= [2  -&]x = s(half(x))
      
                    [0]    [0]      
      log(s(0())) = [1] >= [0] = 0()
     problem:
      strict:
       half(0()) -> 0()
      weak:
       log(s(s(x))) -> s(log(s(half(x))))
       half(s(s(x))) -> s(half(x))
       log(s(0())) -> 0()
     Arctic Interpretation Processor:
      dimension: 2
      interpretation:
                   [2 0]  
       [log](x0) = [1 1]x0,
       
                 [0 3]  
       [s](x0) = [0 2]x0,
       
                    [1  3 ]  
       [half](x0) = [-& 0 ]x0,
       
             [0 ]
       [0] = [-&]
      orientation:
                   [1 ]    [0 ]      
       half(0()) = [-&] >= [-&] = 0()
       
                      [5 7]     [5 7]                      
       log(s(s(x))) = [4 6]x >= [4 6]x = s(log(s(half(x))))
       
                       [5 7]     [1 3]              
       half(s(s(x))) = [2 4]x >= [1 3]x = s(half(x))
       
                     [2]    [0 ]      
       log(s(0())) = [1] >= [-&] = 0()
      problem:
       strict:
        
       weak:
        half(0()) -> 0()
        log(s(s(x))) -> s(log(s(half(x))))
        half(s(s(x))) -> s(half(x))
        log(s(0())) -> 0()
      Qed

Tool IRC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputAG01 3.7

stdout:

YES(?,O(n^1))

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputAG01 3.7

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}

Proof Output:    
  'matrix-interpretation of dimension 1' proved the best result:
  
  Details:
  --------
    'matrix-interpretation of dimension 1' succeeded with the following output:
     'matrix-interpretation of dimension 1'
     --------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  half(0()) -> 0()
          , half(s(s(x))) -> s(half(x))
          , log(s(0())) -> 0()
          , log(s(s(x))) -> s(log(s(half(x))))}
     
     Proof Output:    
       The following argument positions are usable:
         Uargs(half) = {}, Uargs(s) = {1}, Uargs(log) = {1}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        half(x1) = [1] x1 + [1]
        0() = [0]
        s(x1) = [1] x1 + [2]
        log(x1) = [3] x1 + [0]

Tool RC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputAG01 3.7

stdout:

YES(?,O(n^1))

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputAG01 3.7

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}

Proof Output:    
  'matrix-interpretation of dimension 1' proved the best result:
  
  Details:
  --------
    'matrix-interpretation of dimension 1' succeeded with the following output:
     'matrix-interpretation of dimension 1'
     --------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  half(0()) -> 0()
          , half(s(s(x))) -> s(half(x))
          , log(s(0())) -> 0()
          , log(s(s(x))) -> s(log(s(half(x))))}
     
     Proof Output:    
       The following argument positions are usable:
         Uargs(half) = {1}, Uargs(s) = {1}, Uargs(log) = {1}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        half(x1) = [1] x1 + [1]
        0() = [0]
        s(x1) = [1] x1 + [3]
        log(x1) = [2] x1 + [0]

Tool pair1rc

Execution TimeUnknown
Answer
YES(?,O(n^2))
InputAG01 3.7

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^2))

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' proved the goal fastest:
     
     We have the following constructor-restricted (at most 2 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      half(x1) = [1 0 1] x1 + [0]
                 [0 1 0]      [0]
                 [0 0 1]      [0]
      0() = [2]
            [0]
            [2]
      s(x1) = [1 1 0] x1 + [0]
              [0 0 2]      [1]
              [0 0 1]      [0]
      log(x1) = [2 0 0] x1 + [0]
                [0 1 0]      [0]
                [0 0 1]      [0]
  

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

Tool pair2rc

Execution TimeUnknown
Answer
YES(?,O(n^2))
InputAG01 3.7

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^2))

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' proved the goal fastest:
     
     We have the following constructor-restricted (at most 2 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      half(x1) = [1 0 1] x1 + [0]
                 [0 1 0]      [0]
                 [0 0 1]      [0]
      0() = [2]
            [0]
            [2]
      s(x1) = [1 1 0] x1 + [0]
              [0 0 2]      [1]
              [0 0 1]      [0]
      log(x1) = [2 0 0] x1 + [0]
                [0 1 0]      [0]
                [0 0 1]      [0]
  

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

Tool pair3irc

Execution TimeUnknown
Answer
YES(?,O(n^2))
InputAG01 3.7

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^2))

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(half) = {}, Uargs(s) = {1}, Uargs(log) = {1}
     We have the following constructor-restricted (at most 2 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      half(x1) = [1 0 1] x1 + [0]
                 [0 1 0]      [0]
                 [0 0 1]      [0]
      0() = [0]
            [1]
            [2]
      s(x1) = [1 1 0] x1 + [0]
              [0 0 2]      [1]
              [0 0 1]      [0]
      log(x1) = [2 0 0] x1 + [0]
                [0 0 2]      [1]
                [0 0 1]      [0]
  

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

Tool pair3rc

Execution TimeUnknown
Answer
YES(?,O(n^2))
InputAG01 3.7

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^2))

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' proved the goal fastest:
     
     We have the following constructor-restricted (at most 2 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      half(x1) = [1 0 1] x1 + [0]
                 [0 1 0]      [0]
                 [0 0 1]      [0]
      0() = [2]
            [0]
            [2]
      s(x1) = [1 1 0] x1 + [0]
              [0 0 2]      [1]
              [0 0 1]      [0]
      log(x1) = [2 0 0] x1 + [0]
                [0 1 0]      [0]
                [0 0 1]      [0]
  

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

Tool rc

Execution TimeUnknown
Answer
YES(?,O(n^2))
InputAG01 3.7

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^2))

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  'Fastest' proved the goal fastest:
  
  'Sequentially' proved the goal fastest:
  
  'Fastest' succeeded:
  
  'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' proved the goal fastest:
  
  We have the following constructor-restricted (at most 2 in the main diagonals) matrix interpretation:
  Interpretation Functions:
   half(x1) = [1 0 1] x1 + [0]
              [0 1 0]      [0]
              [0 0 1]      [0]
   0() = [2]
         [0]
         [2]
   s(x1) = [1 1 0] x1 + [0]
           [0 0 2]      [1]
           [0 0 1]      [0]
   log(x1) = [2 0 0] x1 + [0]
             [0 1 0]      [0]
             [0 0 1]      [0]

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

Tool tup3irc

Execution Time5.532ms
Answer
YES(?,O(n^2))
InputAG01 3.7

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^2))

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  half(0()) -> 0()
     , half(s(s(x))) -> s(half(x))
     , log(s(0())) -> 0()
     , log(s(s(x))) -> s(log(s(half(x))))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(half) = {}, Uargs(s) = {1}, Uargs(log) = {1}
     We have the following constructor-restricted (at most 2 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      half(x1) = [1 0 1] x1 + [0]
                 [0 1 0]      [0]
                 [0 0 1]      [0]
      0() = [0]
            [1]
            [2]
      s(x1) = [1 1 0] x1 + [0]
              [0 0 2]      [1]
              [0 0 1]      [0]
      log(x1) = [2 0 0] x1 + [0]
                [0 0 2]      [1]
                [0 0 1]      [0]
  

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