YES Time: 0.052566 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)} DP: DP: { eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), 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 Lp) -> eq#(L, Lp), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp)} 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)} EDG: { (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp)) (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> eq#(L, Lp)) (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#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (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 Lp) -> eq#(L, Lp)) (ren#(X, Y, apply(T, S)) -> ren#(X, Y, S), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp))) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp))) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp))) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)) (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, 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, 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#(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#(var L, var K, var Lp) -> eq#(L, Lp)) (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 Lp) -> if#(eq(L, Lp), var K, var Lp)) (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 Lp) -> eq#(L, Lp)) (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 Lp) -> if#(eq(L, Lp), var K, var Lp)) } 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(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)} 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(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)} 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) = x0 + x1, [apply](x0, x1) = x0 + x1, [lambda](x0, x1) = x0 + 1, [var](x0) = 1, [false] = 1, [true] = 1, [nil] = 1, [ren#](x0, x1, x2) = x0 + x1 Strict: ren#(X, Y, lambda(Z, T)) -> ren#(Z, var cons(X, cons(Y, cons(lambda(Z, T), nil()))), T) 1 + 1T + 0X + 1Y + 0Z >= 1 + 1T + 0X + 0Y + 0Z ren#(X, Y, lambda(Z, T)) -> ren#(X, Y, ren(Z, var cons(X, cons(Y, cons(lambda(Z, T), nil()))), T)) 1 + 1T + 0X + 1Y + 0Z >= 0 + 1T + 0X + 1Y + 0Z ren#(X, Y, apply(T, S)) -> ren#(X, Y, S) 0 + 1T + 1S + 0X + 1Y >= 0 + 1S + 0X + 1Y ren#(X, Y, apply(T, S)) -> ren#(X, Y, T) 0 + 1T + 1S + 0X + 1Y >= 0 + 1T + 0X + 1Y Weak: EDG: {(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, 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)) (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#(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, 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#(Z, var cons(X, cons(Y, cons(lambda(Z, T), nil()))), T))} SCCS (1): 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#(Z, var cons(X, cons(Y, cons(lambda(Z, T), nil()))), T)} SCC (3): 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#(Z, var cons(X, cons(Y, cons(lambda(Z, T), nil()))), T)} Weak: { 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)} SPSC: Simple Projection: pi(ren#) = 2 Strict: { 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)} EDG: {(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, 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#(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))} SCCS (1): Scc: { 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)} SCC (2): Strict: { 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)} Weak: { 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)} SPSC: Simple Projection: pi(ren#) = 2 Strict: {ren#(X, Y, lambda(Z, T)) -> ren#(Z, var cons(X, cons(Y, cons(lambda(Z, T), nil()))), T)} EDG: {(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))} 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(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)} SPSC: Simple Projection: pi(ren#) = 2 Strict: {} Qed SCC (7): Strict: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)} Weak: { 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)} SPSC: Simple Projection: pi(eq#) = 1 Strict: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)} EDG: {(eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))} SCCS (1): Scc: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)} SCC (6): Strict: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp)} Weak: { 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)} SPSC: Simple Projection: pi(eq#) = 1 Strict: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)} EDG: {(eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))} SCCS (1): Scc: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)} SCC (5): Strict: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp)} Weak: { 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)} SPSC: Simple Projection: pi(eq#) = 1 Strict: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)} EDG: {(eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))} SCCS (1): Scc: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)} SCC (4): Strict: { eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp)} Weak: { 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)} SPSC: Simple Projection: pi(eq#) = 1 Strict: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)} EDG: {(eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))} SCCS (1): Scc: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)} SCC (3): Strict: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp)} Weak: { 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)} SPSC: Simple Projection: pi(eq#) = 1 Strict: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)} EDG: {(eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)) (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))} SCCS (1): Scc: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)} SCC (2): Strict: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp)} Weak: { 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)} SPSC: Simple Projection: pi(eq#) = 1 Strict: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)} EDG: {(eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))} SCCS (1): Scc: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)} SCC (1): Strict: {eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp)} Weak: { 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)} SPSC: Simple Projection: pi(eq#) = 1 Strict: {} Qed