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┆[]⟧⟭⟭*⟭
  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 }}
  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┆[]⟧⟭⟭ 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 }}
    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 }} 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 }}
    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 }}
    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⟧
    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.