Bonsoir tout le monde, en espérant que vous soyez bien.
Je travaille sur un exo où il faut prouver la décidabilité d'un problème qui est une variante du problème de Prost mais plus simple.
Voici l'énonce:

calc1.PNG

et voici la question:

calc2.png

J'ai pensé à ça:
Pour prouver la décidabilité on va chercher un algorithme qui rend "oui" (s'il y a une dérivation) ou "non" (dans le cas contraire).
Puisque cette dérivation peut être d'ordre fini quelconque, je doute que cet algorithme soit itératif mais je pense à un algorithme récursif ?!
Ca sera très gentil de votre part si vous pouvez m'aider car je suis dans une vraie impasse ...
Merci