Commit 4d5521b5 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent 79f3c265
......@@ -590,9 +590,7 @@ Lemma stack_LIFO_insert_edge G e egV
let G' := graph_insert_edge e egV G Lt in
G.(Es) !! e = Some eV eV.(ge_event) = Push v
( u1 o1, (u1, o1) G.(com) (u1 < e < o1)%nat o1 egV.(ge_lview) False)
eventgraph_consistent G
graph_xo_eco G.(Es)
stack_matches_value G
eventgraph_consistent G graph_xo_eco G.(Es) stack_matches_value G
stack_LIFO G stack_LIFO G'.
Proof.
intros G' Eqe Eqv LF' EGCs MO MA LF u1 o1 oV1 u2 o2 uV2 oV2.
......
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