| N = N'' + 1 until (P(pm, S) ∨ last), [:S | [PL S = s1 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ [PL S = s4]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, P, G1, Post2, s, G2, Pre1, Post1, I, Pre2. N < n → □ (R1(pm, S', S'') ∧ R2(pm, S', S'')) ∧ [: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'))]] ∧ 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) → ¬ N = N'' +1 until (P(pm, S) ∨ last), n = N + 1, I(pm, s2), I(pm, s3), R1(pm, s2, S), R2(pm, s3, S), R1(pm, s3, S), P-restr(pm, P, I, R1), Pre2(pm, s), Pre1(pm, s), stable(pm, I, R2), stable(pm, I, R1), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s2, s2), R1(pm, s2, s3), I(pm, S), ¬ P(pm, s2), ¬ R1(pm, s2, s1), ¬ R2(pm, s3, s4), boolvar → s2 = s3 ∧ N + 1 = n0 ⊦ |