我要证明我可以暗示使用Hoare-Rules

{x >=0} --> {a+y=x} 
 




PROGRAMM
 
 // PRECONDITION
 {x >=0}
     a = x; 
     y = 0;
 // POSTCONDITION
 {a+y=x} 
 

使用我得到的分配规则

// PRECONDITION
 {x >=0}
     {x+0 = x}   // assignment rule
     a = x; 
     {a + 0 = x} // assignment rule
     y = 0;
 // POSTCONDITION
 {a+y=x}

显示

{x >=0} --> {a+y=x} 

因此，我需要在最后一步中显示

{x >=0} --> {x+0 = x} 

我该如何证明这一点或我的证明有什么不对？

谢谢