Skip to content
Snippets Groups Projects
Commit 0bc19271 authored by Ralf Jung's avatar Ralf Jung
Browse files

remove an assumption we no longer need

parent c3c91b70
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/bi/lib/counterexamples.v
+ 0
− 2
View file @ 0bc19271
...@@ -299,8 +299,6 @@ Module linear2. Section linear2. ...@@ -299,8 +299,6 @@ Module linear2. Section linear2.
fupd E E (∃ γ, ∀ P, ▷ P -∗ fupd E E (cinv γ P ∗ cinv_own γ))%I. fupd E E (∃ γ, ∀ P, ▷ P -∗ fupd E E (cinv γ P ∗ cinv_own γ))%I.
Hypothesis cinv_access : ∀ P γ, Hypothesis cinv_access : ∀ P γ,
cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)). cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
Hypothesis cinv_own_excl : ∀ E γ,
▷ cinv_own γ -∗ ▷ cinv_own γ -∗ fupd E E False.
(** Some general lemmas and proof mode compatibility. *) (** Some general lemmas and proof mode compatibility. *)
Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2). Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment