Использование правил Хоара для отображения ПРЕДУСЛОВИЯ подразумевает ПОСТУСЛОВИЕ в простой программе (всего 2 задания)

Используя правила Хоара, я хочу показать, что могу подразумевать

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

ПРОГРАММА

// 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} 

Как я могу показать это или что не так в моем доказательстве?