Quelle  Aodv_Loop_Freedom.thy

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

section "Lift and transfer invariants to show loop freedom"

theory Aodv_Loop_Freedom
imports AWN.OClosed_Transfer AWN.Qmsg_Lifting Global_Invariants Loop_Freedom
begin

subsection ‹Lift to parallel processes with queues›

lemma par_step_no_change_on_send_or_receive:
    fixes σ s a σ' s'
  assumes "((σ, s), a, (σ', s')) ∈ oparp_sos i (oseqp_sos Γ_AODV i) (seqp_sos Γ_QMSG)"
      and "a ≠ τ"
    shows "σ' i = σ i"
  using assms by (rule qmsg_no_change_on_send_or_receive)

lemma par_nhop_quality_increases:
  shows "opaodv i ⟨⟨ qmsg ⊨ (otherwith ((=)) {i} (orecvmsg (λσ m.
                                    msg_fresh σ m ∧ msg_zhops m)),
                                  other quality_increases {i} →)
                        global (λσ. ∀dip. let nhip = the (nhop (rt (σ i)) dip)
                                          in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
                                             ⟶ (rt (σ i)) ⊏ (rt (σ nhip)))"
    proof (rule lift_into_qmsg [OF seq_nhop_quality_increases
    show "opaodv i ⊨_A (otherwith ((=)) {i}
                         (orecvmsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
                        other quality_increases {i} →)
                       globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
    proof (rule ostep_invariant_weakenE [OF oquality_increases], simp_all)
      fix t :: "(((nat ==> state) × (state, msg, pseqp, pseqp label) seqp), msg seq_action) transition"
      assume "onll Γ_AODV (λ((σ, _), _, (σ', _)). ∀j. quality_increases (σ j) (σ' j)) t"
      thus "quality_increases (fst (fst t) i) (fst (snd (snd t)) i)"
        by (cases t) (clarsimp dest!: onllD, metis aodv_ex_label)
    next
      fix σ σ' a
      assume "otherwith ((=)) {i}
                (orecvmsg (λσ m. msg_fresh σ m ∧ msg_zhops m)) σ σ' a"
      thus "otherwith quality_increases {i} (orecvmsg (λ_. rreq_rrep_sn)) σ σ' a"
        by - (erule weaken_otherwith, auto)
    qed
  qed auto

lemma par_rreq_rrep_sn_quality_increases:
  "opaodv i ⟨⟨ qmsg ⊨_A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                            globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
  proof -
    have "opaodv i ⊨_A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF olocal_quality_increases])
         (auto
    hence "opaodv i ⟨⟨ qmsg ⊨_A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                                   globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
      by (rule lift_step_into_qmsg_statelessassm) simp_all
    thus ?thesis by rule auto
  qed

lemma par_rreq_rrep_nsqn_fresh_any_step:
  shows "opaodv i ⟨⟨ qmsg ⊨_A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ,
                                   other (λ_ _. True) {i} →)
                                  globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
  proof -
    have "opaodv i ⊨_A (λσ _. (orecvmsg (λ_. rreq_rrep_sn)) σ, other (λ_ _. True) {i} →)
                       globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
    proof (rule ostep_invariant_weakenE [OF rreq_rrep_nsqn_fresh_any_step_invariant])
      fix t
      assume "onll Γ_AODV (λ((σ, _), a, _). anycast (msg_fresh σ) a) t"
      thus "globala (λ(σ, a, σ'). anycast (msg_fresh σ) a) t"
        by (cases t) (clarsimp dest!: onllD, metis aodv_ex_label)
    qed auto
    hence "opaodv i ⟨⟨ qmsg ⊨_A (λσ _. (orecvmsg (λ_. rreq_rrep_sn)) σ, other (λ_ _. True) {i} →)
                                    globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
      by (rule lift_step_into_qmsg_statelessassm) simp_all
    thus ?thesis by rule auto
  qed

lemma par_anycast_msg_zhops:
  shows "opaodv i ⟨⟨ qmsg ⊨_A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                                  globala (λ(_, a, _). anycast msg_zhops a)"
  proof -
    from anycast_msg_zhops initiali_aodv oaodv_trans aodv_trans
      have "opaodv i ⊨_A (act TT, other (λ_ _. True) {i} →)
                         seqll i (onll Γ_AODV (λ(_, a, _). anycast msg_zhops a))"
        by (rule open_seq_step_invariant)
    hence "opaodv i ⊨_A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                            globala (λ(_, a, _). anycast msg_zhops a)"
    proof (rule ostep_invariant_weakenE)
      fix t :: "(((nat ==> state) × (state, msg, pseqp, pseqp label) seqp), msg seq_action) transition"
      assume "seqll i (onll Γ_AODV (λ(_, a, _). anycast msg_zhops a)) t"
      thus "globala (λ(_, a, _). anycast msg_zhops a) t"
        by (cases t) (clarsimp dest!: seqllD onllD, metis aodv_ex_label)
    qed simp_all
    hence "opaodv i ⟨⟨ qmsg ⊨_A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                                     globala (λ(_, a, _). anycast msg_zhops a)"
      by (rule lift_step_into_qmsg_statelessassm) simp_all
    thus ?thesis by rule auto
  qed

subsection ‹Lift to nodes›

lemma node_step_no_change_on_send_or_receive:
  assumes "((σ, NodeS i P R), a, (σ', NodeS i' P' R')) ∈ onode_sos
                                      (oparp_sos i (oseqp_sos Γ_AODV i) (seqp_sos Γ_QMSG))"
      and "a ≠ τ"
    shows "σ' i = σ i"
  using assms
  by (cases a) (auto elim!: par_step_no_change_on_send_or_receive)

lemma node_nhop_quality_increases:
  shows "⟨ i : opaodv i ⟨⟨:3"‹ y›
           (otherwith ((=)) {i}
              (oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
              other quality_increases {i}
            →) global (λσ. ∀dip. let nhip = the (nhop (rt (σ i)) dip)
                                  in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
                                     ⟶ (rt (σ i)) ⊏ (rt (σ nhip)))"
  by (rule node_lift [OF par_nhop_quality_increases]) auto

lemma node_quality_increases:
  "⟨ i : opaodv i ⟨⟨ qmsg : R ⟩_o ⊨_A (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ,
                                         other (λ_ _. True) {i} →)
                            globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
  by (rule node_lift_step_statelessassm [OF par_rreq_rrep_sn_quality_increases]) simp

lemma node_rreq_rrep_nsqn_fresh_any_step:
  shows "⟨ i : opaodv i ⟨⟨ qmsg : R ⟩_o ⊨_A
          (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
          globala (λ(σ, a, σ'). castmsg (msg_fresh σ) a)"
  by (rule node_lift_anycast_statelessassm [OF par_rreq_rrep_nsqn_fresh_any_step])

lemma node_anycast_msg_zhops:
  shows "⟨ i : opaodv i ⟨⟨ qmsg : R ⟩_o ⊨_A
          (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
          globala (λ(_, a, _). castmsg msg_zhops a)"
  by (rule node_lift_anycast_statelessassm [OF par_anycast_msg_zhops])

lemma node_silent_change_only:
  shows "⟨ i : opaodv i ⟨⟨ qmsg : R_i ⟩_o ⊨_A (λσ _. oarrivemsg (λ_ _. True) σ,
                                               other (λ_ _. True) {i} →)
          globala (λ(σ, a, σ'). a ≠ τ ⟶ σ' i = σ i)"
  proof (rule ostep_invariantI, simp (no_asm), rule impI)
    fix σ ζ a σ' ζ'
    assume or: "(σ, ζ) ∈ oreachable (⟨i : opaodv i ⟨⟨ qmsg : R_i⟩_o)
                                    (λσ _. oarrivemsg (λ_ _. True) σ)
                                    (other (λ_ _. True) {i})"
      and tr: "((σ, ζ), a, (σ', ζ')) ∈ trans (⟨i : opaodv i ⟨⟨ qmsg : R_i⟩_o)"
      and "a ≠ τ_n"
    from or obtain p R where "ζ = NodeS i p R"
      by - (drule node_net_state, metis)
    with hav"\sigma, NodeS R), a, (σ', ζ'))
                     ∈ onode_sos (oparp_sos i (trans (opaodv i)) (trans qmsg))"
      by simp
    thus "σ' i = σ i" using ‹a ≠ τ_n›
      by (cases rule: onode_sos.cases)
         (auto elim: qmsg_no_change_on_send_or_receive)
  qed

subsection ‹Lift to partial networks›

lemma arrive_rreq_rrep_nsqn_fresh_inc_sn [simp]:
  assumes "oarrivemsg (λσ m. msg_fresh σ m ∧ P σ m) σ m"
    shows "oarrivemsg (λ_. rreq_rrep_sn) σ m"
  using assms by (cases m) auto

lemma opnet_nhop_quality_increases:
  shows "opnet (λi. opaodv i ⟨⟨ qmsg) p ⊨
           (otherwith ((=)) (net_tree_ips p)
              (oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
               other quality_increases (net_tree_ips p) →)
              global (λσ. ∀i∈net_tree_ips p. ∀dip.
                          let nhip = the (nhop (rt (σ i)) dip)
                          in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
                             ⟶ (rt (σ i)) ⊏> =<^><R›
  proof (rule pnet_lift [OF node_nhop_quality_increases])
    fix i R
    have "⟨i : opaodv i ⟨⟨ qmsg : R⟩_o ⊨_A (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ,
                                              other (λ_ _. True) {i} →) globala (λ(σ, a, σ').
            castmsg (λm. msg_fresh σ m ∧ msg_zhops m) a)"
    proof (rule ostep_invariantI, simp (no_asm))
      fix σ s a σ' s'
      assume or: "(σ, s) ∈ oreachable (⟨i : opaodv i ⟨⟨ qmsg : R⟩_o)
                                      (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ)
                                      (other (λ_ _. True) {i})"
         and tr: "((σ, s), a, (σ', s')) ∈ trans (⟨i : opaodv i ⟨⟨ qmsg : R⟩_o)"
         and am: "oarrivemsg (λ_. rreq_rrep_sn) σ a"
      from or tr am have "castmsg (msg_fresh σ) a"
        by (auto dest!: ostep_invariantD [OF node_rreq_rrep_nsqn_fresh_any_step])
      moreover from or tr am have "castmsg (msg_zhops) a"
        by (auto dest!: ostep_invariantD [OF node_anycast_msg_zhops])
      ultimately show "castmsg (λm. msg_fresh σ m ∧ msg_zhops m) a"
        by (case_tac a) auto
    qed
    thus "⟨i : opaodv i ⟨⟨ qmsg : R⟩_o ⊨_A
            (λσ _. oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m) σ,
             other quality_increases {i} →) globala (λ(σ, a, _).
               castmsg (λm. msg_fresh σ m ∧ msg_zhops m) a)"
      by rule auto
  next
    fix i R
    show "⟨i : opaodv i ⟨⟨ qmsg : R⟩_o ⊨_A
            (λσ _. oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m) σ,
             other quality_increases {i} →) globala (λ(σ, a, σ').
               a ≠ τ ∧ (∀d. a ≠ i:deliver(d)) ⟶ σ i = σ' i)"
      by (rule ostep_invariant_weakenE [OF node_silent_change_only]) auto
  next
    fix i R
    show "⟨i : opaodv i ⟨⟨ qmsg : R⟩_o ⊨_A
            (λσ _. oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m) σ,
             other quality_increases {i} →) globala (λ(σ, a, σ').
               a = τ ∨ (∃d. a = i:deliver(d)) ⟶ quality_increases (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF node_quality_increases]) auto
  qed simp_all

subsection ‹Lift to closed networks›

lemmaonet_nhop_quality_increases
  shows "oclosed (opnet (\<lambda>i. opaodv i \<langle>\<langle>\<^bsub>i\<^esub> qmsg) p)
           \<Turnstile> (\<lambda>_ _ _. True, other quality_increases (net_tree_ips p) \<rightarrow>)
              global (\<lambda>\<sigma>. \<forall>i\<in>net_tree_ips p. \<forall>dip.
                          let nhip = the (nhop (rt (\<sigma> i)) dip)
                          in dip \<in> vD (rt (\<sigma> i)) \<inter> vD (rt (\<sigma> nhip)) \<and> nhip \<noteq> dip
                             \<longrightarrow> (rt (\<sigma> i)) \<sqsubset>\<^bsub>dip\<^esub> (rt (\<sigma> nhip)))"
  (is "_ \<Turnstile> (_, ?U \<rightarrow>) ?inv")
  proof (rule inclosed_closed)
    from opnet_nhop_quality_increases
      show "opnet (\<lambda>i. opaodv i \<langle>\<langle>\<^bsub>i\<^esub> qmsg) p
               \<Turnstile> (otherwith ((=)) (net_tree_ips p) inoclosed, ?U \<rightarrow>) ?inv"
    proof (rule oinvariant_weakenE)
      fix \<sigma> \<sigma>' :: "ip \<Rightarrow> state" and a :: "msg node_action"
      assume "otherwith ((=)) (net_tree_ips p) inoclosed \<sigma> \<sigma>' a"
      thus "otherwith ((=)) (net_tree_ips p)
              (oarrivemsg (\<lambda>\<sigma> m. msg_fresh \<sigma> m \<and> msg_zhops m)) \<sigma> \<sigma>' a"
      proof (rule otherwithEI)
        fix \<sigma> :: "ip \<Rightarrow> state" and a :: "msg node_action"
        assume "inoclosed \<sigma> a"
        thus "oarrivemsg (\<lambda>\<sigma> m. msg_fresh \<sigma> m \<and> msg_zhops m) \<sigma> a"
        proof (cases a)
          fix ii ni ms
          assume "a = ii\<not>ni:arrive(ms)"
          moreover with \<open>inoclosed \<sigma> a\<close> obtain d di where "ms = newpkt(d, di)"
            by (cases ms) auto
          ultimately show ?thesis by simp
        qed simp_all
      qed
    qed
  qed

subsection \<open>Transfer into the standard model\<close>

interpretation aodv_openproc: openproc paodv opaodv id
  rewrites "aodv_openproc.initmissing = initmissing"
  proof -
    show "openproc paodv opaodv id"
    proof unfold_locales
      fix i :: ip
      have "{(\<sigma>, \<zeta>). (\<sigma> i, \<zeta>) \<in> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V i \<and> (\<forall>j. j \<noteq> i \<longrightarrow> \<sigma> j \<in> fst ` \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V j)} \<subseteq> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V'"
        unfolding \<sigma>\<^sub                     THEN ""\<forall>E"(2),), THEN "\<forall>"(2)
        proof (rule equalityD1)
          show "\<And>f p. {(\<sigma>, \<zeta>). (\<sigma> i, \<zeta>) \<in> {(f i, p)} \<and> (\<forall>j. j \<noteq> i
                      \<longrightarrow> \<sigma> j \<in> fst ` {(f j, p)})} = {(f, p)}"
            by (rule set_eqI) auto
        qed
      thus "{ (\<sigma>, \<zeta>) |\<sigma> \<zeta> s. s \<in> init (paodv i)
                             \<and> (\<sigma> i, \<zeta>) = id s
                             \<                     THEN "\<forall>E(2),THEN"\rightarrow>E"]
        by simp
    next
      show "\<forall>j. init (paodv j) \<noteq> {}"
        unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_def by simp
    next
      fix i s a s' \<sigma> \<sigma>'
      assume "\<sigma> i = fst (id s)"
         and "\<sigma>' i = fst (id s')"
         and "(s, a, s') \<in> trans (paodv i)"
      then obtain q q' where "s = (\<sigma> i, q)"
                         and "s' = (\<sigma>' i, q')"
                         and "((\<sigma> i, q), a, (\<sigma>' i, q')) \<in> trans (paodv i)" 
         by (cases s, cases s') auto
      from this(3) have "((\<sigma>, q), a, (\<sigma>', q')) \<in> trans (opaodv i)"
        by simp (rule open_seqp_action [OF aodv_wf])

      with \<open>s = (\<sigma> i, q)\<close> and \<open>s' = (\<sigma>' i, q')\<close>
        show "((\<sigma>, snd (id s)), a, (\<sigma>', snd (id s'))) \<in> trans (opaodv i)"
          by simp
    qed
    then interpret opn: openproc paodv opaodv id .
    have [simp]: "\<And>i. (SOME x. x \<in> (fst o id) ` init (paodv i)) = aodv_init i"
      unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_def by simp
    hence "\<And>i. openproc.initmissing paodv id i = initmissing i"
      unfolding opn.initmissing_def opn.someinit_def initmissing_def
      by (auto split: option.split)
    thus "openproc.initmissing paodv id = initmissing" ..
  qed

interpretation aodv_openproc_par_qmsg: openproc_parq paodv opaodv id qmsg
  rewrites "aodv_openproc_par_qmsg.netglobal = netglobal"
    and "aodv_openproc_par_qmsg.initmissing = initmissing"
  proof -
    show "openproc_parq paodv opaodv id qmsg"
      by (unfold_locales) simp
    then interpret opq: openproc_parq paodv opaodv id qmsg .

    have im: "\<And>\<sigma>. openproc.initmissing (\<lambda>i. paodv i \<langle>\<langle> qmsg) (\<lambda>(p, q). (fst (id p), snd (id p), q)) \<sigma>
                                                                                    = initmissing \<sigma>"
      unfolding opq.initmissing_def opq.someinit_def initmissing_def
      unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_def \<sigma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G_def by (clarsimp cong: option.case_cong)
    thus "openproc.initmissing (\<lambda>i. paodv i \<langle>\<langle> qmsg) (\<lambda>(p, q). (fst (id p), snd (id p), q)) = initmissing"
      by (rule ext)
    have "\<And>P \<sigma>. openproc.netglobal (\<lambda>i. paodv i \<langle>\<langle> qmsg) (\<lambda>(p, q). (fst (id p), snd (id p), q)) P \<sigma>
                                                                                = netglobal P \<sigma>"
      unfoldingopqnetglobal_defnetglobal_defopqinitmissing_definitmissing_defopqsomeinit_def
      unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_def \<sigma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G_def
      by (clarsimp cong: option.case_cong
                   simp del: One_nat_def
                   simp add: fst_initmissing_netgmap_default_aodv_init_netlift
                                                  [symmetric, unfolded initmissing_def])
    thus "openproc.netglobal (\<lambda>i. paodv i \<langle>\<langle> qmsg) (\<lambda>(p, q). (fst (id p), snd (id p), q)) = netglobal"
      by auto
  qed

lemma net_nhop_quality_increases:
  assumes "wf_net_tree n"
  shows "closed (pnet (\<lambda>i. paodv i \<langle>\<langle> qmsg) n) \<TTurnstile> netglobal
                           (\<lambda>\<sigma>. \<forall>i dip. let nhip = the (nhop (rt (\<sigma> i)) dip)
                                        in dip \<in> vD (rt (\<sigma> i)) \<inter> vD (rt (\<sigma> nhip)) \<and> nhip \<noteq> dip
                                            \<longrightarrow> (rt (\<sigma> i)) \<sqsubset>\<^bsub>dip\<^esub> (rt (\<sigma> nhip)))"
        (is "_ \<TTurnstile> netglobal (\<lambda>\<sigma>. \<forall>i. ?inv \<sigma> i)")
  proof -
    from \<open>wf_net_tree n\<close>
      have proto: "closed (pnet (\<lambda>i. paodv i \<langle>\<langle> qmsg) n) \<TTurnstile> netglobal (\<lambda>\<sigma>. \<forall>i\<in>net_tree_ips n. \<forall>dip.
                                            let nhip = the (nhop (rt (\<sigma> i)) dip)
                                            in dip \<in> vD (rt (\<sigma> i)) \<inter> vD (rt (\<sigma> nhip)) \<and> nhip \<noteq> dip
                                                \<longrightarrow> (rt (\<sigma> i)) \<sqsubset>\<^bsub>dip\<^esub> (rt (\<sigma> nhip)))"
        by (rule aodv_openproc_par_qmsg.close_opnet [OF _ onet_nhop_quality_increases])
    show ?thesis
    unfolding invariant_def opnet_sos.opnet_tau1
    proof (rule, simp only: aodv_openproc_par_qmsg.netglobalsimp
                            fst_initmissing_netgmap_pair_fst, rule allI)
      fix \<sigma> i
      assume sr: "\<sigma> \<in> reachable (closed (pnet (\<lambda>i. paodv i \<langle>\<langle> qmsg) n)) TT"
      hence "\<forall>i\<in>net_tree_ips n. ?inv (fst (initmissing (netgmap fst \<sigma>))) i"
        by - (drule invariantD [OF proto],
              simp only: aodv_openproc_par_qmsg.netglobalsimp
                         fst_initmissing_netgmap_pair_fst)
      thus "?inv (fst (initmissing (netgmap fst \<sigma>))) i"
      proof (cases "i\<in>net_tree_ips n")
        assume "i\<notin>net_tree_ips n"
        from sr have "\<sigma> \<in> reachable (pnet (\<lambda>i. paodv i \<langle>\<langle> qmsg) n) TT" ..
        hence "net_ips \<sigma> = net_tree_ips n" ..
        with \<open>i\<notin>net_tree_ips n\<close> have "i\<notin>net_ips \<sigma>" by simp
        hence "(fst (initmissing (netgmap fst \<sigma>))) i = aodv_init i"
          by simp
        thus ?thesis by simp
      qed metis
    qed
  qed

subsection \<open>Loop freedom of AODV\<close>

theorem aodv_loop_freedom:
  assumes "wf_net_tree n"
  shows "closed (pnet (\<lambda>i. paodv i \<langle>\<langle> qmsg) n) \<TTurnstile> netglobal (\<lambda>\<sigma>. \<forall>dip. irrefl ((rt_graph \<sigma> dip)\<^sup>+))"
  using assms by (rule aodv_openproc_par_qmsg.netglobal_weakenE
                          [OF net_nhop_quality_increases inv_to_loop_freedom])

end