Robinson Arithmetic is order-adequate

In chapter 9, Peter Smith defines the following concept: A theory T that captures the relation ≤ is order-adequate if it satisfies the following nine properties:

• O1: T ⊢ ∀x (0 ≤ x)
• O2: For any n, T ⊢ ∀x ((x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n) → x ≤ n)
• O3: For any n, T ⊢ ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
• O4: For any n, if T ⊢ φ(0) and T ⊢ φ(1) and ... and T ⊢ φ(n) then T ⊢ (∀x ≤ n)φ(x)
• O5: For any n, if T ⊢ φ(0) or T ⊢ φ(1) or ... or T ⊢ φ(n) then T ⊢ (∃x ≤ n)φ(x)
• O6: For any n, T ⊢ ∀x (x ≤ n → x ≤ Sn)
• O7: For any n, T ⊢ ∀x (n ≤ x  → (n = x  ∨ Sn ≤ x))
• O8: For any n, T ⊢ ∀x (x ≤ n ∨ n ≤ x)
• O9: For any n>0, T ⊢ (∀x ≤ n-1)φ(x) → (∀x ≤ n)(x ≠ n → φ(x))

Then, we have the following theorem:

Robinson Arithmetic (or Q) is order-adequate.

Smith proves that Q satisfies a few of the 9 properties above, namely O1, O2, O3, and O8. Below, I attempt to prove a few of the other properties.

Proof of O4: Assume that n is an arbitrary natural number.

1. Assume that a is an arbitrary term of Q such that a ≤ n
2. Using O3: ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
3. a ≤ n → (a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n) [by universal instantiation]
4. a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n [modus ponens 1&3]
5. Sub-proof by cases: 
• According to 4, a is equal to one of the terms in {0,1,2,..., n}
• In all cases, Q ⊢ φ(a) [hypothesis of O4]
• Therefore Q ⊢ φ(a)
6. Q ⊢ a ≤ n → φ(a) [discharging assumption 1]
7. Q ⊢ ∀x (x ≤ n → φ(x)) [by universal generalization]
8. Q ⊢ (∀x ≤ n) φ(x) [by definition of the bounded universal quantifier]

Proof of O5: Assume that n is an arbitrary natural number.

1. There is at least one numeral a such that Q ⊢ φ(a) [hypothesis of O5]
2. Q ⊢ a ≤ n [since 'the number denoted by a' ≤ n and Q captures ≤]
3. Q ⊢ a ≤ n ∧ φ(a) [conjunction of 1 and 2]
4. Q ⊢ ∃x (x ≤ n ∧ φ(x)) [existential generalization]
5. Q ⊢ (∃x ≤ n) φ(x) [by definition of the bounded existential quantifier]

Proof of O6: Assume that n is an arbitrary natural number.

1. Assume (inside Q) that a is an arbitrary term such that a ≤ n
2. Using O3: ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
3. a ≤ n → (a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n) [by universal instantiation]
4. a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n [modus ponens 1&3]
5. a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n ∨ a = Sn [added disjunct to 4]
6. Using O2:  ∀x ((x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n ∨ x = Sn) → x ≤ Sn)
7. (a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n ∨ a = Sn) → a ≤ Sn [by universal instantiation]
8. a ≤ Sn [modus ponens 5&7]
9. a ≤ n → a ≤ Sn [discharging assumption 1]
10. ∀x (x ≤ n → x ≤ Sn) [universal generalization]