proposition: Lemma lseg_cons_right_null (ls: listspec list_structid list_link list_token): forall dsh psh l x h y, 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)) nullval) y * lseg ls dsh psh l x y |-- lseg ls dsh psh (l++(y,h)::nil) x nullval.
proof: Proof. intros. revert x; induction l; simpl; intros. * normalize. autorewrite with subst norm1 norm2; normalize. apply exp_right with nullval. apply andp_right. apply not_prop_right; intro. apply ptr_eq_e in H. subst y. entailer!. destruct H. contradiction H. rewrite prop_true_andp by reflexivity. rewrite prop_true_andp by (unfold nullval; destruct Archi.ptr64 eqn:Hp; simpl; auto). normalize. * destruct a as [v el]. normalize. apply exp_right with x0. normalize. autorewrite with subst norm1 norm2; normalize. specialize (IHl x0). apply andp_right. rewrite prop_and. apply andp_right; [ | apply prop_right; auto]. apply not_prop_right; intro. apply ptr_eq_e in H0. subst x. entailer. destruct H2; contradiction H2. eapply derives_trans. 2: apply sepcon_derives; [ | eassumption]; apply derives_refl. clear IHl. cancel. 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