Dans ce rapport, nous proposons une preuve de confluence générique qui poura être instanciée pour les différents calculs. Pour cela, nous nous intéresserons au lambda-calcul dynamique qui axiomatise la manière dont l'abstraction est réduite. Nous utilisons cette preuve pour l'étendre au cas où le filtrage est fait modulo une théorie, ici la commutativité. Intuitivement il faut que le filtrage soit stable par substitution, par réduction et par équivalence. Nous caractérisons aussi une classe d'algorithmes de filtrage qui conduisent à des calculs non confluents.