Quelle  Quality_Increases.thy

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

section "The quality increases predicate"

theory Quality_Increases
imports Aodv_Predicates Fresher
begin

definition quality_increases :: "state ==> state ==> bool"
where "quality_increases ξ ξ' ≡ (∀dip∈kD(rt ξ). dip ∈ kD(rt ξ') ∧ rt ξ ⊑ rt ξ')
                                               ∧ (∀dip. sqn (rt ξ) dip ≤ sqn (rt ξ') dip)"

lemma quality_increasesI [intro!]:
  assumes "∧dip. dip ∈ kD(rt ξ) ==> dip ∈ kD(rt ξ')"
      and "∧dip. [ dip ∈ kD(rt ξ); dip ∈ kD(rt ξ') ] ==> rt ξ ⊑ rt ξ'"          
      and "∧dip. sqn (rt ξ) dip ≤ sqn (rt ξ') dip"
    shows "quality_increases ξ ξ'"
  unfolding quality_increases_def using assms by clarsimp

lemma quality_increasesE [elim]:
    fixes dip
  assumes "quality_increases ξ ξ'"
      and "dip∈kD(rt ξ)"
      and "[ dip ∈ kD(rt ξ'); rt ξ ⊑ rt ξ'; sqn (rt ξ) dip ≤ sqn (rt ξ') dip ] ==> R dip ξ ξ'"
    shows "R dip ξ ξ'"
  using assms unfolding quality_increases_def by clarsimp

lemma quality_increases_rt_fresherD [dest]:
    fixes ip
  assumes "quality_increases ξ ξ'"
      and "ip∈kD(rt ξ)"
    shows "rt ξ ⊑ rt ξ'"
  using assms by auto

lemma quality_increases_sqnE [elim]:
    fixes dip
  assumes "quality_increases ξ ξ'"
      and "sqn (rt ξ) dip ≤ sqn (rt ξ') dip ==> R dip ξ ξ'"
    shows "R dip ξ ξ'"
  using assms unfolding quality_increases_def by clarsimp

lemma quality_increases_refl [intro, simp]: "quality_increases ξ ξ"
  by rule simp_all

lemma strictly_fresher_quality_increases_right [elim]:
    fixes σ σ' dip
  assumes "rt (σ i) ⊏ rt (σ nhip)"                       
      and qinc: "quality_increases (σ nhip) (σ' nhip)"
      and "dip∈kD(rt (σ nhip))"
    shows "rt (σ i) ⊏ rt (σ' nhip)"
  proof -
    from qinc have "rt (σ nhip) ⊑ rt (σ' nhip)" using ‹dip∈kD(rt (σ nhip))›
      by auto
    with ‹rt (σ i) ⊏ rt (σ nhip)› show ?thesis ..
  qed

lemma kD_quality_increases [elim]:
  assumes "i∈kD(rt ξ)"
      and "quality_increases ξ ξ'"
    shows "i∈kD(rt ξ')"
  using assms by auto

lemma kD_nsqn_quality_increases [elim]:
  assumes "i∈kD(rt ξ)"
      and "quality_increases ξ ξ'"
    shows "i∈kD(rt ξ') ∧ nsqn (rt ξ) i ≤ nsqn (rt ξ') i"
  proof -
    from assms have "i∈kD(rt ξ')" ..
    moreover with assms have "rt ξ ⊑ rt ξ'" by auto
    ultimately have "nsqn (rt ξ) i ≤ nsqn (rt ξ') i"
      using ‹i∈kD(rt ξ)› by - (erule(2) rt_fresher_imp_nsqn_le)
    with ‹i∈kD(rt ξ')› show ?thesis ..
  qed

lemma nsqn_quality_increases [elim]:
  assumes "i∈kD(rt ξ)"
      and "quality_increases ξ ξ'"
    shows "nsqn (rt ξ) i ≤ nsqn (rt ξ') i"
  using assms by (rule kD_nsqn_quality_increases [THEN conjunct2])

lemma kD_nsqn_quality_increases_trans [elim]:
  assumes "i∈kD(rt ξ)"
      and "s ≤ nsqn (rt ξ) i"
      and "quality_increases ξ ξ'"
    shows "i∈kD(rt ξ') ∧ s ≤ nsqn (rt ξ') i"
  proof
    from ‹i∈kD(rt ξ)› and ‹quality_increases ξ ξ'› show "i∈kD(rt ξ')" ..
  next
    from ‹i∈kD(rt ξ)› and ‹quality_increases ξ ξ'› have "nsqn (rt ξ) i ≤ nsqn (rt ξ') i" ..
    with ‹s ≤ nsqn (rt ξ) i› show "s ≤ nsqn (rt ξ') i" by (rule le_trans)
  qed

lemma nsqn_quality_increases_nsqn_lt_lt [elim]:
  assumes "i∈kD(rt ξ)"
      and "quality_increases ξ ξ'"
     and "s < nsqn (rt ξ) i"
    shows "s < nsqn (rt ξ') i"
  proof -
    from assms(1-2) have "nsqn (rt ξ) i ≤ nsqn (rt ξ') i" ..
    with ‹s < nsqn (rt ξ) i› show "s < nsqn (rt ξ') i" by simp
  qed

lemma nsqn_quality_increases_dhops [elim]:
  assumes "i∈kD(rt ξ)"
      and "quality_increases ξ ξ'"
      and "nsqn (rt ξ) i = nsqn (rt ξ') i"
    shows "the (dhops (rt ξ) i) ≥ the (dhops (rt ξ') i)"
  using assms unfolding quality_increases_def
  by (clarsimp) (drule(1) bspec, clarsimp simp: rt_fresher_def2)

lemma nsqn_quality_increases_nsqn_eq_le [elim]:
  assumes "i∈kD(rt ξ)"
      and "quality_increases ξ ξ'"
      and "s = nsqn (rt ξ) i"
    shows "s < nsqn (rt ξ') i ∨ (s = nsqn (rt ξ') i ∧ the (dhops (rt ξ) i) ≥ the (dhops (rt ξ') i))"
  using assms by (metis nat_less_le nsqn_quality_increases nsqn_quality_increases_dhops)

lemma quality_increases_rreq_rrep_props [elim]:
    fixes sn ip hops sip
  assumes qinc: "quality_increases (σ sip) (σ' sip)"
      and "1 ≤ sn"
      and *: "ip∈kD(rt (σ sip)) ∧ sn ≤ nsqn (rt (σ sip)) ip
                                ∧ (nsqn (rt (σ sip)) ip = sn
                                    ⟶ (the (dhops (rt (σ sip)) ip) ≤ hops
                                          ∨ the (flag (rt (σ sip)) ip) = inv))"
    shows "ip∈kD(rt (σ' sip)) ∧ sn ≤ nsqn (rt (σ' sip)) ip
                              ∧ (nsqn (rt (σ' sip)) ip = sn
                                  ⟶ (the (dhops (rt (σ' sip)) ip) ≤ hops
                                        ∨ the (flag (rt (σ' sip)) ip) = inv))"
      (is "_ ∧ ?nsqnafter")
  proof -
    from *  obtain "ip∈kD(rt (σ sip))" and "sn ≤ nsqn (rt (σ sip)) ip" by auto

    from ‹quality_increases (σ sip) (σ' sip)›
       have "sqn (rt (σ sip)) ip ≤ sqn (rt (σ' sip)) ip" ..
    from ‹quality_increases (σ sip) (σ' sip)› and ‹ip∈kD (rt (σ sip))›
      have "ip∈kD (rt (σ' sip))" ..

    from ‹sn ≤ nsqn (rt (σ sip)) ip› have ?nsqnafter
    proof
      assume "sn < nsqn (rt (σ sip)) ip"
      also from ‹ip∈kD(rt (σ sip))› and ‹quality_increases (σ sip) (σ' sip)›
        have "... ≤ nsqn (rt (σ' sip)) ip" ..
      finally have "sn < nsqn (rt (σ' sip)) ip" .
      thus ?thesis by simp
    next
      assume "sn = nsqn (rt (σ sip)) ip"
      with ‹ip∈kD(rt (σ sip))› and ‹quality_increases (σ sip) (σ' sip)›
        have "sn < nsqn (rt (σ' sip)) ip
              ∨ (sn = nsqn (rt (σ' sip)) ip
                 ∧ the (dhops (rt (σ' sip)) ip) ≤ the (dhops (rt (σ sip)) ip))" ..
      hence "sn < nsqn (rt (σ' sip)) ip
              ∨ (nsqn (rt (σ' sip)) ip = sn ∧ (the (dhops (rt (σ' sip)) ip) ≤ hops
                                                 ∨ the (flag (rt (σ' sip)) ip) = inv))"
      proof
        assume "sn < nsqn (rt (σ' sip)) ip" thus ?thesis ..
      next
        assume "sn = nsqn (rt (σ' sip)) ip
                ∧ the (dhops (rt (σ sip)) ip) ≥ the (dhops (rt (σ' sip)) ip)"
        hence "sn = nsqn (rt (σ' sip)) ip"
          and "the (dhops (rt (σ' sip)) ip) ≤ the (dhops (rt (σ sip)) ip)" by auto

        from * and ‹sn = nsqn (rt (σ sip)) ip› have "the (dhops (rt (σ sip)) ip) ≤ hops
                                                       ∨ the (flag (rt (σ sip)) ip) = inv"
          by simp
        thus ?thesis
        proof
          assume "the (dhops (rt (σ sip)) ip) ≤ hops"
          with  ‹the (dhops (rt (σ' sip)) ip) ≤ the (dhops (rt (σ sip)) ip)›
           have "the (dhops (rt (σ' sip)) ip) ≤ hops" by simp
          with ‹sn = nsqn (rt (σ' sip)) ip› show ?thesis by simp
        next
          assume "the (flag (rt (σ sip)) ip) = inv"
          with ‹ip∈kD(rt (σ sip))› have "nsqn (rt (σ sip)) ip = sqn (rt (σ sip)) ip - 1" ..

          with ‹sn ≥ 1› and ‹sn = nsqn (rt (σ sip)) ip›
            have "sqn (rt (σ sip)) ip > 1" by simp

          from ‹ip∈kD(rt (σ' sip))› show ?thesis
          proof (rule vD_or_iD)
            assume "ip∈iD(rt (σ' sip))"
            hence "the (flag (rt (σ' sip)) ip) = inv" ..
            with ‹sn = nsqn (rt (σ' sip)) ip› show ?thesis
              by simp
          next
            (* the tricky case: sn = nsqn (rt (\<sigma>' sip)) ip
                                \<and> ip\<in>iD(rt (\<sigma> sip))
                                \<and> ip\<in>vD(rt (\<sigma>' sip)) *)
            assume "ip∈vD(rt (σ' sip))"
            hence "nsqn (rt (σ' sip)) ip = sqn (rt (σ' sip)) ip" ..
            with ‹sqn (rt (σ sip)) ip ≤ sqn (rt (σ' sip)) ip›
              have "nsqn (rt (σ' sip)) ip ≥ sqn (rt (σ sip)) ip" by simp

            with ‹sqn (rt (σ sip)) ip > 1›
              have "nsqn (rt (σ' sip)) ip > sqn (rt (σ sip)) ip - 1" by simp
            with ‹nsqn (rt (σ sip)) ip = sqn (rt (σ sip)) ip - 1›
              have "nsqn (rt (σ' sip)) ip > nsqn (rt (σ sip)) ip" by simp
            with ‹sn = nsqn (rt (σ sip)) ip› have "nsqn (rt (σ' sip)) ip > sn"
              by simp
            thus ?thesis ..
          qed
        qed
      qed
      thus ?thesis by (metis (mono_tags) le_cases not_le)
    qed
    with ‹ip∈kD (rt (σ' sip))› show "ip∈kD (rt (σ' sip)) ∧ ?nsqnafter" ..
  qed

lemma quality_increases_rreq_rrep_props':
    fixes sn ip hops sip
  assumes "∀j. quality_increases (σ j) (σ' j)"
      and "1 ≤ sn"
      and *: "ip∈kD(rt (σ sip)) ∧ sn ≤ nsqn (rt (σ sip)) ip
                                ∧ (nsqn (rt (σ sip)) ip = sn
                                    ⟶ (the (dhops (rt (σ sip)) ip) ≤ hops
                                          ∨ the (flag (rt (σ sip)) ip) = inv))"
    shows "ip∈kD(rt (σ' sip)) ∧ sn ≤ nsqn (rt (σ' sip)) ip
                              ∧ (nsqn (rt (σ' sip)) ip = sn
                                  ⟶ (the (dhops (rt (σ' sip)) ip) ≤ hops
                                        ∨ the (flag (rt (σ' sip)) ip) = inv))"
  proof -
    from assms(1) have "quality_increases (σ sip) (σ' sip)" ..
    thus ?thesis using assms(2-3) by (rule quality_increases_rreq_rrep_props)
  qed

lemma rteq_quality_increases:
  assumes "∀j. j ≠ i ⟶ quality_increases (σ j) (σ' j)"
      and "rt (σ' i) = rt (σ i)"
    shows "∀j. quality_increases (σ j) (σ' j)"
  using assms by clarsimp (metis order_refl quality_increasesI rt_fresher_refl)

definition msg_fresh :: "(ip ==> state) ==> msg ==> bool"
where "msg_fresh σ m ≡
         case m of Rreq hopsc _ _ _ _ oipc osnc sipc ==> osnc ≥ 1 ∧ (sipc ≠ oipc ⟶
                       oipc∈kD(rt (σ sipc)) ∧ nsqn (rt (σ sipc)) oipc ≥ osnc
                       ∧ (nsqn (rt (σ sipc)) oipc = osnc
                             ⟶ (hopsc ≥ the (dhops (rt (σ sipc)) oipc)
                                  ∨ the (flag (rt (σ sipc)) oipc) = inv)))
                   | Rrep hopsc dipc dsnc _ sipc ==> dsnc ≥ 1 ∧ (sipc ≠ dipc ⟶
                       dipc∈kD(rt (σ sipc)) ∧ nsqn (rt (σ sipc)) dipc ≥ dsnc
                       ∧ (nsqn (rt (σ sipc)) dipc = dsnc
                             ⟶ (hopsc ≥ the (dhops (rt (σ sipc)) dipc)
                                   ∨ the (flag (rt (σ sipc)) dipc) = inv)))
                   | Rerr destsc sipc ==> (∀ripc∈dom(destsc). (ripc∈kD(rt (σ sipc))
                                         ∧ the (destsc ripc) - 1 ≤ nsqn (rt (σ sipc)) ripc))
                   | _ ==> True"

lemma msg_fresh [simp]:
  "∧hops rreqid dip dsn dsk oip osn sip.
           msg_fresh σ (Rreq hops rreqid dip dsn dsk oip osn sip) =
                            (osn ≥ 1 ∧ (sip ≠ oip ⟶ oip∈kD(rt (σ sip))
                                     ∧ nsqn (rt (σ sip)) oip ≥ osn
                                     ∧ (nsqn (rt (σ sip)) oip = osn
                                           ⟶ (hops ≥ the (dhops (rt (σ sip)) oip)
                                                ∨ the (flag (rt (σ sip)) oip) = inv))))"
  "∧hops dip dsn oip sip. msg_fresh σ (Rrep hops dip dsn oip sip) =
                            (dsn ≥ 1 ∧ (sip ≠ dip ⟶ dip∈kD(rt (σ sip))
                                     ∧ nsqn (rt (σ sip)) dip ≥ dsn
                                     ∧ (nsqn (rt (σ sip)) dip = dsn
                                           ⟶ (hops ≥ the (dhops (rt (σ sip)) dip))
                                                 ∨ the (flag (rt (σ sip)) dip) = inv)))"
  "∧dests sip. msg_fresh σ (Rerr dests sip) =
                            (∀ripc∈dom(dests). (ripc∈kD(rt (σ sip))
                                     ∧ the (dests ripc) - 1 ≤ nsqn (rt (σ sip)) ripc))"
  "∧d dip. msg_fresh σ (Newpkt d dip) = True"
  "∧d dip sip. msg_fresh σ (Pkt d dip sip) = True"
  unfolding msg_fresh_def by simp_all

lemma msg_fresh_inc_sn [simp, elim]:
  "msg_fresh σ m ==> rreq_rrep_sn m"
  by (cases m) simp_all

lemma recv_msg_fresh_inc_sn [simp, elim]:
  "orecvmsg (msg_fresh) σ m ==> recvmsg rreq_rrep_sn m"
  by (cases m) simp_all

lemma rreq_nsqn_is_fresh [simp]:
  fixes σ msg hops rreqid dip dsn dsk oip osn sip
  assumes "rreq_rrep_fresh (rt (σ sip)) (Rreq hops rreqid dip dsn dsk oip osn sip)"
      and "rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip)"
  shows "msg_fresh σ (Rreq hops rreqid dip dsn dsk oip osn sip)"
        (is "msg_fresh σ ?msg")
  proof -
    let ?rt = "rt (σ sip)"
    from assms(2) have "1 ≤ osn" by simp
    thus ?thesis
    unfolding msg_fresh_def
    proof (simp only: msg.case, intro conjI impI)
      assume "sip ≠ oip"
      with assms(1) show "oip ∈ kD(?rt)" by simp
    next
      assume "sip ≠ oip"
         and "nsqn ?rt oip = osn"
      show "the (dhops ?rt oip) ≤ hops ∨ the (flag ?rt oip) = inv"
      proof (cases "oip∈vD(?rt)")
        assume "oip∈vD(?rt)"
        hence "nsqn ?rt oip = sqn ?rt oip" ..
        with ‹nsqn ?rt oip = osn› have "sqn ?rt oip = osn" by simp
        with assms(1) and ‹sip ≠ oip› have "the (dhops ?rt oip) ≤ hops"
          by simp
        thus ?thesis ..
      next
        assume "oip∉vD(?rt)"
        moreover from assms(1) and ‹sip ≠ oip› have "oip∈kD(?rt)" by simp
        ultimately have "oip∈iD(?rt)" by auto
        hence "the (flag ?rt oip) = inv" ..
        thus ?thesis ..
      qed
    next
      assume "sip ≠ oip"
      with assms(1) have "osn ≤ sqn ?rt oip" by auto
      thus "osn ≤ nsqn (rt (σ sip)) oip"
      proof (rule nat_le_eq_or_lt)
        assume "osn < sqn ?rt oip"
        hence "osn ≤ sqn ?rt oip - 1" by simp
        also have "... ≤ nsqn ?rt oip" by (rule sqn_nsqn)
        finally show "osn ≤ nsqn ?rt oip" .
      next
        assume "osn = sqn ?rt oip"
        with assms(1) and ‹sip ≠ oip› have "oip∈kD(?rt)"
                                       and "the (flag ?rt oip) = val"
          by auto
        hence "nsqn ?rt oip = sqn ?rt oip" ..
        with ‹osn = sqn ?rt oip› have "nsqn ?rt oip = osn" by simp
        thus "osn ≤ nsqn ?rt oip" by simp
      qed
    qed simp
  qed

lemma rrep_nsqn_is_fresh [simp]:
  fixes σ msg hops dip dsn oip sip
  assumes "rreq_rrep_fresh (rt (σ sip)) (Rrep hops dip dsn oip sip)"
      and "rreq_rrep_sn (Rrep hops dip dsn oip sip)"
  shows "msg_fresh σ (Rrep hops dip dsn oip sip)"
        (is "msg_fresh σ ?msg")
  proof -
    let ?rt = "rt (σ sip)"
    from assms have "sip ≠ dip ⟶ dip∈kD(?rt) ∧ sqn ?rt dip = dsn ∧ the (flag ?rt dip) = val"
      by simp
    hence "sip ≠ dip ⟶ dip∈kD(?rt) ∧ nsqn ?rt dip ≥ dsn"
    by clarsimp
    with assms show "msg_fresh σ ?msg"
      by clarsimp
  qed

lemma rerr_nsqn_is_fresh [simp]:
  fixes σ msg dests sip
  assumes "rerr_invalid (rt (σ sip)) (Rerr dests sip)"
  shows "msg_fresh σ (Rerr dests sip)"
        (is "msg_fresh σ ?msg")
  proof -
    let ?rt = "rt (σ sip)"
    from assms have *: "(∀rip∈dom(dests). (rip∈iD(rt (σ sip))
                                     ∧ the (dests rip) = sqn (rt (σ sip)) rip))"
      by clarsimp
    have "(∀rip∈dom(dests). (rip∈kD(rt (σ sip))
                                     ∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip))"
    proof
      fix rip
      assume "rip ∈ dom dests"
      with * have "rip∈iD(rt (σ sip))" and "the (dests rip) = sqn (rt (σ sip)) rip"
        by auto

      from this(2) have "the (dests rip) - 1 = sqn (rt (σ sip)) rip - 1" by simp
      also have "... ≤ nsqn (rt (σ sip)) rip" by (rule sqn_nsqn)
      finally have "the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip" .

      with ‹rip∈iD(rt (σ sip))›
        show "rip∈kD(rt (σ sip)) ∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
          by clarsimp
    qed
    thus "msg_fresh σ ?msg"
      by simp
  qed

lemma quality_increases_msg_fresh [elim]:
  assumes qinc: "∀j. quality_increases (σ j) (σ' j)"
      and "msg_fresh σ m"
    shows "msg_fresh σ' m"
  using assms(2)
  proof (cases m)
    fix hops rreqid dip dsn dsk oip osn sip
    assume [simp]: "m = Rreq hops rreqid dip dsn dsk oip osn sip"
       and "msg_fresh σ m"
    then have "osn ≥ 1" and "sip = oip ∨ (oip∈kD(rt (σ sip)) ∧ osn ≤ nsqn (rt (σ sip)) oip
                                           ∧ (nsqn (rt (σ sip)) oip = osn
                                                 ⟶ (the (dhops (rt (σ sip)) oip) ≤ hops
                                                      ∨ the (flag (rt (σ sip)) oip) = inv)))"
      by auto
    from this(2) show ?thesis
    proof
      assume "sip = oip" with ‹osn ≥ 1› show ?thesis by simp
    next
      assume "oip∈kD(rt (σ sip)) ∧ osn ≤ nsqn (rt (σ sip)) oip
                                  ∧ (nsqn (rt (σ sip)) oip = osn
                                      ⟶ (the (dhops (rt (σ sip)) oip) ≤ hops
                                           ∨ the (flag (rt (σ sip)) oip) = inv))"
      moreover from qinc have "quality_increases (σ sip) (σ' sip)" ..
      ultimately have "oip∈kD(rt (σ' sip)) ∧ osn ≤ nsqn (rt (σ' sip)) oip
                                           ∧ (nsqn (rt (σ' sip)) oip = osn
                                              ⟶ (the (dhops (rt (σ' sip)) oip) ≤ hops
                                                    ∨ the (flag (rt (σ' sip)) oip) = inv))"
       using ‹osn ≥ 1› by (rule quality_increases_rreq_rrep_props [rotated 2])
      with ‹osn ≥ 1› show "msg_fresh σ' m"
        by (clarsimp)
    qed
  next
    fix hops dip dsn oip sip
    assume [simp]: "m = Rrep hops dip dsn oip sip"
       and "msg_fresh σ m"
    then have "dsn ≥ 1" and "sip = dip ∨ (dip∈kD(rt (σ sip)) ∧ dsn ≤ nsqn (rt (σ sip)) dip
                                           ∧ (nsqn (rt (σ sip)) dip = dsn
                                                 ⟶ (the (dhops (rt (σ sip)) dip) ≤ hops
                                                      ∨ the (flag (rt (σ sip)) dip) = inv)))"
      by auto
    from this(2) show "?thesis"
    proof
      assume "sip = dip" with ‹dsn ≥ 1› show ?thesis by simp
    next
      assume "dip∈kD(rt (σ sip)) ∧ dsn ≤ nsqn (rt (σ sip)) dip
                                  ∧ (nsqn (rt (σ sip)) dip = dsn
                                      ⟶ (the (dhops (rt (σ sip)) dip) ≤ hops
                                           ∨ the (flag (rt (σ sip)) dip) = inv))"
      moreover from qinc have "quality_increases (σ sip) (σ' sip)" ..
      ultimately have "dip∈kD(rt (σ' sip)) ∧ dsn ≤ nsqn (rt (σ' sip)) dip
                                           ∧ (nsqn (rt (σ' sip)) dip = dsn
                                              ⟶ (the (dhops (rt (σ' sip)) dip) ≤ hops
                                                    ∨ the (flag (rt (σ' sip)) dip) = inv))"
        using ‹dsn ≥ 1› by (rule quality_increases_rreq_rrep_props [rotated 2])
      with ‹dsn ≥ 1› show "msg_fresh σ' m"
        by clarsimp
    qed
  next
    fix dests sip
    assume [simp]: "m = Rerr dests sip"
       and "msg_fresh σ m"
    then have *: "∀rip∈dom(dests). rip∈kD(rt (σ sip))
                              ∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
      by simp
    have "∀rip∈dom(dests). rip∈kD(rt (σ' sip))
                         ∧ the (dests rip) - 1 ≤ nsqn (rt (σ' sip)) rip"
      proof
        fix rip
        assume "rip∈dom(dests)"
        with * have "rip∈kD(rt (σ sip))" and "the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
          by - (drule(1) bspec, clarsimp)+
        moreover from qinc have "quality_increases (σ sip) (σ' sip)" by simp
        ultimately show "rip∈kD(rt (σ' sip)) ∧ the (dests rip) - 1 ≤ nsqn (rt (σ' sip)) rip" ..
      qed
    thus ?thesis by simp
  qed simp_all

end