Proof step 41 from proof fair-sustains-implies-always (previous step)

User applied rule step

And obtained the following new goals

• Proof step 42:

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

Rule argument

Additional information