proposition: Lemma disj_trinode_: forall p1 p2, p1 <> p2 -> disjointed (EX v : bool * adr * adr, trinode p1 v) (EX v : bool * adr * adr, trinode p2 v).
proof: Proof. intros. change (EX v : bool * adr * adr, trinode p1 v) with (exp (trinode p1)). change (EX v : bool * adr * adr, trinode p2 v) with (exp (trinode p2)). rewrite !trinode_unfold. pose proof disj_prop_andp_left as HH; simpl in HH; apply HH; clear HH; [apply Zdivide_dec |]. intros. apply align_3_aux in H0; destruct H0 as [k1 ?]. pose proof disj_prop_andp_right as HH; simpl in HH; apply HH; clear HH; [apply Zdivide_dec |]. intros. apply align_3_aux in H1; destruct H1 as [k2 ?]. pose proof disj_sepcon_right as HH; simpl in HH. repeat apply HH; apply disj_comm; repeat apply HH; try (eapply disj_derives; [ first [apply mapsto_derives_aux | apply derives_refl] | first [apply mapsto_derives_aux | apply derives_refl] | apply disj_mapsto_]; lia). 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