proposition: Lemma semax_lseg_neq (ls: listspec list_structid list_link list_token): forall (Espec: OracleKind) Delta P Q dsh psh s v v2 R c Post, ~ (ptr_eq v v2) -> (forall (h: elemtype ls) (r: list (val * elemtype ls)) (y: val), s=(v,h)::r -> is_pointer_or_null y -> semax Delta (PROPx P (LOCALx Q (SEPx (list_token dsh v :: list_cell ls dsh h v :: field_at psh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) y) v :: lseg ls dsh psh r y v2 :: R)))) c Post) -> semax Delta (PROPx P (LOCALx Q (SEPx (lseg ls dsh psh s v v2 :: R)))) c Post.
proof: Proof. intros. rewrite lseg_neq by auto. unfold lseg_cons. apply semax_pre0 with (EX h: elemtype ls, EX r: list (val * elemtype ls), EX y: val, !!(s = (v, h) :: r /\ is_pointer_or_null y) && PROPx P (LOCALx Q (SEPx (list_token dsh v :: list_cell ls dsh h v :: field_at psh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) y) v :: lseg ls dsh psh r y v2 :: R)))). go_lowerx; entailer. Exists h r y. rewrite <- ?sepcon_assoc. normalize. autorewrite with subst norm1 norm2; normalize. Intros h r y. apply semax_extract_prop; intros [? ?]. eapply H0; eauto. 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