# Why does (y < 10) imply everywhere (x > 0 ^ y < 10)?

My lecturer recently released solutions to an assignment. One of the questions was to determine the weakest precondition of:

{y < 10} if (x > 0 OR y < 10) -> y:=10 fi {true}


According to the provided solution, the weakest precondition of the selection command

(x > 0 OR y < 10) -> y:=10


is

(x > 0 OR y < 10)


I understand how the weakest predicate was arrived at, but why does the solution then state that the total assertion is true because

 (y < 10) IMPLIES EVERYWHERE (x > 0 OR y < 10)


Isn't y < 10 weaker than (x > 0 OR y < 10)? Therefore, there are potential precondition states where y < 10 but x !> 0. Since the program doesn't have guards for such a condition, it then aborts.

• " v " stands for or, the upside down " v " stands for and. So your title is wrong, inside the question it's correct. – gnasher729 Aug 14 '17 at 19:02

I'm an idiot.

Of course (y < 10) implies (x > 0 OR y < 10). I was somehow mistaking OR for AND. I'm dumb.

• You're not dumb, you just need to learn to sit on your hands for 5 minutes before you post to stackexchange. – Andrej Bauer Jun 15 '17 at 15:44
• @AndrejBauer, story of my life – Covvar Aug 14 '17 at 21:36