With templates, I meant the formulas that are generated in the recursive calls of algorithm Tp2Od on slide 48 in Chapter VRS-08-PredLogic.

For instance, consider the given formula where I have done some irrelevant variable renaming (since that form came out of my tool):

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

Looking at the above formula, we can clearly see that ∀t1. (t0≤t1 → a[t1] ∧ b[t1]) stems from G(a&b) applied at time t0, hence, we may now consider with alpha(t0) := ∀t1. (t0≤t1 → a[t1] ∧ b[t1]) the following formula:

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

Again, (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ alpha(t0)) is the template of a SU operator with arguments ¬a and alpha, so that the above formula means with beta(t1) = ∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ alpha(t0)

∃t1. t0≤t1 ∧ beta(t1)

The above means F beta (applied at time t0), and thus

F[¬a SU G(a&b)]