Completar de forma apropiada la lineas punteadas de la siguiente de dem de correctitud

problema maximo3(a,b,c:Z) == res : Bool {
asegura res == max(a,max(b,c));
}

int maximo·(int a, int b, int c)
{
int r;
//estado E1
if(a < b)
{
if(b < c) r = c;
else r = b;
}

else
{
if(a < c) r = c;
else r = a;
}
//vale r = = max(a,max(b,c))
return r;
//vale ...;
}

Estos son mis intentos de resolución
caso en el que la guarda de if(a < b) es True


caso en el que la guarda de if(a < b) es False


caso en el que la guarda de if(b<c) es True