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

Strict Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , plus(N, s(M)) -> U41(isNat(M), M, N)
  , plus(N, 0()) -> U31(isNat(N), N)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Arguments of following rules are not normal-forms:

{ plus(N, s(M)) -> U41(isNat(M), M, N)
, plus(N, 0()) -> U31(isNat(N), N) }

All above mentioned rules can be savely removed.

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

Strict Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following dependency tuples:

Strict DPs:
  { U11^#(tt(), V2) ->
    c_1(U12^#(isNat(activate(V2))),
        isNat^#(activate(V2)),
        activate^#(V2))
  , U12^#(tt()) -> c_2()
  , isNat^#(n__0()) -> c_3()
  , isNat^#(n__plus(V1, V2)) ->
    c_4(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)),
        activate^#(V1),
        activate^#(V2))
  , isNat^#(n__s(V1)) ->
    c_5(U21^#(isNat(activate(V1))),
        isNat^#(activate(V1)),
        activate^#(V1))
  , activate^#(X) -> c_6()
  , activate^#(n__0()) -> c_7(0^#())
  , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
  , activate^#(n__s(X)) -> c_9(s^#(X))
  , U21^#(tt()) -> c_10()
  , 0^#() -> c_16()
  , plus^#(X1, X2) -> c_15()
  , s^#(X) -> c_14()
  , U31^#(tt(), N) -> c_11(activate^#(N))
  , U41^#(tt(), M, N) ->
    c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
         isNat^#(activate(N)),
         activate^#(N),
         activate^#(M),
         activate^#(N))
  , U42^#(tt(), M, N) ->
    c_13(s^#(plus(activate(N), activate(M))),
         plus^#(activate(N), activate(M)),
         activate^#(N),
         activate^#(M)) }

and mark the set of starting terms.

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

Strict DPs:
  { U11^#(tt(), V2) ->
    c_1(U12^#(isNat(activate(V2))),
        isNat^#(activate(V2)),
        activate^#(V2))
  , U12^#(tt()) -> c_2()
  , isNat^#(n__0()) -> c_3()
  , isNat^#(n__plus(V1, V2)) ->
    c_4(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)),
        activate^#(V1),
        activate^#(V2))
  , isNat^#(n__s(V1)) ->
    c_5(U21^#(isNat(activate(V1))),
        isNat^#(activate(V1)),
        activate^#(V1))
  , activate^#(X) -> c_6()
  , activate^#(n__0()) -> c_7(0^#())
  , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
  , activate^#(n__s(X)) -> c_9(s^#(X))
  , U21^#(tt()) -> c_10()
  , 0^#() -> c_16()
  , plus^#(X1, X2) -> c_15()
  , s^#(X) -> c_14()
  , U31^#(tt(), N) -> c_11(activate^#(N))
  , U41^#(tt(), M, N) ->
    c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
         isNat^#(activate(N)),
         activate^#(N),
         activate^#(M),
         activate^#(N))
  , U42^#(tt(), M, N) ->
    c_13(s^#(plus(activate(N), activate(M))),
         plus^#(activate(N), activate(M)),
         activate^#(N),
         activate^#(M)) }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {2,3,6,10,11,12,13} by
applications of Pre({2,3,6,10,11,12,13}) = {1,4,5,7,8,9,14,15,16}.
Here rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), V2) ->
         c_1(U12^#(isNat(activate(V2))),
             isNat^#(activate(V2)),
             activate^#(V2))
    , 2: U12^#(tt()) -> c_2()
    , 3: isNat^#(n__0()) -> c_3()
    , 4: isNat^#(n__plus(V1, V2)) ->
         c_4(U11^#(isNat(activate(V1)), activate(V2)),
             isNat^#(activate(V1)),
             activate^#(V1),
             activate^#(V2))
    , 5: isNat^#(n__s(V1)) ->
         c_5(U21^#(isNat(activate(V1))),
             isNat^#(activate(V1)),
             activate^#(V1))
    , 6: activate^#(X) -> c_6()
    , 7: activate^#(n__0()) -> c_7(0^#())
    , 8: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
    , 9: activate^#(n__s(X)) -> c_9(s^#(X))
    , 10: U21^#(tt()) -> c_10()
    , 11: 0^#() -> c_16()
    , 12: plus^#(X1, X2) -> c_15()
    , 13: s^#(X) -> c_14()
    , 14: U31^#(tt(), N) -> c_11(activate^#(N))
    , 15: U41^#(tt(), M, N) ->
          c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
               isNat^#(activate(N)),
               activate^#(N),
               activate^#(M),
               activate^#(N))
    , 16: U42^#(tt(), M, N) ->
          c_13(s^#(plus(activate(N), activate(M))),
               plus^#(activate(N), activate(M)),
               activate^#(N),
               activate^#(M)) }

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

Strict DPs:
  { U11^#(tt(), V2) ->
    c_1(U12^#(isNat(activate(V2))),
        isNat^#(activate(V2)),
        activate^#(V2))
  , isNat^#(n__plus(V1, V2)) ->
    c_4(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)),
        activate^#(V1),
        activate^#(V2))
  , isNat^#(n__s(V1)) ->
    c_5(U21^#(isNat(activate(V1))),
        isNat^#(activate(V1)),
        activate^#(V1))
  , activate^#(n__0()) -> c_7(0^#())
  , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
  , activate^#(n__s(X)) -> c_9(s^#(X))
  , U31^#(tt(), N) -> c_11(activate^#(N))
  , U41^#(tt(), M, N) ->
    c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
         isNat^#(activate(N)),
         activate^#(N),
         activate^#(M),
         activate^#(N))
  , U42^#(tt(), M, N) ->
    c_13(s^#(plus(activate(N), activate(M))),
         plus^#(activate(N), activate(M)),
         activate^#(N),
         activate^#(M)) }
Weak DPs:
  { U12^#(tt()) -> c_2()
  , isNat^#(n__0()) -> c_3()
  , activate^#(X) -> c_6()
  , U21^#(tt()) -> c_10()
  , 0^#() -> c_16()
  , plus^#(X1, X2) -> c_15()
  , s^#(X) -> c_14() }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {4,5,6} by applications of
Pre({4,5,6}) = {1,2,3,7,8,9}. Here rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), V2) ->
         c_1(U12^#(isNat(activate(V2))),
             isNat^#(activate(V2)),
             activate^#(V2))
    , 2: isNat^#(n__plus(V1, V2)) ->
         c_4(U11^#(isNat(activate(V1)), activate(V2)),
             isNat^#(activate(V1)),
             activate^#(V1),
             activate^#(V2))
    , 3: isNat^#(n__s(V1)) ->
         c_5(U21^#(isNat(activate(V1))),
             isNat^#(activate(V1)),
             activate^#(V1))
    , 4: activate^#(n__0()) -> c_7(0^#())
    , 5: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
    , 6: activate^#(n__s(X)) -> c_9(s^#(X))
    , 7: U31^#(tt(), N) -> c_11(activate^#(N))
    , 8: U41^#(tt(), M, N) ->
         c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
              isNat^#(activate(N)),
              activate^#(N),
              activate^#(M),
              activate^#(N))
    , 9: U42^#(tt(), M, N) ->
         c_13(s^#(plus(activate(N), activate(M))),
              plus^#(activate(N), activate(M)),
              activate^#(N),
              activate^#(M))
    , 10: U12^#(tt()) -> c_2()
    , 11: isNat^#(n__0()) -> c_3()
    , 12: activate^#(X) -> c_6()
    , 13: U21^#(tt()) -> c_10()
    , 14: 0^#() -> c_16()
    , 15: plus^#(X1, X2) -> c_15()
    , 16: s^#(X) -> c_14() }

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

Strict DPs:
  { U11^#(tt(), V2) ->
    c_1(U12^#(isNat(activate(V2))),
        isNat^#(activate(V2)),
        activate^#(V2))
  , isNat^#(n__plus(V1, V2)) ->
    c_4(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)),
        activate^#(V1),
        activate^#(V2))
  , isNat^#(n__s(V1)) ->
    c_5(U21^#(isNat(activate(V1))),
        isNat^#(activate(V1)),
        activate^#(V1))
  , U31^#(tt(), N) -> c_11(activate^#(N))
  , U41^#(tt(), M, N) ->
    c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
         isNat^#(activate(N)),
         activate^#(N),
         activate^#(M),
         activate^#(N))
  , U42^#(tt(), M, N) ->
    c_13(s^#(plus(activate(N), activate(M))),
         plus^#(activate(N), activate(M)),
         activate^#(N),
         activate^#(M)) }
Weak DPs:
  { U12^#(tt()) -> c_2()
  , isNat^#(n__0()) -> c_3()
  , activate^#(X) -> c_6()
  , activate^#(n__0()) -> c_7(0^#())
  , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
  , activate^#(n__s(X)) -> c_9(s^#(X))
  , U21^#(tt()) -> c_10()
  , 0^#() -> c_16()
  , plus^#(X1, X2) -> c_15()
  , s^#(X) -> c_14() }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {4,6} by applications of
Pre({4,6}) = {5}. Here rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), V2) ->
         c_1(U12^#(isNat(activate(V2))),
             isNat^#(activate(V2)),
             activate^#(V2))
    , 2: isNat^#(n__plus(V1, V2)) ->
         c_4(U11^#(isNat(activate(V1)), activate(V2)),
             isNat^#(activate(V1)),
             activate^#(V1),
             activate^#(V2))
    , 3: isNat^#(n__s(V1)) ->
         c_5(U21^#(isNat(activate(V1))),
             isNat^#(activate(V1)),
             activate^#(V1))
    , 4: U31^#(tt(), N) -> c_11(activate^#(N))
    , 5: U41^#(tt(), M, N) ->
         c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
              isNat^#(activate(N)),
              activate^#(N),
              activate^#(M),
              activate^#(N))
    , 6: U42^#(tt(), M, N) ->
         c_13(s^#(plus(activate(N), activate(M))),
              plus^#(activate(N), activate(M)),
              activate^#(N),
              activate^#(M))
    , 7: U12^#(tt()) -> c_2()
    , 8: isNat^#(n__0()) -> c_3()
    , 9: activate^#(X) -> c_6()
    , 10: activate^#(n__0()) -> c_7(0^#())
    , 11: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
    , 12: activate^#(n__s(X)) -> c_9(s^#(X))
    , 13: U21^#(tt()) -> c_10()
    , 14: 0^#() -> c_16()
    , 15: plus^#(X1, X2) -> c_15()
    , 16: s^#(X) -> c_14() }

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

Strict DPs:
  { U11^#(tt(), V2) ->
    c_1(U12^#(isNat(activate(V2))),
        isNat^#(activate(V2)),
        activate^#(V2))
  , isNat^#(n__plus(V1, V2)) ->
    c_4(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)),
        activate^#(V1),
        activate^#(V2))
  , isNat^#(n__s(V1)) ->
    c_5(U21^#(isNat(activate(V1))),
        isNat^#(activate(V1)),
        activate^#(V1))
  , U41^#(tt(), M, N) ->
    c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
         isNat^#(activate(N)),
         activate^#(N),
         activate^#(M),
         activate^#(N)) }
Weak DPs:
  { U12^#(tt()) -> c_2()
  , isNat^#(n__0()) -> c_3()
  , activate^#(X) -> c_6()
  , activate^#(n__0()) -> c_7(0^#())
  , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
  , activate^#(n__s(X)) -> c_9(s^#(X))
  , U21^#(tt()) -> c_10()
  , 0^#() -> c_16()
  , plus^#(X1, X2) -> c_15()
  , s^#(X) -> c_14()
  , U31^#(tt(), N) -> c_11(activate^#(N))
  , U42^#(tt(), M, N) ->
    c_13(s^#(plus(activate(N), activate(M))),
         plus^#(activate(N), activate(M)),
         activate^#(N),
         activate^#(M)) }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ U12^#(tt()) -> c_2()
, isNat^#(n__0()) -> c_3()
, activate^#(X) -> c_6()
, activate^#(n__0()) -> c_7(0^#())
, activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2))
, activate^#(n__s(X)) -> c_9(s^#(X))
, U21^#(tt()) -> c_10()
, 0^#() -> c_16()
, plus^#(X1, X2) -> c_15()
, s^#(X) -> c_14()
, U31^#(tt(), N) -> c_11(activate^#(N))
, U42^#(tt(), M, N) ->
  c_13(s^#(plus(activate(N), activate(M))),
       plus^#(activate(N), activate(M)),
       activate^#(N),
       activate^#(M)) }

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

Strict DPs:
  { U11^#(tt(), V2) ->
    c_1(U12^#(isNat(activate(V2))),
        isNat^#(activate(V2)),
        activate^#(V2))
  , isNat^#(n__plus(V1, V2)) ->
    c_4(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)),
        activate^#(V1),
        activate^#(V2))
  , isNat^#(n__s(V1)) ->
    c_5(U21^#(isNat(activate(V1))),
        isNat^#(activate(V1)),
        activate^#(V1))
  , U41^#(tt(), M, N) ->
    c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
         isNat^#(activate(N)),
         activate^#(N),
         activate^#(M),
         activate^#(N)) }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { U11^#(tt(), V2) ->
    c_1(U12^#(isNat(activate(V2))),
        isNat^#(activate(V2)),
        activate^#(V2))
  , isNat^#(n__plus(V1, V2)) ->
    c_4(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)),
        activate^#(V1),
        activate^#(V2))
  , isNat^#(n__s(V1)) ->
    c_5(U21^#(isNat(activate(V1))),
        isNat^#(activate(V1)),
        activate^#(V1))
  , U41^#(tt(), M, N) ->
    c_12(U42^#(isNat(activate(N)), activate(M), activate(N)),
         isNat^#(activate(N)),
         activate^#(N),
         activate^#(M),
         activate^#(N)) }

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

Strict DPs:
  { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
  , isNat^#(n__plus(V1, V2)) ->
    c_2(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)))
  , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
  , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , U31(tt(), N) -> activate(N)
  , U41(tt(), M, N) ->
    U42(isNat(activate(N)), activate(M), activate(N))
  , U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { U11(tt(), V2) -> U12(isNat(activate(V2)))
    , U12(tt()) -> tt()
    , isNat(n__0()) -> tt()
    , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
    , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
    , activate(X) -> X
    , activate(n__0()) -> 0()
    , activate(n__plus(X1, X2)) -> plus(X1, X2)
    , activate(n__s(X)) -> s(X)
    , U21(tt()) -> tt()
    , s(X) -> n__s(X)
    , plus(X1, X2) -> n__plus(X1, X2)
    , 0() -> n__0() }

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

Strict DPs:
  { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
  , isNat^#(n__plus(V1, V2)) ->
    c_2(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)))
  , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
  , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 2: isNat^#(n__plus(V1, V2)) ->
       c_2(U11^#(isNat(activate(V1)), activate(V2)),
           isNat^#(activate(V1)))
  , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
  , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) }
Trs:
  { isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1))) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
    Uargs(c_4) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
          [U11](x1, x2) = [0]                  
                                               
                   [tt] = [0]                  
                                               
              [U12](x1) = [0]                  
                                               
            [isNat](x1) = [1] x1 + [0]         
                                               
         [activate](x1) = [1] x1 + [0]         
                                               
              [U21](x1) = [0]                  
                                               
                [s](x1) = [1] x1 + [4]         
                                               
         [plus](x1, x2) = [1] x1 + [1] x2 + [4]
                                               
                 [n__0] = [4]                  
                                               
      [n__plus](x1, x2) = [1] x1 + [1] x2 + [4]
                                               
             [n__s](x1) = [1] x1 + [4]         
                                               
                    [0] = [4]                  
                                               
        [U11^#](x1, x2) = [1] x2 + [3]         
                                               
          [isNat^#](x1) = [1] x1 + [3]         
                                               
    [U41^#](x1, x2, x3) = [2] x2 + [7] x3 + [5]
                                               
              [c_1](x1) = [1] x1 + [0]         
                                               
          [c_2](x1, x2) = [1] x1 + [1] x2 + [0]
                                               
              [c_3](x1) = [1] x1 + [0]         
                                               
              [c_4](x1) = [1] x1 + [0]         
  
  The order satisfies the following ordering constraints:
  
                [U11(tt(), V2)] =  [0]                                           
                                >= [0]                                           
                                =  [U12(isNat(activate(V2)))]                    
                                                                                 
                    [U12(tt())] =  [0]                                           
                                >= [0]                                           
                                =  [tt()]                                        
                                                                                 
                [isNat(n__0())] =  [4]                                           
                                >  [0]                                           
                                =  [tt()]                                        
                                                                                 
       [isNat(n__plus(V1, V2))] =  [1] V2 + [1] V1 + [4]                         
                                >  [0]                                           
                                =  [U11(isNat(activate(V1)), activate(V2))]      
                                                                                 
              [isNat(n__s(V1))] =  [1] V1 + [4]                                  
                                >  [0]                                           
                                =  [U21(isNat(activate(V1)))]                    
                                                                                 
                  [activate(X)] =  [1] X + [0]                                   
                                >= [1] X + [0]                                   
                                =  [X]                                           
                                                                                 
             [activate(n__0())] =  [4]                                           
                                >= [4]                                           
                                =  [0()]                                         
                                                                                 
    [activate(n__plus(X1, X2))] =  [1] X1 + [1] X2 + [4]                         
                                >= [1] X1 + [1] X2 + [4]                         
                                =  [plus(X1, X2)]                                
                                                                                 
            [activate(n__s(X))] =  [1] X + [4]                                   
                                >= [1] X + [4]                                   
                                =  [s(X)]                                        
                                                                                 
                    [U21(tt())] =  [0]                                           
                                >= [0]                                           
                                =  [tt()]                                        
                                                                                 
                         [s(X)] =  [1] X + [4]                                   
                                >= [1] X + [4]                                   
                                =  [n__s(X)]                                     
                                                                                 
                 [plus(X1, X2)] =  [1] X1 + [1] X2 + [4]                         
                                >= [1] X1 + [1] X2 + [4]                         
                                =  [n__plus(X1, X2)]                             
                                                                                 
                          [0()] =  [4]                                           
                                >= [4]                                           
                                =  [n__0()]                                      
                                                                                 
              [U11^#(tt(), V2)] =  [1] V2 + [3]                                  
                                >= [1] V2 + [3]                                  
                                =  [c_1(isNat^#(activate(V2)))]                  
                                                                                 
     [isNat^#(n__plus(V1, V2))] =  [1] V2 + [1] V1 + [7]                         
                                >  [1] V2 + [1] V1 + [6]                         
                                =  [c_2(U11^#(isNat(activate(V1)), activate(V2)),
                                        isNat^#(activate(V1)))]                  
                                                                                 
            [isNat^#(n__s(V1))] =  [1] V1 + [7]                                  
                                >  [1] V1 + [3]                                  
                                =  [c_3(isNat^#(activate(V1)))]                  
                                                                                 
            [U41^#(tt(), M, N)] =  [7] N + [2] M + [5]                           
                                >  [1] N + [3]                                   
                                =  [c_4(isNat^#(activate(N)))]                   
                                                                                 

We return to the main proof. Consider the set of all dependency
pairs

:
  { 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
  , 2: isNat^#(n__plus(V1, V2)) ->
       c_2(U11^#(isNat(activate(V1)), activate(V2)),
           isNat^#(activate(V1)))
  , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
  , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2,3,4}. These cover all (indirect) predecessors of
dependency pairs {1,2,3,4}, their number of application is equally
bounded. The dependency pairs are shifted into the weak component.

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

Weak DPs:
  { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
  , isNat^#(n__plus(V1, V2)) ->
    c_2(U11^#(isNat(activate(V1)), activate(V2)),
        isNat^#(activate(V1)))
  , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
  , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) }
Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
  c_2(U11^#(isNat(activate(V1)), activate(V2)),
      isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) }

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

Weak Trs:
  { U11(tt(), V2) -> U12(isNat(activate(V2)))
  , U12(tt()) -> tt()
  , isNat(n__0()) -> tt()
  , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
  , isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__plus(X1, X2)) -> plus(X1, X2)
  , activate(n__s(X)) -> s(X)
  , U21(tt()) -> tt()
  , s(X) -> n__s(X)
  , plus(X1, X2) -> n__plus(X1, X2)
  , 0() -> n__0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

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

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

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