Proof step 3 from proof rg2-sound-main-unfair (previous step)

User applied rule step

And obtained the following new goals

• Proof step 4:

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

• Proof step 6:

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

Rule argument

Additional information