| □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s35 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s34 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, \A ∀ N, R1, pm, S, R2, Boolvar, P, Post1, s, G1, Post2, G2, Pre1, I, Pre2. N < n → □ (R1(pm, S', S'') ∧ R2(pm, S', S'')) ∧ N = N'' +1 until Boolvar ∧ [:S | Boolvar ::- [PL ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ stable(pm, I, R1) ∧ stable(pm, I, R2) ∧ I(pm, S) ∧ Pre1(pm, s) ∧ Pre2(pm, s) ∧ P-restr(pm, P, I, R1) → ◇ □ (¬ P(pm, S) ∧ ¬ last), R2(pm, s2, S), I(pm, s2), I(pm, s3), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), G2(pm, s2, s2), R2(pm, s2, s34), G1(pm, s2, s3), R1(pm, s3, s35), R2(pm, s2, s3), R1(pm, s2, s2), I(pm, s34), I(pm, s35), I(pm, S), ¬ P(pm, s2), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0 ⊦ ◇ □ (¬ P(pm, S) ∧ ¬ last), □ (¬ P(pm, S) ∧ ¬ last), [:S | [PL □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]] |