Hier matin, l'intuition me vint : ce problème est EXPTIME-dur, je rédigeai donc la preuve dans l'après-midi.

Je suis bien évidemment encore infichu de montrer qu'il est NEXPTIME-dur (non, la preuve pour EXPTIME ne fonctionne plus si je remplace la machine déterministe par une non-déterministe, ce serait trop simple jeune impudent), Mais je ne sais pas si c'est NEXPTIME-dur, en fait. C'est un peu cela la différence entre la recherche et les examens : dans ces derniers, a priori, les résultats à démontrer sont vrais (et démontrables en pas trop d'étapes).

PS Je commence à soupçonner une complexité intermédiaire... Je peux montrer qu'un problème voisin de celui que j'étudie est NEXPTIME-complet, mais celui-ci met en jeu plus de « choix » tandis que le mien a une sorte de propriété de monotonie !