[Solved]: Proving Linear Time Temporal Logic formula □ ◊ f ⇔ ◊ □ f

Problem Detail: I am new to this topic, Linear Time Temporal Logic and I am trying to prove this equivalence — $BoxDiamond f Leftrightarrow DiamondBox f$ This is my take — Basic definitions: $(sigma, j) models Box f: forall k , [(k ge j) Rightarrow ((sigma, k) models f)]$ $(sigma, j) models Diamond f: exists k , [(k ge j) Rightarrow ((sigma, k) models f)]$ Here, $(sigma, j) models f$ means $sigma$ satisfies $f$ at $sigma(j)$, for more details about this syntax, please see here. Now the LHS: $begin{eqnarray} (sigma, j) models Box Diamond f & : & forall k , [(k ge j) Rightarrow ((sigma, k) models Diamond f)]\ & equiv & forall k , [(k ge j) Rightarrow [exists p , [(p ge k) Rightarrow ((sigma, p) models f)]]]\ & equiv & forall k , [(k<j) vee [exists p , [(p<k) vee ((sigma,p) models f)]]]\ & equiv & forall k , exists p , [(k<j) vee (p<k) vee ((sigma,p) models f)]\ & equiv & forall k , exists p , [(p<k<j) vee ((sigma,p) models f)]\ end{eqnarray} $ Again, the RHS: $begin{eqnarray} (sigma, j) models Diamond Box f & : & exists k , [(k ge j) Rightarrow ((sigma, k) models Box f)]\ & equiv & exists k , [(k ge j) Rightarrow [forall p , [(p ge k) Rightarrow ((sigma, p) models f)]]]\ & equiv & exists k , [(k<j) vee [forall p , [(p<k) vee ((sigma,p) models f)]]]\ & equiv & exists k , forall p , [(p<k<j) vee ((sigma,p) models f)]\ end{eqnarray} $ Now if we look at the last line of the both sides, the statement $forall k , exists p , [(p<k<j) vee ((sigma,p) models f)] equiv exists k , forall p , [(p<k<j) vee ((sigma,p) models f)]$ needs to be true to complete the proof, however intuitively, this is not true. What I am missing? How do I proceed? Any idea?

Asked By : ramgorur