proposition: Lemma disj_ocon_right_d {A: Type} {JA: Join A} {SA: Sep_alg A} {PA : Perm_alg A} {CrA: Cross_alg A} {TA: Trip_alg A}: forall P Q R, disjointed P Q -> disjointed P R -> disjointed P (ocon Q R).
proof: Proof. unfold ocon, disjointed, precise; simpl. intros P Q R ? ? hP hp1p2p3 hr1r2r3 hPp h123. intros. destruct H4 as [h1 [h2 [h3 [h12 [h23 [? [? [? [? ?]]]]]]]]]. destruct (join_assoc H4 H6) as [h23' [? ?]]; equate_join h23 h23'. destruct (cross_split _ _ _ _ _ H10 H2) as [[[[hp1 hr1] hp2p3] hr2r3] [? [? [? ?]]]]. destruct (cross_split _ _ _ _ _ H5 H11) as [[[[hp2 hr2] hp3] hr3] [? [? [? ?]]]]. try_join hp1 hp2 hp1p2. try_join hr1 hr2 hr1r2. assert (join hp1p2 hr1r2 h12). 1: { try_join hp1 h2 hp1p2r2. destruct (join_assoc (join_comm H14) (join_comm H22)) as [hp1p2' [? ?]]. equate_join hp1p2 hp1p2'. destruct (join_assoc (join_comm H25) (join_comm H23)) as [hr1r2' [? ?]]. equate_join hr1r2 hr1r2'. auto. } try_join hP hp3 hPp3. assert (identity hp1p2 /\ joins hPp3 hr1r2) as [? ?] by (apply H with hPp h12; auto). try_join hP hp1 hPp1. assert (identity hp2p3 /\ joins hPp1 hr2r3) as [? ?] by (apply H0 with hPp h23; auto). assert (identity hp1) by (apply split_identity with hp2 hp1p2; auto). assert (identity hp3) by (apply split_identity with hp2 hp2p3; auto). split. + apply join_identity with hp1 hp2p3; auto. + apply H31 in H27. apply H32 in H23. subst hPp1 hPp3. destruct H26 as [hPr1r2 ?]. destruct H30 as [hPr1r3 ?]. destruct (join_assoc H20 (join_comm H23)) as [hPr1 [? ?]]. destruct (triple_join_exists _ _ _ _ _ _ H13 (join_comm H26) H27) as [hPr1r2r3 ?H]. apply joins_comm; eauto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg