In linear time logic, is $\mathbf{GF}p$ equivalent to $ \mathbf{G}p$ ?
$\mathbf{GF}p$ means that it is always the case that p is true eventually.
Let $\mathbf{G} p$ be defined as: $\forall j \ge0,\ p$ holds in the suffix $q_j, q_{j+1}, q_{j+2},\ldots$
and since: formula $φ$ holds for state machine $M$ if $φ$ holds for all possible traces of $M$
Isn't $\mathbf{G}$ in $\mathbf{GF}p$ redundant then?