MAYBE

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

Strict Trs:
  { and(true(), y) -> y
  , and(false(), y) -> false()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(t, l)) -> false()
  , eq(cons(t, l), nil()) -> false()
  , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
  , eq(var(l), var(l')) -> eq(l, l')
  , eq(var(l), apply(t, s)) -> false()
  , eq(var(l), lambda(x, t)) -> false()
  , eq(apply(t, s), var(l)) -> false()
  , eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
  , eq(apply(t, s), lambda(x, t)) -> false()
  , eq(lambda(x, t), var(l)) -> false()
  , eq(lambda(x, t), apply(t, s)) -> false()
  , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
  , if(true(), var(k), var(l')) -> var(k)
  , if(false(), var(k), var(l')) -> var(l')
  , ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
  , ren(x, y, lambda(z, t)) ->
    lambda(var(cons(x, cons(y, cons(lambda(z, t), nil())))),
           ren(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)))
  , ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l')) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { and^#(true(), y) -> c_1()
  , and^#(false(), y) -> c_2()
  , eq^#(nil(), nil()) -> c_3()
  , eq^#(nil(), cons(t, l)) -> c_4()
  , eq^#(cons(t, l), nil()) -> c_5()
  , eq^#(cons(t, l), cons(t', l')) ->
    c_6(and^#(eq(t, t'), eq(l, l')), eq^#(t, t'), eq^#(l, l'))
  , eq^#(var(l), var(l')) -> c_7(eq^#(l, l'))
  , eq^#(var(l), apply(t, s)) -> c_8()
  , eq^#(var(l), lambda(x, t)) -> c_9()
  , eq^#(apply(t, s), var(l)) -> c_10()
  , eq^#(apply(t, s), apply(t', s')) ->
    c_11(and^#(eq(t, t'), eq(s, s')), eq^#(t, t'), eq^#(s, s'))
  , eq^#(apply(t, s), lambda(x, t)) -> c_12()
  , eq^#(lambda(x, t), var(l)) -> c_13()
  , eq^#(lambda(x, t), apply(t, s)) -> c_14()
  , eq^#(lambda(x, t), lambda(x', t')) ->
    c_15(and^#(eq(x, x'), eq(t, t')), eq^#(x, x'), eq^#(t, t'))
  , if^#(true(), var(k), var(l')) -> c_16()
  , if^#(false(), var(k), var(l')) -> c_17()
  , ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s))
  , ren^#(x, y, lambda(z, t)) ->
    c_19(ren^#(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)),
         ren^#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t))
  , ren^#(var(l), var(k), var(l')) ->
    c_20(if^#(eq(l, l'), var(k), var(l')), eq^#(l, l')) }

and mark the set of starting terms.

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

Strict DPs:
  { and^#(true(), y) -> c_1()
  , and^#(false(), y) -> c_2()
  , eq^#(nil(), nil()) -> c_3()
  , eq^#(nil(), cons(t, l)) -> c_4()
  , eq^#(cons(t, l), nil()) -> c_5()
  , eq^#(cons(t, l), cons(t', l')) ->
    c_6(and^#(eq(t, t'), eq(l, l')), eq^#(t, t'), eq^#(l, l'))
  , eq^#(var(l), var(l')) -> c_7(eq^#(l, l'))
  , eq^#(var(l), apply(t, s)) -> c_8()
  , eq^#(var(l), lambda(x, t)) -> c_9()
  , eq^#(apply(t, s), var(l)) -> c_10()
  , eq^#(apply(t, s), apply(t', s')) ->
    c_11(and^#(eq(t, t'), eq(s, s')), eq^#(t, t'), eq^#(s, s'))
  , eq^#(apply(t, s), lambda(x, t)) -> c_12()
  , eq^#(lambda(x, t), var(l)) -> c_13()
  , eq^#(lambda(x, t), apply(t, s)) -> c_14()
  , eq^#(lambda(x, t), lambda(x', t')) ->
    c_15(and^#(eq(x, x'), eq(t, t')), eq^#(x, x'), eq^#(t, t'))
  , if^#(true(), var(k), var(l')) -> c_16()
  , if^#(false(), var(k), var(l')) -> c_17()
  , ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s))
  , ren^#(x, y, lambda(z, t)) ->
    c_19(ren^#(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)),
         ren^#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t))
  , ren^#(var(l), var(k), var(l')) ->
    c_20(if^#(eq(l, l'), var(k), var(l')), eq^#(l, l')) }
Weak Trs:
  { and(true(), y) -> y
  , and(false(), y) -> false()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(t, l)) -> false()
  , eq(cons(t, l), nil()) -> false()
  , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
  , eq(var(l), var(l')) -> eq(l, l')
  , eq(var(l), apply(t, s)) -> false()
  , eq(var(l), lambda(x, t)) -> false()
  , eq(apply(t, s), var(l)) -> false()
  , eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
  , eq(apply(t, s), lambda(x, t)) -> false()
  , eq(lambda(x, t), var(l)) -> false()
  , eq(lambda(x, t), apply(t, s)) -> false()
  , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
  , if(true(), var(k), var(l')) -> var(k)
  , if(false(), var(k), var(l')) -> var(l')
  , ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
  , ren(x, y, lambda(z, t)) ->
    lambda(var(cons(x, cons(y, cons(lambda(z, t), nil())))),
           ren(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)))
  , ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l')) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: and^#(true(), y) -> c_1()
    , 2: and^#(false(), y) -> c_2()
    , 3: eq^#(nil(), nil()) -> c_3()
    , 4: eq^#(nil(), cons(t, l)) -> c_4()
    , 5: eq^#(cons(t, l), nil()) -> c_5()
    , 6: eq^#(cons(t, l), cons(t', l')) ->
         c_6(and^#(eq(t, t'), eq(l, l')), eq^#(t, t'), eq^#(l, l'))
    , 7: eq^#(var(l), var(l')) -> c_7(eq^#(l, l'))
    , 8: eq^#(var(l), apply(t, s)) -> c_8()
    , 9: eq^#(var(l), lambda(x, t)) -> c_9()
    , 10: eq^#(apply(t, s), var(l)) -> c_10()
    , 11: eq^#(apply(t, s), apply(t', s')) ->
          c_11(and^#(eq(t, t'), eq(s, s')), eq^#(t, t'), eq^#(s, s'))
    , 12: eq^#(apply(t, s), lambda(x, t)) -> c_12()
    , 13: eq^#(lambda(x, t), var(l)) -> c_13()
    , 14: eq^#(lambda(x, t), apply(t, s)) -> c_14()
    , 15: eq^#(lambda(x, t), lambda(x', t')) ->
          c_15(and^#(eq(x, x'), eq(t, t')), eq^#(x, x'), eq^#(t, t'))
    , 16: if^#(true(), var(k), var(l')) -> c_16()
    , 17: if^#(false(), var(k), var(l')) -> c_17()
    , 18: ren^#(x, y, apply(t, s)) ->
          c_18(ren^#(x, y, t), ren^#(x, y, s))
    , 19: ren^#(x, y, lambda(z, t)) ->
          c_19(ren^#(x,
                     y,
                     ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)),
               ren^#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t))
    , 20: ren^#(var(l), var(k), var(l')) ->
          c_20(if^#(eq(l, l'), var(k), var(l')), eq^#(l, l')) }

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

Strict DPs:
  { eq^#(cons(t, l), cons(t', l')) ->
    c_6(and^#(eq(t, t'), eq(l, l')), eq^#(t, t'), eq^#(l, l'))
  , eq^#(var(l), var(l')) -> c_7(eq^#(l, l'))
  , eq^#(apply(t, s), apply(t', s')) ->
    c_11(and^#(eq(t, t'), eq(s, s')), eq^#(t, t'), eq^#(s, s'))
  , eq^#(lambda(x, t), lambda(x', t')) ->
    c_15(and^#(eq(x, x'), eq(t, t')), eq^#(x, x'), eq^#(t, t'))
  , ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s))
  , ren^#(x, y, lambda(z, t)) ->
    c_19(ren^#(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)),
         ren^#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t))
  , ren^#(var(l), var(k), var(l')) ->
    c_20(if^#(eq(l, l'), var(k), var(l')), eq^#(l, l')) }
Weak DPs:
  { and^#(true(), y) -> c_1()
  , and^#(false(), y) -> c_2()
  , eq^#(nil(), nil()) -> c_3()
  , eq^#(nil(), cons(t, l)) -> c_4()
  , eq^#(cons(t, l), nil()) -> c_5()
  , eq^#(var(l), apply(t, s)) -> c_8()
  , eq^#(var(l), lambda(x, t)) -> c_9()
  , eq^#(apply(t, s), var(l)) -> c_10()
  , eq^#(apply(t, s), lambda(x, t)) -> c_12()
  , eq^#(lambda(x, t), var(l)) -> c_13()
  , eq^#(lambda(x, t), apply(t, s)) -> c_14()
  , if^#(true(), var(k), var(l')) -> c_16()
  , if^#(false(), var(k), var(l')) -> c_17() }
Weak Trs:
  { and(true(), y) -> y
  , and(false(), y) -> false()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(t, l)) -> false()
  , eq(cons(t, l), nil()) -> false()
  , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
  , eq(var(l), var(l')) -> eq(l, l')
  , eq(var(l), apply(t, s)) -> false()
  , eq(var(l), lambda(x, t)) -> false()
  , eq(apply(t, s), var(l)) -> false()
  , eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
  , eq(apply(t, s), lambda(x, t)) -> false()
  , eq(lambda(x, t), var(l)) -> false()
  , eq(lambda(x, t), apply(t, s)) -> false()
  , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
  , if(true(), var(k), var(l')) -> var(k)
  , if(false(), var(k), var(l')) -> var(l')
  , ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
  , ren(x, y, lambda(z, t)) ->
    lambda(var(cons(x, cons(y, cons(lambda(z, t), nil())))),
           ren(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)))
  , ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l')) }
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^#(true(), y) -> c_1()
, and^#(false(), y) -> c_2()
, eq^#(nil(), nil()) -> c_3()
, eq^#(nil(), cons(t, l)) -> c_4()
, eq^#(cons(t, l), nil()) -> c_5()
, eq^#(var(l), apply(t, s)) -> c_8()
, eq^#(var(l), lambda(x, t)) -> c_9()
, eq^#(apply(t, s), var(l)) -> c_10()
, eq^#(apply(t, s), lambda(x, t)) -> c_12()
, eq^#(lambda(x, t), var(l)) -> c_13()
, eq^#(lambda(x, t), apply(t, s)) -> c_14()
, if^#(true(), var(k), var(l')) -> c_16()
, if^#(false(), var(k), var(l')) -> c_17() }

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

Strict DPs:
  { eq^#(cons(t, l), cons(t', l')) ->
    c_6(and^#(eq(t, t'), eq(l, l')), eq^#(t, t'), eq^#(l, l'))
  , eq^#(var(l), var(l')) -> c_7(eq^#(l, l'))
  , eq^#(apply(t, s), apply(t', s')) ->
    c_11(and^#(eq(t, t'), eq(s, s')), eq^#(t, t'), eq^#(s, s'))
  , eq^#(lambda(x, t), lambda(x', t')) ->
    c_15(and^#(eq(x, x'), eq(t, t')), eq^#(x, x'), eq^#(t, t'))
  , ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s))
  , ren^#(x, y, lambda(z, t)) ->
    c_19(ren^#(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)),
         ren^#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t))
  , ren^#(var(l), var(k), var(l')) ->
    c_20(if^#(eq(l, l'), var(k), var(l')), eq^#(l, l')) }
Weak Trs:
  { and(true(), y) -> y
  , and(false(), y) -> false()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(t, l)) -> false()
  , eq(cons(t, l), nil()) -> false()
  , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
  , eq(var(l), var(l')) -> eq(l, l')
  , eq(var(l), apply(t, s)) -> false()
  , eq(var(l), lambda(x, t)) -> false()
  , eq(apply(t, s), var(l)) -> false()
  , eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
  , eq(apply(t, s), lambda(x, t)) -> false()
  , eq(lambda(x, t), var(l)) -> false()
  , eq(lambda(x, t), apply(t, s)) -> false()
  , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
  , if(true(), var(k), var(l')) -> var(k)
  , if(false(), var(k), var(l')) -> var(l')
  , ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
  , ren(x, y, lambda(z, t)) ->
    lambda(var(cons(x, cons(y, cons(lambda(z, t), nil())))),
           ren(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)))
  , ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l')) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { eq^#(cons(t, l), cons(t', l')) ->
    c_6(and^#(eq(t, t'), eq(l, l')), eq^#(t, t'), eq^#(l, l'))
  , eq^#(apply(t, s), apply(t', s')) ->
    c_11(and^#(eq(t, t'), eq(s, s')), eq^#(t, t'), eq^#(s, s'))
  , eq^#(lambda(x, t), lambda(x', t')) ->
    c_15(and^#(eq(x, x'), eq(t, t')), eq^#(x, x'), eq^#(t, t'))
  , ren^#(var(l), var(k), var(l')) ->
    c_20(if^#(eq(l, l'), var(k), var(l')), eq^#(l, l')) }

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

Strict DPs:
  { eq^#(cons(t, l), cons(t', l')) -> c_1(eq^#(t, t'), eq^#(l, l'))
  , eq^#(var(l), var(l')) -> c_2(eq^#(l, l'))
  , eq^#(apply(t, s), apply(t', s')) -> c_3(eq^#(t, t'), eq^#(s, s'))
  , eq^#(lambda(x, t), lambda(x', t')) ->
    c_4(eq^#(x, x'), eq^#(t, t'))
  , ren^#(x, y, apply(t, s)) -> c_5(ren^#(x, y, t), ren^#(x, y, s))
  , ren^#(x, y, lambda(z, t)) ->
    c_6(ren^#(x,
              y,
              ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)),
        ren^#(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t))
  , ren^#(var(l), var(k), var(l')) -> c_7(eq^#(l, l')) }
Weak Trs:
  { and(true(), y) -> y
  , and(false(), y) -> false()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(t, l)) -> false()
  , eq(cons(t, l), nil()) -> false()
  , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
  , eq(var(l), var(l')) -> eq(l, l')
  , eq(var(l), apply(t, s)) -> false()
  , eq(var(l), lambda(x, t)) -> false()
  , eq(apply(t, s), var(l)) -> false()
  , eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
  , eq(apply(t, s), lambda(x, t)) -> false()
  , eq(lambda(x, t), var(l)) -> false()
  , eq(lambda(x, t), apply(t, s)) -> false()
  , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
  , if(true(), var(k), var(l')) -> var(k)
  , if(false(), var(k), var(l')) -> var(l')
  , ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
  , ren(x, y, lambda(z, t)) ->
    lambda(var(cons(x, cons(y, cons(lambda(z, t), nil())))),
           ren(x,
               y,
               ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)))
  , ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l')) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..