9.9 Suppose you are given the following axioms:
1. 0 ≤ 3.
2. 7 ≤ 9.
3.∀x x≤x.
4.∀x x≤x+0.
5.∀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

Give a backward-chaining proof of the sentence 7 ≤ 3 + 9. (Be sure, of course, to use only the axioms given here, not anything else you may know about arithmetic.) Show only the steps that leads to success, not the irrelevant steps.

Query: 7 ≤ 3 + 9
7:  w=0, x=7, y=3, z=9
	0 ≤ 3 ^ 7 ≤ 9 => 0 + 7 ≤ 3 + 9
Goal: 0 ≤ 3 ^ 7 ≤ 9
1: 0 ≤ 3 == True
Goal: True ^ 7 ≤ 9
2: 7 ≤ 9 == True
True ^ True => (0 + 7 ≤ 3 + 9 == True)

Give a forward-chaining proof of the sentence 7 ≤ 3 + 9. Again, show only the steps that lead to success.

Query: 7 ≤ 3 + 9