interpretations
TIMEOUT
We are left with following problem, upon which TcT provides the
certificate TIMEOUT.
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:
TIMEOUT
Computation stopped due to timeout after 20.0 seconds.
Arrrr..
lmpo
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(cons(t, l), nil()) -> false()
, eq(nil(), cons(t, l)) -> 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(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), 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))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
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(cons(t, l), nil()) -> false()
, eq(nil(), cons(t, l)) -> 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(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), 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))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
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(cons(t, l), nil()) -> false()
, eq(nil(), cons(t, l)) -> 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(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), 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))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
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(cons(t, l), nil()) -> false()
, eq(nil(), cons(t, l)) -> 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(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), 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))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..