Implicit Types p q : loc.

Goal Some MListSeg_cons = None.
Some MListSeg_cons = None
  pose proof MListSeg_cons.
H:forall p q (A : Type) (EA : Enc A) (x : A)
  (L' : list A),
{* p ~> MListSeg q (x :: L') *} =
{* ∃ p', p ~> MCell x p' * p' ~> MListSeg q L' *}
Some MListSeg_cons = None
  revert H.
(forall p q (A : Type) (EA : Enc A) (x : A)
   (L' : list A),
 {* p ~> MListSeg q (x :: L') *} =
 {* ∃ p', p ~> MCell x p' * p' ~> MListSeg q L' *}) ->
Some MListSeg_cons = None
Admitted.

Lemma Triple_transfer : forall A `{EA:Enc A} (L1 L2:list A) p1 p2,
  TRIPLE (transfer p1 p2)
    PRE (p1 ~> MQueue L1 \* p2 ~> MQueue L2)
    POST (fun (_:unit) => p1 ~> MQueue (L1 ++ L2) \* p2 ~> MQueue (@nil A)).
forall (A : Type) (EA : Enc A) (L1 L2 : list A) p1 p2,
TRIPLE (transfer p1 p2)
PRE {* p1 ~> MQueue L1 * p2 ~> MQueue L2 *}
POST (fun _ : unit =>
      {* p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil *})
Proof using.
forall (A : Type) (EA : Enc A) (L1 L2 : list A) p1 p2,
TRIPLE (transfer p1 p2)
PRE {* p1 ~> MQueue L1 * p2 ~> MQueue L2 *}
POST (fun _ : unit =>
      {* p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil *})

  xwp.
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
PRE {* p1 ~> MQueue L1 * p2 ~> MQueue L2 *}
CODE (Let_ b0 := `Let_ [A1 EA1] V1 := `App is_empty p2 in
                   `App val_neg (``V1) in
       `Ifval b0
        Then `Let_ [A EA] X := `App (val_get_field
                                       tail) p1 in
               `Let_ [A0 EA0] X0 := `App (val_get_field
                                            head) p2 in
                 `Let_ [A1 EA1] X1 := `App (val_get_field
                                              head)
                                       (``X) in
                   `Seq `Let_ [A2 EA2] V1 := `App 
                                              (val_get_field
                                                 head)
                                              (``X0) in
                          `App (val_set_field head)
                           (``X) (``V1)';
                     (`Seq `Let_ [A2 EA2] V1 := `App 
                                                 (val_get_field
                                                 tail)
                                                 (``X0) in
                             `App (val_set_field tail)
                              (``X) (``V1)';
                        (`Seq `Let_ [A2 EA2] V1 := `
                               App (val_get_field tail)
                               p2 in
                                `App (val_set_field
                                        tail) p1
                                 (``V1)';
                           (`Seq `App (val_set_field
                                         head) (``X0)
                                  (``X1)';
                              (`Seq `App (...) (``X0)
                                     (``null)';
                                 (`App ... p2 ...)))))
        Else (`Val '()))
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil * \GC
      *}) xapp.
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
PRE {* p2 ~> MQueue L2 * p1 ~> MQueue L1 *}
CODE (App val_neg (``(isTrue (L2 = nil))))
POST (fun X : bool =>
      (`Ifval X
        Then `Let_ [A EA] X0 := `App (val_get_field
                                        tail) p1 in
               `Let_ [A0 EA0] X1 := `App (val_get_field
                                            head) p2 in
                 `Let_ [A1 EA1] X2 := `App (val_get_field
                                              head)
                                       (``X0) in
                   `Seq `Let_ [A2 EA2] V1 := `App 
                                              (val_get_field
                                                 head)
                                              (``X1) in
                          `App (val_set_field head)
                           (``X0) (``V1)';
                     (`Seq `Let_ [A2 EA2] V1 := `App 
                                                 (val_get_field
                                                 tail)
                                                 (``X1) in
                             `App (val_set_field tail)
                              (``X0) (``V1)';
                        (`Seq `Let_ [A2 EA2] V1 := `
                               App (val_get_field tail)
                               p2 in
                                `App (val_set_field
                                        tail) p1
                                 (``V1)';
                           (`Seq `App (val_set_field
                                         head) (``X1)
                                  (``X2)';
                              (`Seq `App ... ... ...';
                                 (`...)))))
        Else (`Val '())) Enc_unit
        (fun _ : unit =>
         {*
         p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil *
         \GC *})) xapp.
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
PRE {* p2 ~> MQueue L2 * p1 ~> MQueue L1 *}
CODE (Ifval ! isTrue (L2 = nil)
      Then `Let_ [A EA] X := `App (val_get_field tail)
                              p1 in
             `Let_ [A0 EA0] X0 := `App (val_get_field
                                          head) p2 in
               `Let_ [A1 EA1] X1 := `App (val_get_field
                                            head)
                                     (``X) in
                 `Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                 head)
                                            (``X0) in
                        `App (val_set_field head)
                         (``X) (``V1)';
                   (`Seq `Let_ [A2 EA2] V1 := `App 
                                               (val_get_field
                                                 tail)
                                               (``X0) in
                           `App (val_set_field tail)
                            (``X) (``V1)';
                      (`Seq `Let_ [A2 EA2] V1 := `
                             App (val_get_field tail)
                             p2 in
                              `App (val_set_field tail)
                               p1 (``V1)';
                         (`Seq `App (val_set_field
                                       head) (``X0)
                                (``X1)';
                            (`Seq `App (val_set_field
                                          tail) (``X0)
                                   (``null)';
                               (`App (val_set_field
                                        tail) p2
                                 (``X0))))))
      Else (`Val '()))
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil * \GC
      *}) xif ;=> C.
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
C:L2 <> nil
PRE {* p2 ~> MQueue L2 * p1 ~> MQueue L1 *}
CODE (Let_ [A EA] X := `App (val_get_field tail) p1 in
       `Let_ [A0 EA0] X0 := `App (val_get_field head)
                             p2 in
         `Let_ [A1 EA1] X1 := `App (val_get_field head)
                               (``X) in
           `Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                             head)
                                      (``X0) in
                  `App (val_set_field head) (``X)
                   (``V1)';
             (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                tail)
                                         (``X0) in
                     `App (val_set_field tail) (``X)
                      (``V1)';
                (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                 tail)
                                            p2 in
                        `App (val_set_field tail) p1
                         (``V1)';
                   (`Seq `App (val_set_field head)
                          (``X0) (``X1)';
                      (`Seq `App (val_set_field tail)
                             (``X0) (``null)';
                         (`App (val_set_field tail) p2
                           (``X0)))))))
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil * \GC
      *})
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
C:L2 = nil
PRE {* p2 ~> MQueue L2 * p1 ~> MQueue L1 *}
CODE (Val '())
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil * \GC
      *})
  {
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
C:L2 <> nil
PRE {* p2 ~> MQueue L2 * p1 ~> MQueue L1 *}
CODE (Let_ [A EA] X := `App (val_get_field tail) p1 in
       `Let_ [A0 EA0] X0 := `App (val_get_field head)
                             p2 in
         `Let_ [A1 EA1] X1 := `App (val_get_field head)
                               (``X) in
           `Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                             head)
                                      (``X0) in
                  `App (val_set_field head) (``X)
                   (``V1)';
             (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                tail)
                                         (``X0) in
                     `App (val_set_field tail) (``X)
                      (``V1)';
                (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                 tail)
                                            p2 in
                        `App (val_set_field tail) p1
                         (``V1)';
                   (`Seq `App (val_set_field head)
                          (``X0) (``X1)';
                      (`Seq `App (val_set_field tail)
                             (``X0) (``null)';
                         (`App (val_set_field tail) p2
                           (``X0)))))))
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil * \GC
      *}) xunfold MQueue.
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
C:L2 <> nil
PRE {*
    (∃ f,
     ∃ b,
     ∃ d,
     p2 ~> MCell f b *
     f ~> MListSeg b L2 * b ~> MCell d null) *
    (∃ f,
     ∃ b,
     ∃ d,
     p1 ~> MCell f b *
     f ~> MListSeg b L1 * b ~> MCell d null) *}
CODE (Let_ [A EA] X := `App (val_get_field tail) p1 in
       `Let_ [A0 EA0] X0 := `App (val_get_field head)
                             p2 in
         `Let_ [A1 EA1] X1 := `App (val_get_field head)
                               (``X) in
           `Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                             head)
                                      (``X0) in
                  `App (val_set_field head) (``X)
                   (``V1)';
             (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                tail)
                                         (``X0) in
                     `App (val_set_field tail) (``X)
                      (``V1)';
                (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                 tail)
                                            p2 in
                        `App (val_set_field tail) p1
                         (``V1)';
                   (`Seq `App (val_set_field head)
                          (``X0) (``X1)';
                      (`Seq `App (val_set_field tail)
                             (``X0) (``null)';
                         (`App (val_set_field tail) p2
                           (``X0)))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ L2) * b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xpull ;=> f2 b2 d2 f1 b1 d1. (* TODO: fix order, should be preserved *)
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
C:L2 <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
PRE {*
    p2 ~> MCell f2 b2 *
    f2 ~> MListSeg b2 L2 *
    b2 ~> MCell d2 null *
    p1 ~> MCell f1 b1 *
    f1 ~> MListSeg b1 L1 * b1 ~> MCell d1 null *}
CODE (Let_ [A EA] X := `App (val_get_field tail) p1 in
       `Let_ [A0 EA0] X0 := `App (val_get_field head)
                             p2 in
         `Let_ [A1 EA1] X1 := `App (val_get_field head)
                               (``X) in
           `Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                             head)
                                      (``X0) in
                  `App (val_set_field head) (``X)
                   (``V1)';
             (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                tail)
                                         (``X0) in
                     `App (val_set_field tail) (``X)
                      (``V1)';
                (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                 tail)
                                            p2 in
                        `App (val_set_field tail) p1
                         (``V1)';
                   (`Seq `App (val_set_field head)
                          (``X0) (``X1)';
                      (`Seq `App (val_set_field tail)
                             (``X0) (``null)';
                         (`App (val_set_field tail) p2
                           (``X0)))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ L2) * b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *})
    destruct L2 as [|x L2']; tryfalse.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
PRE {*
    p2 ~> MCell f2 b2 *
    f2 ~> MListSeg b2 (x :: L2') *
    b2 ~> MCell d2 null *
    p1 ~> MCell f1 b1 *
    f1 ~> MListSeg b1 L1 * b1 ~> MCell d1 null *}
CODE (Let_ [A EA] X := `App (val_get_field tail) p1 in
       `Let_ [A0 EA0] X0 := `App (val_get_field head)
                             p2 in
         `Let_ [A1 EA1] X1 := `App (val_get_field head)
                               (``X) in
           `Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                             head)
                                      (``X0) in
                  `App (val_set_field head) (``X)
                   (``V1)';
             (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                tail)
                                         (``X0) in
                     `App (val_set_field tail) (``X)
                      (``V1)';
                (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                 tail)
                                            p2 in
                        `App (val_set_field tail) p1
                         (``V1)';
                   (`Seq `App (val_set_field head)
                          (``X0) (``X1)';
                      (`Seq `App (val_set_field tail)
                             (``X0) (``null)';
                         (`App (val_set_field tail) p2
                           (``X0)))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *})
    xchange MListSeg_cons ;=> c2.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    f2 ~> MCell x c2 *
    c2 ~> MListSeg b2 L2' *
    p2 ~> MCell f2 b2 *
    b2 ~> MCell d2 null *
    p1 ~> MCell f1 b1 *
    f1 ~> MListSeg b1 L1 * b1 ~> MCell d1 null *}
CODE (Let_ [A EA] X := `App (val_get_field tail) p1 in
       `Let_ [A0 EA0] X0 := `App (val_get_field head)
                             p2 in
         `Let_ [A1 EA1] X1 := `App (val_get_field head)
                               (``X) in
           `Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                             head)
                                      (``X0) in
                  `App (val_set_field head) (``X)
                   (``V1)';
             (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                tail)
                                         (``X0) in
                     `App (val_set_field tail) (``X)
                      (``V1)';
                (`Seq `Let_ [A2 EA2] V1 := `App (val_get_field
                                                 tail)
                                            p2 in
                        `App (val_set_field tail) p1
                         (``V1)';
                   (`Seq `App (val_set_field head)
                          (``X0) (``X1)';
                      (`Seq `App (val_set_field tail)
                             (``X0) (``null)';
                         (`App (val_set_field tail) p2
                           (``X0)))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *})
    xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    p1 ~> MCell f1 b1 *
    f2 ~> MCell x c2 *
    c2 ~> MListSeg b2 L2' *
    p2 ~> MCell f2 b2 *
    b2 ~> MCell d2 null *
    f1 ~> MListSeg b1 L1 * b1 ~> MCell d1 null *}
CODE (Let_ [A EA] X := `Wpgen_app
                          ('App (val_get_field head) p2) in
       `Let_ [A0 EA0] X0 := `Wpgen_app
                               ('App (val_get_field
                                        head) (``b1)) in
         `Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                      ('App (val_get_field
                                               head) 
                                       (``X)) in
                `Wpgen_app
                   ('App (val_set_field head) (``b1) 
                    (``V1))';
           (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                         ('App (val_get_field
                                                 tail) 
                                          (``X)) in
                   `Wpgen_app
                      ('App (val_set_field tail) (``b1) 
                       (``V1))';
              (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                            ('App 
                                             (val_get_field
                                                tail) p2) in
                      `Wpgen_app
                         ('App (val_set_field tail) p1 
                          (``V1))';
                 (`Seq `Wpgen_app
                          ('App (val_set_field head) 
                           (``X) (``X0))';
                    (`Seq `Wpgen_app
                             ('App (val_set_field tail) 
                              (``X) (``null))';
                       (`Wpgen_app
                           ('App (val_set_field tail) p2 
                            (``X))))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    p2 ~> MCell f2 b2 *
    p1 ~> MCell f1 b1 *
    f2 ~> MCell x c2 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null *
    f1 ~> MListSeg b1 L1 * b1 ~> MCell d1 null *}
CODE (Let_ [A EA] X := `Wpgen_app
                          ('App (val_get_field head) 
                           (``b1)) in
       `Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                    ('App (val_get_field
                                             head) 
                                     (``f2)) in
              `Wpgen_app
                 ('App (val_set_field head) (``b1) 
                  (``V1))';
         (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                       ('App (val_get_field
                                                tail) 
                                        (``f2)) in
                 `Wpgen_app
                    ('App (val_set_field tail) (``b1) 
                     (``V1))';
            (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                          ('App (val_get_field
                                                 tail) p2) in
                    `Wpgen_app
                       ('App (val_set_field tail) p1 
                        (``V1))';
               (`Seq `Wpgen_app
                        ('App (val_set_field head) 
                         (``f2) (``X))';
                  (`Seq `Wpgen_app
                           ('App (val_set_field tail) 
                            (``f2) (``null))';
                     (`Wpgen_app
                         ('App (val_set_field tail) p2 
                          (``f2))))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    b1 ~> MCell d1 null *
    p2 ~> MCell f2 b2 *
    p1 ~> MCell f1 b1 *
    f2 ~> MCell x c2 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                  ('App (val_get_field
                                           head) (``f2)) in
            `Wpgen_app
               ('App (val_set_field head) (``b1) (``V1))';
       (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                     ('App (val_get_field
                                              tail) 
                                      (``f2)) in
               `Wpgen_app
                  ('App (val_set_field tail) (``b1) 
                   (``V1))';
          (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                        ('App (val_get_field
                                                 tail) p2) in
                  `Wpgen_app
                     ('App (val_set_field tail) p1 
                      (``V1))';
             (`Seq `Wpgen_app
                      ('App (val_set_field head) (``f2) 
                       (``d1))';
                (`Seq `Wpgen_app
                         ('App (val_set_field tail) 
                          (``f2) (``null))';
                   (`Wpgen_app
                       ('App (val_set_field tail) p2 
                        (``f2))))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    f2 ~> MCell x c2 *
    b1 ~> MCell d1 null *
    p2 ~> MCell f2 b2 *
    p1 ~> MCell f1 b1 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Wpgen_app
        ('App (val_set_field head) (``b1) (``x)))
POST (fun _ : unit =>
      (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                    ('App (val_get_field
                                             tail) 
                                     (``f2)) in
              `Wpgen_app
                 ('App (val_set_field tail) (``b1) 
                  (``V1))';
         (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                       ('App (val_get_field
                                                tail) p2) in
                 `Wpgen_app
                    ('App (val_set_field tail) p1 
                     (``V1))';
            (`Seq `Wpgen_app
                     ('App (val_set_field head) (``f2) 
                      (``d1))';
               (`Seq `Wpgen_app
                        ('App (val_set_field tail) 
                         (``f2) (``null))';
                  (`Wpgen_app
                      ('App (val_set_field tail) p2 
                       (``f2))))))) Enc_unit
        (fun _ : unit =>
         {*
         (∃ f,
          ∃ b,
          ∃ d,
          p1 ~> MCell f b *
          f ~> MListSeg b (L1 ++ x :: L2') *
          b ~> MCell d null) *
         (∃ f,
          ∃ b,
          ∃ d,
          p2 ~> MCell f b *
          f ~> MListSeg b nil * b ~> MCell d null) *
         \GC *})) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    b1 ~> MCell x null *
    f2 ~> MCell x c2 *
    p2 ~> MCell f2 b2 *
    p1 ~> MCell f1 b1 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                  ('App (val_get_field
                                           tail) (``f2)) in
            `Wpgen_app
               ('App (val_set_field tail) (``b1) (``V1))';
       (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                     ('App (val_get_field
                                              tail) p2) in
               `Wpgen_app
                  ('App (val_set_field tail) p1 (``V1))';
          (`Seq `Wpgen_app
                   ('App (val_set_field head) (``f2) 
                    (``d1))';
             (`Seq `Wpgen_app
                      ('App (val_set_field tail) (``f2) 
                       (``null))';
                (`Wpgen_app
                    ('App (val_set_field tail) p2 
                     (``f2)))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    f2 ~> MCell x c2 *
    b1 ~> MCell x null *
    p2 ~> MCell f2 b2 *
    p1 ~> MCell f1 b1 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Wpgen_app
        ('App (val_set_field tail) (``b1) (``c2)))
POST (fun _ : unit =>
      (`Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                    ('App (val_get_field
                                             tail) p2) in
              `Wpgen_app
                 ('App (val_set_field tail) p1 (``V1))';
         (`Seq `Wpgen_app
                  ('App (val_set_field head) (``f2) 
                   (``d1))';
            (`Seq `Wpgen_app
                     ('App (val_set_field tail) (``f2) 
                      (``null))';
               (`Wpgen_app
                   ('App (val_set_field tail) p2 (``f2))))))
        Enc_unit
        (fun _ : unit =>
         {*
         (∃ f,
          ∃ b,
          ∃ d,
          p1 ~> MCell f b *
          f ~> MListSeg b (L1 ++ x :: L2') *
          b ~> MCell d null) *
         (∃ f,
          ∃ b,
          ∃ d,
          p2 ~> MCell f b *
          f ~> MListSeg b nil * b ~> MCell d null) *
         \GC *})) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    b1 ~> MCell x c2 *
    f2 ~> MCell x c2 *
    p2 ~> MCell f2 b2 *
    p1 ~> MCell f1 b1 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Seq `Let_ [A1 EA1] V1 := `Wpgen_app
                                  ('App (val_get_field
                                           tail) p2) in
            `Wpgen_app
               ('App (val_set_field tail) p1 (``V1))';
       (`Seq `Wpgen_app
                ('App (val_set_field head) (``f2) 
                 (``d1))';
          (`Seq `Wpgen_app
                   ('App (val_set_field tail) (``f2) 
                    (``null))';
             (`Wpgen_app
                 ('App (val_set_field tail) p2 (``f2))))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    p2 ~> MCell f2 b2 *
    b1 ~> MCell x c2 *
    f2 ~> MCell x c2 *
    p1 ~> MCell f1 b1 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Wpgen_app ('App (val_set_field tail) p1 (``b2)))
POST (fun _ : unit =>
      (`Seq `Wpgen_app
               ('App (val_set_field head) (``f2) (``d1))';
         (`Seq `Wpgen_app
                  ('App (val_set_field tail) (``f2) 
                   (``null))';
            (`Wpgen_app
                ('App (val_set_field tail) p2 (``f2)))))
        Enc_unit
        (fun _ : unit =>
         {*
         (∃ f,
          ∃ b,
          ∃ d,
          p1 ~> MCell f b *
          f ~> MListSeg b (L1 ++ x :: L2') *
          b ~> MCell d null) *
         (∃ f,
          ∃ b,
          ∃ d,
          p2 ~> MCell f b *
          f ~> MListSeg b nil * b ~> MCell d null) *
         \GC *})) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    p1 ~> MCell f1 b2 *
    p2 ~> MCell f2 b2 *
    b1 ~> MCell x c2 *
    f2 ~> MCell x c2 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Seq `Wpgen_app
             ('App (val_set_field head) (``f2) (``d1))';
       (`Seq `Wpgen_app
                ('App (val_set_field tail) (``f2) 
                 (``null))';
          (`Wpgen_app
              ('App (val_set_field tail) p2 (``f2)))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    f2 ~> MCell d1 c2 *
    p1 ~> MCell f1 b2 *
    p2 ~> MCell f2 b2 *
    b1 ~> MCell x c2 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Seq `Wpgen_app
             ('App (val_set_field tail) (``f2) (``null))';
       (`Wpgen_app
           ('App (val_set_field tail) p2 (``f2))))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
PRE {*
    f2 ~> MCell d1 null *
    p1 ~> MCell f1 b2 *
    p2 ~> MCell f2 b2 *
    b1 ~> MCell x c2 *
    c2 ~> MListSeg b2 L2' *
    b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *}
CODE (Wpgen_app ('App (val_set_field tail) p2 (``f2)))
POST (fun _ : unit =>
      {*
      (∃ f,
       ∃ b,
       ∃ d,
       p1 ~> MCell f b *
       f ~> MListSeg b (L1 ++ x :: L2') *
       b ~> MCell d null) *
      (∃ f,
       ∃ b,
       ∃ d,
       p2 ~> MCell f b *
       f ~> MListSeg b nil * b ~> MCell d null) * \GC
      *}) xapp.
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
{*
p2 ~> MCell f2 f2 *
f2 ~> MCell d1 null *
p1 ~> MCell f1 b2 *
b1 ~> MCell x c2 *
c2 ~> MListSeg b2 L2' *
b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *} ==>
{*
(∃ f,
 ∃ b,
 ∃ d,
 p1 ~> MCell f b *
 f ~> MListSeg b (L1 ++ x :: L2') * b ~> MCell d null) *
(∃ f,
 ∃ b,
 ∃ d,
 p2 ~> MCell f b *
 f ~> MListSeg b nil * b ~> MCell d null) * \GC *}
    xchange <- (MListSeg_cons b1).
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
{*
b1 ~> MListSeg b2 (x :: L2') *
p2 ~> MCell f2 f2 *
f2 ~> MCell d1 null *
p1 ~> MCell f1 b2 *
b2 ~> MCell d2 null * f1 ~> MListSeg b1 L1 *} ==>
{*
(∃ f,
 ∃ b,
 ∃ d,
 p1 ~> MCell f b *
 f ~> MListSeg b (L1 ++ x :: L2') * b ~> MCell d null) *
(∃ f,
 ∃ b,
 ∃ d,
 p2 ~> MCell f b *
 f ~> MListSeg b nil * b ~> MCell d null) * \GC *} xchange <- (MListSeg_concat f1).
A:Type
EA:Enc A
L1:list A
x:A
L2':list A
p1, p2:loc
C:x :: L2' <> nil
f2, b2:loc
d2:A
f1, b1:loc
d1:A
c2:loc
{*
f1 ~> MListSeg b2 (L1 ++ x :: L2') *
p2 ~> MCell f2 f2 *
f2 ~> MCell d1 null *
p1 ~> MCell f1 b2 * b2 ~> MCell d2 null *} ==>
{*
(∃ f,
 ∃ b,
 ∃ d,
 p1 ~> MCell f b *
 f ~> MListSeg b (L1 ++ x :: L2') * b ~> MCell d null) *
(∃ f,
 ∃ b,
 ∃ d,
 p2 ~> MCell f b *
 f ~> MListSeg b nil * b ~> MCell d null) * \GC *}
    xchanges (MListSeg_nil_intro f2). }
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
C:L2 = nil
PRE {* p2 ~> MQueue L2 * p1 ~> MQueue L1 *}
CODE (Val '())
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil * \GC
      *})
  {
A:Type
EA:Enc A
L1, L2:list A
p1, p2:loc
C:L2 = nil
PRE {* p2 ~> MQueue L2 * p1 ~> MQueue L1 *}
CODE (Val '())
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ L2) * p2 ~> MQueue nil * \GC
      *}) subst.
A:Type
EA:Enc A
L1:list A
p1, p2:loc
PRE {* p2 ~> MQueue nil * p1 ~> MQueue L1 *}
CODE (Val '())
POST (fun _ : unit =>
      {*
      p1 ~> MQueue (L1 ++ nil) * p2 ~> MQueue nil *
      \GC *}) rew_list.
A:Type
EA:Enc A
L1:list A
p1, p2:loc
PRE {* p2 ~> MQueue nil * p1 ~> MQueue L1 *}
CODE (Val '())
POST (fun _ : unit =>
      {* p1 ~> MQueue L1 * p2 ~> MQueue nil * \GC *}) xvals~. }
Qed.