Axiome d'affectation en logique de Hoare ?

{P} x=E; {P[x:=E]} {P[x:=E]} x=E; {P} {P} x=E; {x=E} x=E => P Valider