Require Import VST.floyd.proofauto.
Require Import VST.progs.list_dt. Import LsegSpecial.
Require Import VST.progs.append.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Instance LS: listspec _list _tail (fun _ _ => emp).
Proof. eapply mk_listspec; reflexivity. Defined.
Definition t_struct_list := Tstruct _list noattr.

Lemma is_pointer_or_null_not_null:
 forall x, is_pointer_or_null x -> x <> nullval -> isptr x.
Proof.
(* Goal: forall (x : val) (_ : is_pointer_or_null x) (_ : not (@eq val x nullval)), isptr x *)
intros.
(* Goal: isptr x *)
 destruct x; try contradiction. hnf in H; subst i. contradiction H0; reflexivity.
(* Goal: isptr (Vptr b i) *)
 apply I.
Qed.

Definition append_spec :=
 DECLARE _append
  WITH sh : share, x: val, y: val, s1: list val, s2: list val
  PRE [ _x OF (tptr t_struct_list) , _y OF (tptr t_struct_list)]
     PROP(writable_share sh)
     LOCAL (temp _x x; temp _y y)
     SEP (lseg LS sh s1 x nullval; lseg LS sh s2 y nullval)
  POST [ tptr t_struct_list ]
    EX r: val,
     PROP()
     LOCAL(temp ret_temp r)
     SEP (lseg LS sh (s1++s2) r nullval).

Definition Gprog : funspecs :=   ltac:(with_library prog [ append_spec ]).

Lemma ENTAIL_refl: forall Delta P, ENTAIL Delta, P |-- P.
Proof. intros; apply andp_left2; auto. Qed.

Lemma body_append: semax_body Vprog Gprog f_append append_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_append append_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1 x nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))) (Sifthenelse (Ebinop Oeq (Etempvar _x (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Sreturn (@Some expr (Etempvar _y (tptr (Tstruct _list noattr))))) (Ssequence (Sset _t (Etempvar _x (tptr (Tstruct _list noattr)))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) (Ssequence (Swhile (Ebinop One (Etempvar _u (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr)))))))))) POSTCONDITION *)
forward_if.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u nullval) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: @derives mpred Nveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val y a)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)) s2) a nullval))) *)
 Exists y.
(* Goal: @derives mpred Nveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@andp mpred Nveric (@prop mpred Nveric (@eq val y y)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)) s2) y nullval)) *)
 simpl app.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval)) *)
 entailer!.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u nullval) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1 x nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 apply semax_lseg_nonnull; [ | intros a s3 u ? ?].
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval)) *)
 entailer!.
(* Goal: isptr u *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a1 u) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield))) u2) u) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s4 u2 nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 apply is_pointer_or_null_not_null; auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u nullval) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield))) y) t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a0 (@nil val))) x y) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval) *)
 simpl valinject.
 forward_while
      (EX s1a: list val, EX s1b: list val, EX t: val, EX u: val, EX a: val,
            PROP (s1 = s1a ++ a :: s1b)
            LOCAL (temp _x x; temp _t t; temp _u u; temp _y y)
            SEP (lseg LS sh s1a x t;
                   list_cell LS sh a t;
                   field_at sh list_struct [StructField _tail] u t;
                   lseg LS sh s1b u nullval;
                   lseg LS sh s2 y nullval))%assert.
 + Exists (@nil val) s3 x u a.  entailer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval)) *)
 + entailer!.
 + clear u H1; rename u0 into u. clear a s3 H0. rename a0 into a.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) u t) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   gather_SEP 1 2 0 3.
   replace_SEP 0 (lseg LS sh (s1a++[a]) x u * lseg LS sh s1b u nullval).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a t) (@sepcon mpred Nveric Sveric (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) u t) (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   entailer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a t) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) u t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   rewrite <- (emp_sepcon (list_cell LS sh a t)).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) u t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   apply (lseg_cons_right_list LS); auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval)) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   Intros. gather_SEP 1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   apply semax_lseg_nonnull; [ | intros a1 s4 u2 ? ?].
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval)) *)
   entailer!.
(* Goal: isptr u *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a1 u) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield))) u2) u) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s4 u2 nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   apply is_pointer_or_null_not_null; auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield))) y) t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a0 (@nil val))) x y) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval) *)
   simpl valinject.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u nullval) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u nullval) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _u u2) (@cons localdef (temp _t u) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a1 u) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) u2 u) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s4 u2 nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a (@nil val))) x u) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (prod (prod (prod (prod (list val) (list val)) val) val) val) (fun a : prod (prod (prod (prod (list val) (list val)) val) val) val => PROPx (@cons Prop (@eq (list val) s1 (@app val (@fst (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)))) (@cons val (@snd (prod (prod (prod (list val) (list val)) val) val) val a) (@snd (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a))))))) (@nil Prop)) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t (@snd (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)))) (@cons localdef (temp _u (@snd (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a))) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@fst (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)))) x (@snd (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)))) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@snd (prod (prod (prod (list val) (list val)) val) val) val a) (@snd (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)))) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) (@snd (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)) (@snd (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)))) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@snd (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)))) (@snd (prod (prod (list val) (list val)) val) val (@fst (prod (prod (prod (list val) (list val)) val) val) val a)) nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred)))))))))) *)
   subst s1b. subst s1.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval)) *)
  Exists (s1a++[a],s4,u,u2,a1).  simpl fst; simpl snd. entailer!.
(* Goal: @eq (list val) (@app val s1a (@cons val a (@cons (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) a1 s4))) (@app val (@app val s1a (@cons val a (@nil val))) (@cons val a1 s4)) *)
  rewrite app_ass. reflexivity.
 +
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) u0 t) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1b u0 nullval) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
    clear a s3 H0. subst u0. rewrite lseg_eq by reflexivity. normalize. subst s1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u nullval) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
    forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u nullval) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@cons mpred (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t) (@cons mpred (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval) (@nil mpred))))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
    forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval)) *)
    Exists x. entailer!.
    apply derives_trans with (lseg LS sh (s1a++[a0]) x y * lseg LS sh s2 y nullval).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a0 (@nil val))) x y) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a0 (@nil val))) x y) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval) *)
    eapply derives_trans; [ | apply (lseg_cons_right_list LS) with (y:=t)]; auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield))) y) t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a0 (@nil val))) x y) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval) *)
    simpl valinject.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh a0 t)) (@field_at CompSpecs sh (@list_struct CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS) (@cons gfield (StructField _tail) (@nil gfield)) y t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s1a x t)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a0 (@nil val))) x y) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval) *)
    cancel.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val s1a (@cons val a0 (@nil val))) x y) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh s2 y nullval)) (@lseg CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS sh (@app val (@app val s1a (@cons val a0 (@nil (@elemtype CompSpecs _list _tail (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) LS)))) s2) x nullval) *)
   apply (list_append_null LS).
Qed.
