proposition: Lemma body_sum: semax_body Vprog Gprog f_sum sum_spec.
proof: Proof. start_function. forward_if. - forward. entailer!. rewrite (proj1 H0) by auto. reflexivity. - destruct t. + assert_PROP False. entailer!. rewrite (proj2 H0) in H by auto. contradiction. contradiction. + unfold tree_rep; fold tree_rep. Intros pa pb. forward. forward_call. forward. forward_call. forward. forward. entailer!. * simpl. rewrite Int.add_assoc. auto. * unfold tree_rep at 3; fold tree_rep. Exists pa pb. cancel. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread