proposition: Lemma trinode__precise: forall x, precise (exp (trinode x)).
proof: Proof. intros. rewrite trinode_unfold. pose proof (@precise_andp_right _ _ _ PSLdirect). simpl in H. apply H. repeat apply precise_sepcon; try apply mapsto__precise. apply derives_precise with (exp (mapsto x)); [| apply mapsto__precise]. apply mapsto_derives_aux. Qed.
imports: CertiGraph.msl_application.Graph VST.msl.seplog VST.msl.log_normalize VST.msl.alg_seplog_direct CertiGraph.msl_ext.abs_addr CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.precise_direct CertiGraph.msl_ext.overlapping_direct CertiGraph.msl_ext.alg_seplog_direct CertiGraph.msl_ext.ramify_tactics CertiGraph.heap_model_direct.SeparationAlgebra CertiGraph.heap_model_direct.mapsto CertiGraph.heap_model_direct.SeparationLogic VST.msl.msl_direct VST.msl.predicates_sa Coq.Numbers.Natural.Peano.NPeano Coq.ZArith.Znumtheory