1. On commence par mettre les assertions c'est assez facile.
      static int f(int x) {
            int r ;
    // ∀ x. P(x,f(x))
            if (x > 100) {
    // x > 100
          r = x-10 ;
    // x > 100 ∧ r = x-10
        }     else {
    // x ≤ 100 ∧ ∀ x. P(x,f(x))
          r = f(f(x+11)) ;
    // x ≤ 100 ∧ r = 91
        }
    // P(x,r)
            return r ;
      }
    Le passage difficile est de x ≤ 100 ∧ ∀ x. P(x,f(x)) à x ≤ 100 ∧ r = 91. Par instanciantion (remplacer x par x+11) on a
    f(x+11) = if x+11 > 100 then x+11-10 else 91
    D'où il vient, par quelques calculs et par f(if e then et else ef) égal à if e then f(et) else f(ef)
    f(f(x+11)) = if x > 89 then f(x+1) else f(91)
    On instancie deux fois ∀ x. P(x,f(x)) un fois par x+1 et l'autre par 91.
    f(f(x+11)) = if x > 89 then (if x+1 > 100  then   x+1-10  else 91) else 91
    Soit en tenant compte enfin de l'hypothèse x ≤ 100.
    f(f(x+11)) = if x > 89 then (if x=100  then   100+1-10  else 91) else 91


  2. Il faut donc montrer x+11 ≺ x et f(x+11) ≺ x sous l'hypothèse x ≤ 100.

    La propriété x+11 ≺ x est facile par définition de l'ordre, et ceci nous donne le droit d'utiliser la proposition P(x+11,f(x+11)), dans le sens que nous savons maintenant que f termine pour l'argument x+11.