Symbolic Computation of Predecessors

Question

In this question for computing the universal predecessors, I do not understand how in highlight 1: (p' XOR q') was omitted (it is not present in the next step)

and in highlight 2: p' was omitted.

Can someone please explain? 

Answer 1

Doubt 1: (p' xor q') is equivalent to !(p'<->q'), so when we multiply out, we get

    (((p<->q) | (p' xor q')) & ((p<->q')|(p' xor q))&(p'<->q'))
    <->
    (
     (p<->q) & ((p<->q')|(p' xor q))&(p'<->q')
    |(p' xor q') & ((p<->q')|(p' xor q)) & (p'<->q')
    )
    <->
     (p<->q) & ((p<->q')|(p' xor q))&(p'<->q')

Note that (p' xor q') & (...) & (p'<->q') is just false.

Doubt 2: 

    exists q'. (p<->q) & ((p<->q')|(p' xor q)) & (p'<->q')
    <-> (p<->q) & ((p<->0)|(p' xor q)) & (p'<->0)
      | (p<->q) & ((p<->1)|(p' xor q)) & (p'<->1)
    <-> (p<->q) & (!p|(p' xor q)) & !p'
      | (p<->q) & ( p|(p' xor q)) &  p'
    <-> (p<->q) & (!p|(0 xor q)) & !p'
      | (p<->q) & ( p|(1 xor q)) &  p'
    <-> (p<->q) & (!p| q) & !p'
      | (p<->q) & ( p|!q) &  p'

p' was omitted because of φ ∧ x ⇔ φ[x<-1] ∧ x and φ ∧ ¬x ⇔ φ[x<-0] ∧ x (see page 69 on the Chapter on transition systems where the symbolic computation of predecessors and successors is explained with this trick.