[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 9 from proof fair-always-left-rely (previous step)

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

User applied rule case distinction

And obtained the following new goals

Proof step 10:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s0] ∥ false ::- [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s3), ¬ R1(pm, s3, s0), ¬ boolvar1 ⊦
Proof step 14:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s1] ∥ false ::- [PL S = s4]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s1), ¬ R2(pm, s3, s4) ⊦
Proof step 16:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s5] ∥ false ::- [PL S = s6 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s6), ¬ R1(pm, s2, s5) ⊦
Proof step 20:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s7 ∧ ¬ Boolvar until ¬ R1(pm, S', S'')] ∥ false ::- [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s3), ¬ boolvar, ¬ R1(pm, s3, s7), ¬ boolvar1 ⊦
Proof step 24:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s8 ∧ ¬ Boolvar until ¬ R1(pm, S', S'')] ∥ false ::- [PL S = s9]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), ¬ boolvar, ¬ R1(pm, s2, s8), ¬ R2(pm, s3, s9) ⊦
Proof step 26:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s10 ∧ ¬ Boolvar until ¬ R1(pm, S', S'')] ∥ false ::- [PL S = s11 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s11), ¬ boolvar, ¬ R1(pm, s2, s10) ⊦
Proof step 30:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s12 ∧ ¬ 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'))] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s3), R1(pm, s3, s12), ¬ boolvar, ¬ boolvar1 ⊦
Proof step 34:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s13 ∧ ¬ Boolvar until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s14] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s13), G2(pm, s2, s3), ¬ boolvar, ¬ R2(pm, s3, s14) ⊦
Proof step 38:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s15 ∧ ¬ Boolvar until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s16 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s15), G2(pm, s2, s3), R2(pm, s3, s16), ¬ boolvar ⊦
Proof step 42:
boolvar ∨ n = N + 1 ∧ 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 S = s17]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, ¬ boolvar, G2(pm, s2, s3), ¬ R2(pm, s3, s17), ¬ boolvar1 ⊦
Proof step 46:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s19] ∥ false ::- [PL S = s18]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), ¬ R2(pm, s2, s18), ¬ R1(pm, s3, s19) ⊦
Proof step 48:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s21 ∧ ¬ Boolvar until ¬ R1(pm, S', S'')] ∥ false ::- [PL S = s20]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), ¬ R2(pm, s2, s20), ¬ boolvar, ¬ R1(pm, s3, s21) ⊦
Proof step 50:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s23 ∧ ¬ Boolvar until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s22] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), R1(pm, s3, s23), ¬ R2(pm, s2, s22), ¬ boolvar ⊦
Proof step 54:
boolvar ∨ n = N + 1 ∧ 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 S = s24 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, ¬ boolvar, G2(pm, s2, s3), R2(pm, s3, s24), ¬ boolvar1 ⊦
Proof step 58:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s26] ∥ false ::- [PL S = s25 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s25), G1(pm, s2, s3), ¬ R1(pm, s3, s26) ⊦
Proof step 62:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s28 ∧ ¬ Boolvar until ¬ R1(pm, S', S'')] ∥ false ::- [PL S = s27 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s27), G1(pm, s2, s3), ¬ boolvar, ¬ R1(pm, s3, s28) ⊦
Proof step 66:
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, [:S | Boolvar ::- [PL S = s30 ∧ ¬ Boolvar until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ false ::- [PL S = s29 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, Boolvar, 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 ¬ 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, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s29), G1(pm, s2, s3), R1(pm, s3, s30), ¬ boolvar ⊦

Rule argument

pos: left 3

Additional information

Used simplifier rules: r1-refl: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ ¬ R1(pm, s, s) ∧ I(pm, s) → false;%g2-r1: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ G2(pm, s, s0) ∧ I(pm, s) → R1(pm, s, s0);