proposition: Lemma lseg_unroll (ls: listspec list_structid list_link list_token): forall sh l x z , lseg ls sh l x z = (!! (ptr_eq x z) && !! (l=nil) && emp) || lseg_cons ls sh l x z.
proof: Proof. intros. unfold lseg, lseg_cons. apply pred_ext. * apply exp_left; intros. apply derives_extract_prop; intro. rewrite LsegGeneral.lseg_unroll. apply orp_left; [apply orp_right1 | apply orp_right2]. rewrite andp_assoc; repeat (apply derives_extract_prop; intro). subst. simpl. normalize. unfold LsegGeneral.lseg_cons. apply derives_extract_prop; intro. rewrite prop_true_andp by auto. apply exp_derives; intro h. apply exp_left; intro r; apply exp_right with (map snd r). apply exp_derives; intro y. normalize. subst l. unfold lseg. cancel. apply exp_right with r; normalize. * apply orp_left. rewrite andp_assoc; repeat (apply derives_extract_prop; intro). subst. apply exp_right with nil. simpl. normalize. autorewrite with subst norm1 norm2; normalize. apply derives_extract_prop; intro. apply exp_left; intro h. apply exp_left; intro r. apply exp_left; intro y. normalize. unfold lseg. normalize. apply exp_right with ((x,h)::al). normalize. simpl. normalize. apply exp_right with y. normalize. autorewrite with subst norm1 norm2; 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