LTL to L01 - Clarification regarding solution

Question

To Convert [(X a) SU (F b)] to L01, 

I solved on my own and I got solution which is similar to the one generated in the teaching tool.

(∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → (∃t0. t2<t0 ∧ (∀t1. (t2<t1 → t0≤t1)) ∧ a[t0]))) ∧ (∃t0. t1≤t0 ∧ b[t0]))) 

However The exam solution contains a different answer and I am wondering is that a shortened version of the solution?(2017.02 Paper)

Answer 1

It seems that both solutions are similar, the example solution evaluates the formula at time 0 while yours starts at a general time t0. Based on that the bound variables are renamed, but then the formulas are the same, right?

Comments

Yes, now I get it. Thank you for clarifying.