Well, there are many ways how you can solve this. As I can see, you used the sum automaton to compute the disjunction of the two automata, and then you translated the result to LO2. That is fine.
However, you do not need the sum automaton here. The disjunction of universal automata is dual to the conjunction of existential automata, and for the latter, the simple product automaton would be sufficient. Hence, you don't need an additional state variable.
I would have solved it as follows without modifying the automata:
∀p.
(
(∀t1. (t0≤t1 → (∃t0. t1<t0 ∧ (∀t2. (t1<t2 → t0≤t2)) ∧ p[t0]) ∧ p[t1] ∧ a[t1]))
→
(∀t1. (t0≤t1 → ¬p[t1]))
)
∨ ∀q.q[t0]
