Sepviz Tutorial (Part 1): Heap Predicates as Memory Diagrams

Welcome to Part 1 of the Sepviz tutorial! Discover how our separation-logic visualization tool turns heap predicates into intuitive heap-memory diagrams.

Display all goals and responses

Separation-logic proofs of heap-manipulating programs require careful accounting of objects and pointers in memory. On paper, these proofs are often accompanied by heap-memory diagrams that help authors and readers track the evolution of the program’s abstract state. However, users of interactive theorem provers must instead work with plain-text notations that obscure object relationships.

In Sepviz, we imitate an intuitive diagrammatic notation commonly used in research and educational materials about separation logic, support animation across proof steps, and make it easy to port to new frameworks.

Warm-up

This webpage uses Alectryon, a literate proof tool, to convert Rocq commands and tactics into interactive elements that show their output and let you navigate them, like the Compute command below.

 Compute 1 + 2.= 3
: nat

(A quick how-to page has more about this embedded Rocq interaction.)

The problem

Separation logic is a powerful way to reason about programs that use shared mutable data structures, or in other words, that manipulate heap objects and pointers. Proofs in separation logic (and its extensions) are often performed in interactive theorem provers with one of many different mechanizations. On this page, we will be using Iris.

 From iris.heap_lang Require Import lang proofmode notation.

A problem with using any mechanization of separation logic is that the proofs are hard to follow: proof-writers must work with all the formulae as just algebra, when in reality, the formulae describe data structures and pointers typically explained at a whiteboard or on paper with memory diagrams. Let’s look at a concrete example. (The example we use below and throughout the rest of this tutorial is adapted from CFML, specifically this source file, as an example of a realistic development.)

First, we define a representation predicate isQueue for queues. We assume the definition of isListSeg f L b, which describes a linked list segment L that starts at location f and ends at location b. Note that in Iris' HeapLang, (x, y) denotes a pair of values x and y stored in a single heap cell, and #f denotes the location f represented as a value.

 Definition isQueue (p : loc) (L : list val): iProp Σ :=
   ∃ (f b: loc) (d: val),
     p ↦ (#f, #b) ∗ isListSeg f L b ∗ b ↦ (d, NONEV).

In English, the definition above states that a pointer p is considered to point to a queue containing the elements L if:

p points to a pair with values #f and #b;
f (the front pointer) points to a linked list segment with the elements of L, ending with b; and
b (the back pointer) points to a pair with values d and NONEV, where d is a dummy “end marker” element and NONEV represents the null pointer.

Now, the following function transfer concatenates two queues in place. It takes as input two pointers, p1 and p2, that are assumed to point to queues.

 Definition is_empty : val :=
   λ: "p",
     let: "q" := !"p" in
     let: "f" := Fst "q" in
     let: "b" := Snd "q" in
     "f" = "b".

 Definition transfer : val :=
   λ: "p1" "p2",
     if: ~(is_empty "p2") then
       let: "b1" := Snd !"p1" in
       let: "f2" := Fst !"p2" in
       let: "d" := Fst !"b1" in
       "b1" <- (Fst !"f2", Snd !"f2");;
       "p1" <- (Fst !"p1", Snd !"p2");;
       "f2" <- ("d", NONEV);;
       "p2" <- (Fst !"p2", "f2")
     else
       #().

We would like to prove that if the two input pointers indeed point to valid, non-aliased queues that contain the elements in L1 and L2, respectively (the precondition), then after executing the code, the queue at the first pointer will contain the concatenation L1 ++ L2, and the queue at the second pointer will be empty (the postcondition).

 Lemma transfer_spec (L1 L2 : list val) (p1 p2 : loc) :
   {{{ isQueue p1 L1 ∗ isQueue p2 L2 }}}
     transfer #p1 #p2
   {{{ RET #(); isQueue p1 (L1 ++ L2) ∗ isQueue p2 [] }}}.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
{{{ isQueue p1 L1 ∗ isQueue p2 L2 }}}
  transfer #p1 #p2
{{{ RET #(); isQueue p1 (L1 ++ L2) ∗ isQueue p2 [] }}}
 Proof.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
{{{ isQueue p1 L1 ∗ isQueue p2 L2 }}}
  transfer #p1 #p2
{{{ RET #(); isQueue p1 (L1 ++ L2) ∗ isQueue p2 [] }}}

We won’t walk through the entire proof, but instead jump to the middle of the proof and focus on two steps that illustrate our point. (The proof is omitted below but available in full at the end of this page.)

In the step below, we symbolically evaluate the code that sets the back pointer of the first queue to the back pointer of the second queue. Above the wp_store tactic we see the symbolic state before setting the back pointer, and below the state after:

Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
"Hp1" : p1 ↦ (#f1, #b1)
"HL1" : isListSeg f1 L1 b1
"Hb1" : b1 ↦ (x, #c2)
"HΦ" : isQueue p1 (L1 ++ x :: L2') ∗ 
       isQueue p2 [] -∗ Φ #()
"Hp2" : p2 ↦ (#f2, #b2)
"Hb2" : b2 ↦ (d2, NONEV)
"Hf2" : f2 ↦ (x, #c2)
"HL2'" : isListSeg c2 L2' b2
--------------------------------------∗
WP #p1 <- (#f1, #b2)%V;; 
   #f2 <- (d1, NONEV);; #p2 <- (Fst ! #p2, #f2)
{{ v, Φ v }}   wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
"Hp1" : p1 ↦ (#f1, #b2)
"HL1" : isListSeg f1 L1 b1
"Hb1" : b1 ↦ (x, #c2)
"HΦ" : isQueue p1 (L1 ++ x :: L2') ∗ 
       isQueue p2 [] -∗ Φ #()
"Hp2" : p2 ↦ (#f2, #b2)
"Hb2" : b2 ↦ (d2, NONEV)
"Hf2" : f2 ↦ (x, #c2)
"HL2'" : isListSeg c2 L2' b2
--------------------------------------∗
WP #f2 <- (d1, NONEV);; #p2 <- (Fst ! #p2, #f2)
{{ v, Φ v }}

And then, we simulate setting the pair pointed-to by f2, the front pointer of the second queue, to d1 and the null pointer, where d1 is the queue-ending dummy value we previously read from the first queue:

   wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
"Hp1" : p1 ↦ (#f1, #b2)
"HL1" : isListSeg f1 L1 b1
"Hb1" : b1 ↦ (x, #c2)
"HΦ" : isQueue p1 (L1 ++ x :: L2') ∗ 
       isQueue p2 [] -∗ Φ #()
"Hp2" : p2 ↦ (#f2, #b2)
"Hb2" : b2 ↦ (d2, NONEV)
"Hf2" : f2 ↦ (d1, NONEV)
"HL2'" : isListSeg c2 L2' b2
--------------------------------------∗
WP #p2 <- (Fst ! #p2, #f2) {{ v, Φ v }}

Could you follow what happened? Us neither. To understand the proof, we have to follow pointers by hand to keep track of how the data structure is changing, maybe even drawing it out on scratch paper. This quickly gets cumbersome for longer or more complicated proofs. This is the problem that our tool solves.

Our solution

Let’s try the same proof again, with some diagrammatic aids. We imitate an intuitive diagrammatic notation commonly used in research and educational materials about separation logic:

Each points-to predicate has its location at the top left, the type of representation predicate at the top right, and a body.
- The body of a flat representation predicate, like a (#f1, #b1) pair, is visualized as a table, with one row for every argument.
- The body of an abstract representation predicate, like an isListSeg linked list segment, is shown simply as a textual label.
When an argument of a predicate is a location, i.e., a pointer, it is visualized as an arrow. If the argument is explicitly shown as a row in a table, the pointer starts at a black dot in the same row.
Top-level pointers (e.g. p1) are shown to the left of the whole structure.

⟬ Star ┆ ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair ┆ 
           ⟦ $LitV ┆ f1 ⟧ ┆ ⟦ $LitV ┆ b2 ⟧
           ⟧ ┆ DfracOwn 1
         ⟭
  ┆ ⟬ Star ┆ ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭
      ┆ ⟬ Star ┆ ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭
          ┆ ⟬ Star ┆ ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                       ┆ ⟦ $LitV ┆ f2 ⟧
                       ┆ ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                       DfracOwn 1
                     ⟭
              ┆ ⟬ Star ┆ ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair
                           ┆ d2 ┆ NONEV ⟧ ┆ 
                           DfracOwn 1
                         ⟭
                  ┆ ⟬ Star ┆ ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair
                               ┆ x ┆ 
                               ⟦ $LitV ┆ c2 ⟧
                               ⟧ ┆ DfracOwn 1
                             ⟭
                      ┆ ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧
                        ⟭
                    ⟭
                ⟭
            ⟭
        ⟭
    ⟭
⟭
     : iPropI Σ

Now for the proof. First, we show just the two steps we saw in the previous section. Then, we include the full illustrated proof below, as optional reading.

 Lemma transfer_spec' (L1 L2 : list val) (p1 p2 : loc) :
 {{{ isQueue p1 L1 ∗ isQueue p2 L2 }}}
     transfer #p1 #p2
 {{{ RET #(); isQueue p1 (L1 ++ L2) ∗ isQueue p2 [] }}}.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
⟬* PRE @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
         ⟭ *⟭
transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
RET ⟦ $LitV ┆ () ⟧;
⟬* POST @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ L2⟧ ⟭
            ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
          ⟭ *⟭
 Proof.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
⟬* PRE @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
         ⟭ *⟭
transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
RET ⟦ $LitV ┆ () ⟧;
⟬* POST @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ L2⟧ ⟭
            ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
          ⟭ *⟭

Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p1 ⟧ <-
   (⟦ $LitV ┆ f1 ⟧, ⟦ $LitV ┆ b2 ⟧)%V;; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}   wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

   wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

Try comparing the diagrams. In the first pair, p1 detaches from b1 and attaches to b2. In the second pair, f2 detaches from c2, and f2's first field (a value) changes from x to d1.

If you want to see the full proof, keep reading. Else, this concludes Part 1 of the tutorial. Continue to Part 2: Interactive proofs, Animations, and Extensions…

Full proof

 Lemma transfer_spec_full (L1 L2 : list val) (p1 p2 : loc) :
   {{{ isQueue p1 L1 ∗ isQueue p2 L2 }}}
     transfer #p1 #p2
   {{{ RET #(); isQueue p1 (L1 ++ L2) ∗ isQueue p2 [] }}}.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
⟬* PRE @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
         ⟭ *⟭
transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
RET ⟦ $LitV ┆ () ⟧;
⟬* POST @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ L2⟧ ⟭
            ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
          ⟭ *⟭
 Proof.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
⟬* PRE @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
         ⟭ *⟭
transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
RET ⟦ $LitV ┆ () ⟧;
⟬* POST @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ L2⟧ ⟭
            ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
          ⟭ *⟭
   iIntros "%Φ [HQ1 HQ2] HΦ".Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Modality ┆ ▷ ┆ ⟬ Wand ┆ 
                                   ⟬ 
                                   Star ┆ 
                                   ⟬ PointsTo┆p1┆⟦isQueue┆
                                   L1 ++ L2⟧ ⟭
                                   ┆ 
                                   ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                                   ⟭ ⟭
                                   ┆ 
                                   Φ ⟦ $LitV ┆ ()%V ⟧
                                 ⟭
                ⟭ *⟭
--------------------------------------∗
WP transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧ {{ v, Φ v }}
   rewrite /transfer.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Modality ┆ ▷ ┆ ⟬ Wand ┆ 
                                   ⟬ 
                                   Star ┆ 
                                   ⟬ PointsTo┆p1┆⟦isQueue┆
                                   L1 ++ L2⟧ ⟭
                                   ┆ 
                                   ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                                   ⟭ ⟭
                                   ┆ 
                                   Φ ⟦ $LitV ┆ ()%V ⟧
                                 ⟭
                ⟭ *⟭
--------------------------------------∗
WP (λ: "p1" "p2",
      if: ~ is_empty "p2"
      then let: "b1" := Snd ! "p1" in
           let: "f2" := Fst ! "p2" in
           let: "d" := Fst ! "b1" in
           "b1" <- (Fst ! "f2", Snd ! "f2");; 
           "p1" <- (Fst ! "p1", Snd ! "p2");; 
           "f2" <- ("d", NONEV);; 
           "p2" <- (Fst ! "p2", "f2")
      else ⟦ $LitV ┆ () ⟧)%V
     ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
{{ v, Φ v }}
   wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ L2⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
--------------------------------------∗
WP if: ~ is_empty ⟦ $LitV ┆ p2 ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}
   wp_apply (is_empty_spec with "HQ2").Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ L2⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
--------------------------------------∗
⟬ Wand ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
  ┆ WP if: ~ ⟦ $LitV ┆ bool_decide (L2 = []) ⟧
       then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
            let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
            let: "d" := Fst ! "b1" in
            "b1" <- (Fst ! "f2", Snd ! "f2");; 
            ⟦ $LitV ┆ p1 ⟧ <-
            (Fst ! ⟦ $LitV ┆ p1 ⟧,
             Snd ! ⟦ $LitV ┆ p2 ⟧);; 
            "f2" <- ("d", NONEV);; 
            ⟦ $LitV ┆ p2 ⟧ <-
            (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
       else ⟦ $LitV ┆ ()%V ⟧
    {{ v, Φ v }}
⟭ iIntros "HQ2".Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ L2⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide (L2 = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}

transfer has two branches depending on whether the second queue is empty or not. The proof thus has the same two cases. If it isn’t empty, we can destruct L2 as x :: L2'.

   destruct L2 as [ | x L2'].Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ []⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide ([] = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}
Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide (x :: L2' = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}
   -Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ []⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide ([] = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ []⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=> Φ ⟦ $LitV ┆ ()%V ⟧ iApply "HΦ".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=>
  ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ []⟧ ⟭
    ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
  ⟭ rewrite app_nil_r.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=>
  ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
    ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
  ⟭ iModIntro.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
  ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
⟭ by iFrame.
   -Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide (x :: L2' = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
   let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! "b1" in
   "b1" <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}

Then, symbolically executing the code, we read some values…

     iDestruct "HQ1" as (f1 b1 d1) "(Hp1 & HL1 & Hb1)".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
   let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! "b1" in
   "b1" <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}
     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "b1" := Snd (⟦ $LitV ┆ f1 ⟧, ⟦ $LitV ┆ b1 ⟧)%V in
   let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! "b1" in
   "b1" <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! ⟦ $LitV ┆ b1 ⟧ in
   ⟦ $LitV ┆ b1 ⟧ <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}
     iDestruct "HQ2" as (f2 b2 d2) "(Hp2 & HL2 & Hb2)".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! ⟦ $LitV ┆ b1 ⟧ in
   ⟦ $LitV ┆ b1 ⟧ <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}
     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP let: "f2" := Fst (⟦ $LitV ┆ f2 ⟧, ⟦ $LitV ┆ b2 ⟧)%V in
   let: "d" := Fst ! ⟦ $LitV ┆ b1 ⟧ in
   ⟦ $LitV ┆ b1 ⟧ <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP let: "d" := Fst (d1, NONEV)%V in
   ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd ! ⟦ $LitV ┆ f2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd ! ⟦ $LitV ┆ f2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}
     iDestruct (isListSeg_cons_inv with "HL2") as (c2) "[Hf2 HL2']".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd ! ⟦ $LitV ┆ f2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}
     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd (x, ⟦ $LitV ┆ c2 ⟧)%V);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst (x, ⟦ $LitV ┆ c2 ⟧)%V, ⟦ $LitV ┆ c2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

… and set Fst b1 (the queue-ending dummy element d1) to the value x, the first element of L2; set Snd b1 (originally the null pointer) to #c2, the front pointer of list segment L2'.

     wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

Next, we update the back pointer of the first queue to point to the original ending pair of the second queue.

     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧,
    Snd (⟦ $LitV ┆ f2 ⟧, ⟦ $LitV ┆ b2 ⟧)%V);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p1 ⟧ <-
   (Fst (⟦ $LitV ┆ f1 ⟧, ⟦ $LitV ┆ b1 ⟧)%V,
    ⟦ $LitV ┆ b2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

We set the pair pointed-to by the second queue's front pointer f2 to (d1, NONEV) (the first queue's original queue-ending element and the null pointer). After that, we update this queue's back pointer to f2 as well.

     wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p2 ⟧ <-
   (Fst (⟦ $LitV ┆ f2 ⟧, ⟦ $LitV ┆ b2 ⟧)%V,
    ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ f2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=> Φ ⟦ $LitV ┆ ()%V ⟧

Having moved all the elements of the queue at p2 to p1, we apply some lemmas to fold back and unify the representations of the queues between the pre- and postconditions.

     iApply "HΦ"; iModIntro.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ f2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
  ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
⟭
     iPoseProof (isQueue_fold_empty with "[$Hp2 $Hf2]") as "HQ2".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
  ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
⟭
     iFrame "HQ2".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     iPoseProof (isListSeg_cons_app with "[$Hb1 $HL2']") as "HL2".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆b1┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     iPoseProof (isListSeg_concat with "[$HL1 $HL2]") as "HL".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL" : ⟬ PointsTo┆f1┆⟦isListSeg┆
                L1 ++ x :: L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     iPoseProof (isQueue_fold with "[$Hp1 $HL $Hb2]") as "HQ1".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆
                 L1 ++ x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     by iFrame.
 Qed.