Je ne comprends pas à quoi sert le z dans la règle 13 (ADD 2) car il n'est pas réutilisé dans la conclusion.