proposition: Lemma trinode_unfold: forall x, exp (trinode x) = !! Z.divide 3 (Z.of_nat x) && ((EX d: bool, (mapsto x (if d then 1 else 0))) * (exp (mapsto (x + 1))) * (exp (mapsto (x + 2)))).
proof: Proof. intros. replace (exp (trinode x) = !! Z.divide 3 (Z.of_nat x) && ((EX d: bool, (mapsto x (if d then 1 else 0))) * exp (mapsto (x + 1)) * exp (mapsto (x + 2)))) with ((EX dlr : bool * adr * adr, !! Z.divide 3 (Z.of_nat x) && (mapsto x (if (fst (fst dlr)) then 1 else 0) * mapsto (x + 1) (snd (fst dlr)) * mapsto (x + 2) (snd dlr))) = !! Z.divide 3 (Z.of_nat x) && ((EX d: bool, (mapsto x (if d then 1 else 0))) * seplog.exp (mapsto (x + 1)) * seplog.exp (mapsto (x + 2))))%logic. 2: { f_equal. simpl. f_equal. extensionality dlr; destruct dlr as [[? ?] ?]. reflexivity. } rewrite <- log_normalize.exp_andp2. f_equal. repeat rewrite exp_curry; simpl fst; simpl snd. rewrite seplog.sepcon_assoc. rewrite log_normalize.exp_sepcon1. f_equal. extensionality s. rewrite log_normalize.exp_sepcon1. rewrite log_normalize.exp_sepcon2. f_equal; extensionality l. rewrite !log_normalize.exp_sepcon2. f_equal; extensionality r. rewrite seplog.sepcon_assoc. reflexivity. Qed.
imports: CertiGraph.msl_application.Graph VST.msl.seplog VST.msl.log_normalize VST.msl.alg_seplog_direct CertiGraph.msl_ext.abs_addr CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.precise_direct CertiGraph.msl_ext.overlapping_direct CertiGraph.msl_ext.alg_seplog_direct CertiGraph.msl_ext.ramify_tactics CertiGraph.heap_model_direct.SeparationAlgebra CertiGraph.heap_model_direct.mapsto CertiGraph.heap_model_direct.SeparationLogic VST.msl.msl_direct VST.msl.predicates_sa Coq.Numbers.Natural.Peano.NPeano Coq.ZArith.Znumtheory