MAYBE

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

Strict Trs:
  { f(x, y) -> cond(and(isNat(x), isNat(y)), x, y)
  , cond(tt(), x, y) -> f(s(x), s(y))
  , and(x, ff()) -> ff()
  , and(tt(), tt()) -> tt()
  , and(ff(), x) -> ff()
  , isNat(s(x)) -> isNat(x)
  , isNat(0()) -> tt() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { f^#(x, y) ->
    c_1(cond^#(and(isNat(x), isNat(y)), x, y),
        and^#(isNat(x), isNat(y)),
        isNat^#(x),
        isNat^#(y))
  , cond^#(tt(), x, y) -> c_2(f^#(s(x), s(y)))
  , and^#(x, ff()) -> c_3()
  , and^#(tt(), tt()) -> c_4()
  , and^#(ff(), x) -> c_5()
  , isNat^#(s(x)) -> c_6(isNat^#(x))
  , isNat^#(0()) -> c_7() }

and mark the set of starting terms.

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

Strict DPs:
  { f^#(x, y) ->
    c_1(cond^#(and(isNat(x), isNat(y)), x, y),
        and^#(isNat(x), isNat(y)),
        isNat^#(x),
        isNat^#(y))
  , cond^#(tt(), x, y) -> c_2(f^#(s(x), s(y)))
  , and^#(x, ff()) -> c_3()
  , and^#(tt(), tt()) -> c_4()
  , and^#(ff(), x) -> c_5()
  , isNat^#(s(x)) -> c_6(isNat^#(x))
  , isNat^#(0()) -> c_7() }
Weak Trs:
  { f(x, y) -> cond(and(isNat(x), isNat(y)), x, y)
  , cond(tt(), x, y) -> f(s(x), s(y))
  , and(x, ff()) -> ff()
  , and(tt(), tt()) -> tt()
  , and(ff(), x) -> ff()
  , isNat(s(x)) -> isNat(x)
  , isNat(0()) -> tt() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: f^#(x, y) ->
         c_1(cond^#(and(isNat(x), isNat(y)), x, y),
             and^#(isNat(x), isNat(y)),
             isNat^#(x),
             isNat^#(y))
    , 2: cond^#(tt(), x, y) -> c_2(f^#(s(x), s(y)))
    , 3: and^#(x, ff()) -> c_3()
    , 4: and^#(tt(), tt()) -> c_4()
    , 5: and^#(ff(), x) -> c_5()
    , 6: isNat^#(s(x)) -> c_6(isNat^#(x))
    , 7: isNat^#(0()) -> c_7() }

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

Strict DPs:
  { f^#(x, y) ->
    c_1(cond^#(and(isNat(x), isNat(y)), x, y),
        and^#(isNat(x), isNat(y)),
        isNat^#(x),
        isNat^#(y))
  , cond^#(tt(), x, y) -> c_2(f^#(s(x), s(y)))
  , isNat^#(s(x)) -> c_6(isNat^#(x)) }
Weak DPs:
  { and^#(x, ff()) -> c_3()
  , and^#(tt(), tt()) -> c_4()
  , and^#(ff(), x) -> c_5()
  , isNat^#(0()) -> c_7() }
Weak Trs:
  { f(x, y) -> cond(and(isNat(x), isNat(y)), x, y)
  , cond(tt(), x, y) -> f(s(x), s(y))
  , and(x, ff()) -> ff()
  , and(tt(), tt()) -> tt()
  , and(ff(), x) -> ff()
  , isNat(s(x)) -> isNat(x)
  , isNat(0()) -> tt() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

{ and^#(x, ff()) -> c_3()
, and^#(tt(), tt()) -> c_4()
, and^#(ff(), x) -> c_5()
, isNat^#(0()) -> c_7() }

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

Strict DPs:
  { f^#(x, y) ->
    c_1(cond^#(and(isNat(x), isNat(y)), x, y),
        and^#(isNat(x), isNat(y)),
        isNat^#(x),
        isNat^#(y))
  , cond^#(tt(), x, y) -> c_2(f^#(s(x), s(y)))
  , isNat^#(s(x)) -> c_6(isNat^#(x)) }
Weak Trs:
  { f(x, y) -> cond(and(isNat(x), isNat(y)), x, y)
  , cond(tt(), x, y) -> f(s(x), s(y))
  , and(x, ff()) -> ff()
  , and(tt(), tt()) -> tt()
  , and(ff(), x) -> ff()
  , isNat(s(x)) -> isNat(x)
  , isNat(0()) -> tt() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { f^#(x, y) ->
    c_1(cond^#(and(isNat(x), isNat(y)), x, y),
        and^#(isNat(x), isNat(y)),
        isNat^#(x),
        isNat^#(y)) }

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

Strict DPs:
  { f^#(x, y) ->
    c_1(cond^#(and(isNat(x), isNat(y)), x, y), isNat^#(x), isNat^#(y))
  , cond^#(tt(), x, y) -> c_2(f^#(s(x), s(y)))
  , isNat^#(s(x)) -> c_3(isNat^#(x)) }
Weak Trs:
  { f(x, y) -> cond(and(isNat(x), isNat(y)), x, y)
  , cond(tt(), x, y) -> f(s(x), s(y))
  , and(x, ff()) -> ff()
  , and(tt(), tt()) -> tt()
  , and(ff(), x) -> ff()
  , isNat(s(x)) -> isNat(x)
  , isNat(0()) -> tt() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { and(x, ff()) -> ff()
    , and(tt(), tt()) -> tt()
    , and(ff(), x) -> ff()
    , isNat(s(x)) -> isNat(x)
    , isNat(0()) -> tt() }

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

Strict DPs:
  { f^#(x, y) ->
    c_1(cond^#(and(isNat(x), isNat(y)), x, y), isNat^#(x), isNat^#(y))
  , cond^#(tt(), x, y) -> c_2(f^#(s(x), s(y)))
  , isNat^#(s(x)) -> c_3(isNat^#(x)) }
Weak Trs:
  { and(x, ff()) -> ff()
  , and(tt(), tt()) -> tt()
  , and(ff(), x) -> ff()
  , isNat(s(x)) -> isNat(x)
  , isNat(0()) -> tt() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..