Stutter bisimulation

In theoretical computer science, a stutter bisimulation is defined in a coinductive manner, as is bisimulation.
Let TS=(S,Act,→,I,AP,L) be a transition system. A stutter bisimulation for TS is
a binary relation R on S such that for all (s₁,s₂) which is in R:

1. L(s₁) = L(s₂).
2. If s₁^' is in Post(s₁) with (s₁^',s₂) is not in R,
   

then there exists a finite path fragment s₂u₁…u_ns₂^' with n≥0 and
(s₁,u_i) is in R, and (s₁^',s₂^') is in R.

1. If s₂^' is in Post(s₂) with (s₁,s₂^') is not in R,
   

then there exists a finite path fragment s₁v₁…v_ns₁^' with n≥0 and
(v_i,s₂) is in R, and (s₁^',s₂^') is in R.