Commit a9cd56f7 authored by Ralf Jung's avatar Ralf Jung

adapt naming scheme: inv_acc

parent 334e0d9d
Pipeline #24553 failed with stage
in 22 minutes and 10 seconds
......@@ -114,7 +114,7 @@ Section proofs.
rewrite /discrete_fun_singleton /discrete_fun_insert. destruct decide=>//. by subst i.
Qed.
Lemma na_inv_open p E F N (P : vProp) :
Lemma na_inv_acc p E F N (P : vProp) :
N E N F
na_inv p N P - na_own p F ={E}= P na_own p (F∖↑N)
( P na_own p (F∖↑N) ={E}= na_own p F).
......
......@@ -32,7 +32,7 @@ Proof.
by iExists _.
Qed.
Lemma subj_inv_open N P E :
Lemma subj_inv_acc N P E :
N E subj_inv N P ={E,E∖↑N}=
Vb, (monPred_in Vb P) ((monPred_in Vb P) ={E∖↑N,E}= True).
Proof.
......@@ -66,7 +66,7 @@ Global Instance into_acc_subj_inv E N P :
Proof.
rewrite /IntoAcc /accessor.
iIntros (?) "#Hinv _". simpl. setoid_rewrite <- bi.True_emp.
by iApply subj_inv_open.
by iApply subj_inv_acc.
Qed.
End subj_inv.
......
Markdown is supported
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