title: Using Hoare-Rules to show PRECONDITION implies POSTCONDITION in a simple program (just 2 assignments)
body: <p>Using the Hoare-Rules I want to show that I can imply</p>
  <pre><code>{x &gt;= 0} --&gt; {a + y = x} 
  </code></pre>
  <p>PROGRAMM</p>
  <pre><code>// PRECONDITION
  {x &gt;= 0}
  a = x; 
  y = 0;
  // POSTCONDITION
  {a + y = x}
  </code></pre>
  <p>Using the assignment rules I get</p>
  <pre><code>// PRECONDITION
  {x &gt;= 0}
  {x + 0 = x}   // assignment rule
  a = x; 
  {a + 0 = x}   // assignment rule
  y = 0;
  // POSTCONDITION
  {a + y = x}
  </code></pre>
  <p>To show</p>
  <pre><code>{x &gt;= 0} --&gt; {a + y = x} 
  </code></pre>
  <p>therefore I need to show in a last step</p>
  <pre><code>{x &gt;= 0} --&gt; {x + 0 = x} 
  </code></pre>
  <p>How can I show this or what is wrong in my proof?</p>