MAYBE
* Step 1: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            add(0(),X) -> X
            add(s(X),Y) -> s(add(X,Y))
            from(X) -> cons(X,from(s(X)))
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,fst(X,Z))
            len(cons(X,Z)) -> s(len(Z))
            len(nil()) -> 0()
        - Signature:
            {add/2,from/1,fst/2,len/1} / {0/0,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,from,fst,len} and constructors {0,cons,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
               p(0) = [3]                  
             p(add) = [8] x1 + [4] x2 + [0]
            p(cons) = [1] x2 + [2]         
            p(from) = [5] x1 + [9]         
             p(fst) = [8] x1 + [5] x2 + [3]
             p(len) = [5] x1 + [9]         
             p(nil) = [2]                  
               p(s) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
                   add(0(),X) = [4] X + [24]        
                              > [1] X + [0]         
                              = X                   
          
                   fst(0(),Z) = [5] Z + [27]        
                              > [2]                 
                              = nil()               
          
          fst(s(X),cons(Y,Z)) = [8] X + [5] Z + [13]
                              > [8] X + [5] Z + [5] 
                              = cons(Y,fst(X,Z))    
          
               len(cons(X,Z)) = [5] Z + [19]        
                              > [5] Z + [9]         
                              = s(len(Z))           
          
                   len(nil()) = [19]                
                              > [3]                 
                              = 0()                 
          
          
          Following rules are (at-least) weakly oriented:
          add(s(X),Y) =  [8] X + [4] Y + [0]
                      >= [8] X + [4] Y + [0]
                      =  s(add(X,Y))        
          
              from(X) =  [5] X + [9]        
                      >= [5] X + [11]       
                      =  cons(X,from(s(X))) 
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            add(s(X),Y) -> s(add(X,Y))
            from(X) -> cons(X,from(s(X)))
        - Weak TRS:
            add(0(),X) -> X
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,fst(X,Z))
            len(cons(X,Z)) -> s(len(Z))
            len(nil()) -> 0()
        - Signature:
            {add/2,from/1,fst/2,len/1} / {0/0,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,from,fst,len} and constructors {0,cons,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
               p(0) = [2]                  
             p(add) = [2] x1 + [4] x2 + [1]
            p(cons) = [1] x2 + [1]         
            p(from) = [0]                  
             p(fst) = [4] x1 + [0]         
             p(len) = [1] x1 + [1]         
             p(nil) = [2]                  
               p(s) = [1] x1 + [1]         
          
          Following rules are strictly oriented:
          add(s(X),Y) = [2] X + [4] Y + [3]
                      > [2] X + [4] Y + [2]
                      = s(add(X,Y))        
          
          
          Following rules are (at-least) weakly oriented:
                   add(0(),X) =  [4] X + [5]       
                              >= [1] X + [0]       
                              =  X                 
          
                      from(X) =  [0]               
                              >= [1]               
                              =  cons(X,from(s(X)))
          
                   fst(0(),Z) =  [8]               
                              >= [2]               
                              =  nil()             
          
          fst(s(X),cons(Y,Z)) =  [4] X + [4]       
                              >= [4] X + [1]       
                              =  cons(Y,fst(X,Z))  
          
               len(cons(X,Z)) =  [1] Z + [2]       
                              >= [1] Z + [2]       
                              =  s(len(Z))         
          
                   len(nil()) =  [3]               
                              >= [2]               
                              =  0()               
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          from(X) -> cons(X,from(s(X)))
      - Weak TRS:
          add(0(),X) -> X
          add(s(X),Y) -> s(add(X,Y))
          fst(0(),Z) -> nil()
          fst(s(X),cons(Y,Z)) -> cons(Y,fst(X,Z))
          len(cons(X,Z)) -> s(len(Z))
          len(nil()) -> 0()
      - Signature:
          {add/2,from/1,fst/2,len/1} / {0/0,cons/2,nil/0,s/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {add,from,fst,len} and constructors {0,cons,nil,s}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE