Proof step 7 from proof fair-always-left-rely (previous step)

User applied rule step

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information