Lemma Triple_transfer : forall {A} `{EA: Enc A} (L1 L2: list A) p1 p2,
  Triple (transfer p1 p2)
    (p1 ~> MQueue L1 \* p2 ~> MQueue L2)
    (fun (r:unit) => p1 ~> MQueue (L1 ++ L2) \* p2 ~> MQueue (@nil A)).
forall (A : Type) (EA : Enc A) (L1 L2 : list A) p1 p2,
SPEC (transfer p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MQueue ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit =>
       ⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
       $MQueue ┆ nil⟧⟭⟭*⟭
Proof using.
forall (A : Type) (EA : Enc A) (L1 L2 : list A) p1 p2,
SPEC (transfer p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MQueue ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit =>
       ⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
       $MQueue ┆ nil⟧⟭⟭*⟭
  xwp.
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MQueue ┆ L2⟧⟭⟭*⟭
CODE (`Let b0 := `Let {A1 EA1} V1 := `App is_empty p2 in
                  `App val_neg (``V1) in
       `If_ b0 Then 
          `Let {A0 EA0} X := `App (val_get_field tail) p1 in
           `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
            `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
             `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
                `App (val_set_field head) (``X) (``V1)) ;
              `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
                 `App (val_set_field tail) (``X) (``V1)) ;
               `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
                  `App (val_set_field tail) p1 (``V1)) ;
                `(`App (val_set_field head) (``X0) (``X1)) ;
                 `(`App (val_set_field tail) (``X0) (``null)) ;
                  `App (val_set_field tail) p2 (``X0)
        Else
          `$(``tt))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_is_empty.
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ L2⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`App val_neg (``(isTrue (L2 = nil))))
⟬*POST@ Bind X : bool In
        `(If_ X Then 
            `Let {A0 EA0} X0 := `App (val_get_field tail) p1 in
             `Let {A1 EA1} X1 := `App (val_get_field head) p2 in
              `Let {A2 EA2} X2 := `App (val_get_field head) (``X0) in
               `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X1) in
                  `App (val_set_field head) (``X0) (``V1)) ;
                `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X1) in
                   `App (val_set_field tail) (``X0) (``V1)) ;
                 `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
                    `App (val_set_field tail) p1 (``V1)) ;
                  `(`App (val_set_field head) (``X1) (``X2)) ;
                   `(`App (val_set_field tail) (``X1) (``null)) ;
                    `App (val_set_field tail) p2 (``X1)
          Else
            `$(``tt))
        ;
        fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_neg.
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ L2⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`If_ ! isTrue (L2 = nil) Then 
         `Let {A0 EA0} X := `App (val_get_field tail) p1 in
          `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
           `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
            `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
               `App (val_set_field head) (``X) (``V1)) ;
             `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
                `App (val_set_field tail) (``X) (``V1)) ;
              `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
                 `App (val_set_field tail) p1 (``V1)) ;
               `(`App (val_set_field head) (``X0) (``X1)) ;
                `(`App (val_set_field tail) (``X0) (``null)) ;
                 `App (val_set_field tail) p2 (``X0)
       Else
         `$(``tt))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xif ;=> C.
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
C: L2 <> nil
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ L2⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field tail) p1 in
       `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
        `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
         `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
            `App (val_set_field head) (``X) (``V1)) ;
          `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
             `App (val_set_field tail) (``X) (``V1)) ;
           `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
              `App (val_set_field tail) p1 (``V1)) ;
            `(`App (val_set_field head) (``X0) (``X1)) ;
             `(`App (val_set_field tail) (``X0) (``null)) ;
              `App (val_set_field tail) p2 (``X0))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
C: L2 = nil
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ L2⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`$(``tt))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  -
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
C: L2 <> nil
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ L2⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field tail) p1 in
       `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
        `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
         `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
            `App (val_set_field head) (``X) (``V1)) ;
          `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
             `App (val_set_field tail) (``X) (``V1)) ;
           `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
              `App (val_set_field tail) p1 (``V1)) ;
            `(`App (val_set_field head) (``X0) (``X1)) ;
             `(`App (val_set_field tail) (``X0) (``null)) ;
              `App (val_set_field tail) p2 (``X0))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xunfold MQueue.
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
C: L2 <> nil
⟬*PRE@⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆L2 ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆L1 ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field tail) p1 in
       `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
        `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
         `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
            `App (val_set_field head) (``X) (``V1)) ;
          `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
             `App (val_set_field tail) (``X) (``V1)) ;
           `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
              `App (val_set_field tail) p1 (``V1)) ;
            `(`App (val_set_field head) (``X0) (``X1)) ;
             `(`App (val_set_field tail) (``X0) (``null)) ;
              `App (val_set_field tail) p2 (``X0))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ L2 ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xpull ;=> f2 b2 d2 f1 b1 d1.
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@⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MListSeg┆b2┆L2 ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭┆⟬PointsTo┆b1┆⟦$MCell┆d1┆null⟧⟭⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field tail) p1 in
       `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
        `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
         `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
            `App (val_set_field head) (``X) (``V1)) ;
          `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
             `App (val_set_field tail) (``X) (``V1)) ;
           `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
              `App (val_set_field tail) p1 (``V1)) ;
            `(`App (val_set_field head) (``X0) (``X1)) ;
             `(`App (val_set_field tail) (``X0) (``null)) ;
              `App (val_set_field tail) p2 (``X0))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ L2 ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    destruct L2 as [| x L2']; [solve [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@⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MListSeg┆b2┆
x :: L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭┆⟬PointsTo┆b1┆⟦$MCell┆d1┆null⟧⟭⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field tail) p1 in
       `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
        `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
         `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
            `App (val_set_field head) (``X) (``V1)) ;
          `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
             `App (val_set_field tail) (``X) (``V1)) ;
           `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
              `App (val_set_field tail) p1 (``V1)) ;
            `(`App (val_set_field head) (``X0) (``X1)) ;
             `(`App (val_set_field tail) (``X0) (``null)) ;
              `App (val_set_field tail) p2 (``X0))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆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@⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭┆⟬PointsTo┆b1┆⟦$MCell┆d1┆null⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field tail) p1 in
       `Let {A1 EA1} X0 := `App (val_get_field head) p2 in
        `Let {A2 EA2} X1 := `App (val_get_field head) (``X) in
         `(`Let {A3 EA3} V1 := `App (val_get_field head) (``X0) in
            `App (val_set_field head) (``X) (``V1)) ;
          `(`Let {A3 EA3} V1 := `App (val_get_field tail) (``X0) in
             `App (val_set_field tail) (``X) (``V1)) ;
           `(`Let {A3 EA3} V1 := `App (val_get_field tail) p2 in
              `App (val_set_field tail) p1 (``V1)) ;
            `(`App (val_set_field head) (``X0) (``X1)) ;
             `(`App (val_set_field tail) (``X0) (``null)) ;
              `App (val_set_field tail) p2 (``X0))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_get_tail.
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@⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬Star┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭┆⟬PointsTo┆b1┆⟦$MCell┆d1┆null⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field head) p2 in
       `Let {A1 EA1} X0 := `App (val_get_field head) (``b1) in
        `(`Let {A2 EA2} V1 := `App (val_get_field head) (``X) in
           `App (val_set_field head) (``b1) (``V1)) ;
         `(`Let {A2 EA2} V1 := `App (val_get_field tail) (``X) in
            `App (val_set_field tail) (``b1) (``V1)) ;
          `(`Let {A2 EA2} V1 := `App (val_get_field tail) p2 in
             `App (val_set_field tail) p1 (``V1)) ;
           `(`App (val_set_field head) (``X) (``X0)) ;
            `(`App (val_set_field tail) (``X) (``null)) ;
             `App (val_set_field tail) p2 (``X))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_get_head.
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@⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬Star┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭┆⟬PointsTo┆b1┆⟦$MCell┆d1┆null⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field head) (``b1) in
       `(`Let {A1 EA1} V1 := `App (val_get_field head) (``f2) in
          `App (val_set_field head) (``b1) (``V1)) ;
        `(`Let {A1 EA1} V1 := `App (val_get_field tail) (``f2) in
           `App (val_set_field tail) (``b1) (``V1)) ;
         `(`Let {A1 EA1} V1 := `App (val_get_field tail) p2 in
            `App (val_set_field tail) p1 (``V1)) ;
          `(`App (val_set_field head) (``f2) (``X)) ;
           `(`App (val_set_field tail) (``f2) (``null)) ;
            `App (val_set_field tail) p2 (``f2))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_get_head.
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@⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆d1┆null⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`(`Let {A1 EA1} V1 := `App (val_get_field head) (``f2) in
         `App (val_set_field head) (``b1) (``V1)) ;
       `(`Let {A1 EA1} V1 := `App (val_get_field tail) (``f2) in
          `App (val_set_field tail) (``b1) (``V1)) ;
        `(`Let {A1 EA1} V1 := `App (val_get_field tail) p2 in
           `App (val_set_field tail) p1 (``V1)) ;
         `(`App (val_set_field head) (``f2) (``d1)) ;
          `(`App (val_set_field tail) (``f2) (``null)) ;
           `App (val_set_field tail) p2 (``f2))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_get_head.
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@⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆d1┆null⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`App (val_set_field head) (``b1) (``x))
⟬*POST@ Bind _ : unit In
        `((`Let {A1 EA1} V1 := `App (val_get_field tail) (``f2) in
            `App (val_set_field tail) (``b1) (``V1)) ;
          `(`Let {A1 EA1} V1 := `App (val_get_field tail) p2 in
             `App (val_set_field tail) p1 (``V1)) ;
           `(`App (val_set_field head) (``f2) (``d1)) ;
            `(`App (val_set_field tail) (``f2) (``null)) ;
             `App (val_set_field tail) p2 (``f2))
        ;
        fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_set_head.
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@⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆null⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`(`Let {A1 EA1} V1 := `App (val_get_field tail) (``f2) in
         `App (val_set_field tail) (``b1) (``V1)) ;
       `(`Let {A1 EA1} V1 := `App (val_get_field tail) p2 in
          `App (val_set_field tail) p1 (``V1)) ;
        `(`App (val_set_field head) (``f2) (``d1)) ;
         `(`App (val_set_field tail) (``f2) (``null)) ;
          `App (val_set_field tail) p2 (``f2))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_get_tail.
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@⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆null⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`App (val_set_field tail) (``b1) (``c2))
⟬*POST@ Bind _ : unit In
        `((`Let {A1 EA1} V1 := `App (val_get_field tail) p2 in
            `App (val_set_field tail) p1 (``V1)) ;
          `(`App (val_set_field head) (``f2) (``d1)) ;
           `(`App (val_set_field tail) (``f2) (``null)) ;
            `App (val_set_field tail) p2 (``f2))
        ;
        fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_set_tail.
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@⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`(`Let {A1 EA1} V1 := `App (val_get_field tail) p2 in
         `App (val_set_field tail) p1 (``V1)) ;
       `(`App (val_set_field head) (``f2) (``d1)) ;
        `(`App (val_set_field tail) (``f2) (``null)) ;
         `App (val_set_field tail) p2 (``f2))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_get_tail.
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@⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b1⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`App (val_set_field tail) p1 (``b2))
⟬*POST@ Bind _ : unit In
        `((`App (val_set_field head) (``f2) (``d1)) ;
          `(`App (val_set_field tail) (``f2) (``null)) ;
           `App (val_set_field tail) p2 (``f2))
        ;
        fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_set_tail.
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@⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`(`App (val_set_field head) (``f2) (``d1)) ;
       `(`App (val_set_field tail) (``f2) (``null)) ;
        `App (val_set_field tail) p2 (``f2))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_set_head.
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@⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆d1┆c2⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`(`App (val_set_field tail) (``f2) (``null)) ;
       `App (val_set_field tail) p2 (``f2))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_set_tail.
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@⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆d1┆null⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b2⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭
CODE (`App (val_set_field tail) p2 (``f2))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
        L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp Triple_set_tail.
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@⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆f2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆d1┆null⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b1┆⟦$MCell┆x┆c2⟧⟭┆⟬Star┆⟬PointsTo┆c2┆⟦$MListSeg┆b2┆L2' ⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    xchange <- (@MListSeg_cons A EA 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
⟬*PRE@⟬Star┆⟬PointsTo┆b1┆⟦$MListSeg┆b2┆x :: L2' ⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆f2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆d1┆null⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b2⟧⟭┆⟬Star┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭┆⟬PointsTo┆f1┆⟦$MListSeg┆b1┆L1 ⟧⟭⟭⟭⟭⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    xchange <- (@MListSeg_concat A EA 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
⟬*PRE@⟬Star┆⟬PointsTo┆f1┆⟦$MListSeg┆b2┆L1 ++ x :: L2' ⟧⟭┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f2┆f2⟧⟭┆⟬Star┆⟬PointsTo┆f2┆⟦$MCell┆d1┆null⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f1┆b2⟧⟭┆⟬PointsTo┆b2┆⟦$MCell┆d2┆null⟧⟭⟭⟭⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆
L1 ++ x :: L2' ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭┆⟬Exist┆f┆⟬Exist┆b┆⟬Exist┆d┆⟬Star┆⟬PointsTo┆p2┆⟦$MCell┆f┆b⟧⟭┆⟬Star┆⟬PointsTo┆f┆⟦$MListSeg┆b┆nil ⟧⟭┆⟬PointsTo┆b┆⟦$MCell┆d┆null⟧⟭⟭⟭⟭⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    xchanges (@MListSeg_nil_intro A EA f2).
  -
A: Type
EA: Enc A
L1, L2: list A
p1, p2: loc
C: L2 = nil
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ L2⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`$(``tt))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ L2⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ subst.
A: Type
EA: Enc A
L1: list A
p1, p2: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ nil⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`$(``tt))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1 ++ nil⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ rew_list.
A: Type
EA: Enc A
L1: list A
p1, p2: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p2┆⟦$MQueue ┆ nil⟧⟭┆⟬PointsTo┆p1┆⟦
$MQueue ┆ L1⟧⟭⟭*⟭
CODE (`$(``tt))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p1┆⟦$MQueue ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
        $MQueue ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxvals.
Qed.