Proof step 5 from proof rg-blocked1-not-r1-term-unfair (previous step)

User applied rule step

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information