LTL to Omega Automata, substitution of x by /var_phi in /phi

Question

Let's take [(Fa) SU b] into consideration, seen on slide 70 (printed version).

When calculating SU, we have to replace /var_phi in /phi by q. Later this q is moved to the initial states.

We were wondering how this substitution is done ( we don't know where exactly the 'x' appears and how this results into 'q')

Answer 1

I guess that your question refers to the following rules: 

The Φ<α>x means that we consider a formula Φ that may have several occurrences of a subformula α. To denote some of these, we consider a stub/template of Φ where the occurrences of interest are replaced with a new variable x. 

For example, let Φ be the formula (Fa)⋁¬(Fa) that has two occurrences of the subformula Fa. We consider it now as a substitution of variable x in formula x⋁¬x by formula Fa, so Φ=(Fa)⋁¬(Fa), α=Fa. But you may also consider x⋁¬(Fa) and just replace the first occurrence of Fa (for whatever reason).

When we abbreviate one subformula, we can replace this way also other occurrences of the same subformula with the new abbreviation variable, and calling them x, we can control which of them should be abbreviated.

So, you can decide which of the occurrences you want to call x, means you want to replace with the new abbreviation this way. Ideally, all of them, but sometimes you may not want this.