[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 60 from proof rg2-sound-main-unfair (previous step)

[:S | [PL S = s19] ∥nf [PL S = s18 ∧ 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 < n → [: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')), n = N + 1, R2(pm, s2, S), I(pm, s3), I(pm, s2), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s), G2(pm, s2, s2), R2(pm, s2, s18), G1(pm, s2, s3), R1(pm, s3, S), R2(pm, s3, S), R2(pm, s2, s3), R1(pm, s2, s2), I(pm, s18), I(pm, S), ¬ R1(pm, s3, s19), boolvar → s2 = s3 ∧ N + 1 = n0 ⊦ (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'))

User applied rule insert lemma

And obtained the following new goals

Proof step 61:
[:S | [PL S = s] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s1, S);G2(pm, S, S'))]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), R1(pm, s0, S), ¬ R1(pm, s0, s), I(pm, s0), Pre1(pm, s1), Pre2(pm, s1) ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s1, S) ∧ Post2(pm, s1, S);G1(pm, S, S') ∨ G2(pm, S, S'))
Proof step 62:
[:S | [PL S = s19] ∥nf [PL S = s18 ∧ 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 < n → [: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')), n = N + 1, R2(pm, s2, S), I(pm, s3), I(pm, s2), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s), G2(pm, s2, s2), R2(pm, s2, s18), G1(pm, s2, s3), R1(pm, s3, S), R2(pm, s3, S), R2(pm, s2, s3), R1(pm, s2, s2), I(pm, s18), I(pm, S), ¬ R1(pm, s3, s19), boolvar → s2 = s3 ∧ N + 1 = n0 ⊦ [:S | [PL S = s19] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, 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'))
Proof step 63:
(R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')), [:S | [PL S = s19] ∥nf [PL S = s18 ∧ 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 < n → [: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')), n = N + 1, R2(pm, s2, S), I(pm, s3), I(pm, s2), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s), G2(pm, s2, s2), R2(pm, s2, s18), G1(pm, s2, s3), R1(pm, s3, S), R2(pm, s3, S), R2(pm, s2, s3), R1(pm, s2, s2), I(pm, s18), I(pm, S), ¬ R1(pm, s3, s19), boolvar → s2 = s3 ∧ N + 1 = n0 ⊦ (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

spec: inst: name: rg-blocked1-not-r1-unfair seq: [:S | [PL S = s] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s1, S);G2(pm, S, S')) ] ], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), R1(pm, s0, S), ¬ R1(pm, s0, s), I(pm, s0), Pre1(pm, s1), Pre2(pm, s1) ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s1, S) ∧ Post2(pm, s1, S) ;G1(pm, S, S') ∨ G2(pm, S, S') ) subst: [S, s, Post2, pm, s1, G2, R2, R1, G1, Pre1, Post1, I, Pre2, s0] → [S, s19, Post2, pm, s, G2, R2, R1, G1, Pre1, Post1, I, Pre2, s3] flags: current, []

Additional information

Used terms: S, s19, Post2, pm, s, G2, R2, R1, G1, Pre1, Post1, I, Pre2, s3