Quelle  Qmsg_Lifting.thy

(*  Title:       Qmsg_Lifting.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Lifting rules for parallel compositions with QMSG"

theory Qmsg_Lifting
imports Qmsg OAWN_SOS Inv_Cterms OAWN_Invariants
begin

lemma oseq_no_change_on_send:
  fixes σ s a σ' s'
  assumes "((σ, s), a, (σ', s')) ∈ oseqp_sos Γ i"
  shows "case a of
           broadcast m ==> σ' i = σ i
         | groupcast ips m ==> σ' i = σ i
         | unicast ips m ==> σ' i = σ i
         | ¬unicast ips ==> σ' i = σ i
         | send m ==> σ' i = σ i
         | deliver m ==> σ' i = σ i
         | _ ==> True"
  using assms by induction simp_all

lemma qmsg_no_change_on_send_or_receive:
    fixes σ s a σ' s'
  assumes "((σ, s), a, (σ', s')) ∈ oparp_sos i (oseqp_sos Γ i) (seqp_sos Γ_QMSG)"
      and "a ≠ τ"
    shows "σ' i = σ i"
  proof -
    from assms(1) obtain p q p' q'
      where "((σ, (p, q)), a, (σ', (p', q'))) ∈ oparp_sos i (oseqp_sos Γ i) (seqp_sos Γ_QMSG)"
      by (cases s, cases s', simp)
    thus ?thesis
    proof
      assume "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i"
         and "∧m. a ≠ receive m"
      with ‹a ≠ τ› show "σ' i = σ i"
        by - (drule oseq_no_change_on_send, cases a, auto)
    next
      assume "(q, a, q') ∈ seqp_sos Γ_QMSG"
         and "σ' i = σ i"
        thus "σ' i = σ i" by simp
    next
      assume "a = τ" with ‹a ≠ τ› show ?thesis by auto
    qed
  qed

lemma qmsg_msgs_not_empty:
  "qmsg ⊨!!! onl Γ_QMSG (λ(msgs, l). l = ()-:1 ⟶ msgs ≠ [])"
  by inv_cterms

lemma qmsg_send_from_queue:
  "qmsg ⊨!!!_A (λ((msgs, q), a, _). sendmsg (λm. m∈set msgs) a)"
  proof -
    have "qmsg ⊨!!!_A onll Γ_QMSG (λ((msgs, _), a, _). sendmsg (λm. m∈set msgs) a)"
      by (inv_cterms inv add: onl_invariant_sterms [OF qmsg_wf qmsg_msgs_not_empty])
    thus ?thesis
      by (rule step_invariant_weakenE) (auto dest!: onllD)
  qed

lemma qmsg_queue_contents:
  "qmsg ⊨!!!_A (λ((msgs, q), a, (msgs', q')). case a of
                                             receive m ==> set msgs' ⊆ set (msgs @ [m])
                                           | _ ==> set msgs' ⊆ set msgs)"
  proof -
    have "qmsg ⊨!!!_A onll Γ_QMSG (λ((msgs, q), a, (msgs', q')).
                                     case a of
                                       receive m ==> set msgs' ⊆ set (msgs @ [m])
                                     | _ ==> set msgs' ⊆ set msgs)"
      by (inv_cterms) (clarsimp simp add: in_set_tl)+
    thus ?thesis
      by (rule step_invariant_weakenE) (auto dest!: onllD)
  qed

lemma qmsg_send_receive_or_tau:
  "qmsg ⊨!!!_A (λ(_, a, _). ∃m. a = send m ∨ a = receive m ∨ a = τ)"
  proof -
   have "qmsg ⊨!!!_A onll Γ_QMSG (λ(_, a, _). ∃m. a = send m ∨ a = receive m ∨ a = τ)"
     by inv_cterms
   thus ?thesis
    by rule (auto dest!: onllD)
  qed

lemma par_qmsg_oreachable:
  assumes "(σ, ζ) ∈ oreachable (A ⟨⟨ qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
           (is "_ ∈ oreachable _ ?owS _")
      and pinv: "A ⊨_A (otherwith S {i} (orecvmsg R), other U {i} →)
                       globala (λ(σ, _, σ'). U (σ i) (σ' i))"
      and ustutter: "∧ξ. U ξ ξ"
      and sgivesu: "∧ξ ξ'. S ξ ξ' ==> U ξ ξ'"
      and upreservesq: "∧σ σ' m. [ ∀j. U (σ j) (σ' j); R σ m ] ==> R σ' m"
  shows "(σ, fst ζ) ∈ oreachable A ?owS (other U {i})
         ∧ snd ζ ∈ reachable qmsg (recvmsg (R σ))
         ∧ (∀m∈set (fst (snd ζ)). R σ m)"
  using assms(1) proof (induction rule: oreachable_pair_induct)
    fix σ pq
    assume "(σ, pq) ∈ init (A ⟨⟨ qmsg)"
    then obtain p ms q where "pq = (p, (ms, q))"
                         and "(σ, p) ∈ init A"
                         and "(ms, q) ∈ init qmsg"
      by (clarsimp simp del: Γ_{QMSG_simps})
    from this(2) have "(σ, p) ∈ oreachable A ?owS (other U {i})" ..
    moreover from ‹(ms, q) ∈ init qmsg› have "(ms, q) ∈ reachable qmsg (recvmsg (R σ))" ..
    moreover from ‹(ms, q) ∈ init qmsg› have "ms = []"
        unfolding σ_{QMSG_def} by simp
    ultimately show "(σ, fst pq) ∈ oreachable A ?owS (other U {i})
                     ∧ snd pq ∈ reachable qmsg (recvmsg (R σ))
                     ∧ (∀m∈set (fst (snd pq)). R σ m)"
      using ‹pq = (p, (ms, q))› by simp
  next
    note Γ_{QMSG_simps} [simp del]
    case (other σ pq σ')
    hence "(σ, fst pq) ∈ oreachable A ?owS (other U {i})"
      and "other U {i} σ σ'"
      and qr: "snd pq ∈ reachable qmsg (recvmsg (R σ))"
      and "∀m∈set (fst (snd pq)). R σ m"
      by simp_all
    from ‹other U {i} σ σ'› and ustutter have "∀j. U (σ j) (σ' j)"
        by (clarsimp elim!: otherE) metis
    from ‹other U {i} σ σ'›
     and ‹(σ, fst pq) ∈ oreachable A ?owS (other U {i})›
      have "(σ', fst pq) ∈ oreachable A ?owS (other U {i})"
        by - (rule oreachable_other')
    moreover have "∀m∈set (fst (snd pq)). R σ' m"
    proof
      fix m assume "m ∈ set (fst (snd pq))"
      with ‹∀m∈set (fst (snd pq)). R σ m› have "R σ m" ..
      with ‹∀j. U (σ j) (σ' j)› show "R σ' m" by (rule upreservesq)
    qed
    moreover from qr have "snd pq ∈ reachable qmsg (recvmsg (R σ'))"
    proof
      fix a
      assume "recvmsg (R σ) a"
      thus "recvmsg (R σ') a"
      proof (rule recvmsgE [where R=R])
        fix m assume "R σ m"
        with ‹∀j. U (σ j) (σ' j)› show "R σ' m" by (rule upreservesq)
      qed
    qed
    ultimately show ?case using qr by simp
  next
    case (local σ pq σ' pq' a)
    obtain p ms q p' ms' q' where "pq = (p, (ms, q))"
                              and "pq' = (p', (ms', q'))"
      by (cases pq, cases pq') metis
    with local.hyps local.IH
      have pqtr: "((σ, (p, (ms, q))), a, (σ', (p', (ms', q'))))
                    ∈ oparp_sos i (trans A) (seqp_sos Γ_QMSG)"
        and por: "(σ, p) ∈ oreachable A ?owS (other U {i})"
        and qr: "(ms, q) ∈ reachable qmsg (recvmsg (R σ))"
        and "∀m∈set ms. R σ m"
        and "?owS σ σ' a"
      by (simp_all del: Γ_{QMSG_simps})

    from ‹?owS σ σ' a› have "∀j. j≠i ⟶ S (σ j) (σ' j)"
      by (clarsimp dest!: otherwith_syncD)
    with sgivesu have "∀j. j≠i ⟶ U (σ j) (σ' j)" by simp

    from ‹?owS σ σ' a› have "orecvmsg R σ a" by (rule otherwithE)
    hence "recvmsg (R σ) a" ..

    from pqtr have "(σ', p') ∈ oreachable A ?owS (other U {i})
                  ∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
                  ∧ (∀m∈set ms'. R σ' m)"
    proof
      assume "((σ, p), a, (σ', p')) ∈ trans A"
         and "∧m. a ≠ receive m"
         and "(ms', q') = (ms, q)"
      from this(1) have ptr: "((σ, p), a, (σ', p')) ∈ trans A" by simp
      with pinv por and ‹?owS σ σ' a› have "U (σ i) (σ' i)"
        by (auto dest!: ostep_invariantD)
      with ‹∀j. j≠i ⟶ U (σ j) (σ' j)› have "∀j. U (σ j) (σ' j)" by auto

      hence recvmsg': "∧a. recvmsg (R σ) a ==> recvmsg (R σ') a"
        by (auto elim!: recvmsgE [where R=R] upreservesq)

      from por ptr ‹?owS σ σ' a› have "(σ', p') ∈ oreachable A ?owS (other U {i})"
        by - (rule oreachable_local')

      moreover have "(ms', q') ∈ reachable qmsg (recvmsg (R σ'))"
      proof -
        from qr and ‹(ms', q') = (ms, q)›
          have "(ms', q') ∈ reachable qmsg (recvmsg (R σ))" by simp
        thus ?thesis by (rule reachable_weakenE) (erule recvmsg')
      qed

      moreover have "∀m∈set ms'. R σ' m"
      proof
        fix m
        assume "m∈set ms'"
        with ‹(ms', q') = (ms, q)› have "m∈set ms" by simp
        with ‹∀m∈set ms. R σ m› have "R σ m" ..
        with ‹∀j. U (σ j) (σ' j)› show "R σ' m"
          by (rule upreservesq)
      qed

      ultimately show
        "(σ', p') ∈ oreachable A ?owS (other U {i})
          ∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
          ∧ (∀m∈set ms'. R σ' m)" by simp_all
    next
      assume qtr: "((ms, q), a, (ms', q')) ∈ seqp_sos Γ_QMSG"
         and "∧m. a ≠ send m"
         and "p' = p"
         and "σ' i = σ i"

      from this(4) and ‹∧ξ. U ξ ξ› have "U (σ i) (σ' i)" by simp
      with ‹∀j. j≠i ⟶ U (σ j) (σ' j)› have "∀j. U (σ j) (σ' j)" by auto

      hence recvmsg': "∧a. recvmsg (R σ) a ==> recvmsg (R σ') a"
        by (auto elim!: recvmsgE [where R=R] upreservesq)

      from qtr have tqtr: "((ms, q), a, (ms', q')) ∈ trans qmsg" by simp

      from ‹∀j. U (σ j) (σ' j)› and  ‹σ' i = σ i› have "other U {i} σ σ'" by auto
      with por and ‹p' = p›
        have "(σ', p') ∈ oreachable A ?owS (other U {i})"
          by (auto dest: oreachable_other)

      moreover have "(ms', q') ∈ reachable qmsg (recvmsg (R σ'))"
      proof (rule reachable_weakenE [where P="recvmsg (R σ)"])
        from qr tqtr ‹recvmsg (R σ) a› show "(ms', q') ∈ reachable qmsg (recvmsg (R σ))" ..
      qed (rule recvmsg')

      moreover have "∀m∈set ms'. R σ' m"
      proof
        fix m
        assume "m ∈ set ms'"
        moreover have "case a of receive m ==> set ms' ⊆ set (ms @ [m]) | _ ==> set ms' ⊆ set ms"
          proof -
            from qr have "(ms, q) ∈ reachable qmsg TT" ..
            thus ?thesis using tqtr
              by (auto dest!: step_invariantD [OF qmsg_queue_contents])
          qed
        ultimately have "R σ m" using ‹∀m∈set ms. R σ m› and ‹orecvmsg R σ a›
          by (cases a) auto
        with ‹∀j. U (σ j) (σ' j)› show "R σ' m"
          by (rule upreservesq)
      qed

      ultimately show "(σ', p') ∈ oreachable A ?owS (other U {i})
                     ∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
                     ∧ (∀m∈set ms'. R σ' m)" by simp
    next
      fix m
      assume "a = τ"
         and "((σ, p), receive m, (σ', p')) ∈ trans A"
         and "((ms, q), send m, (ms', q')) ∈ seqp_sos Γ_QMSG"
      from this(2-3)
        have ptr: "((σ, p), receive m, (σ', p')) ∈ trans A"
         and qtr: "((ms, q), send m, (ms', q')) ∈ trans qmsg" by simp_all

      from qr have "(ms, q) ∈ reachable qmsg TT" ..
      with qtr have "m ∈ set ms"
        by (auto dest!: step_invariantD [OF qmsg_send_from_queue])
      with ‹∀m∈set ms. R σ m› have "R σ m" ..
      hence "orecvmsg R σ (receive m)" by simp

      with ‹∀j. j≠i ⟶ S (σ j) (σ' j)› have "?owS σ σ' (receive m)"
        by (auto intro!: otherwithI)
      with pinv por ptr have "U (σ i) (σ' i)"
        by (auto dest!: ostep_invariantD)
      with ‹∀j. j≠i ⟶ U (σ j) (σ' j)› have "∀j. U (σ j) (σ' j)" by auto
      hence recvmsg': "∧a. recvmsg (R σ) a ==> recvmsg (R σ') a"
        by (auto elim!: recvmsgE [where R=R] upreservesq)

      from por ptr have "(σ', p') ∈ oreachable A ?owS (other U {i})"
        using ‹?owS σ σ' (receive m)› by - (erule(1) oreachable_local, simp)

      moreover have "(ms', q') ∈ reachable qmsg (recvmsg (R σ'))"
      proof (rule reachable_weakenE [where P="recvmsg (R σ)"])
        have "recvmsg (R σ) (send m)" by simp
        with qr qtr show "(ms', q') ∈ reachable qmsg (recvmsg (R σ))" ..
      qed (rule recvmsg')

      moreover have "∀m∈set ms'. R σ' m"
      proof
        fix m
        assume "m ∈ set ms'"
        moreover have "set ms' ⊆ set ms"
          proof -
            from qr have "(ms, q) ∈ reachable qmsg TT" ..
            thus ?thesis using qtr
              by (auto dest!: step_invariantD [OF qmsg_queue_contents])
          qed
        ultimately have "R σ m" using ‹∀m∈set ms. R σ m› by auto
        with ‹∀j. U (σ j) (σ' j)› show "R σ' m"
          by (rule upreservesq)
      qed

      ultimately show "(σ', p') ∈ oreachable A ?owS (other U {i})
                     ∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
                     ∧ (∀m∈set ms'. R σ' m)" by simp
    qed
    with ‹pq = (p, (ms, q))› and ‹pq' = (p', (ms', q'))› show ?case
      by (simp_all del: Γ_{QMSG_simps})
  qed

lemma par_qmsg_oreachable_statelessassm:
  assumes "(σ, ζ) ∈ oreachable (A ⟨⟨ qmsg)
                               (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})"
      and ustutter: "∧ξ. U ξ ξ"
  shows "(σ, fst ζ) ∈ oreachable A (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})
         ∧ snd ζ ∈ reachable qmsg (recvmsg R)
         ∧ (∀m∈set (fst (snd ζ)). R m)"
  proof -
    from assms(1)
      have "(σ, ζ) ∈ oreachable (A ⟨⟨ qmsg)
                                (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)))
                                (other (λ_ _. True) {i})" by auto
    moreover
      have "A ⊨_A (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)),
                  other (λ_ _. True) {i} →) globala (λ(σ, _, σ'). True)"
        by auto
    ultimately
      obtain "(σ, fst ζ) ∈ oreachable A
                           (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R))) (other (λ_ _. True) {i})"
         and  *: "snd ζ ∈ reachable qmsg (recvmsg R)"
         and **: "(∀m∈set (fst (snd ζ)). R m)"
        by (auto dest!: par_qmsg_oreachable)
    from this(1)
      have "(σ, fst ζ) ∈ oreachable A (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})"
        by rule auto
    thus ?thesis using * ** by simp
  qed

lemma lift_into_qmsg:
  assumes "A ⊨ (otherwith S {i} (orecvmsg R), other U {i} →) global P"
      and "∧ξ. U ξ ξ"
      and "∧ξ ξ'. S ξ ξ' ==> U ξ ξ'"
      and "∧σ σ' m. [ ∀j. U (σ j) (σ' j); R σ m ] ==> R σ' m"
      and "A ⊨_A (otherwith S {i} (orecvmsg R), other U {i} →)
                 globala (λ(σ, _, σ'). U (σ i) (σ' i))"
    shows "A ⟨⟨ qmsg ⊨ (otherwith S {i} (orecvmsg R), other U {i} →) global P"
  proof (rule oinvariant_oreachableI)
    fix σ ζ
    assume "(σ, ζ) ∈ oreachable (A ⟨⟨ qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
    then obtain s where "(σ, s) ∈ oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})"
      by (auto dest!: par_qmsg_oreachable [OF _ assms(5,2-4)])
    with assms(1) show "global P (σ, ζ)"
      by (auto dest: oinvariant_weakenD [OF assms(1)])
  qed

lemma lift_step_into_qmsg:
  assumes inv: "A ⊨_A (otherwith S {i} (orecvmsg R), other U {i} →) globala P"
      and ustutter: "∧ξ. U ξ ξ"
      and sgivesu: "∧ξ ξ'. S ξ ξ' ==> U ξ ξ'"
      and upreservesq: "∧σ σ' m. [ ∀j. U (σ j) (σ' j); R σ m ] ==> R σ' m"
      and self_sync: "A ⊨_A (otherwith S {i} (orecvmsg R), other U {i} →)
                            globala (λ(σ, _, σ'). U (σ i) (σ' i))"

      and recv_stutter:  "∧σ σ' m. [ ∀j. U (σ j) (σ' j); σ' i = σ i ] ==> P (σ, receive m, σ')"
      and receive_right: "∧σ σ' m. P (σ, receive m, σ') ==> P (σ, τ, σ')"
    shows "A ⟨⟨ qmsg ⊨_A (otherwith S {i} (orecvmsg R), other U {i} →) globala P"
      (is "_ ⊨_A (?owS, ?U →) _")
  proof (rule ostep_invariantI)
    fix σ ζ a σ' ζ'
    assume or: "(σ, ζ) ∈ oreachable (A ⟨⟨ qmsg) ?owS ?U"
       and otr: "((σ, ζ), a, (σ', ζ')) ∈ trans (A ⟨⟨ qmsg)"
       and "?owS σ σ' a"
    from this(2) have "((σ, ζ), a, (σ', ζ')) ∈ oparp_sos i (trans A) (seqp_sos Γ_QMSG)"
        by simp
    then obtain s msgs q s' msgs' q'
      where "ζ = (s, (msgs, q))" "ζ' = (s', (msgs', q'))"
        and "((σ, (s, (msgs, q))), a, (σ', (s', (msgs', q'))))
               ∈ oparp_sos i (trans A) (seqp_sos Γ_QMSG)"
        by (metis prod_cases3)
    from this(1-2) and or
      obtain "(σ, s) ∈ oreachable A ?owS ?U"
             "(msgs, q) ∈ reachable qmsg (recvmsg (R σ))"
             "(∀m∈set msgs. R σ m)"
       by (auto dest: par_qmsg_oreachable [OF _ self_sync ustutter sgivesu]
                elim!: upreservesq)
    from otr ‹ζ = (s, (msgs, q))› ‹ζ' = (s', (msgs', q'))›
      have "((σ, (s, (msgs, q))), a, (σ', (s', (msgs', q'))))
              ∈ oparp_sos i (trans A) (seqp_sos Γ_QMSG)"
        by simp
    hence "globala P ((σ, s), a, (σ', s'))"
    proof
      assume "((σ, s), a, (σ', s')) ∈ trans A"
      with ‹(σ, s) ∈ oreachable A ?owS ?U›
        show "globala P ((σ, s), a, (σ', s'))"
          using ‹?owS σ σ' a› by (rule ostep_invariantD [OF inv])
    next
      assume "((msgs, q), a, (msgs', q')) ∈ seqp_sos Γ_QMSG"
         and "∧m. a ≠ send m"
         and "σ' i = σ i"
      from this(3) and ustutter have "U (σ i) (σ' i)" by simp
      with ‹?owS σ σ' a› and sgivesu have "∀j. U (σ j) (σ' j)"
        by (clarsimp dest!: otherwith_syncD) metis
      moreover have "(∃m. a = receive m) ∨ (a = τ)"
      proof -
        from ‹(msgs, q) ∈ reachable qmsg (recvmsg (R σ))›
          have "(msgs, q) ∈ reachable qmsg TT" ..
        moreover from ‹((msgs, q), a, (msgs', q')) ∈ seqp_sos Γ_QMSG›
          have "((msgs, q), a, (msgs', q')) ∈ trans qmsg" by simp
        ultimately show ?thesis
          using ‹∧m. a ≠ send m›
          by (auto dest!: step_invariantD [OF qmsg_send_receive_or_tau])
      qed
      ultimately show "globala P ((σ, s), a, (σ', s'))"
        using ‹σ' i = σ i›
        by simp (metis receive_right recv_stutter step_seq_tau)
    next
      fix m
      assume "a = τ"
         and "((σ, s), receive m, (σ', s')) ∈ trans A"
         and "((msgs, q), send m, (msgs', q')) ∈ seqp_sos Γ_QMSG"

      from ‹(msgs, q) ∈ reachable qmsg (recvmsg (R σ))›
        have "(msgs, q) ∈ reachable qmsg TT" ..
      moreover from ‹((msgs, q), send m, (msgs', q')) ∈ seqp_sos Γ_QMSG›
        have "((msgs, q), send m, (msgs', q')) ∈ trans qmsg" by simp
      ultimately have "m∈set msgs"
        by (auto dest!: step_invariantD [OF qmsg_send_from_queue])

      with ‹∀m∈set msgs. R σ m› have "R σ m" ..
      with ‹?owS σ σ' a› have "?owS σ σ' (receive m)"
          by (auto dest!: otherwith_syncD)

      with ‹((σ, s), receive m, (σ', s')) ∈ trans A›
        have "globala P ((σ, s), receive m, (σ', s'))"
          using ‹(σ, s) ∈ oreachable A ?owS ?U›
          by - (rule ostep_invariantD [OF inv])
      hence "P (σ, receive m, σ')" by simp
      hence "P (σ, τ, σ')" by (rule receive_right)
      with ‹a = τ› show "globala P ((σ, s), a, (σ', s'))" by simp
    qed
    with ‹ζ = (s, (msgs, q))› and ‹ζ' = (s', (msgs', q'))› show "globala P ((σ, ζ), a, (σ', ζ'))"
      by simp
  qed

lemma lift_step_into_qmsg_statelessassm:
  assumes "A ⊨_A (λσ _. orecvmsg (λ_. R) σ, other (λ_ _. True) {i} →) globala P"
      and "∧σ σ' m. σ' i = σ i ==> P (σ, receive m, σ')"
      and "∧σ σ' m. P (σ, receive m, σ') ==> P (σ, τ, σ')"
    shows "A ⟨⟨ qmsg ⊨_A (λσ _. orecvmsg (λ_. R) σ, other (λ_ _. True) {i} →) globala P"
  proof -
    from assms(1) have *: "A ⊨_A (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)),
                                 other (λ_ _. True) {i} →) globala P"
      by rule auto
    hence "A ⟨⟨ qmsg ⊨_A
              (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)), other (λ_ _. True) {i} →) globala P"
      by (rule lift_step_into_qmsg)
         (auto elim!: assms(2-3) simp del: step_seq_tau)
    thus ?thesis by rule auto
  qed

end