Montrer un invariant

Bonjour à tous,
Auriez-vous une idée comment montrer que l'invariant suivant est vrai, pour un tableau non trié, pour i= n/2 + 1 = 2^k-1

Code:

---

invariant 1 Pour tout i compris entre 1 et n, le sous-arbre de racine i est un tas.

---

Merci

Données : T , un tableau de n réels (la première case numérotée 1)
Résultat : T est modifié. Ne renvoie rien
//: étape 1 : transformation de T en tas
pour i de n/2 à 1 faire
Descente(i,T[1..n])
// étape 2 : tri. On extrait la racine du tas T [1..i] pour la mettre en T [i]
pour i de n à 1 faire
Échanger T [1] et T [i]
// équivaut à supprimer T [1] car i va décroître
Descente(1,T[1..i-1])

Code:

---

1 2 3 4 5 6 7 8

Procédure Descente(x : indice, T [1..b], un tableau de b réels ) Résultat : T est modifié. Ne renvoie rien début tant que 2x + 1 <= b et (T [x] < T [2x] ou T [x] < T [2x + 1]) faire si T [2x] > T [2x + 1] alors y = 2x sinon y = 2x + 1 Échanger T [x] et T [y] x=y fin

---