| [:S | Boolvar ::- [PL S = s21 ∧ ¬ Boolvar until ¬ R1(pm, S', S'')] ∥ false ::- [PL S = s20]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), N = N'' + 1 until Boolvar, \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ R1(pm, S', S'') ∧ 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) ∧ Pre1(pm, s) ∧ Pre2(pm, s) ∧ I(pm, S) ∧ I(pm, s) → false, n = N + 1, R2(pm, s2, S), I(pm, s3), I(pm, s2), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), G2(pm, s2, s2), G1(pm, s2, s3), R2(pm, s2, s3), R1(pm, s2, s2), I(pm, S), ¬ R2(pm, s2, s20), ¬ R1(pm, s3, s21), boolvar1 → s2 = s3 ∧ ¬ boolvar0 ∧ N + 1 = n0 ⊦ |