Commit ea15c157 by Simon Friis Vindum

### Change formatting

parent 76eb7cd1
Pipeline #48634 passed with stage
in 7 minutes and 49 seconds
 ... @@ -1464,8 +1464,10 @@ Qed. ... @@ -1464,8 +1464,10 @@ Qed. Lemma big_sepM_impl_strong `{Countable K} {A B} Φ (Ψ : K → B → PROP) m1 (m2 : gmap K B) : Lemma big_sepM_impl_strong `{Countable K} {A B} Φ (Ψ : K → B → PROP) m1 (m2 : gmap K B) : ([∗ map] k↦x ∈ m1, Φ k x) -∗ ([∗ map] k↦x ∈ m1, Φ k x) -∗ □ (∀ (k : K) (y : B), ⌜m2 !! k = Some y⌝ → □ (∀ (k : K) (y : B), ((∃ (x : A), ⌜m1 !! k = Some x⌝ ∧ Φ k x) ∨ ⌜m1 !! k = None⌝) -∗ Ψ k y) -∗ ⌜m2 !! k = Some y⌝ → ((∃ (x : A), ⌜m1 !! k = Some x⌝ ∧ Φ k x) ∨ ⌜m1 !! k = None⌝) -∗ Ψ k y) -∗ ([∗ map] k↦y ∈ m2, Ψ k y) ∗ ([∗ map] k↦y ∈ m2, Ψ k y) ∗ ([∗ map] k↦x ∈ (filter (λ '(k, _), m2 !! k = None) m1), Φ k x). ([∗ map] k↦x ∈ (filter (λ '(k, _), m2 !! k = None) m1), Φ k x). Proof. Proof. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!