Proof step 7 from proof no-progress-left (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s3), ¬ P(pm, s2), ¬ R1(pm, s3, s0), ¬ boolvar1 ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 12:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s1 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s4]], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), ¬ P(pm, s2), ¬ R1(pm, s2, s1), ¬ R2(pm, s3, s4) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 14:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s5 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s6 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s6), ¬ P(pm, s2), ¬ R1(pm, s2, s5) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 18:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s7 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s3), R1(pm, s3, s7), ¬ P(pm, s2), ¬ boolvar1 ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 23:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s8 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s9]], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s8), G2(pm, s2, s3), ¬ P(pm, s2), ¬ R2(pm, s3, s9) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 27:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s10 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s11 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s10), G2(pm, s2, s3), R2(pm, s3, s11), ¬ P(pm, s2) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 32:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s12 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s3), ¬ boolvar, ¬ R1(pm, s3, s12), ¬ boolvar1 ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 36:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s13 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s14]], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), ¬ boolvar, ¬ R1(pm, s2, s13), ¬ R2(pm, s3, s14) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 38:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s15 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s16 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s16), ¬ boolvar, ¬ R1(pm, s2, s15) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 42:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s17 ∧ ¬ 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'))] ], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s3), R1(pm, s3, s17), ¬ boolvar, ¬ boolvar1 ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 46:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s18 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s19] ], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s18), G2(pm, s2, s3), ¬ boolvar, ¬ R2(pm, s3, s19) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 50:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s20 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s21 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s20), G2(pm, s2, s3), R2(pm, s3, s21), ¬ boolvar ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 54:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s22]], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, ¬ boolvar, G2(pm, s2, s3), ¬ R2(pm, s3, s22), ¬ boolvar1 ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 58:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s24 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s23]], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), ¬ R2(pm, s2, s23), ¬ P(pm, s2), ¬ R1(pm, s3, s24) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 60:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s26 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s25]], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), R1(pm, s3, s26), ¬ R2(pm, s2, s25), ¬ P(pm, s2) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 64:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s28 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s27]], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), ¬ R2(pm, s2, s27), ¬ boolvar, ¬ R1(pm, s3, s28) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 66:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s30 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s29] ], 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), R1(pm, s3, s30), ¬ R2(pm, s2, s29), ¬ boolvar ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 70:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s31 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, ¬ boolvar, G2(pm, s2, s3), R2(pm, s3, s31), ¬ boolvar1 ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 74:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s33 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s32 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s32), G1(pm, s2, s3), ¬ P(pm, s2), ¬ R1(pm, s3, s33) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 78:

  □ (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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s34), G1(pm, s2, s3), R1(pm, s3, s35), ¬ P(pm, s2) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 83:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s37 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s36 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s36), G1(pm, s2, s3), ¬ boolvar, ¬ R1(pm, s3, s37) ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

• Proof step 87:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s39 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s38 ∧ 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), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s38), G1(pm, s2, s3), R1(pm, s3, s39), ¬ boolvar ⊦ ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last), ◇ □ (¬ P(pm, S) ∧ ¬ last)

Rule argument

Additional information