proposition: Lemma trinode_inj: forall p v1 v2, trinode p v1 && trinode p v2 |-- !! (v1 = v2).
proof: Proof. intros. unfold trinode. destruct v1 as [[d1 l1] r1]. destruct v2 as [[d2 l2] r2]. eapply derives_trans. + apply andp_derives; (apply andp_derives; [apply (@TT_right _ Ndirect) | apply derives_refl]). + pose proof TT_andp. simpl in H; rewrite !H; clear H. rewrite !sepcon_assoc. eapply derives_trans. apply precise_left_sepcon_andp_distr with (exp (mapsto p)). 1: apply mapsto__precise. 1: apply (exp_right (if d1 then 1 else 0)); auto. 1: apply (exp_right (if d2 then 1 else 0)); auto. eapply derives_trans; [apply sepcon_derives |]. 1: apply mapsto_inj. eapply derives_trans. apply precise_left_sepcon_andp_distr with (exp (mapsto (p + 1))). 1: apply mapsto__precise. 1: apply (exp_right l1); auto. 1: apply (exp_right l2); auto. eapply derives_trans; [apply sepcon_derives |]. 1: apply mapsto_inj. 1: apply mapsto_inj. 1: apply derives_refl. pose proof sepcon_prop_prop. simpl in H; rewrite !H; clear H. intro; simpl in *; intros. unfold prop in *. destruct d1, d2; destruct H as [? [? ?]]; congruence. 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