proposition: Lemma ocon_wand_i {A}{JA: Join A}{PA: Perm_alg A}{AG : ageable A} {AA : Age_alg A}: forall P Q, P ⊗ Q = EX R : pred A, (R -* P) * (R -* Q) * R.
proof: Proof. intros; apply pred_ext; hnf; intros; simpl in *. destruct H as [h1 [h2 [h3 [h12 [h23 [? [? [? [? ?]]]]]]]]]. try_join h2 h3 h23'; equate_join h23 h23'; try_join h1 h3 h13. exists (exactly h2), h13, h2; repeat split; simpl; auto; exists h1, h3; repeat split; auto. intros h1' h2' h12'; intros; apply (pred_nec_hereditary P h12); auto; apply (join_necR h1 h2 _ h1' h2' _); auto. intros h3' h2' h23'; intros; apply (pred_nec_hereditary Q h23); auto; apply (join_necR h2 h3 _ h2' h3' _); auto. destruct H as [R [w13 [w2 [? [[w1 [w3 [? [HP HQ]]]] HR]]]]]. try_join w2 w3 w23; try_join w1 w2 w12. exists w1, w2, w3, w12, w23; repeat split; auto. apply (HP w1 w2); auto. apply (HQ w3 w2); auto. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg