Commit 4f667b31 authored by charguer's avatar charguer

cleanup_sepmodel

parent ff5aa240
......@@ -15,7 +15,8 @@ SRC :=\
ModelRO
PWD := $(shell pwd)
V := $(wildcard $(TLC)/*.v) $(CFML)/lib/coq/Shared.v $(addprefix $(PWD)/,$(SRC:=.v))
V_AUX := $(wildcard $(TLC)/*.v) $(CFML)/lib/coq/Shared.v
V := $(addprefix $(PWD)/,$(SRC:=.v))
COQINCLUDE := \
-R $(TLC) TLC \
......
This diff is collapsed.
......@@ -304,6 +304,12 @@ Proof using.
apply state_disjoint_union_eq_r.
Qed.
Lemma state_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
state_disjoint (state_single l v1) (state_single l v2) -> False.
Proof using.
introv D. specializes D l. simpls. case_if. destruct D; tryfalse.
Qed.
Lemma state_disjoint_3_unfold : forall h1 h2 h3,
\# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.
......
This diff is collapsed.
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