Hi,

I have a doubt regarding LO2 ,

F[a WU b] to LO2 formula. The answer for this is given :

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

But i got,

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

I'm not sure how can we give the time.

What i have is ,

we have: Fa = ∃t1. t0≤t1 ∧ a[t1]

so F[a WU b] = ∃t1. t0≤t1 ∧ [a WU b][t1]

[a WU b] = ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) → a[t1]), but we are starting from the time t1, so i replaced the time accordingly.

And finally

F[a WU b]= ∃t1. t0≤t1 ∧ (∀t2. (t1≤t2 ∧ (∀t3. (t1≤t3 ∧ t3≤t2 → ¬b[t3])) → a[t2]))

but timing are little bit different from tool and what i got. Could you please help on this, how can i give the time?