Encore une autre question

Bonjour,
Pour la question 6.4 Le raffinage,
J'ai mis dans l'invariant:
size(profseq) <= maxprof & ran(profseq) = prof (comme vu en TD de spec1
avec M.HadjRabia)
alors qu'a la correction il est mis seulement ran(profseq) = prof
Ai-je quand même bon ?

Vous aviez le corrigé dans mon polycop page 189. J'y implante un ensemble de portes sur une suite injective. Et la preuve a été faite.

A voir

Ayant parcouru quelques copies ... j'ai mis un corrigé où il n'y a que la partie reliant la variable abstraite à la concrète ... pour avoir des points en plus. MAIS vous avez raison