transition le_bateau_traverse ()
requires { V = True }
{
Bateau_droite := case
		| Bateau_droite=True : False
		| _ : True;
V := False;
}