proposition: Lemma semax_ramification: forall Delta G L s L' G', closed_wrt_modvars s (L' -* G') -> G |-- L * (L' -* G') -> semax Delta L s (normal_ret_assert L') -> semax Delta G s (normal_ret_assert G').
proof: Proof. intros. apply semax_pre_post with (P' := L * (L' -* G')) (R' := normal_ret_assert (L' * (L' -* G'))). + intros. apply andp_left2; auto. + intros. apply andp_left2. unfold normal_ret_assert. apply andp_derives; [auto |]. apply andp_derives; [auto |]. rewrite sepcon_comm, wand_sepcon_adjoint; auto. + apply semax_frame with (F := L' -* G') in H1; [| auto]. rewrite frame_normal in H1. auto. Qed.
imports: CertiGraph.lib.Equivalence_ext CertiGraph.veric_ext.SeparationLogic VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.closed_lemmas VST.floyd.forward_lemmas