Dimostrazione correttezza parziale

[Michele/96]

Ciao a tutti, di recente mi sono trovato di fronte al seguente esercizio:
Dimostrare per induzione su un opportuno parametro che, per ogni n >=
e' vero il predicato P(n) = "exTre(2^n) == n",
dove il metodo ricorsivo exTre e' definito da:

static int exTre(int n){
if (n > 1)
return 1 + exTre(n/2); // la divisione e' intera
else
return 0;
}

Io ho provato a risolverlo come segue e, dato che, penso sia quasi sicuramente sbagliato chiedo gentilmente a qualcuno di farmi notare gli errori:
Caso base: P(0)==exTre(2^0)==n''
// ==1+(0/2)==1==n''
Ipotesi induttiva: P(n+1)==exTre(2^(n+1))==n''
Dimostrazione: P(n+1)==1+(n+1)/2==1+(n/2)
// ==((n+2)/2)+(1/2)==(n+2)/2==P(n)
Mille grazie in anticipo per la risposta,
saluti.

[apatriarca]

Questo forum permette l'inserimento di formule e ti consiglio quindi di leggere la guida che trovi in alto per scoprire come fare. E' anche possibile inserire il codice in modo che mantenga la formattazione originale usando i tag [ code ] e [ /code ] (devi togliere gli spazi all'interno delle parentesi quadre e inserire il codice tra di loro).

Venendo al tuo problema. Se quella che hai scritto fosse una risposta ad un esame la troverei prima di tutto poco chiara e precisa. Forse è perché sono laureato in matematica, ma le formule vanno scritte in modo corretto. In particolare è sparito l'elevamento a potenza, nella ipotesi induttiva hai scritto alla fine n al posto di n+1 e nella dimostrazione alcuni passaggi non mi sono chiari.

Il caso base è corretto. Abbiamo infatti abbastanza chiaramente che:
\[ P(0) = \mathrm{exTre}(2^0) = \mathrm{exTre}(1) = 0. \]
La nostra ipotesi induttiva è che
\[ P(n) = n \implies P(n+1) = n+1 \quad (\forall n \geq 0) \].
Per dimostrarlo è sufficiente svolgere i calcoli. Infatti abbiamo che
\[ \begin{align*}
P(n+1) &= \mathrm{exTre}(2^{n+1}) = 1 +\mathrm{exTre}(2^{n+1}/2) \\
&= 1 + \mathrm{exTre}(2^{n+1-1}) = 1 + \mathrm{exTre}(2^n) = 1 + P(n) = 1 + n.
\end{align*} \]

[Michele/96]

Ti ringrazio per la risposta