proposition: Lemma precise_tri_exp_ocon {A} {JA : Join A} {PA : Perm_alg A} {SA: Sep_alg A} {CrA : Cross_alg A} {DA : Disj_alg A}{AG : ageable A} {AA : Age_alg A} B: forall (P : B -> B -> B -> pred A) (Q R: B -> pred A), precise (EX x : B, EX y : B, EX z : B, P x y z) -> precise (exp Q) -> precise (exp R) -> precise (EX x : B, EX y : B, EX z : B, P x y z ⊗ Q y ⊗ R z).
proof: Proof. repeat intro. destruct H2 as [x1 [y1 [z1 ?]]]; destruct_ocon H2 h; destruct_ocon H8 j; destruct H3 as [x2 [y2 [z2 ?]]]; destruct_ocon H3 i; destruct_ocon H16 k. assert (j12 = k12) by (hnf in H; apply H with (w := w); [exists x1, y1, z1 | exists x2, y2, z2 | assertSub j12 w Hsub | assertSub k12 w Hsub]; auto). assert (j23 = k23) by (hnf in H0; apply H0 with (w := w); [exists y1 | exists y2 | try_join j2 j3 j23'; equate_join j23 j23'; assertSub j23 w Hsub | try_join k2 k3 k23'; equate_join k23 k23'; assertSub k23 w Hsub]; auto). rewrite H22 in *; rewrite H23 in *; assert (h12 = i12) by (apply (overlapping_eq j1 j2 j3 k1 k2 k3 k12 k23); trivial). assert (h23 = i23) by (hnf in H1; apply H1 with (w := w); [exists z1 | exists z2 | try_join h2 h3 h23'; equate_join h23 h23'; assertSub h23 w Hsub | try_join i2 i3 i23'; equate_join i23 i23'; assertSub i23 w Hsub]; auto). rewrite H24 in *; rewrite H25 in *; apply (overlapping_eq h1 h2 h3 i1 i2 i3 i12 i23); trivial. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg