proposition: Lemma solve_LOCALx_entailer: forall {cs: compspecs} P Ptemp Pvar Q Qtemp Qvar, local2ptree P = (Ptemp, Pvar, nil, nil) -> local2ptree Q = (Qtemp, Qvar, nil, nil) -> Forall (check_one_var_spec' Pvar) (PTree.elements Qvar) -> Forall (check_one_temp_spec Ptemp) (PTree.elements Qtemp) -> LOCALx P TT |-- LOCALx Q TT.
proof: Proof. intros. erewrite (local2ptree_soundness'' P) by eauto. erewrite (local2ptree_soundness'' Q) by eauto. unfold LOCALx, local, lift1; simpl; normalize; intros. eapply check_specs_lemma'; eauto. 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