proposition: Lemma later_ocon {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: forall P Q, ((|> (P ⊗ Q)) = |> Q ⊗ |> P).
proof: Proof. intros; repeat rewrite later_age; apply pred_ext; hnf; intros; simpl in *. case_eq (age1 a); intros. destruct (H a0) as [h1' [h2' [h3' [h12' [h23' [? [? [? [? ?]]]]]]]]]; auto. destruct (unage_join2 _ H3 H0) as [x12 [x3 [? [? ?]]]]. destruct (unage_join2 _ H1 H7) as [x1 [x2 [? [? ?]]]]. try_join x2 x3 x23; exists x3, x2, x1, x23, x12; repeat (split; auto). assert (age x23 h23') by (apply (join_age x2 x3 _ h2' h3' _); auto); intro h23; intros; equate_age h23' h23; auto. assert (age x12 h12') by (apply (join_age x1 x2 _ h1' h2' _); auto); intro h12; intros; equate_age h12' h12; auto. exists (core a), a, (core a), a, a. repeat split. apply core_unit. apply join_comm, core_unit. apply join_comm, core_unit. intros; unfold age in H1; rewrite H0 in H1; discriminate H1. intros; unfold age in H1; rewrite H0 in H1; discriminate H1. destruct H as [x1 [x2 [x3 [x12 [x23 [? [? [? [? ?]]]]]]]]]; intros. destruct (age1_join2 _ H1 H4) as [h12 [h3 [? [? ?]]]]. destruct (age1_join2 _ H H6) as [h1 [h2 [? [? ?]]]]. try_join h2 h3 h23; exists h3, h2, h1, h23, h12; repeat (split; auto). apply H3; apply (join_age x2 x3 _ h2 h3 _); auto. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg