From 38010bcf3d0e0b74f8fc546bdb0daf6c46d108cc Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Wed, 1 Apr 2020 13:17:10 +0200
Subject: [PATCH] Bumped model update
---
theories/channel/channel.v | 28 ++++++++++++++--------------
1 file changed, 14 insertions(+), 14 deletions(-)
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 092cf81..fa62229 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -179,20 +179,20 @@ Section channel.
by apply iProto_message_proper=> /= -[].
Qed.
- Lemma iProto_le_branch a P1 P2 p1 p2 p1' p2' :
- ▷ (P1 -∗ P1 ∗ iProto_le p1 p1') ∧ ▷ (P2 -∗ P2 ∗ iProto_le p2 p2') -∗
- iProto_le (iProto_branch a P1 P2 p1 p2) (iProto_branch a P1 P2 p1' p2').
- Proof.
- iIntros "H". rewrite /iProto_branch. destruct a.
- - iApply iProto_le_send'; iIntros "!>" (b) "HP /=".
- iExists b; iSplit; [done|]. destruct b.
- + iDestruct "H" as "[H _]". by iApply "H".
- + iDestruct "H" as "[_ H]". by iApply "H".
- - iApply iProto_le_recv'; iIntros "!>" (b) "HP /=".
- iExists b; iSplit; [done|]. destruct b.
- + iDestruct "H" as "[H _]". by iApply "H".
- + iDestruct "H" as "[_ H]". by iApply "H".
- Qed.
+ (* Lemma iProto_le_branch a P1 P2 p1 p2 p1' p2' : *)
+ (* ▷ (P1 -∗ P1 ∗ iProto_le p1 p1') ∧ ▷ (P2 -∗ P2 ∗ iProto_le p2 p2') -∗ *)
+ (* iProto_le (iProto_branch a P1 P2 p1 p2) (iProto_branch a P1 P2 p1' p2'). *)
+ (* Proof. *)
+ (* iIntros "H". rewrite /iProto_branch. destruct a. *)
+ (* - iApply iProto_le_send'; iIntros "!>" (b) "HP /=". *)
+ (* iExists b; iSplit; [done|]. destruct b. *)
+ (* + iDestruct "H" as "[H _]". by iApply "H". *)
+ (* + iDestruct "H" as "[_ H]". by iApply "H". *)
+ (* - iApply iProto_le_recv'; iIntros "!>" (b) "HP /=". *)
+ (* iExists b; iSplit; [done|]. destruct b. *)
+ (* + iDestruct "H" as "[H _]". by iApply "H". *)
+ (* + iDestruct "H" as "[_ H]". by iApply "H". *)
+ (* Qed. *)
(** ** Specifications of [send] and [recv] *)
Lemma new_chan_spec p :
--
GitLab