proposition: Lemma lseg_unroll_right (ls: listspec list_structid list_link list_token): forall sh sh' l x z , lseg ls sh sh' l x z = (!! (ptr_eq x z) && !! (l=nil) && emp) || lseg_cons_right ls sh sh' l x z.
proof: Proof. Abort. Lemma lseg_local_facts: forall ls dsh psh contents p q, lseg ls dsh psh contents p q |-- !! (is_pointer_or_null p /\ (p=q <-> contents=nil)). Proof. intros. rewrite lseg_unfold. destruct contents. apply derives_extract_prop; intro. unfold ptr_eq in H. apply prop_right. destruct p; try contradiction; simpl; auto. destruct q; try contradiction; auto. destruct H as [? [? ?]]. rewrite H. unfold Int.cmpu in *. apply int_eq_e in H0. apply int_eq_e in H1. subst. split; auto; split; auto. destruct q; try contradiction; auto. destruct H as [? [? ?]]. rewrite H. unfold Int64.cmpu in *. apply int64_eq_e in H0. apply int64_eq_e in H1. subst. split; auto; split; auto. destruct q; try contradiction; auto. destruct H; subst. unfold Ptrofs.cmpu in *. apply ptrofs_eq_e in H0. subst. intuition. normalize. rewrite field_at_isptr. normalize. autorewrite with subst norm1 norm2; normalize. apply prop_right. split. intro; subst q. contradiction H. normalize. intros. discriminate. Qed.
imports: VST.floyd.base2 VST.floyd.client_lemmas VST.floyd.closed_lemmas VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.efield_lemmas VST.floyd.mapsto_memory_block VST.floyd.reptype_lemmas VST.floyd.data_at_rec_lemmas VST.floyd.field_at VST.floyd.nested_loadstore VST.floyd.entailer