Φ = F([a SU b] | G a)
Step 1: Tp2Od(t0, F([a SU b] | G a)), which is FΦ
Ψ := ∃t1. t0≤t1 ∧ Φ ;
ΨA := ∃t1. t1≤t0 ∧ ([a SU b] | G a) ;
Step 2: Tp2Od(t0, [a SU b] | G a), which is ϕ ∨ ψ
Ψ := Tp2Od(t0, [a SU b]) ∨ Tp2Od(t0, G a);
Step 3: Tp2Od(t0, [a SU b]), which is [ϕ SU ψ]
Ψ := ∃t1. t0 ≤ t1 ∧ Tp2Od(t1, b) ∧ interval((t0, 1,t1, 0), a)
Tp2Od(t1, b) = b(t1)
interval((t0, 1,t1, 0), a) = ∀t2. t0 ≤ t2 ∧ t2 < t1 → Tp2Od(t2, a);
Tp2Od(t2, a) = a(t2)
ΨB := ∃t1. t0 ≤ t1 ∧ b(t1) ∧ ∀t2. t0 ≤ t2 ∧ t2 < t1 →a(t2)
Step 4: Tp2Od(t0, G a), which is Gϕ
Ψ := ∀t1. t0 ≤ t1 ∧ Φ
ΨC:= ∀t1. t0≤ t1 ∧ a(t0)
Step 5: Combining all :
ΨA ∧ (ΨB ∨ ΨC)(t0)
My final solution is :
∃t1. t0≤t1 ∧ ((∃t1. t0 ≤ t1 ∧ b(t1) ∧ ∀t2. t0 ≤ t2 ∧ t2 < t1 →a(t2) )∨ (∀t1. t0≤ t1 ∧ a(t0)))
Is this formula in reduced form? Or are they different? I am not sure how to give the numbering for "t".
∃t1. (
(∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2])) ∧ b[t0]) ∨
(∀t0. (t1≤t0 → a[t0]))) ∧ t0≤t1