proposition: Lemma split_by_closed_spec: forall s Q Q1 Q2, split_by_closed s Q Q1 Q2 -> EnvironStable (vars_relation (modifiedvars s)) (LOCALx Q1 TT) /\ LOCALx Q TT = LOCALx Q1 TT && LOCALx Q2 TT.
proof: Proof. intros. split. + rewrite EnvironStable_var_relation_closed. induction H. - auto with closed. - rewrite <- insert_local'. auto with closed. - auto. + induction H. - apply add_andp; auto. - rewrite <- !insert_local'. rewrite IHsplit_by_closed. rewrite andp_assoc; auto. - rewrite <- !insert_local'. rewrite IHsplit_by_closed. rewrite <- !andp_assoc. rewrite (andp_comm (local (locald_denote q))); auto. Qed.
imports: VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.reptype_lemmas VST.floyd.semax_tactics VST.floyd.local2ptree_denote VST.floyd.local2ptree_eval VST.floyd.call_lemmas VST.floyd.diagnosis VST.floyd.forward CertiGraph.lib.Coqlib CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification CertiGraph.floyd_ext.semax_ram_lemmas CertiGraph.floyd_ext.exists_trick CertiGraph.floyd_ext.closed_lemmas