We have a FSM: =(2Vin,2Vout,φ,2Vstate,φ)A=(2Vin,2Vout,φI,2Vstate,φR), where Vin={a}Vin={a}, Vout={o}Vout={o}, Vstate={p,q}Vstate={p,q}, φ=p∨qφI=p∨q, φ=φR=((a->next(p)&(q|p))<->next(q))&o

How to compute the existential predecessors of **!(q->a) **step by step?