Backward Chaining First Order Logic

Question

1. 0 ≤ 4
2. 5 ≤ 9
3. ∀x x ≤ x
4. ∀x x ≤ x + 0
5. ∀x x ≤ x + 0 ≤ x
6. ∀ x, y x + y ≤ y + x
7. ∀ w, x ,y ,z w ≤ y ᴧ x ≤ z => w + x ≤ y + z
8. ∀ x, y, z x ≤ y ᴧ y ≤ z => x ≤ z

How can these be used to derive 5 ≤ 4 + 9

i.e how can we start at the goal and go back to prove the goal?

The only statement that can be used in the first step is statement 7, but I cannot figure out how to work with the variable w

Answer 1

Using rule 7 with $w,x,y,z$ equalling $0,5,4,9$ respectively gives you $0+5\leq 4+9$, since rules 1 and 2 tell you that the hypothesis of 7 holds.

Using rule 8 with $x=0+5, y=5+0$ and $z=4+9$ tells you that you can rewrite to $5+0\leq4+9$, but only after rule 6 has confirmed that the hypothesis (that is, $0+5\leq5+0$) holds.

Now rules 5 and 8 let you strip away the $0$, and you're left with what you wanted to prove.