proposition: Lemma ocon_assoc_d {A}{JA: Join A}{PA: Perm_alg A}{CA: Cross_alg A}: forall P Q R: pred A, P ⊗ Q ⊗ R = P ⊗ (Q ⊗ R).
proof: Proof. intros; apply pred_ext; hnf; intros; simpl in *; intros. destruct H as [w124 [w567 [w3 [w124567 [w3567 [? [? [? [[w15 [w47 [w26 [w1457 [w2467 [? [? [? [? ?]]]]]]]]] ?]]]]]]]]]. destruct (cross_split _ _ _ _ _ H H4) as [[[[w14 w2] w57] w6] [? [? [? ?]]]]. destruct (cross_split _ _ _ _ _ H2 H10) as [[[[w1 w5] w4] w7] [? [? [? ?]]]]. try_join w5 w47 w457; try_join w3 w26 w236; try_join w236 w457 w234567. exists w1, w457, w236, w1457, w234567; repeat split; auto. try_join w2 w4 w24; try_join w6 w7 w67; try_join w3 w5 w35. exists w24, w67, w35, w2467, w3567; repeat split; auto. apply (cross_rev_d w2 w6 w4 w7 w26 w47); auto. apply (cross_rev_d w47 w5 w26 w3 w457 w236); auto. destruct H as [w1 [w457 [w236 [w1457 [w234567 [? [? [? [? [w24 [w67 [w35 [w2467 [w3567 [? [? [? [? ?]]]]]]]]]]]]]]]]]]. destruct (cross_split _ _ _ _ _ H0 H5) as [[[[w47 w5] w26] w3] [? [? [? ?]]]]. destruct (cross_split _ _ _ _ _ H3 H10) as [[[[w4 w2] w7] w6] [? [? [? ?]]]]. try_join w26 w1457 w124567; try_join w5 w67 w567; try_join w5 w7 w57; try_join w1 w4 w14; try_join w14 w26 w1246; try_join w2 w14 w124. exists w124, w567, w3, w124567, w3567; repeat split; auto. apply join_comm; apply (cross_rev_d w6 w2 w57 w14 w26 w1457); auto. try_join_through w67 w5 w7 w57'; equate_join w57 w57'; auto. try_join w1 w5 w15; exists w15, w47, w26, w1457, w2467; repeat split; auto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg