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