[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 progress-left (previous step)

□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), P(pm, s2) ∧ Post1(pm, s, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s2) ∧ □ (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∨ P(pm, s2) ∧ Post1(pm, s, s2) ∧ R1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ □ (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∨ G1(pm, s2, s3) ∧ ¬ R1(pm, s3, s0) ∧ ¬ boolvar ∧ [:S | [PL S = s0 ∧ □ ◇ P(pm, S)] ∥ [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 | [PL S = s1 ∧ □ ◇ P(pm, S)] ∥ [PL S = s4]] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s6) ∧ ¬ R1(pm, s2, s5) ∧ [:S | [PL S = s5 ∧ □ ◇ P(pm, S)] ∥ [PL S = s6 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]] ∨ G1(pm, s2, s3) ∧ R1(pm, s3, s7) ∧ ¬ boolvar ∧ [:S | [PL S = s7 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [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) ∧ ¬ R2(pm, s3, s9) ∧ [:S | [PL S = s8 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s9]] ∨ G1(pm, s2, s2) ∧ R1(pm, s2, s10) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s11) ∧ [:S | [PL S = s10 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s11 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ Post2(pm, s, s2) ∧ G1(pm, s2, s3) ∧ ¬ R2(pm, s2, s2) ∧ □ ◇ P(pm, S) ∧ □ (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∨ G2(pm, s2, s3) ∧ ¬ R2(pm, s3, s12) ∧ ¬ boolvar ∧ [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s12]] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ ¬ R2(pm, s2, s13) ∧ ¬ R1(pm, s3, s14) ∧ [:S | [PL S = s14 ∧ □ ◇ P(pm, S)] ∥ [PL S = s13]] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s16) ∧ ¬ R2(pm, s2, s15) ∧ [:S | [PL S = s16 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s15]] ∨ Post2(pm, s, s2) ∧ R2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ □ ◇ P(pm, S) ∧ □ (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∨ G2(pm, s2, s3) ∧ R2(pm, s3, s17) ∧ ¬ boolvar ∧ [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s17 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s18) ∧ G1(pm, s2, s3) ∧ ¬ R1(pm, s3, s19) ∧ [:S | [PL S = s19 ∧ □ ◇ P(pm, S)] ∥ [PL S = s18 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s20) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s21) ∧ [:S | [PL S = s21 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s20 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0 ⊦

User applied rule case distinction

And obtained the following new goals

Proof step 7:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), □ (last ⊃ Post2(pm, s, S);G2(pm, S, S')), ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, P(pm, s2), Post1(pm, s, s2), R1(pm, s2, s2), G2(pm, s2, s3) ⊦
Proof step 13:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s0 ∧ □ ◇ P(pm, S)] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G1(pm, s2, s3), ¬ R1(pm, s3, s0), ¬ boolvar ⊦
Proof step 17:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s1 ∧ □ ◇ P(pm, S)] ∥ [PL S = s4]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s1), ¬ R2(pm, s3, s4) ⊦
Proof step 19:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s5 ∧ □ ◇ P(pm, S)] ∥ [PL S = s6 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s6), ¬ R1(pm, s2, s5) ⊦
Proof step 23:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s7 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G1(pm, s2, s3), R1(pm, s3, s7), ¬ boolvar ⊦
Proof step 31:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s8 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s9]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s8), G2(pm, s2, s3), ¬ R2(pm, s3, s9) ⊦
Proof step 35:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s10 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s11 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G1(pm, s2, s2), R1(pm, s2, s10), G2(pm, s2, s3), R2(pm, s3, s11) ⊦
Proof step 43:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s12]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G2(pm, s2, s3), ¬ R2(pm, s3, s12), ¬ boolvar ⊦
Proof step 47:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s14 ∧ □ ◇ P(pm, S)] ∥ [PL S = s13]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), ¬ R2(pm, s2, s13), ¬ R1(pm, s3, s14) ⊦
Proof step 49:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s16 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s15]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G2(pm, s2, s2), G1(pm, s2, s3), R1(pm, s3, s16), ¬ R2(pm, s2, s15) ⊦
Proof step 53:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s17 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G2(pm, s2, s3), R2(pm, s3, s17), ¬ boolvar ⊦
Proof step 61:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s19 ∧ □ ◇ P(pm, S)] ∥ [PL S = s18 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s18), G1(pm, s2, s3), ¬ R1(pm, s3, s19) ⊦
Proof step 65:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s21 ∧ □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL S = s20 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], ¬ P(pm, s2) ∧ ¬ ◇ P(pm, S) ∨ n = N + 1 ∧ N = N'' + 1 until ¬ ◇ P(pm, S), \A ∀ N, P, pm, S, Post1, s, G1, R1, Post2, G2, R2, Pre1, I, Pre2. N < n → [:S | [PL □ ◇ P(pm, S) ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ∧ □ (R1(pm, S', S'') ∧ R2(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) → ¬ N = N'' +1 until ¬ ◇ P(pm, S), 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), boolvar → s2 = s3 ∧ n = n0, G2(pm, s2, s2), R2(pm, s2, s20), G1(pm, s2, s3), R1(pm, s3, s21) ⊦

Rule argument

pos: left 3

Additional information

Used simplifier rules: r2-refl: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ ¬ R2(pm, s, s) ∧ I(pm, s) → false; (forward) from specification RG-I-2-Theory%g1-r2: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ G1(pm, s, s0) ∧ I(pm, s) → R2(pm, s, s0); (forward) from specification RG-I-2-Theory%r1-refl: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ ¬ R1(pm, s, s) ∧ I(pm, s) → false; (forward) from specification RG-I-2-Theory%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); (forward) from specification RG-I-2-Theory