proposition: Lemma lseg_unroll (ls: listspec list_structid list_link list_token): forall dsh psh l x z , lseg ls dsh psh l x z = (!! (ptr_eq x z) && !! (l=nil) && emp) || lseg_cons ls dsh psh l x z.
proof: Proof. intros. rewrite lseg_unfold at 1. apply pred_ext; destruct l. apply derives_extract_prop; intros. rewrite prop_true_andp by auto. rewrite prop_true_andp by auto. apply orp_right1; auto. destruct p. apply orp_right2. unfold lseg_cons. apply derives_extract_prop; intros. destruct H. apply exp_left; intro tail. normalize. apply exp_right with e. rewrite TT_andp. apply exp_right with l. apply exp_right with tail. repeat rewrite sepcon_andp_prop'. apply andp_right. apply prop_right; split; auto. subst. auto. subst. auto. apply orp_left. rewrite andp_assoc; do 2 (apply derives_extract_prop; intro). rewrite prop_true_andp by auto. auto. unfold lseg_cons. apply derives_extract_prop; intros. apply exp_left; intro h. apply exp_left; intro r. apply exp_left; intro y. do 3 rewrite sepcon_andp_prop'. apply derives_extract_prop; intros [? ?]. inv H0. destruct p. apply orp_left. rewrite andp_assoc; do 2 (apply derives_extract_prop; intro). inv H0. unfold lseg_cons. apply derives_extract_prop; intros. apply exp_left; intro h. apply exp_left; intro r. apply exp_left; intro y. do 3 rewrite sepcon_andp_prop'. apply derives_extract_prop; intros [? ?]. symmetry in H0; inv H0. rewrite prop_true_andp by auto. apply exp_right with y. normalize. 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