proposition: Lemma lseg_cons_right_neq (ls: listspec list_structid list_link list_token): forall dsh psh l x h y w z, sepalg.nonidentity psh -> list_token dsh y * list_cell ls dsh h y * field_at psh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) z) y * lseg ls dsh psh l x y * field_at psh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) w) z |-- lseg ls dsh psh (l++(y,h)::nil) x z * field_at psh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) w) z.
proof: Proof. intros. rename H into SH. assert (SZ: 0 < sizeof (nested_field_type list_struct (DOT list_link))). unfold sizeof; rewrite list_link_type; simpl; destruct Archi.ptr64; computable. rewrite (field_at_isptr _ _ _ _ z). normalize. revert x; induction l; simpl; intros. * normalize. autorewrite with subst norm1 norm2; normalize. apply exp_right with z. entailer!. * destruct a as [v el]. normalize. apply exp_right with x0. normalize. rewrite <- ?sepcon_assoc. autorewrite with subst norm1 norm2; normalize. specialize (IHl x0). entailer. pull_right (list_cell ls dsh el x). apply sepcon_derives; auto. pull_right (field_at psh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) x0) x). pull_right (list_token dsh x). apply sepcon_derives; auto. apply sepcon_derives; auto. 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