C(l,v) = plist (reverse l) v * exists l'. j=(reverse l)@l' /\ (v<>nil iff v=hd l') /\ (F(v) =* list l' nil)
F(v) = if v<>nil then v.val -> - else emp
D(l) = vlist l

plist l v = match l with
  |  nil => emp
  |  x::nil => x<>nil /\ x.next -> v
  |  w::x::l => w<>nil /\ w.next ->x * plist x::l v
vlist l = match l with
  | nil => emp
  |  v::l' => v<>nil /\ v.val -> - * vlist l'
list l t = vlist l * plist l t


Lemma plist (reverse x::l) y |- plist (reverse l) x * x.next -> y /\ x<>nil
  > plist (reverse x::l) y |- plist (reverse l) x * x.next -> y /\ x<>nil
  > plist (reverse l)@x::nil y |- plist (reverse l) x * x.next -> y /\ x<>nil
  > plist l'@x::nil y |- plist l' x * x.next -> y /\ x<>nil
  Proof by induction on l'
  Case l' = nil
    > plist x::nil y |- plist nil x * x.next -> y /\ x<>nil
    > x<>nil /\ x.next->y |- plist nil x * x.next -> y /\ x<>nil
    > x<>nil /\ x.next->y |- emp * x.next -> y /\ x<>nil
    > x<>nil /\ x.next->y |- x.next -> y /\ x<>nil
  Case l' = z::nil
    > plist z::x::nil y |- plist z::nil x * x.next -> y /\ x<>nil
    > z<>nil /\ z.next->x * plist x::nil y  |-  plist z::nil x * x.next -> y /\ x<>nil
    > z.next->x * x.next->y /\ x<>nil /\ z<>nil  |-  plist z::nil x * x.next -> y /\ x<>nil
    > z.next->x * x.next->y /\ x<>nil /\ z<>nil  |-  z.next->x * x.next->y /\ x<>nil /\ z<>nil
  Case l' = z::w::l''
    IH: plist w::l''@x::nil y |- plist w::l'' x * x.next -> y /\ x<>nil
    > plist z::w::l''@x::nil y |- plist z::w::l'' x * x.next -> y /\ x<>nil
    > z.next->w * plist w::l''@x::nil y /\ z<>nil  |-  plist z::w::l'' x * x.next -> y /\ x<>nil
    > z.next->w * plist w::l''@x::nil y /\ z<>nil  |-  z.next->w * plist w::l'' x * x.next -> y /\ x<>nil /\ z<>nil
    > plist w::l''@x::nil y  |-  plist w::l'' x * x.next -> y /\ x<>nil
    True by IH
[]


Lemma plist l x * x.next -> y /\ x<>nil  |-  plist l@[x] y
  > plist l x * x.next -> y /\ x<>nil  |-  plist l@[x] y
  Induction on l
  Case l=nil
    > plist nil x * x.next -> y /\ x<>nil  |-  plist [x] y
    > x.next -> y /\ x<>nil  |-  plist [x] y
    > x.next -> y /\ x<>nil  |-  x<>nil /\ x.next->y
  Case l=z::nil
    > plist z::nil x * x.next -> y /\ x<>nil  |-  plist z::x::nil y
    > z.next->x * x.next->y /\ x<>nil /\ z<>nil |-  z.next->x * plist x::nil y /\ z<>nil
    > z.next->x * x.next->y /\ x<>nil /\ z<>nil |-  z.next->x * x.next->y /\ z<>nil /\ x<>nil
  Case l=z::w::l'
    IH: plist w::l' x * x.next -> y /\ x<>nil  |-  plist w::l'@[x] y
    > plist z::w::l' x * x.next -> y /\ x<>nil  |-  plist z::w::l'@[x] y
    > plist w::l' x * z.next->w * x.next -> y /\ x<>nil /\ z<>nil  |-  plist w::l'@[x] y * z.next->w /\ z<>nil
    > plist w::l' x * x.next -> y /\ x<>nil  |-  plist w::l'@[x] y
    True by IH
[]



Lemma list x::y::l t |- x.val->- * x.next->y * list y::l t
  > list x::y::l t |- x.val->- * x.next->y * list y::l t
  > vlist x::y::l * plist x::y::l t |- x.val->- * x.next->y * list y::l t
  > (x<>nil/\x.val->-*vlist y::l ) * (x<>nil /\ x.next->y * plist y::l t) |- x.val->- * x.next->y * list y::l t
  > (x<>nil/\x.val->-) * (x<>nil /\ x.next->y) * vlist y::l * plist y::l t  |- x.val->- * x.next->y * list y::l t
  > (x<>nil/\x.val->-) * (x<>nil /\ x.next->y) * list y::l t  |- x.val->- * x.next->y * list y::l t
  > x.val->- * x.next->y * list y::l t  |- x.val->- * x.next->y * list y::l t
[]  


Lemma: F(v) =* list v::l nil  |-  if v<>nil then  exists y. v.next->y * list l nil /\ (if y<>nil then y=hd l else l=nil) else emp
Case v<>nil
  > F(v) =* list v::l nil  |-  exists y. v.next->y * list l nil /\ (if y<>nil then y=hd l else l=nil)
  > (if v<>nil then v.val -> - else emp) =* list v::l nil  |-  exists y. v.next->y * list l nil /\ (if y<>nil then y=hd l else l=nil)
  list v::l nil  implies that v<>nil
  > v.val->- =* list v::l nil  |-  exists y. v.next->y * list l nil /\ (if y<>nil then y=hd l else l=nil)
  > v.val->- =* (vlist v::l * plist v::l nil)  |-  exists y. v.next->y * list l nil /\ (if y<>nil then y=hd l else l=nil)
  > v.val->- =* (v.val->- * vlist l * plist v::l nil)  |-  exists y. v.next->y * list l nil /\ (if y<>nil then y=hd l else l=nil)
  > v.val->- is satisfiable, so:
  > vlist l * plist v::l nil  |-  exists y. v.next->y * list l nil /\ (if y<>nil then y=hd l else l=nil)
  Case l=nil
    > vlist nil * plist v::nil nil  |-  exists y. v.next->y * list nil nil /\ (if y<>nil then y=hd l else l=nil)
    > v.next->nil |-  exists y. v.next->y * list nil nil /\ (if y<>nil then y=hd nil else nil=nil)
    > v.next->nil |-  exists y. v.next->y /\ (if y<>nil then y=hd nil else nil=nil)
    exists y=nil -- true!
    > v.next->nil |-  v.next->nil /\ (if nil<>nil then nil=hd nil else nil=nil)
    > v.next->nil |-  v.next->nil /\ (nil=nil)
    > v.next->nil |-  v.next->nil
  Case l = z::l'
    > vlist z::l' * plist v::z::l' nil  |-  exists y. v.next->y * list z::l' nil /\ (if y<>nil then y=hd z::l' else z::l'=nil)
    > vlist z::l' * plist v::z::l' nil  |-  exists y. v.next->y * list z::l' nil /\ (if y<>nil then y=z else z::l'=nil)
    > vlist z::l' * (v.next->z * plist z::l' nil /\ v<>nil)  |-  exists y. v.next->y * list z::l' nil /\ (if y<>nil then y=z else z::l'=nil)
    > v.next->z * plist z::l' nil * vlist z::l'  |-  exists y. v.next->y * list z::l' nil /\ (if y<>nil then y=z else z::l'=nil)
    > v.next->z * list z::l' nil |-  exists y. v.next->y * list z::l' nil /\ (if y<>nil then y=z else z::l'=nil)
    exists y=z
    > v.next->z * list z::l' nil |-  v.next->z * list z::l' nil /\ (if z<>nil then z=z else z::l'=nil)
    Case z=nil
      > v.next->z * list nil::l' nil |-  v.next->z * list z::l' nil /\ (if z<>nil then z=z else z::l'=nil)
      Contraditiction:  list nil::l' nil
    Case z<>nil
      > v.next->z * list z::l' nil |-  v.next->z * list z::l' nil /\ z=z
      > v.next->z * list z::l' nil /\ z=z |-  v.next->z * list z::l' nil /\ z=z
Case v=nil
  > emp =* list nil::l' nil  |- emp
  > list nil::l' nil  |- emp
  contradiction
[]
  

Lemma: v<>nil /\ v.next->y * list y::l' nil  |-  F(v) =* list v::y::l' nil
  > F(v) * v<>nil /\ v.next->y * list y::l' nil  |-  list v::y::l' nil
  > v.val->- * v.next->y * list y::l' nil |-  list v::y::l' nil
  > v.val->- * v.next->y * list y::l' nil |-  list v::y::l' nil
  > v.val->- * v.next->y * list y::l' nil |-  v.val->- * v.next->y * list y::l' nil
[]    


Lemma: C(l,x) /\ x<>nil  |-  exists z. C(x::l,z) * F(z)
  > C(l,x) /\ x<>nil  |-  exists z. C(x::l,z) * F(z)
  > plist (rev l) x * exists l'. j=(rev l)@l' /\ (if x<>nil then x=hd l' else l'=nil) /\ (F(x) =* list l' nil) /\ x<>nil  |-  ...
  > plist (rev l) x * exists l'. j=(rev l)@l' /\ x=hd l' /\ (F(x) =* list l' nil) /\ x<>nil  |-  ...
  > plist (rev l) x * j=(rev l)@l' /\ x=hd l' /\ (F(x) =* list l' nil) /\ x<>nil  |-  ...
  destruct l' into x::l' (because x=hd l'; reuse name l')
  > plist (rev l) x * j=(rev l)@x::l' /\ (F(x) =* list x::l' nil) /\ x<>nil  |-  ...
  > plist (rev l) x * j=(rev l)@x::l' /\ (if x<>nil then  exists y. x.next->y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) else emp) /\ x<>nil  |-  ...
  > plist (rev l) x * j=(rev l)@x::l' /\ (exists y. x.next->y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil)) /\ x<>nil  |-  ...
  > plist (rev l) x * x.next->y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev l)@x::l' /\ x<>nil  |-  ...
  exists z=y
  > plist (rev l) x * x.next->y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev l)@x::l' /\ x<>nil  |-  C(x::l,y) * F(y)
  > plist (rev l)@[x] y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev l)@x::l' /\ x<>nil  |-  C(x::l,y) * F(y)
  > plist (rev x::l) y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev l)@x::l' /\ x<>nil  |-  C(x::l,y) * F(y)
  > plist (rev x::l) y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev x::l)@l' /\ x<>nil  |-  C(x::l,y) * F(y)
  > plist (rev x::l) y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev x::l)@l' /\ x<>nil
      |-  (plist (rev x::l) y * exists l'. j=(rev x::l)@l' /\ (if y<>nil then y=hd l' else l'=nil) /\ (F(y) =* list l' nil)) * F(y)
  > plist (rev x::l) y * list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev x::l)@l' /\ x<>nil
      |-  plist (rev x::l) y * exists l'. j=(rev x::l)@l' /\ (if y<>nil then y=hd l' else l'=nil) /\ list l' nil
  > list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev x::l)@l' /\ x<>nil
      |-  exists l'. j=(rev x::l)@l' /\ (if y<>nil then y=hd l' else l'=nil) /\ list l' nil
  exists l'=l'
  > list l' nil /\ (if y<>nil then y=hd l' else l'=nil) /\ j=(rev x::l)@l' /\ x<>nil
      |-  j=(rev x::l)@l' /\ (if y<>nil then y=hd l' else l'=nil) /\ list l' nil
  > j=(rev x::l)@l' /\ (if y<>nil then y=hd l' else l'=nil) /\ list l' nil  |-  j=(rev x::l)@l' /\ (if y<>nil then y=hd l' else l'=nil) /\ list l' nil
[]


Lemma: ~R;G,p |- {C(h,p) /\ p<>nil /\ p|:v} p:= [p.next] {F(p) * C(v::h,p) /\ v<>nil}
  > {C(h,p) /\ p<>nil /\ p|:v} p:= [p.next] {F(p) * C(v::h,p) /\ v<>nil}
  Apply H-Consequence , H-Fetch
  > C(h,p) /\ p<>nil /\ p|:v  |-  exists x1.(p.next -> x1) * ((p.next -> x1) -* (F(p) * C(v::h,p) /\ v<>nil)[x1/p])
  > C(h,v) /\ v<>nil  |-  exists x1.(p.next -> x1) * ((p.next -> x1) -* (F(p) * C(v::h,p) /\ v<>nil)[x1/p])
  exists z. C(v::h,z) * F(v) /\ v<>nil  |-  exists x1.(p.next -> x1) * ((p.next -> x1) -* (F(p) * C(v::h,p) /\ v<>nil)[x1/p])
  > C(v::h,z) * F(z) /\ v<>nil  |-  exists x1.(p.next -> x1) * ((p.next -> x1) -* (F(p) * C(v::h,p) /\ v<>nil)[x1/p])
  exists x1=z
  > C(v::h,z) * F(z) /\ v<>nil  |-  (p.next -> z) * ((p.next -> z) -* (F(p) * C(v::h,p) /\ v<>nil)[z/p])
  > C(v::h,z) * F(z) /\ v<>nil  |-  (p.next -> z) * ((p.next -> z) -* (F(z) * C(v::h,z) /\ v<>nil))
  > C(v::h,z) * F(z) /\ v<>nil  |-  F(z) * C(v::h,z) /\ v<>nil
[]


Lemma: ~R;G |- {F(p) * D(h) /\ p<>nil} t:=[p.val]; [p.val]:=t+1 {D(p::h) /\ p<>nil}
  > ~R;G |- {F(p) * D(h) /\ p<>nil} t:=[p.val]; [p.val]:=t+1 {D(p::h) /\ p<>nil}
  Apply H-Seq
  > exists B s.t.: ~R;G |- {F(p) * D(h) /\ p<>nil} t:=[p.val] {B}  AND  ~R;G |- {B} [p.val]:=t+1 {D(p::h) /\ p<>nil}
  exists B = p.val->t * D(h) /\ p<>nil
  1> ~R;G |- {F(p) * D(h) /\ p<>nil} t:=[p.val] {p.val->t * D(h) /\ p<>nil}
  2> ~R;G |- {p.val->t * D(h) /\ p<>nil} [p.val]:=t+1 {D(p::h) /\ p<>nil}
  Goal 1:
    > ~R;G |- {F(p) * D(h) /\ p<>nil} t:=[p.val] {p.val->t * D(h) /\ p<>nil}
    apply H-Consequence, H-Fetch
    > F(p) * D(h) /\ p<>nil  |-  exists x1.(p.val -> x1) * ((p.val -> x1) -* (p.val->t * D(h) /\ p<>nil)[x1/t])
    > F(p) * D(h) /\ p<>nil  |-  exists x1.(p.val -> x1) * ((p.val -> x1) -* (p.val->t * D(h) /\ p<>nil)[x1/t])
    > (if p<>nil then p.val -> - else emp) * D(h) /\ p<>nil  |-  ...
    > p.val->- * D(h) /\ p<>nil  |-  ...
    intro fresh v
    > p.val->v * D(h) /\ p<>nil  |-  exists x1.(p.val -> x1) * ((p.val -> x1) -* (p.val->t * D(h) /\ p<>nil)[x1/t])
    exists x1=v
    > p.val->v * D(h) /\ p<>nil  |-  p.val -> v * ((p.val -> v) -* (p.val->t * D(h) /\ p<>nil)[v/t])
    > p.val->v * D(h) /\ p<>nil  |-  p.val -> v * ((p.val -> v) -* p.val->v * D(h) /\ p<>nil)
    > p.val->v * D(h) /\ p<>nil  |-  p.val->v * D(h) /\ p<>nil
  Goal 2:
    > ~R;G |- {p.val->t * D(h) /\ p<>nil} [p.val]:=t+1 {D(p::h) /\ p<>nil}
    apply H-Consequence, H-Store
    > p.val->t * D(h) /\ p<>nil  |-  p.val->- * ((p.val->t+1) -* (D(p::h) /\ p<>nil))
    > D(h) /\ p<>nil  |-  p.val->t+1 -* (D(p::h) /\ p<>nil)
    > p.val->t+1 * D(h) /\ p<>nil  |-  D(p::h) /\ p<>nil
    > p.val->t+1 * D(h) /\ p<>nil  |-  D(p::h) /\ p<>nil
    > D(p::h) /\ p<>nil  |-  D(p::h) /\ p<>nil
[]