VRS Exam [February 17, 2021], Problem 8e

Question

I tried solving it as follows:

A([d U 0] ∧ F [d U b]) 

= A(Gd ∧ F [d U b]) 

= A(Gd ∧ (FGd ∨ Fb)) 

= A ( (Gd ∧ FGd) ∨ (Gd ∧ Fb))

= A (Gd ∨ (Gd ∧ Fb))    {s.t FGd = Gd}

Why are we avoiding (Gd ∧ Fb)?

The solution provided is as follows:

1) A([d U 0] ∧ F [d U b]) 

2) A(Gd ∧ F [d U b]) 

3) A(Gd ∧ (FGd ∨ Fb)) 

4) AGd

From Step 3  to Step 4, how is
Gd ∧ (FGd ∨ Fb) = Gd  ?

Answer 1

Well for:

Gd ∧ (FGd ∨ Fb)

to hold, it is clear that Gd needs to hold. However Gd directly implies that FGd also holds due to:

Gd => FGd

so if Gd holds, FGd holds too and thus we don't need to care about the Fb part. That's the reason why the whole term reduces to Gd.