YES
Time: 0.346122
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')}
DP:
DP:
{ eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')),
eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
eq#(var l, var l') -> eq#(l, l'),
eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')),
eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')),
eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'),
ren#(x, y, apply(t, s)) -> ren#(x, y, t),
ren#(x, y, apply(t, s)) -> ren#(x, y, s),
ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)),
ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t),
ren#(var l, var k, var l') -> eq#(l, l'),
ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l')}
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')}
EDG:
{
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(var l, var l') -> eq#(l, l'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(eq#(var l, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(eq#(var l, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(eq#(var l, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(eq#(var l, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(eq#(var l, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(eq#(var l, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(eq#(var l, var l') -> eq#(l, l'), eq#(var l, var l') -> eq#(l, l'))
(eq#(var l, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(eq#(var l, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(eq#(var l, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(ren#(x, y, lambda(z, t)) -> 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'))
(ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(var l, var k, var l') -> eq#(l, l'))
(ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
(ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
(ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
(ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(var l, var l') -> eq#(l, l'))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l'))
(ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(var l, var k, var l') -> eq#(l, l'))
(ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
(ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
(ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
(ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(var l, var l') -> eq#(l, l'))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(var l, var l') -> eq#(l, l'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(var l, var l') -> eq#(l, l'))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
(ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
(ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
(ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
(ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(var l, var k, var l') -> eq#(l, l'))
(ren#(x, y, lambda(z, t)) -> 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'))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(var l, var l') -> eq#(l, l'))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(ren#(var l, var k, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(var l, var l') -> eq#(l, l'))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
(eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
(ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
(ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
(ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
(ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
(ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(var l, var k, var l') -> eq#(l, l'))
(ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l'))
}
STATUS:
arrows: 0.593750
SCCS (2):
Scc:
{ ren#(x, y, apply(t, s)) -> ren#(x, y, t),
ren#(x, y, apply(t, s)) -> ren#(x, y, s),
ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)),
ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)}
Scc:
{ eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
eq#(var l, var l') -> eq#(l, l'),
eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
SCC (4):
Strict:
{ ren#(x, y, apply(t, s)) -> ren#(x, y, t),
ren#(x, y, apply(t, s)) -> ren#(x, y, s),
ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)),
ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)}
Weak:
{ 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')}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[if](x0, x1, x2) = x0,
[ren](x0, x1, x2) = x0,
[and](x0, x1) = x0 + 1,
[eq](x0, x1) = x0 + 1,
[cons](x0, x1) = 0,
[apply](x0, x1) = x0 + x1 + 1,
[lambda](x0, x1) = x0 + 1,
[var](x0) = 1,
[true] = 1,
[false] = 1,
[nil] = 1,
[ren#](x0, x1, x2) = x0 + x1 + 1
Strict:
ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)
2 + 1y + 1t + 0x + 0z >= 2 + 0y + 1t + 0x + 0z
ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
2 + 1y + 1t + 0x + 0z >= 1 + 1y + 1t + 0x + 0z
ren#(x, y, apply(t, s)) -> ren#(x, y, s)
2 + 1y + 1t + 1s + 0x >= 1 + 1y + 1s + 0x
ren#(x, y, apply(t, s)) -> ren#(x, y, t)
2 + 1y + 1t + 1s + 0x >= 1 + 1y + 1t + 0x
Weak:
ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')
1 + 0l + 0l' + 0k >= 1 + 0l + 0l' + 0k
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)))
1 + 0y + 1t + 0x + 0z >= 1 + 0y + 1t + 0x + 0z
ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
1 + 0y + 1t + 1s + 0x >= 1 + 0y + 1t + 1s + 0x
if(false(), var k, var l') -> var l'
1 + 0l' + 0k >= 1 + 0l'
if(true(), var k, var l') -> var k
1 + 0l' + 0k >= 1 + 0k
eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
2 + 1t + 0t' + 0x + 0x' >= 2 + 0t + 0t' + 1x + 0x'
eq(lambda(x, t), apply(t, s)) -> false()
2 + 1t + 0s + 0x >= 1
eq(lambda(x, t), var l) -> false()
2 + 1t + 0l + 0x >= 1
eq(apply(t, s), lambda(x, t)) -> false()
2 + 1t + 1s + 0x >= 1
eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
2 + 1t + 0t' + 1s + 0s' >= 2 + 1t + 0t' + 0s + 0s'
eq(apply(t, s), var l) -> false()
2 + 1t + 0l + 1s >= 1
eq(var l, lambda(x, t)) -> false()
2 + 0t + 0l + 0x >= 1
eq(var l, apply(t, s)) -> false()
2 + 0t + 0l + 0s >= 1
eq(var l, var l') -> eq(l, l')
2 + 0l + 0l' >= 1 + 1l + 0l'
eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
1 + 0t + 0l + 0t' + 0l' >= 2 + 1t + 0l + 0t' + 0l'
eq(cons(t, l), nil()) -> false()
1 + 0t + 0l >= 1
eq(nil(), cons(t, l)) -> false()
2 + 0t + 0l >= 1
eq(nil(), nil()) -> true()
2 >= 1
and(false(), y) -> false()
2 + 0y >= 1
and(true(), y) -> y
2 + 0y >= 1y
SCCS (1):
Scc:
{ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)}
SCC (1):
Strict:
{ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)}
Weak:
{ 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')}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[if](x0, x1, x2) = 1,
[ren](x0, x1, x2) = 0,
[and](x0, x1) = x0 + 1,
[eq](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1,
[apply](x0, x1) = 1,
[lambda](x0, x1) = x0 + 1,
[var](x0) = 0,
[true] = 1,
[false] = 1,
[nil] = 1,
[ren#](x0, x1, x2) = x0
Strict:
ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)
1 + 0y + 1t + 0x + 0z >= 0 + 0y + 1t + 0x + 0z
Weak:
ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')
0 + 0l + 0l' + 0k >= 1 + 0l + 0l' + 0k
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)))
0 + 0y + 0t + 0x + 0z >= 1 + 0y + 0t + 0x + 0z
ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
0 + 0y + 0t + 0s + 0x >= 1 + 0y + 0t + 0s + 0x
if(false(), var k, var l') -> var l'
1 + 0l' + 0k >= 0 + 0l'
if(true(), var k, var l') -> var k
1 + 0l' + 0k >= 0 + 0k
eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
2 + 1t + 0t' + 0x + 0x' >= 2 + 0t + 0t' + 1x + 0x'
eq(lambda(x, t), apply(t, s)) -> false()
2 + 1t + 0s + 0x >= 1
eq(lambda(x, t), var l) -> false()
2 + 1t + 0l + 0x >= 1
eq(apply(t, s), lambda(x, t)) -> false()
2 + 0t + 0s + 0x >= 1
eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
2 + 0t + 0t' + 0s + 0s' >= 2 + 1t + 0t' + 0s + 0s'
eq(apply(t, s), var l) -> false()
2 + 0t + 0l + 0s >= 1
eq(var l, lambda(x, t)) -> false()
1 + 0t + 0l + 0x >= 1
eq(var l, apply(t, s)) -> false()
1 + 0t + 0l + 0s >= 1
eq(var l, var l') -> eq(l, l')
1 + 0l + 0l' >= 1 + 1l + 0l'
eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
1 + 1t + 1l + 0t' + 0l' >= 2 + 1t + 0l + 0t' + 0l'
eq(cons(t, l), nil()) -> false()
1 + 1t + 1l >= 1
eq(nil(), cons(t, l)) -> false()
2 + 0t + 0l >= 1
eq(nil(), nil()) -> true()
2 >= 1
and(false(), y) -> false()
2 + 0y >= 1
and(true(), y) -> y
2 + 0y >= 1y
Qed
SCC (7):
Strict:
{ eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
eq#(var l, var l') -> eq#(l, l'),
eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
Weak:
{ 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')}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[if](x0, x1, x2) = x0 + 1,
[ren](x0, x1, x2) = x0 + x1 + x2,
[and](x0, x1) = x0 + 1,
[eq](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1,
[apply](x0, x1) = x0 + x1,
[lambda](x0, x1) = x0 + x1 + 1,
[var](x0) = x0,
[true] = 1,
[false] = 1,
[nil] = 1,
[eq#](x0, x1) = x0
Strict:
eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')
1 + 0t + 1t' + 0x + 1x' >= 0 + 0x + 1x'
eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t')
1 + 0t + 1t' + 0x + 1x' >= 0 + 0t + 1t'
eq#(apply(t, s), apply(t', s')) -> eq#(s, s')
0 + 0t + 1t' + 0s + 1s' >= 0 + 0s + 1s'
eq#(apply(t, s), apply(t', s')) -> eq#(t, t')
0 + 0t + 1t' + 0s + 1s' >= 0 + 0t + 1t'
eq#(var l, var l') -> eq#(l, l')
0 + 0l + 1l' >= 0 + 0l + 1l'
eq#(cons(t, l), cons(t', l')) -> eq#(l, l')
0 + 0t + 0l + 1t' + 1l' >= 0 + 0l + 1l'
eq#(cons(t, l), cons(t', l')) -> eq#(t, t')
0 + 0t + 0l + 1t' + 1l' >= 0 + 0t + 1t'
Weak:
ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')
0 + 1l + 1l' + 1k >= 2 + 1l + 0l' + 0k
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)))
1 + 1y + 1t + 1x + 1z >= 5 + 3y + 3t + 3x + 3z
ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
0 + 1y + 1t + 1s + 1x >= 0 + 2y + 1t + 1s + 2x
if(false(), var k, var l') -> var l'
2 + 0l' + 0k >= 0 + 1l'
if(true(), var k, var l') -> var k
2 + 0l' + 0k >= 0 + 1k
eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
2 + 1t + 0t' + 1x + 0x' >= 2 + 0t + 0t' + 1x + 0x'
eq(lambda(x, t), apply(t, s)) -> false()
2 + 1t + 0s + 1x >= 1
eq(lambda(x, t), var l) -> false()
2 + 1t + 0l + 1x >= 1
eq(apply(t, s), lambda(x, t)) -> false()
1 + 1t + 1s + 0x >= 1
eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
1 + 1t + 0t' + 1s + 0s' >= 2 + 1t + 0t' + 0s + 0s'
eq(apply(t, s), var l) -> false()
1 + 1t + 0l + 1s >= 1
eq(var l, lambda(x, t)) -> false()
1 + 0t + 1l + 0x >= 1
eq(var l, apply(t, s)) -> false()
1 + 0t + 1l + 0s >= 1
eq(var l, var l') -> eq(l, l')
1 + 1l + 0l' >= 1 + 1l + 0l'
eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
1 + 1t + 1l + 0t' + 0l' >= 2 + 1t + 0l + 0t' + 0l'
eq(cons(t, l), nil()) -> false()
1 + 1t + 1l >= 1
eq(nil(), cons(t, l)) -> false()
2 + 0t + 0l >= 1
eq(nil(), nil()) -> true()
2 >= 1
and(false(), y) -> false()
2 + 0y >= 1
and(true(), y) -> y
2 + 0y >= 1y
SCCS (1):
Scc:
{ eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
eq#(var l, var l') -> eq#(l, l'),
eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
SCC (5):
Strict:
{ eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
eq#(var l, var l') -> eq#(l, l'),
eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
eq#(apply(t, s), apply(t', s')) -> eq#(s, s')}
Weak:
{ 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')}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[if](x0, x1, x2) = x0 + 1,
[ren](x0, x1, x2) = x0 + x1 + x2 + 1,
[and](x0, x1) = x0 + 1,
[eq](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1,
[apply](x0, x1) = x0 + x1 + 1,
[lambda](x0, x1) = 1,
[var](x0) = x0,
[true] = 1,
[false] = 1,
[nil] = 1,
[eq#](x0, x1) = x0
Strict:
eq#(apply(t, s), apply(t', s')) -> eq#(s, s')
1 + 0t + 1t' + 0s + 1s' >= 0 + 0s + 1s'
eq#(apply(t, s), apply(t', s')) -> eq#(t, t')
1 + 0t + 1t' + 0s + 1s' >= 0 + 0t + 1t'
eq#(var l, var l') -> eq#(l, l')
0 + 0l + 1l' >= 0 + 0l + 1l'
eq#(cons(t, l), cons(t', l')) -> eq#(l, l')
0 + 0t + 0l + 1t' + 1l' >= 0 + 0l + 1l'
eq#(cons(t, l), cons(t', l')) -> eq#(t, t')
0 + 0t + 0l + 1t' + 1l' >= 0 + 0t + 1t'
Weak:
ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')
1 + 1l + 1l' + 1k >= 2 + 1l + 0l' + 0k
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)))
2 + 1y + 0t + 1x + 0z >= 1 + 0y + 0t + 0x + 0z
ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
2 + 1y + 1t + 1s + 1x >= 3 + 2y + 1t + 1s + 2x
if(false(), var k, var l') -> var l'
2 + 0l' + 0k >= 0 + 1l'
if(true(), var k, var l') -> var k
2 + 0l' + 0k >= 0 + 1k
eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
2 + 0t + 0t' + 0x + 0x' >= 2 + 0t + 0t' + 1x + 0x'
eq(lambda(x, t), apply(t, s)) -> false()
2 + 0t + 0s + 0x >= 1
eq(lambda(x, t), var l) -> false()
2 + 0t + 0l + 0x >= 1
eq(apply(t, s), lambda(x, t)) -> false()
2 + 1t + 1s + 0x >= 1
eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
2 + 1t + 0t' + 1s + 0s' >= 2 + 1t + 0t' + 0s + 0s'
eq(apply(t, s), var l) -> false()
2 + 1t + 0l + 1s >= 1
eq(var l, lambda(x, t)) -> false()
1 + 0t + 1l + 0x >= 1
eq(var l, apply(t, s)) -> false()
1 + 0t + 1l + 0s >= 1
eq(var l, var l') -> eq(l, l')
1 + 1l + 0l' >= 1 + 1l + 0l'
eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
1 + 1t + 1l + 0t' + 0l' >= 2 + 1t + 0l + 0t' + 0l'
eq(cons(t, l), nil()) -> false()
1 + 1t + 1l >= 1
eq(nil(), cons(t, l)) -> false()
2 + 0t + 0l >= 1
eq(nil(), nil()) -> true()
2 >= 1
and(false(), y) -> false()
2 + 0y >= 1
and(true(), y) -> y
2 + 0y >= 1y
SCCS (1):
Scc:
{eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
eq#(var l, var l') -> eq#(l, l')}
SCC (3):
Strict:
{eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
eq#(var l, var l') -> eq#(l, l')}
Weak:
{ 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')}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[if](x0, x1, x2) = x0 + 1,
[ren](x0, x1, x2) = x0 + x1 + 1,
[and](x0, x1) = x0 + 1,
[eq](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1,
[apply](x0, x1) = 1,
[lambda](x0, x1) = x0 + x1 + 1,
[var](x0) = x0 + 1,
[true] = 1,
[false] = 1,
[nil] = 1,
[eq#](x0, x1) = x0
Strict:
eq#(var l, var l') -> eq#(l, l')
1 + 0l + 1l' >= 0 + 0l + 1l'
eq#(cons(t, l), cons(t', l')) -> eq#(l, l')
0 + 0t + 0l + 1t' + 1l' >= 0 + 0l + 1l'
eq#(cons(t, l), cons(t', l')) -> eq#(t, t')
0 + 0t + 0l + 1t' + 1l' >= 0 + 0t + 1t'
Weak:
ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')
3 + 0l + 1l' + 1k >= 2 + 0l + 1l' + 0k
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)))
2 + 1y + 1t + 0x + 1z >= 9 + 3y + 3t + 2x + 2z
ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
2 + 1y + 0t + 0s + 0x >= 1 + 0y + 0t + 0s + 0x
if(false(), var k, var l') -> var l'
2 + 1l' + 0k >= 1 + 1l'
if(true(), var k, var l') -> var k
2 + 1l' + 0k >= 1 + 1k
eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
2 + 1t + 0t' + 1x + 0x' >= 2 + 0t + 0t' + 1x + 0x'
eq(lambda(x, t), apply(t, s)) -> false()
2 + 1t + 0s + 1x >= 1
eq(lambda(x, t), var l) -> false()
2 + 1t + 0l + 1x >= 1
eq(apply(t, s), lambda(x, t)) -> false()
2 + 0t + 0s + 0x >= 1
eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
2 + 0t + 0t' + 0s + 0s' >= 2 + 1t + 0t' + 0s + 0s'
eq(apply(t, s), var l) -> false()
2 + 0t + 0l + 0s >= 1
eq(var l, lambda(x, t)) -> false()
2 + 0t + 1l + 0x >= 1
eq(var l, apply(t, s)) -> false()
2 + 0t + 1l + 0s >= 1
eq(var l, var l') -> eq(l, l')
2 + 1l + 0l' >= 1 + 1l + 0l'
eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
1 + 1t + 1l + 0t' + 0l' >= 2 + 1t + 0l + 0t' + 0l'
eq(cons(t, l), nil()) -> false()
1 + 1t + 1l >= 1
eq(nil(), cons(t, l)) -> false()
2 + 0t + 0l >= 1
eq(nil(), nil()) -> true()
2 >= 1
and(false(), y) -> false()
2 + 0y >= 1
and(true(), y) -> y
2 + 0y >= 1y
SCCS (1):
Scc:
{eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l')}
SCC (2):
Strict:
{eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
eq#(cons(t, l), cons(t', l')) -> eq#(l, l')}
Weak:
{ 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')}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[if](x0, x1, x2) = x0 + 1,
[ren](x0, x1, x2) = x0 + 1,
[and](x0, x1) = x0 + 1,
[eq](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[apply](x0, x1) = 1,
[lambda](x0, x1) = 1,
[var](x0) = 1,
[true] = 1,
[false] = 1,
[nil] = 1,
[eq#](x0, x1) = x0
Strict:
eq#(cons(t, l), cons(t', l')) -> eq#(l, l')
1 + 0t + 0l + 1t' + 1l' >= 0 + 0l + 1l'
eq#(cons(t, l), cons(t', l')) -> eq#(t, t')
1 + 0t + 0l + 1t' + 1l' >= 0 + 0t + 1t'
Weak:
ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')
2 + 0l + 0l' + 0k >= 2 + 0l + 0l' + 0k
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)))
2 + 0y + 0t + 0x + 0z >= 1 + 0y + 0t + 0x + 0z
ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
2 + 0y + 0t + 0s + 0x >= 1 + 0y + 0t + 0s + 0x
if(false(), var k, var l') -> var l'
2 + 0l' + 0k >= 1 + 0l'
if(true(), var k, var l') -> var k
2 + 0l' + 0k >= 1 + 0k
eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
2 + 0t + 0t' + 0x + 0x' >= 2 + 0t + 0t' + 1x + 0x'
eq(lambda(x, t), apply(t, s)) -> false()
2 + 0t + 0s + 0x >= 1
eq(lambda(x, t), var l) -> false()
2 + 0t + 0l + 0x >= 1
eq(apply(t, s), lambda(x, t)) -> false()
2 + 0t + 0s + 0x >= 1
eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
2 + 0t + 0t' + 0s + 0s' >= 2 + 1t + 0t' + 0s + 0s'
eq(apply(t, s), var l) -> false()
2 + 0t + 0l + 0s >= 1
eq(var l, lambda(x, t)) -> false()
2 + 0t + 0l + 0x >= 1
eq(var l, apply(t, s)) -> false()
2 + 0t + 0l + 0s >= 1
eq(var l, var l') -> eq(l, l')
2 + 0l + 0l' >= 1 + 1l + 0l'
eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
2 + 1t + 1l + 0t' + 0l' >= 2 + 1t + 0l + 0t' + 0l'
eq(cons(t, l), nil()) -> false()
2 + 1t + 1l >= 1
eq(nil(), cons(t, l)) -> false()
2 + 0t + 0l >= 1
eq(nil(), nil()) -> true()
2 >= 1
and(false(), y) -> false()
2 + 0y >= 1
and(true(), y) -> y
2 + 0y >= 1y
Qed