Commit 37db79b9 authored by Robbert Krebbers's avatar Robbert Krebbers

Comment out admitted sts_frag_included, it is not used anyway.

Should be restored later.
parent ce4c7913
...@@ -385,6 +385,7 @@ Qed. ...@@ -385,6 +385,7 @@ Qed.
(* This is surprisingly different from to_validity_included. I am not sure (* This is surprisingly different from to_validity_included. I am not sure
whether this is because to_validity_included is non-canonical, or this whether this is because to_validity_included is non-canonical, or this
one here is non-canonical - but I suspect both. *) one here is non-canonical - but I suspect both. *)
(*
Lemma sts_frag_included S1 S2 T1 T2 : Lemma sts_frag_included S1 S2 T1 T2 :
closed S2 T2 → S2 ≢ ∅ → closed S2 T2 → S2 ≢ ∅ →
(sts_frag S1 T1 ≼ sts_frag S2 T2) ↔ (sts_frag S1 T1 ≼ sts_frag S2 T2) ↔
...@@ -392,7 +393,7 @@ Lemma sts_frag_included S1 S2 T1 T2 : ...@@ -392,7 +393,7 @@ Lemma sts_frag_included S1 S2 T1 T2 :
S2 ≡ S1 ∩ up_set S2 Tf). S2 ≡ S1 ∩ up_set S2 Tf).
Proof. Proof.
intros ??; split. intros ??; split.
- intros [[???] ?]. (* - intros [[???] ?].
destruct (to_validity_included (sts_dra.car sts) (sts_dra.frag S1 T1) (sts_dra.frag S2 T2)) as [Hfincl Htoincl]. destruct (to_validity_included (sts_dra.car sts) (sts_dra.frag S1 T1) (sts_dra.frag S2 T2)) as [Hfincl Htoincl].
intros Hcl2 HS2ne. split. intros Hcl2 HS2ne. split.
- intros Hincl. destruct Hfincl as ((Hcl1 & ?) & (z & EQ & Hval & Hdisj)). - intros Hincl. destruct Hfincl as ((Hcl1 & ?) & (z & EQ & Hval & Hdisj)).
...@@ -413,7 +414,6 @@ Proof. ...@@ -413,7 +414,6 @@ Proof.
* by apply up_set_non_empty. * by apply up_set_non_empty.
+ constructor; last done. by rewrite -HS. + constructor; last done. by rewrite -HS.
Qed. Qed.
*) Admitted.
Lemma sts_frag_included' S1 S2 T : Lemma sts_frag_included' S1 S2 T :
closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ → closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ →
...@@ -421,7 +421,7 @@ Lemma sts_frag_included' S1 S2 T : ...@@ -421,7 +421,7 @@ Lemma sts_frag_included' S1 S2 T :
Proof. Proof.
intros. apply sts_frag_included; split_and?; auto. intros. apply sts_frag_included; split_and?; auto.
exists ∅; split_and?; done || set_solver+. exists ∅; split_and?; done || set_solver+.
Qed. Qed. *)
End stsRA. End stsRA.
(** STSs without tokens: Some stuff is simpler *) (** STSs without tokens: Some stuff is simpler *)
......
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