[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 6 from proof no-progress-left (previous step)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 7:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, G1(pm, s2, s3) ∧ ¬ P(pm, s2) ∧ ¬ R1(pm, s3, s0) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ P(pm, s2) ∧ ¬ R1(pm, s2, s1) ∧ ¬ R2(pm, s3, s4) ∧ [:S | Boolvar ::- [PL S = s1 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s4]] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s6) ∧ ¬ P(pm, s2) ∧ ¬ R1(pm, s2, s5) ∧ [:S | Boolvar ::- [PL S = s5 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s6 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]] ∨ G1(pm, s2, s3) ∧ R1(pm, s3, s7) ∧ ¬ P(pm, s2) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL S = s7 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G1(pm, s2, s2) ∧ R1(pm, s2, s8) ∧ G2(pm, s2, s3) ∧ ¬ P(pm, s2) ∧ ¬ R2(pm, s3, s9) ∧ [:S | Boolvar ::- [PL S = s8 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s9]] ∨ G1(pm, s2, s2) ∧ R1(pm, s2, s10) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s11) ∧ ¬ P(pm, s2) ∧ [:S | Boolvar ::- [PL S = s10 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s11 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G1(pm, s2, s3) ∧ ¬ boolvar ∧ ¬ R1(pm, s3, s12) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL S = s12 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ boolvar ∧ ¬ R1(pm, s2, s13) ∧ ¬ R2(pm, s3, s14) ∧ [:S | Boolvar ::- [PL S = s13 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s14]] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s16) ∧ ¬ boolvar ∧ ¬ R1(pm, s2, s15) ∧ [:S | Boolvar ::- [PL S = s15 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s16 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G1(pm, s2, s3) ∧ R1(pm, s3, s17) ∧ ¬ boolvar ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL S = s17 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ 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'))] ] ∨ G1(pm, s2, s2) ∧ R1(pm, s2, s18) ∧ G2(pm, s2, s3) ∧ ¬ boolvar ∧ ¬ R2(pm, s3, s19) ∧ [:S | Boolvar ::- [PL S = s18 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s19] ] ∨ G1(pm, s2, s2) ∧ R1(pm, s2, s20) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s21) ∧ ¬ boolvar ∧ [:S | Boolvar ::- [PL S = s20 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s21 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ ¬ R2(pm, s3, s22) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s22] ] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ ¬ R2(pm, s2, s23) ∧ ¬ P(pm, s2) ∧ ¬ R1(pm, s3, s24) ∧ [:S | Boolvar ::- [PL S = s24 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s23]] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s26) ∧ ¬ R2(pm, s2, s25) ∧ ¬ P(pm, s2) ∧ [:S | Boolvar ::- [PL S = s26 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s25]] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ ¬ R2(pm, s2, s27) ∧ ¬ boolvar ∧ ¬ R1(pm, s3, s28) ∧ [:S | Boolvar ::- [PL S = s28 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s27]] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s30) ∧ ¬ R2(pm, s2, s29) ∧ ¬ boolvar ∧ [:S | Boolvar ::- [PL S = s30 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s29] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s31) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s31 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s32) ∧ G1(pm, s2, s3) ∧ ¬ P(pm, s2) ∧ ¬ R1(pm, s3, s33) ∧ [:S | Boolvar ::- [PL S = s33 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s32 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s34) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s35) ∧ ¬ P(pm, s2) ∧ [:S | Boolvar ::- [PL S = s35 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ false ::- [PL S = s34 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s36) ∧ G1(pm, s2, s3) ∧ ¬ boolvar ∧ ¬ R1(pm, s3, s37) ∧ [:S | Boolvar ::- [PL S = s37 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last)] ∥ false ::- [PL S = s36 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s38) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s39) ∧ ¬ boolvar ∧ [:S | Boolvar ::- [PL S = s39 ∧ ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s38 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], \A ∀ N, R1, pm, S, R2, Boolvar, P, Post1, s, G1, Post2, G2, Pre1, I, Pre2. N < n → □ (R1(pm, S', S'') ∧ R2(pm, S', S'')) ∧ N = N'' +1 until Boolvar ∧ [:S | Boolvar ::- [PL ¬ Boolvar until □ (¬ P(pm, S) ∧ ¬ last) ∧ 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) ∧ stable(pm, I, R1) ∧ stable(pm, I, R2) ∧ I(pm, S) ∧ Pre1(pm, s) ∧ Pre2(pm, s) ∧ P-restr(pm, P, I, R1) → ◇ □ (¬ P(pm, S) ∧ ¬ last), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), R1(pm, s3, S), R2(pm, s3, S), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0 ⊦ ◇ □ (¬ P(pm, S) ∧ ¬ last), ¬ P(pm, s2) ∧ □ (¬ P(pm, S) ∧ ¬ last)

Rule argument

Additional information

Used simplifier rules: succ: ⊦ m +1 = m + 1; from specification nat-basic2