1 subgoal (ID 16822)

  Σ : gFunctors
  proto_chanG0 : proto_chanG Σ
  heapG0 : heapG Σ
  l, v : val
  ls : list val
  p1 : iProto Σ
  pc : val → (laterO (proto val (iPropO Σ) (iPropO Σ)) -n> iPropO Σ) -n> iPropO Σ
  r' : val
  rs' : list val
  Heq : S (strings.length ls + S (strings.length rs')) =
        strings.length (v :: ls) + strings.length (r' :: rs')
  pc' : val → (laterO (proto val (iPropO Σ) (iPropO Σ)) -n> iPropO Σ) -n> iPropO Σ
  p1' : iProto Σ
  ============================
  "IH" : ∀ (a : val) (a0 a1 : list val) (a2 : iProto Σ)
           (a3 : val
                 → (laterO (proto val (iPropO Σ) (iPropO Σ)) -n> iPropO Σ) -n>
                   iPropO Σ),
           ⌜(strings.length ls + S (strings.length rs'))%nat =
            (strings.length a0 + strings.length a1)%nat⌝
           → proto_interp_aux (strings.length (a :: a0) + strings.length a1)
               (a :: a0) a1 a2 (proto_message Receive a3)
             -∗ ∃ p2 : iProto Σ,
                  a3 a (proto_eq_next p2)
                  ∗ proto_interp_aux (strings.length a0 + strings.length a1) a0 a1
                      a2 p2
  --------------------------------------□
  "Heq" : p1 ≡ proto_message Receive pc'
  "Hpc'" : pc' r' (proto_eq_next p1')
  "Hrec" : (∃ (v0 : val) (l' : list val) (pc0 : val
                                                → (laterO
                                                     (proto val
                                                       (iPropO Σ)
                                                       (iPropO Σ)) -n>
                                                   iPropO Σ) -n>
                                                  iPropO Σ)
              (p2' : iProto Σ),
              ⌜l :: v :: ls = v0 :: l'⌝
              ∗ proto_message Receive pc ≡ proto_message Receive pc0
                ∗ pc0 v0 (proto_eq_next p2')
                  ∗ (fix
                     proto_interp_aux (Σ0 : gFunctors) (n : nat)
                                      (l0 r : list val)
                                      (p0 p2 : iProto Σ0) {struct n} :
                     iProp Σ0 :=
                       match n with
                       | 0 => ⌜l0 = []⌝ ∧ ⌜r = []⌝ ∧ iProto_dual p0 ≡ p2
                       | S n0 =>
                           (∃ (v1 : val) (l'0 : list val)
                              (pc1 : val
                                     → (laterO (proto val (iPropO Σ0) (iPropO Σ0)) -n>
                                        iPropO Σ0) -n> iPropO Σ0)
                              (p2'0 : iProto Σ0),
                              ⌜l0 = v1 :: l'0⌝
                              ∗ p2 ≡ proto_message Receive pc1
                                ∗ pc1 v1 (proto_eq_next p2'0)
                                  ∗ proto_interp_aux Σ0 n0 l'0 r p0 p2'0)
                           ∨ (∃ (v1 : val) (r'0 : list val)
                                (pc1 : val
                                       → (laterO (proto val (iPropO Σ0) (iPropO Σ0)) -n>
                                          iPropO Σ0) -n>
                                         iPropO Σ0) (p1'0 : iProto Σ0),
                                ⌜r = v1 :: r'0⌝
                                ∗ p0 ≡ proto_message Receive pc1
                                  ∗ pc1 v1 (proto_eq_next p1'0)
                                    ∗ proto_interp_aux Σ0 n0 l0 r'0 p1'0 p2)
                       end) Σ
                      ((fix add (n m : nat) {struct n} : nat :=
                          match n with
                          | 0 => m
                          | S p => S (add p m)
                          end)
                         ((fix length (l0 : list val) : nat :=
                             match l0 with
                             | [] => 0
                             | _ :: l'0 => S (length l'0)
                             end) ls) (strings.length (r' :: rs'))) l' rs' p1' p2')
           ∨ (∃ (v0 : val) (r'0 : list val) (pc0 : val
                                                   → (laterO
                                                       (proto val
                                                       (iPropO Σ)
                                                       (iPropO Σ)) -n>
                                                      iPropO Σ) -n>
                                                     iPropO Σ)
                (p1'0 : iProto Σ),
                ⌜rs' = v0 :: r'0⌝
                ∗ p1' ≡ proto_message Receive pc0
                  ∗ pc0 v0 (proto_eq_next p1'0)
                    ∗ (fix
                       proto_interp_aux (Σ0 : gFunctors)
                                        (n : nat) (l0 r : list val)
                                        (p0 p2 : iProto Σ0) {struct n} :
                       iProp Σ0 :=
                         match n with
                         | 0 => ⌜l0 = []⌝ ∧ ⌜r = []⌝ ∧ iProto_dual p0 ≡ p2
                         | S n0 =>
                             (∃ (v1 : val) (l' : list val)
                                (pc1 : val
                                       → (laterO (proto val (iPropO Σ0) (iPropO Σ0)) -n>
                                          iPropO Σ0) -n>
                                         iPropO Σ0) (p2' : iProto Σ0),
                                ⌜l0 = v1 :: l'⌝
                                ∗ p2 ≡ proto_message Receive pc1
                                  ∗ pc1 v1 (proto_eq_next p2')
                                    ∗ proto_interp_aux Σ0 n0 l' r p0 p2')
                             ∨ (∃ (v1 : val) (r'1 : list val)
                                  (pc1 : val
                                         → (laterO
                                              (proto val (iPropO Σ0) (iPropO Σ0)) -n>
                                            iPropO Σ0) -n>
                                           iPropO Σ0) (p1'1 : iProto Σ0),
                                  ⌜r = v1 :: r'1⌝
                                  ∗ p0 ≡ proto_message Receive pc1
                                    ∗ pc1 v1 (proto_eq_next p1'1)
                                      ∗ proto_interp_aux Σ0 n0 l0 r'1 p1'1 p2)
                         end) Σ
                        ((fix add (n m : nat) {struct n} : nat :=
                            match n with
                            | 0 => m
                            | S p => S (add p m)
                            end)
                           ((fix length (l0 : list val) : nat :=
                               match l0 with
                               | [] => 0
                               | _ :: l' => S (length l')
                               end) ls) (strings.length (r' :: rs')))
                        (l :: v :: ls) r'0 p1'0 (proto_message Receive pc))
  --------------------------------------∗
  ∃ p2 : iProto Σ,
    pc l (proto_eq_next p2)
    ∗ proto_interp_aux (strings.length (v :: ls) + strings.length (r' :: rs'))
        (v :: ls) (r' :: rs') p1 p2