Problem Transformed CSR 04 PEANO nosorts-noand FR

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 PEANO nosorts-noand FR

stdout:

YES(?,O(n^2))

Problem:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
activate(X) -> X

Proof:
Complexity Transformation Processor:
  strict:
   U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
   U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
   plus(N,0()) -> N
   plus(N,s(M)) -> U11(tt(),M,N)
   activate(X) -> X
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [0] = 248,

     [s](x0) = x0 + 51,

     [plus](x0, x1) = x0 + x1 + 70,

     [U12](x0, x1, x2) = x0 + x1 + x2 + 236,

     [activate](x0) = x0 + 4,

     [U11](x0, x1, x2) = x0 + x1 + x2 + 120,

     [tt] = 148
    orientation:
     U11(tt(),M,N) = M + N + 268 >= M + N + 392 = U12(tt(),activate(M),activate(N))

     U12(tt(),M,N) = M + N + 384 >= M + N + 129 = s(plus(activate(N),activate(M)))

     plus(N,0()) = N + 318 >= N = N

     plus(N,s(M)) = M + N + 121 >= M + N + 268 = U11(tt(),M,N)

     activate(X) = X + 4 >= X = X
    problem:
     strict:
      U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
      plus(N,s(M)) -> U11(tt(),M,N)
     weak:
      U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
      plus(N,0()) -> N
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [0] = 0,

       [s](x0) = x0 + 3,

       [plus](x0, x1) = x0 + x1,

       [U12](x0, x1, x2) = x0 + x1 + x2 + 3,

       [activate](x0) = x0,

       [U11](x0, x1, x2) = x0 + x1 + x2 + 10,

       [tt] = 0
      orientation:
       U11(tt(),M,N) = M + N + 10 >= M + N + 3 = U12(tt(),activate(M),activate(N))

       plus(N,s(M)) = M + N + 3 >= M + N + 10 = U11(tt(),M,N)

       U12(tt(),M,N) = M + N + 3 >= M + N + 3 = s(plus(activate(N),activate(M)))

       plus(N,0()) = N >= N = N

       activate(X) = X >= X = X
      problem:
       strict:
        plus(N,s(M)) -> U11(tt(),M,N)
       weak:
        U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
        U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
        plus(N,0()) -> N
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
               [0]
         [0] = [0],

                        [1]
         [s](x0) = x0 + [2],

                               [1 1]
         [plus](x0, x1) = x0 + [0 1]x1,

                             [1 0]     [1 1]          [0]
         [U12](x0, x1, x2) = [0 0]x0 + [0 1]x1 + x2 + [2],


         [activate](x0) = x0,

                             [1 0]     [1 1]          [0]
         [U11](x0, x1, x2) = [0 0]x0 + [0 1]x1 + x2 + [2],

                [1]
         [tt] = [0]
        orientation:
                        [1 1]        [3]    [1 1]        [1]
         plus(N,s(M)) = [0 1]M + N + [2] >= [0 1]M + N + [2] = U11(tt(),M,N)

                         [1 1]        [1]    [1 1]        [1]
         U11(tt(),M,N) = [0 1]M + N + [2] >= [0 1]M + N + [2] = U12(tt(),activate(M),activate(N))

                         [1 1]        [1]    [1 1]        [1]
         U12(tt(),M,N) = [0 1]M + N + [2] >= [0 1]M + N + [2] = s(plus(activate(N),activate(M)))


         plus(N,0()) = N >= N = N


         activate(X) = X >= X = X
        problem:
         strict:

         weak:
          plus(N,s(M)) -> U11(tt(),M,N)
          U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
          U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
          plus(N,0()) -> N
          activate(X) -> X
        Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 PEANO nosorts-noand FR

stdout:

YES(?,O(n^1))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 PEANO nosorts-noand FR

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:
    {  U11(tt(), M, N) -> U12(tt(), activate(M), activate(N))
     , U12(tt(), M, N) -> s(plus(activate(N), activate(M)))
     , plus(N, 0()) -> N
     , plus(N, s(M)) -> U11(tt(), M, N)
     , activate(X) -> X}

Proof Output:
  'wdg' proved the best result:

  Details:
  --------
    'wdg' succeeded with the following output:
     'wdg'
     -----
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  U11(tt(), M, N) -> U12(tt(), activate(M), activate(N))
          , U12(tt(), M, N) -> s(plus(activate(N), activate(M)))
          , plus(N, 0()) -> N
          , plus(N, s(M)) -> U11(tt(), M, N)
          , activate(X) -> X}

     Proof Output:
       Transformation Details:
       -----------------------
         We have computed the following set of weak (innermost) dependency pairs:

           {  1: U11^#(tt(), M, N) ->
                 c_0(U12^#(tt(), activate(M), activate(N)))
            , 2: U12^#(tt(), M, N) -> c_1(plus^#(activate(N), activate(M)))
            , 3: plus^#(N, 0()) -> c_2()
            , 4: plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N))
            , 5: activate^#(X) -> c_4()}

         Following Dependency Graph (modulo SCCs) was computed. (Answers to
         subproofs are indicated to the right.)

           ->{5}                                                       [    YES(?,O(1))     ]

           ->{1,4,2}                                                   [   YES(?,O(n^1))    ]
              |
              `->{3}                                                   [   YES(?,O(n^1))    ]



       Sub-problems:
       -------------
         * Path {1,4,2}: YES(?,O(n^1))
           ---------------------------

           The usable rules for this path are:

             {activate(X) -> X}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(U11) = {}, Uargs(U12) = {}, Uargs(activate) = {},
               Uargs(s) = {}, Uargs(plus) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {1}, Uargs(U12^#) = {2, 3}, Uargs(c_1) = {1},
               Uargs(plus^#) = {1, 2}, Uargs(c_3) = {1}, Uargs(activate^#) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              tt() = [0]
              U12(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              activate(x1) = [1] x1 + [3]
              s(x1) = [1] x1 + [0]
              plus(x1, x2) = [0] x1 + [0] x2 + [0]
              0() = [0]
              U11^#(x1, x2, x3) = [0] x1 + [3] x2 + [3] x3 + [0]
              c_0(x1) = [1] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [3] x2 + [3] x3 + [0]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [3] x1 + [3] x2 + [0]
              c_2() = [0]
              c_3(x1) = [1] x1 + [0]
              activate^#(x1) = [0] x1 + [0]
              c_4() = [0]
           Complexity induced by the adequate RMI: YES(?,O(n^1))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 1'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules:
               {  U11^#(tt(), M, N) -> c_0(U12^#(tt(), activate(M), activate(N)))
                , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N))
                , U12^#(tt(), M, N) -> c_1(plus^#(activate(N), activate(M)))}
             Weak Rules: {activate(X) -> X}

           Proof Output:
             The following argument positions are usable:
               Uargs(activate) = {}, Uargs(s) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {1}, Uargs(U12^#) = {}, Uargs(c_1) = {1},
               Uargs(plus^#) = {}, Uargs(c_3) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              tt() = [0]
              activate(x1) = [1] x1 + [0]
              s(x1) = [1] x1 + [2]
              U11^#(x1, x2, x3) = [0] x1 + [4] x2 + [0] x3 + [5]
              c_0(x1) = [1] x1 + [3]
              U12^#(x1, x2, x3) = [0] x1 + [4] x2 + [0] x3 + [1]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [0] x1 + [4] x2 + [0]
              c_3(x1) = [1] x1 + [1]

         * Path {1,4,2}->{3}: YES(?,O(n^1))
           --------------------------------

           The usable rules for this path are:

             {activate(X) -> X}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(U11) = {}, Uargs(U12) = {}, Uargs(activate) = {},
               Uargs(s) = {}, Uargs(plus) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {1}, Uargs(U12^#) = {2, 3}, Uargs(c_1) = {1},
               Uargs(plus^#) = {1, 2}, Uargs(c_3) = {1}, Uargs(activate^#) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              tt() = [0]
              U12(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              activate(x1) = [3] x1 + [3]
              s(x1) = [0] x1 + [0]
              plus(x1, x2) = [0] x1 + [0] x2 + [0]
              0() = [0]
              U11^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              c_0(x1) = [1] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [3] x2 + [3] x3 + [0]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [3] x1 + [3] x2 + [0]
              c_2() = [0]
              c_3(x1) = [1] x1 + [0]
              activate^#(x1) = [0] x1 + [0]
              c_4() = [0]
           Complexity induced by the adequate RMI: YES(?,O(1))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 1'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules: {plus^#(N, 0()) -> c_2()}
             Weak Rules:
               {  U11^#(tt(), M, N) -> c_0(U12^#(tt(), activate(M), activate(N)))
                , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N))
                , U12^#(tt(), M, N) -> c_1(plus^#(activate(N), activate(M)))
                , activate(X) -> X}

           Proof Output:
             The following argument positions are usable:
               Uargs(activate) = {}, Uargs(s) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {1}, Uargs(U12^#) = {}, Uargs(c_1) = {1},
               Uargs(plus^#) = {}, Uargs(c_3) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              tt() = [0]
              activate(x1) = [1] x1 + [0]
              s(x1) = [1] x1 + [2]
              0() = [2]
              U11^#(x1, x2, x3) = [0] x1 + [2] x2 + [0] x3 + [4]
              c_0(x1) = [1] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [2] x2 + [0] x3 + [4]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [0] x1 + [2] x2 + [4]
              c_2() = [1]
              c_3(x1) = [1] x1 + [4]

         * Path {5}: YES(?,O(1))
           ---------------------

           The usable rules of this path are empty.

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(U11) = {}, Uargs(U12) = {}, Uargs(activate) = {},
               Uargs(s) = {}, Uargs(plus) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {}, Uargs(U12^#) = {}, Uargs(c_1) = {},
               Uargs(plus^#) = {}, Uargs(c_3) = {}, Uargs(activate^#) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              tt() = [0]
              U12(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              activate(x1) = [0] x1 + [0]
              s(x1) = [0] x1 + [0]
              plus(x1, x2) = [0] x1 + [0] x2 + [0]
              0() = [0]
              U11^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              c_0(x1) = [0] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              c_1(x1) = [0] x1 + [0]
              plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
              c_2() = [0]
              c_3(x1) = [0] x1 + [0]
              activate^#(x1) = [0] x1 + [0]
              c_4() = [0]

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 1'
           --------------------------------------
           Answer:           YES(?,O(1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules: {activate^#(X) -> c_4()}
             Weak Rules: {}

           Proof Output:
             The following argument positions are usable:
               Uargs(activate^#) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              activate^#(x1) = [0] x1 + [7]
              c_4() = [0]

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 PEANO nosorts-noand FR

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 PEANO nosorts-noand FR

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  U11(tt(), M, N) -> U12(tt(), activate(M), activate(N))
     , U12(tt(), M, N) -> s(plus(activate(N), activate(M)))
     , plus(N, 0()) -> N
     , plus(N, s(M)) -> U11(tt(), M, N)
     , activate(X) -> X}

Proof Output:
  'wdg' proved the best result:

  Details:
  --------
    'wdg' succeeded with the following output:
     'wdg'
     -----
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  U11(tt(), M, N) -> U12(tt(), activate(M), activate(N))
          , U12(tt(), M, N) -> s(plus(activate(N), activate(M)))
          , plus(N, 0()) -> N
          , plus(N, s(M)) -> U11(tt(), M, N)
          , activate(X) -> X}

     Proof Output:
       Transformation Details:
       -----------------------
         We have computed the following set of weak (innermost) dependency pairs:

           {  1: U11^#(tt(), M, N) ->
                 c_0(U12^#(tt(), activate(M), activate(N)))
            , 2: U12^#(tt(), M, N) -> c_1(plus^#(activate(N), activate(M)))
            , 3: plus^#(N, 0()) -> c_2(N)
            , 4: plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N))
            , 5: activate^#(X) -> c_4(X)}

         Following Dependency Graph (modulo SCCs) was computed. (Answers to
         subproofs are indicated to the right.)

           ->{5}                                                       [    YES(?,O(1))     ]

           ->{1,4,2}                                                   [   YES(?,O(n^1))    ]
              |
              `->{3}                                                   [   YES(?,O(n^1))    ]



       Sub-problems:
       -------------
         * Path {1,4,2}: YES(?,O(n^1))
           ---------------------------

           The usable rules for this path are:

             {activate(X) -> X}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(U11) = {}, Uargs(U12) = {}, Uargs(activate) = {1},
               Uargs(s) = {}, Uargs(plus) = {}, Uargs(U11^#) = {3},
               Uargs(c_0) = {1}, Uargs(U12^#) = {2, 3}, Uargs(c_1) = {1},
               Uargs(plus^#) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(activate^#) = {}, Uargs(c_4) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              tt() = [0]
              U12(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              activate(x1) = [1] x1 + [3]
              s(x1) = [1] x1 + [0]
              plus(x1, x2) = [0] x1 + [0] x2 + [0]
              0() = [0]
              U11^#(x1, x2, x3) = [0] x1 + [3] x2 + [3] x3 + [0]
              c_0(x1) = [1] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [3] x2 + [3] x3 + [0]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [3] x1 + [3] x2 + [0]
              c_2(x1) = [0] x1 + [0]
              c_3(x1) = [1] x1 + [0]
              activate^#(x1) = [0] x1 + [0]
              c_4(x1) = [0] x1 + [0]
           Complexity induced by the adequate RMI: YES(?,O(n^1))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 1'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules:
               {  U11^#(tt(), M, N) -> c_0(U12^#(tt(), activate(M), activate(N)))
                , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N))
                , U12^#(tt(), M, N) -> c_1(plus^#(activate(N), activate(M)))}
             Weak Rules: {activate(X) -> X}

           Proof Output:
             The following argument positions are usable:
               Uargs(activate) = {}, Uargs(s) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {1}, Uargs(U12^#) = {}, Uargs(c_1) = {1},
               Uargs(plus^#) = {}, Uargs(c_3) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              tt() = [0]
              activate(x1) = [1] x1 + [0]
              s(x1) = [1] x1 + [2]
              U11^#(x1, x2, x3) = [0] x1 + [4] x2 + [0] x3 + [5]
              c_0(x1) = [1] x1 + [3]
              U12^#(x1, x2, x3) = [0] x1 + [4] x2 + [0] x3 + [1]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [0] x1 + [4] x2 + [0]
              c_3(x1) = [1] x1 + [1]

         * Path {1,4,2}->{3}: YES(?,O(n^1))
           --------------------------------

           The usable rules for this path are:

             {activate(X) -> X}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(U11) = {}, Uargs(U12) = {}, Uargs(activate) = {1},
               Uargs(s) = {}, Uargs(plus) = {}, Uargs(U11^#) = {3},
               Uargs(c_0) = {1}, Uargs(U12^#) = {2, 3}, Uargs(c_1) = {1},
               Uargs(plus^#) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(activate^#) = {}, Uargs(c_4) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              tt() = [0]
              U12(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              activate(x1) = [3] x1 + [3]
              s(x1) = [0] x1 + [0]
              plus(x1, x2) = [0] x1 + [0] x2 + [0]
              0() = [0]
              U11^#(x1, x2, x3) = [0] x1 + [0] x2 + [3] x3 + [0]
              c_0(x1) = [1] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [3] x2 + [3] x3 + [0]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [3] x1 + [3] x2 + [0]
              c_2(x1) = [1] x1 + [0]
              c_3(x1) = [1] x1 + [0]
              activate^#(x1) = [0] x1 + [0]
              c_4(x1) = [0] x1 + [0]
           Complexity induced by the adequate RMI: YES(?,O(1))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 1'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules: {plus^#(N, 0()) -> c_2(N)}
             Weak Rules:
               {  U11^#(tt(), M, N) -> c_0(U12^#(tt(), activate(M), activate(N)))
                , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N))
                , U12^#(tt(), M, N) -> c_1(plus^#(activate(N), activate(M)))
                , activate(X) -> X}

           Proof Output:
             The following argument positions are usable:
               Uargs(activate) = {}, Uargs(s) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {1}, Uargs(U12^#) = {}, Uargs(c_1) = {1},
               Uargs(plus^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              tt() = [0]
              activate(x1) = [1] x1 + [0]
              s(x1) = [1] x1 + [0]
              0() = [0]
              U11^#(x1, x2, x3) = [0] x1 + [0] x2 + [4] x3 + [1]
              c_0(x1) = [1] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [0] x2 + [4] x3 + [1]
              c_1(x1) = [1] x1 + [0]
              plus^#(x1, x2) = [4] x1 + [0] x2 + [1]
              c_2(x1) = [3] x1 + [0]
              c_3(x1) = [1] x1 + [0]

         * Path {5}: YES(?,O(1))
           ---------------------

           The usable rules of this path are empty.

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(U11) = {}, Uargs(U12) = {}, Uargs(activate) = {},
               Uargs(s) = {}, Uargs(plus) = {}, Uargs(U11^#) = {},
               Uargs(c_0) = {}, Uargs(U12^#) = {}, Uargs(c_1) = {},
               Uargs(plus^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {},
               Uargs(activate^#) = {}, Uargs(c_4) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              tt() = [0]
              U12(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              activate(x1) = [0] x1 + [0]
              s(x1) = [0] x1 + [0]
              plus(x1, x2) = [0] x1 + [0] x2 + [0]
              0() = [0]
              U11^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              c_0(x1) = [0] x1 + [0]
              U12^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
              c_1(x1) = [0] x1 + [0]
              plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
              c_2(x1) = [0] x1 + [0]
              c_3(x1) = [0] x1 + [0]
              activate^#(x1) = [3] x1 + [0]
              c_4(x1) = [1] x1 + [0]

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 1'
           --------------------------------------
           Answer:           YES(?,O(1))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules: {activate^#(X) -> c_4(X)}
             Weak Rules: {}

           Proof Output:
             The following argument positions are usable:
               Uargs(activate^#) = {}, Uargs(c_4) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              activate^#(x1) = [7] x1 + [7]
              c_4(x1) = [1] x1 + [0]