proposition: Lemma trinode_conflict: forall p1 p2 v1 v2, p1 = p2 -> trinode p1 v1 * trinode p2 v2 |-- FF.
proof: Proof. intros. destruct v1 as [[d1 l1] r1]. destruct v2 as [[d2 l2] r2]. change (trinode p1 (d1, l1, r1) * trinode p2 (d2, l2, r2) |-- FF) with (seplog.derives (!! Z.divide 3 (Z.of_nat p1) && (mapsto p1 (if d1 then 1 else 0) * mapsto (p1 + 1) l1 * mapsto (p1 + 2) r1) * (!! Z.divide 3 (Z.of_nat p2) && (mapsto p2 (if d2 then 1 else 0) * mapsto (p2 + 1) l2 * mapsto (p2 + 2) r2))) FF)%logic. eapply seplog.derives_trans. + apply seplog.sepcon_derives; (apply log_normalize.andp_derives; [| apply seplog.sepcon_derives; [apply seplog.sepcon_derives | apply seplog.derives_refl ]]); apply TT_right. + rewrite !TT_andp. simpl. rewrite !sepcon_assoc. rewrite (sepcon_comm (mapsto (p1 + 2) r1)). rewrite !sepcon_assoc. pose proof sepcon_left2_corable_right as HH; simpl in HH. do 4 (try apply HH); try apply corable_prop. apply mapsto_conflict. 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