MAYBE

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

Strict Trs:
  { and(false(), false()) -> false()
  , and(false(), true()) -> false()
  , and(true(), false()) -> false()
  , and(true(), true()) -> true()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(T, L)) -> false()
  , eq(cons(T, L), nil()) -> false()
  , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp))
  , eq(var(L), var(Lp)) -> eq(L, Lp)
  , 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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp))
  , eq(apply(T, S), lambda(X, Tp)) -> false()
  , eq(lambda(X, T), var(L)) -> false()
  , eq(lambda(X, T), apply(Tp, Sp)) -> false()
  , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp))
  , if(false(), var(K), var(L)) -> var(L)
  , if(true(), var(K), var(L)) -> var(K)
  , 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(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { and^#(false(), false()) -> c_1()
  , and^#(false(), true()) -> c_2()
  , and^#(true(), false()) -> c_3()
  , and^#(true(), true()) -> c_4()
  , eq^#(nil(), nil()) -> c_5()
  , eq^#(nil(), cons(T, L)) -> c_6()
  , eq^#(cons(T, L), nil()) -> c_7()
  , eq^#(cons(T, L), cons(Tp, Lp)) ->
    c_8(and^#(eq(T, Tp), eq(L, Lp)), eq^#(T, Tp), eq^#(L, Lp))
  , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp))
  , eq^#(var(L), apply(T, S)) -> c_10()
  , eq^#(var(L), lambda(X, T)) -> c_11()
  , eq^#(apply(T, S), var(L)) -> c_12()
  , eq^#(apply(T, S), apply(Tp, Sp)) ->
    c_13(and^#(eq(T, Tp), eq(S, Sp)), eq^#(T, Tp), eq^#(S, Sp))
  , eq^#(apply(T, S), lambda(X, Tp)) -> c_14()
  , eq^#(lambda(X, T), var(L)) -> c_15()
  , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16()
  , eq^#(lambda(X, T), lambda(Xp, Tp)) ->
    c_17(and^#(eq(T, Tp), eq(X, Xp)), eq^#(T, Tp), eq^#(X, Xp))
  , if^#(false(), var(K), var(L)) -> c_18()
  , if^#(true(), var(K), var(L)) -> c_19()
  , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S))
  , ren^#(X, Y, lambda(Z, T)) ->
    c_21(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(Lp)) ->
    c_22(if^#(eq(L, Lp), var(K), var(Lp)), eq^#(L, Lp)) }

and mark the set of starting terms.

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

Strict DPs:
  { and^#(false(), false()) -> c_1()
  , and^#(false(), true()) -> c_2()
  , and^#(true(), false()) -> c_3()
  , and^#(true(), true()) -> c_4()
  , eq^#(nil(), nil()) -> c_5()
  , eq^#(nil(), cons(T, L)) -> c_6()
  , eq^#(cons(T, L), nil()) -> c_7()
  , eq^#(cons(T, L), cons(Tp, Lp)) ->
    c_8(and^#(eq(T, Tp), eq(L, Lp)), eq^#(T, Tp), eq^#(L, Lp))
  , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp))
  , eq^#(var(L), apply(T, S)) -> c_10()
  , eq^#(var(L), lambda(X, T)) -> c_11()
  , eq^#(apply(T, S), var(L)) -> c_12()
  , eq^#(apply(T, S), apply(Tp, Sp)) ->
    c_13(and^#(eq(T, Tp), eq(S, Sp)), eq^#(T, Tp), eq^#(S, Sp))
  , eq^#(apply(T, S), lambda(X, Tp)) -> c_14()
  , eq^#(lambda(X, T), var(L)) -> c_15()
  , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16()
  , eq^#(lambda(X, T), lambda(Xp, Tp)) ->
    c_17(and^#(eq(T, Tp), eq(X, Xp)), eq^#(T, Tp), eq^#(X, Xp))
  , if^#(false(), var(K), var(L)) -> c_18()
  , if^#(true(), var(K), var(L)) -> c_19()
  , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S))
  , ren^#(X, Y, lambda(Z, T)) ->
    c_21(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(Lp)) ->
    c_22(if^#(eq(L, Lp), var(K), var(Lp)), eq^#(L, Lp)) }
Weak Trs:
  { and(false(), false()) -> false()
  , and(false(), true()) -> false()
  , and(true(), false()) -> false()
  , and(true(), true()) -> true()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(T, L)) -> false()
  , eq(cons(T, L), nil()) -> false()
  , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp))
  , eq(var(L), var(Lp)) -> eq(L, Lp)
  , 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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp))
  , eq(apply(T, S), lambda(X, Tp)) -> false()
  , eq(lambda(X, T), var(L)) -> false()
  , eq(lambda(X, T), apply(Tp, Sp)) -> false()
  , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp))
  , if(false(), var(K), var(L)) -> var(L)
  , if(true(), var(K), var(L)) -> var(K)
  , 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(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: and^#(false(), false()) -> c_1()
    , 2: and^#(false(), true()) -> c_2()
    , 3: and^#(true(), false()) -> c_3()
    , 4: and^#(true(), true()) -> c_4()
    , 5: eq^#(nil(), nil()) -> c_5()
    , 6: eq^#(nil(), cons(T, L)) -> c_6()
    , 7: eq^#(cons(T, L), nil()) -> c_7()
    , 8: eq^#(cons(T, L), cons(Tp, Lp)) ->
         c_8(and^#(eq(T, Tp), eq(L, Lp)), eq^#(T, Tp), eq^#(L, Lp))
    , 9: eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp))
    , 10: eq^#(var(L), apply(T, S)) -> c_10()
    , 11: eq^#(var(L), lambda(X, T)) -> c_11()
    , 12: eq^#(apply(T, S), var(L)) -> c_12()
    , 13: eq^#(apply(T, S), apply(Tp, Sp)) ->
          c_13(and^#(eq(T, Tp), eq(S, Sp)), eq^#(T, Tp), eq^#(S, Sp))
    , 14: eq^#(apply(T, S), lambda(X, Tp)) -> c_14()
    , 15: eq^#(lambda(X, T), var(L)) -> c_15()
    , 16: eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16()
    , 17: eq^#(lambda(X, T), lambda(Xp, Tp)) ->
          c_17(and^#(eq(T, Tp), eq(X, Xp)), eq^#(T, Tp), eq^#(X, Xp))
    , 18: if^#(false(), var(K), var(L)) -> c_18()
    , 19: if^#(true(), var(K), var(L)) -> c_19()
    , 20: ren^#(X, Y, apply(T, S)) ->
          c_20(ren^#(X, Y, T), ren^#(X, Y, S))
    , 21: ren^#(X, Y, lambda(Z, T)) ->
          c_21(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))
    , 22: ren^#(var(L), var(K), var(Lp)) ->
          c_22(if^#(eq(L, Lp), var(K), var(Lp)), eq^#(L, Lp)) }

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

Strict DPs:
  { eq^#(cons(T, L), cons(Tp, Lp)) ->
    c_8(and^#(eq(T, Tp), eq(L, Lp)), eq^#(T, Tp), eq^#(L, Lp))
  , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp))
  , eq^#(apply(T, S), apply(Tp, Sp)) ->
    c_13(and^#(eq(T, Tp), eq(S, Sp)), eq^#(T, Tp), eq^#(S, Sp))
  , eq^#(lambda(X, T), lambda(Xp, Tp)) ->
    c_17(and^#(eq(T, Tp), eq(X, Xp)), eq^#(T, Tp), eq^#(X, Xp))
  , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S))
  , ren^#(X, Y, lambda(Z, T)) ->
    c_21(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(Lp)) ->
    c_22(if^#(eq(L, Lp), var(K), var(Lp)), eq^#(L, Lp)) }
Weak DPs:
  { and^#(false(), false()) -> c_1()
  , and^#(false(), true()) -> c_2()
  , and^#(true(), false()) -> c_3()
  , and^#(true(), true()) -> c_4()
  , eq^#(nil(), nil()) -> c_5()
  , eq^#(nil(), cons(T, L)) -> c_6()
  , eq^#(cons(T, L), nil()) -> c_7()
  , eq^#(var(L), apply(T, S)) -> c_10()
  , eq^#(var(L), lambda(X, T)) -> c_11()
  , eq^#(apply(T, S), var(L)) -> c_12()
  , eq^#(apply(T, S), lambda(X, Tp)) -> c_14()
  , eq^#(lambda(X, T), var(L)) -> c_15()
  , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16()
  , if^#(false(), var(K), var(L)) -> c_18()
  , if^#(true(), var(K), var(L)) -> c_19() }
Weak Trs:
  { and(false(), false()) -> false()
  , and(false(), true()) -> false()
  , and(true(), false()) -> false()
  , and(true(), true()) -> true()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(T, L)) -> false()
  , eq(cons(T, L), nil()) -> false()
  , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp))
  , eq(var(L), var(Lp)) -> eq(L, Lp)
  , 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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp))
  , eq(apply(T, S), lambda(X, Tp)) -> false()
  , eq(lambda(X, T), var(L)) -> false()
  , eq(lambda(X, T), apply(Tp, Sp)) -> false()
  , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp))
  , if(false(), var(K), var(L)) -> var(L)
  , if(true(), var(K), var(L)) -> var(K)
  , 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(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) }
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^#(false(), false()) -> c_1()
, and^#(false(), true()) -> c_2()
, and^#(true(), false()) -> c_3()
, and^#(true(), true()) -> c_4()
, eq^#(nil(), nil()) -> c_5()
, eq^#(nil(), cons(T, L)) -> c_6()
, eq^#(cons(T, L), nil()) -> c_7()
, eq^#(var(L), apply(T, S)) -> c_10()
, eq^#(var(L), lambda(X, T)) -> c_11()
, eq^#(apply(T, S), var(L)) -> c_12()
, eq^#(apply(T, S), lambda(X, Tp)) -> c_14()
, eq^#(lambda(X, T), var(L)) -> c_15()
, eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16()
, if^#(false(), var(K), var(L)) -> c_18()
, if^#(true(), var(K), var(L)) -> c_19() }

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

Strict DPs:
  { eq^#(cons(T, L), cons(Tp, Lp)) ->
    c_8(and^#(eq(T, Tp), eq(L, Lp)), eq^#(T, Tp), eq^#(L, Lp))
  , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp))
  , eq^#(apply(T, S), apply(Tp, Sp)) ->
    c_13(and^#(eq(T, Tp), eq(S, Sp)), eq^#(T, Tp), eq^#(S, Sp))
  , eq^#(lambda(X, T), lambda(Xp, Tp)) ->
    c_17(and^#(eq(T, Tp), eq(X, Xp)), eq^#(T, Tp), eq^#(X, Xp))
  , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S))
  , ren^#(X, Y, lambda(Z, T)) ->
    c_21(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(Lp)) ->
    c_22(if^#(eq(L, Lp), var(K), var(Lp)), eq^#(L, Lp)) }
Weak Trs:
  { and(false(), false()) -> false()
  , and(false(), true()) -> false()
  , and(true(), false()) -> false()
  , and(true(), true()) -> true()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(T, L)) -> false()
  , eq(cons(T, L), nil()) -> false()
  , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp))
  , eq(var(L), var(Lp)) -> eq(L, Lp)
  , 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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp))
  , eq(apply(T, S), lambda(X, Tp)) -> false()
  , eq(lambda(X, T), var(L)) -> false()
  , eq(lambda(X, T), apply(Tp, Sp)) -> false()
  , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp))
  , if(false(), var(K), var(L)) -> var(L)
  , if(true(), var(K), var(L)) -> var(K)
  , 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(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) }
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(Tp, Lp)) ->
    c_8(and^#(eq(T, Tp), eq(L, Lp)), eq^#(T, Tp), eq^#(L, Lp))
  , eq^#(apply(T, S), apply(Tp, Sp)) ->
    c_13(and^#(eq(T, Tp), eq(S, Sp)), eq^#(T, Tp), eq^#(S, Sp))
  , eq^#(lambda(X, T), lambda(Xp, Tp)) ->
    c_17(and^#(eq(T, Tp), eq(X, Xp)), eq^#(T, Tp), eq^#(X, Xp))
  , ren^#(var(L), var(K), var(Lp)) ->
    c_22(if^#(eq(L, Lp), var(K), var(Lp)), eq^#(L, Lp)) }

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

Strict DPs:
  { eq^#(cons(T, L), cons(Tp, Lp)) -> c_1(eq^#(T, Tp), eq^#(L, Lp))
  , eq^#(var(L), var(Lp)) -> c_2(eq^#(L, Lp))
  , eq^#(apply(T, S), apply(Tp, Sp)) -> c_3(eq^#(T, Tp), eq^#(S, Sp))
  , eq^#(lambda(X, T), lambda(Xp, Tp)) ->
    c_4(eq^#(T, Tp), eq^#(X, Xp))
  , 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(Lp)) -> c_7(eq^#(L, Lp)) }
Weak Trs:
  { and(false(), false()) -> false()
  , and(false(), true()) -> false()
  , and(true(), false()) -> false()
  , and(true(), true()) -> true()
  , eq(nil(), nil()) -> true()
  , eq(nil(), cons(T, L)) -> false()
  , eq(cons(T, L), nil()) -> false()
  , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp))
  , eq(var(L), var(Lp)) -> eq(L, Lp)
  , 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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp))
  , eq(apply(T, S), lambda(X, Tp)) -> false()
  , eq(lambda(X, T), var(L)) -> false()
  , eq(lambda(X, T), apply(Tp, Sp)) -> false()
  , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp))
  , if(false(), var(K), var(L)) -> var(L)
  , if(true(), var(K), var(L)) -> var(K)
  , 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(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..