Proof step 6 from proof no-init-violation-left (previous step)

User applied rule step

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information