[STATEMENT]
lemma nsqn_quality_increases_nsqn_lt_lt [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "quality_increases \<xi> \<xi>'"
     and "s < nsqn (rt \<xi>) i"
    shows "s < nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i
[PROOF STEP]
from assms(1-2)
[PROOF STATE]
proof (chain)
picking this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
[PROOF STEP]
have "nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'

goal (1 subgoal):
 1. nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i

goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i
[PROOF STEP]
with \<open>s < nsqn (rt \<xi>) i\<close>
[PROOF STATE]
proof (chain)
picking this:
s < nsqn (rt \<xi>) i
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
show "s < nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
using this:
s < nsqn (rt \<xi>) i
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i

goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s < nsqn (rt \<xi>') i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nsqn_quality_increases_dhops [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "quality_increases \<xi> \<xi>'"
      and "nsqn (rt \<xi>) i = nsqn (rt \<xi>') i"
    shows "the (dhops (rt \<xi>) i) \<ge> the (dhops (rt \<xi>') i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (dhops (rt \<xi>') i) \<le> the (dhops (rt \<xi>) i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
nsqn (rt \<xi>) i = nsqn (rt \<xi>') i

goal (1 subgoal):
 1. the (dhops (rt \<xi>') i) \<le> the (dhops (rt \<xi>) i)
[PROOF STEP]
unfolding quality_increases_def
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
(\<forall>dip\<in>kD (rt \<xi>). dip \<in> kD (rt \<xi>') \<and> rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>') \<and> (\<forall>dip. sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip)
nsqn (rt \<xi>) i = nsqn (rt \<xi>') i

goal (1 subgoal):
 1. the (dhops (rt \<xi>') i) \<le> the (dhops (rt \<xi>) i)
[PROOF STEP]
by (clarsimp) (drule(1) bspec, clarsimp simp: rt_fresher_def2)


[STATEMENT]
lemma nsqn_quality_increases_nsqn_eq_le [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "quality_increases \<xi> \<xi>'"
      and "s = nsqn (rt \<xi>) i"
    shows "s < nsqn (rt \<xi>') i \<or> (s = nsqn (rt \<xi>') i \<and> the (dhops (rt \<xi>) i) \<ge> the (dhops (rt \<xi>') i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i \<or> s = nsqn (rt \<xi>') i \<and> the (dhops (rt \<xi>') i) \<le> the (dhops (rt \<xi>) i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
s = nsqn (rt \<xi>) i

goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i \<or> s = nsqn (rt \<xi>') i \<and> the (dhops (rt \<xi>') i) \<le> the (dhops (rt \<xi>) i)
[PROOF STEP]
by (metis nat_less_le nsqn_quality_increases nsqn_quality_increases_dhops)


[STATEMENT]
lemma quality_increases_rreq_rrep_props [elim]:
    fixes sn ip hops sip
  assumes qinc: "quality_increases (\<sigma> sip) (\<sigma>' sip)"
      and "1 \<le> sn"
      and *: "ip\<in>kD(rt (\<sigma> sip)) \<and> sn \<le> nsqn (rt (\<sigma> sip)) ip
                                \<and> (nsqn (rt (\<sigma> sip)) ip = sn
                                    \<longrightarrow> (the (dhops (rt (\<sigma> sip)) ip) \<le> hops
                                          \<or> the (flag (rt (\<sigma> sip)) ip) = inv))"
    shows "ip\<in>kD(rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip
                              \<and> (nsqn (rt (\<sigma>' sip)) ip = sn
                                  \<longrightarrow> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops
                                        \<or> the (flag (rt (\<sigma>' sip)) ip) = inv))"
      (is "_ \<and> ?nsqnafter")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt (\<sigma> sip)) \<and> sn \<le> nsqn (rt (\<sigma> sip)) ip \<and> (nsqn (rt (\<sigma> sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
obtain "ip\<in>kD(rt (\<sigma> sip))" and "sn \<le> nsqn (rt (\<sigma> sip)) ip"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt (\<sigma> sip)) \<and> sn \<le> nsqn (rt (\<sigma> sip)) ip \<and> (nsqn (rt (\<sigma> sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. (\<lbrakk>ip \<in> kD (rt (\<sigma> sip)); sn \<le> nsqn (rt (\<sigma> sip)) ip\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt (\<sigma> sip))
sn \<le> nsqn (rt (\<sigma> sip)) ip

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from \<open>quality_increases (\<sigma> sip) (\<sigma>' sip)\<close>
[PROOF STATE]
proof (chain)
picking this:
quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
have "sqn (rt (\<sigma> sip)) ip \<le> sqn (rt (\<sigma>' sip)) ip"
[PROOF STATE]
proof (prove)
using this:
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. sqn (rt (\<sigma> sip)) ip \<le> sqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sqn (rt (\<sigma> sip)) ip \<le> sqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from \<open>quality_increases (\<sigma> sip) (\<sigma>' sip)\<close> and \<open>ip\<in>kD (rt (\<sigma> sip))\<close>
[PROOF STATE]
proof (chain)
picking this:
quality_increases (\<sigma> sip) (\<sigma>' sip)
ip \<in> kD (rt (\<sigma> sip))
[PROOF STEP]
have "ip\<in>kD (rt (\<sigma>' sip))"
[PROOF STATE]
proof (prove)
using this:
quality_increases (\<sigma> sip) (\<sigma>' sip)
ip \<in> kD (rt (\<sigma> sip))

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt (\<sigma>' sip))

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from \<open>sn \<le> nsqn (rt (\<sigma> sip)) ip\<close>
[PROOF STATE]
proof (chain)
picking this:
sn \<le> nsqn (rt (\<sigma> sip)) ip
[PROOF STEP]
have ?nsqnafter
[PROOF STATE]
proof (prove)
using this:
sn \<le> nsqn (rt (\<sigma> sip)) ip

goal (1 subgoal):
 1. sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. sn < nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "sn < nsqn (rt (\<sigma> sip)) ip"
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma> sip)) ip

goal (2 subgoals):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. sn < nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma> sip)) ip

goal (2 subgoals):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. sn < nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from \<open>ip\<in>kD(rt (\<sigma> sip))\<close> and \<open>quality_increases (\<sigma> sip) (\<sigma>' sip)\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt (\<sigma> sip))
quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
have "... \<le> nsqn (rt (\<sigma>' sip)) ip"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt (\<sigma> sip))
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. nsqn (rt (\<sigma> sip)) ip \<le> nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn (rt (\<sigma> sip)) ip \<le> nsqn (rt (\<sigma>' sip)) ip

goal (2 subgoals):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. sn < nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sn < nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
have "sn < nsqn (rt (\<sigma>' sip)) ip"
[PROOF STATE]
proof (prove)
using this:
sn < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip

goal (2 subgoals):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. sn < nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sn < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "sn = nsqn (rt (\<sigma> sip)) ip"
[PROOF STATE]
proof (state)
this:
sn = nsqn (rt (\<sigma> sip)) ip

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>ip\<in>kD(rt (\<sigma> sip))\<close> and \<open>quality_increases (\<sigma> sip) (\<sigma>' sip)\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt (\<sigma> sip))
quality_increases (\<sigma> sip) (\<sigma>' sip)
sn = nsqn (rt (\<sigma> sip)) ip
[PROOF STEP]
have "sn < nsqn (rt (\<sigma>' sip)) ip
              \<or> (sn = nsqn (rt (\<sigma>' sip)) ip
                 \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip))"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt (\<sigma> sip))
quality_increases (\<sigma> sip) (\<sigma>' sip)
sn = nsqn (rt (\<sigma> sip)) ip

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
hence "sn < nsqn (rt (\<sigma>' sip)) ip
              \<or> (nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops
                                                 \<or> the (flag (rt (\<sigma>' sip)) ip) = inv))"
[PROOF STATE]
proof (prove)
using this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "sn < nsqn (rt (\<sigma>' sip)) ip"
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip

goal (2 subgoals):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sn < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "sn = nsqn (rt (\<sigma>' sip)) ip
                \<and> the (dhops (rt (\<sigma> sip)) ip) \<ge> the (dhops (rt (\<sigma>' sip)) ip)"
[PROOF STATE]
proof (state)
this:
sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
hence "sn = nsqn (rt (\<sigma>' sip)) ip"
          and "the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)"
[PROOF STATE]
proof (prove)
using this:
sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma>' sip)) ip &&& the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sn = nsqn (rt (\<sigma>' sip)) ip
the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from * and \<open>sn = nsqn (rt (\<sigma> sip)) ip\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt (\<sigma> sip)) \<and> sn \<le> nsqn (rt (\<sigma> sip)) ip \<and> (nsqn (rt (\<sigma> sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv)
sn = nsqn (rt (\<sigma> sip)) ip
[PROOF STEP]
have "the (dhops (rt (\<sigma> sip)) ip) \<le> hops
                                                       \<or> the (flag (rt (\<sigma> sip)) ip) = inv"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt (\<sigma> sip)) \<and> sn \<le> nsqn (rt (\<sigma> sip)) ip \<and> (nsqn (rt (\<sigma> sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv)
sn = nsqn (rt (\<sigma> sip)) ip

goal (1 subgoal):
 1. the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma>' sip)) ip \<and> the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "the (dhops (rt (\<sigma> sip)) ip) \<le> hops"
[PROOF STATE]
proof (state)
this:
the (dhops (rt (\<sigma> sip)) ip) \<le> hops

goal (2 subgoals):
 1. the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with  \<open>the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)\<close>
[PROOF STATE]
proof (chain)
picking this:
the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)
the (dhops (rt (\<sigma> sip)) ip) \<le> hops
[PROOF STEP]
have "the (dhops (rt (\<sigma>' sip)) ip) \<le> hops"
[PROOF STATE]
proof (prove)
using this:
the (dhops (rt (\<sigma>' sip)) ip) \<le> the (dhops (rt (\<sigma> sip)) ip)
the (dhops (rt (\<sigma> sip)) ip) \<le> hops

goal (1 subgoal):
 1. the (dhops (rt (\<sigma>' sip)) ip) \<le> hops
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (dhops (rt (\<sigma>' sip)) ip) \<le> hops

goal (2 subgoals):
 1. the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>sn = nsqn (rt (\<sigma>' sip)) ip\<close>
[PROOF STATE]
proof (chain)
picking this:
sn = nsqn (rt (\<sigma>' sip)) ip
the (dhops (rt (\<sigma>' sip)) ip) \<le> hops
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sn = nsqn (rt (\<sigma>' sip)) ip
the (dhops (rt (\<sigma>' sip)) ip) \<le> hops

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "the (flag (rt (\<sigma> sip)) ip) = inv"
[PROOF STATE]
proof (state)
this:
the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>ip\<in>kD(rt (\<sigma> sip))\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt (\<sigma> sip))
the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv
[PROOF STEP]
have "nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt (\<sigma> sip))
the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1

goal (1 subgoal):
 1. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>sn \<ge> 1\<close> and \<open>sn = nsqn (rt (\<sigma> sip)) ip\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> sn
sn = nsqn (rt (\<sigma> sip)) ip
nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1
[PROOF STEP]
have "sqn (rt (\<sigma> sip)) ip > 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> sn
sn = nsqn (rt (\<sigma> sip)) ip
nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1

goal (1 subgoal):
 1. 1 < sqn (rt (\<sigma> sip)) ip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < sqn (rt (\<sigma> sip)) ip

goal (1 subgoal):
 1. the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from \<open>ip\<in>kD(rt (\<sigma>' sip))\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt (\<sigma>' sip))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt (\<sigma>' sip))

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
proof (rule vD_or_iD)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. ip \<in> iD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "ip\<in>iD(rt (\<sigma>' sip))"
[PROOF STATE]
proof (state)
this:
ip \<in> iD (rt (\<sigma>' sip))

goal (2 subgoals):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. ip \<in> iD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
hence "the (flag (rt (\<sigma>' sip)) ip) = inv"
[PROOF STATE]
proof (prove)
using this:
ip \<in> iD (rt (\<sigma>' sip))

goal (1 subgoal):
 1. the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv

goal (2 subgoals):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
 2. ip \<in> iD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>sn = nsqn (rt (\<sigma>' sip)) ip\<close>
[PROOF STATE]
proof (chain)
picking this:
sn = nsqn (rt (\<sigma>' sip)) ip
the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sn = nsqn (rt (\<sigma>' sip)) ip
the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
(* the tricky case: sn = nsqn (rt (\<sigma>' sip)) ip
                                \<and> ip\<in>iD(rt (\<sigma> sip))
                                \<and> ip\<in>vD(rt (\<sigma>' sip)) *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
assume "ip\<in>vD(rt (\<sigma>' sip))"
[PROOF STATE]
proof (state)
this:
ip \<in> vD (rt (\<sigma>' sip))

goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
hence "nsqn (rt (\<sigma>' sip)) ip = sqn (rt (\<sigma>' sip)) ip"
[PROOF STATE]
proof (prove)
using this:
ip \<in> vD (rt (\<sigma>' sip))

goal (1 subgoal):
 1. nsqn (rt (\<sigma>' sip)) ip = sqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn (rt (\<sigma>' sip)) ip = sqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>sqn (rt (\<sigma> sip)) ip \<le> sqn (rt (\<sigma>' sip)) ip\<close>
[PROOF STATE]
proof (chain)
picking this:
sqn (rt (\<sigma> sip)) ip \<le> sqn (rt (\<sigma>' sip)) ip
nsqn (rt (\<sigma>' sip)) ip = sqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
have "nsqn (rt (\<sigma>' sip)) ip \<ge> sqn (rt (\<sigma> sip)) ip"
[PROOF STATE]
proof (prove)
using this:
sqn (rt (\<sigma> sip)) ip \<le> sqn (rt (\<sigma>' sip)) ip
nsqn (rt (\<sigma>' sip)) ip = sqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. sqn (rt (\<sigma> sip)) ip \<le> nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqn (rt (\<sigma> sip)) ip \<le> nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>sqn (rt (\<sigma> sip)) ip > 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 < sqn (rt (\<sigma> sip)) ip
sqn (rt (\<sigma> sip)) ip \<le> nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
have "nsqn (rt (\<sigma>' sip)) ip > sqn (rt (\<sigma> sip)) ip - 1"
[PROOF STATE]
proof (prove)
using this:
1 < sqn (rt (\<sigma> sip)) ip
sqn (rt (\<sigma> sip)) ip \<le> nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. sqn (rt (\<sigma> sip)) ip - 1 < nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqn (rt (\<sigma> sip)) ip - 1 < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1\<close>
[PROOF STATE]
proof (chain)
picking this:
nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1
sqn (rt (\<sigma> sip)) ip - 1 < nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
have "nsqn (rt (\<sigma>' sip)) ip > nsqn (rt (\<sigma> sip)) ip"
[PROOF STATE]
proof (prove)
using this:
nsqn (rt (\<sigma> sip)) ip = sqn (rt (\<sigma> sip)) ip - 1
sqn (rt (\<sigma> sip)) ip - 1 < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. nsqn (rt (\<sigma> sip)) ip < nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nsqn (rt (\<sigma> sip)) ip < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>sn = nsqn (rt (\<sigma> sip)) ip\<close>
[PROOF STATE]
proof (chain)
picking this:
sn = nsqn (rt (\<sigma> sip)) ip
nsqn (rt (\<sigma> sip)) ip < nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
have "nsqn (rt (\<sigma>' sip)) ip > sn"
[PROOF STATE]
proof (prove)
using this:
sn = nsqn (rt (\<sigma> sip)) ip
nsqn (rt (\<sigma> sip)) ip < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. ip \<in> vD (rt (\<sigma>' sip)) \<Longrightarrow> sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sn < nsqn (rt (\<sigma>' sip)) ip

goal (1 subgoal):
 1. sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. sn = nsqn (rt (\<sigma> sip)) ip \<Longrightarrow> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sn < nsqn (rt (\<sigma>' sip)) ip \<or> nsqn (rt (\<sigma>' sip)) ip = sn \<and> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
by (metis (mono_tags) le_cases not_le)
[PROOF STATE]
proof (state)
this:
sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
with \<open>ip\<in>kD (rt (\<sigma>' sip))\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt (\<sigma>' sip))
sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
show "ip\<in>kD (rt (\<sigma>' sip)) \<and> ?nsqnafter"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt (\<sigma>' sip))
sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quality_increases_rreq_rrep_props':
    fixes sn ip hops sip
  assumes "\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)"
      and "1 \<le> sn"
      and *: "ip\<in>kD(rt (\<sigma> sip)) \<and> sn \<le> nsqn (rt (\<sigma> sip)) ip
                                \<and> (nsqn (rt (\<sigma> sip)) ip = sn
                                    \<longrightarrow> (the (dhops (rt (\<sigma> sip)) ip) \<le> hops
                                          \<or> the (flag (rt (\<sigma> sip)) ip) = inv))"
    shows "ip\<in>kD(rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip
                              \<and> (nsqn (rt (\<sigma>' sip)) ip = sn
                                  \<longrightarrow> (the (dhops (rt (\<sigma>' sip)) ip) \<le> hops
                                        \<or> the (flag (rt (\<sigma>' sip)) ip) = inv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
have "quality_increases (\<sigma> sip) (\<sigma>' sip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
using assms(2-3)
[PROOF STATE]
proof (prove)
using this:
quality_increases (\<sigma> sip) (\<sigma>' sip)
1 \<le> sn
ip \<in> kD (rt (\<sigma> sip)) \<and> sn \<le> nsqn (rt (\<sigma> sip)) ip \<and> (nsqn (rt (\<sigma> sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma> sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) ip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)
[PROOF STEP]
by (rule quality_increases_rreq_rrep_props)
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt (\<sigma>' sip)) \<and> sn \<le> nsqn (rt (\<sigma>' sip)) ip \<and> (nsqn (rt (\<sigma>' sip)) ip = sn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) ip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) ip) = Aodv_Basic.inv)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rteq_quality_increases:
  assumes "\<forall>j. j \<noteq> i \<longrightarrow> quality_increases (\<sigma> j) (\<sigma>' j)"
      and "rt (\<sigma>' i) = rt (\<sigma> i)"
    shows "\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>j. j \<noteq> i \<longrightarrow> quality_increases (\<sigma> j) (\<sigma>' j)
rt (\<sigma>' i) = rt (\<sigma> i)

goal (1 subgoal):
 1. \<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by clarsimp (metis order_refl quality_increasesI rt_fresher_refl)


[STATEMENT]
lemma msg_fresh [simp]:
  "\<And>hops rreqid dip dsn dsk oip osn sip handled.
           msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled) =
                            (osn \<ge> 1 \<and> (sip \<noteq> oip \<longrightarrow> oip\<in>kD(rt (\<sigma> sip))
                                     \<and> nsqn (rt (\<sigma> sip)) oip \<ge> osn
                                     \<and> (nsqn (rt (\<sigma> sip)) oip = osn
                                           \<longrightarrow> (hops \<ge> the (dhops (rt (\<sigma> sip)) oip)
                                                \<or> the (flag (rt (\<sigma> sip)) oip) = inv))))"
  "\<And>hops dip dsn oip sip. msg_fresh \<sigma> (Rrep hops dip dsn oip sip) =
                            (dsn \<ge> 1 \<and> (sip \<noteq> dip \<longrightarrow> dip\<in>kD(rt (\<sigma> sip))
                                     \<and> nsqn (rt (\<sigma> sip)) dip \<ge> dsn
                                     \<and> (nsqn (rt (\<sigma> sip)) dip = dsn
                                           \<longrightarrow> (hops \<ge> the (dhops (rt (\<sigma> sip)) dip))
                                                 \<or> the (flag (rt (\<sigma> sip)) dip) = inv)))"
  "\<And>dests sip.            msg_fresh \<sigma> (Rerr dests sip) =
                            (\<forall>ripc\<in>dom(dests). (ripc\<in>kD(rt (\<sigma> sip))
                                     \<and> the (dests ripc) - 1 \<le> nsqn (rt (\<sigma> sip)) ripc))"
  "\<And>d dip.                msg_fresh \<sigma> (Newpkt d dip)   = True"
  "\<And>d dip sip.            msg_fresh \<sigma> (Pkt d dip sip)  = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip handled. msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled) = (1 \<le> osn \<and> (sip \<noteq> oip \<longrightarrow> oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)))) &&& (\<And>hops dip dsn oip sip. msg_fresh \<sigma> (Rrep hops dip dsn oip sip) = (1 \<le> dsn \<and> (sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv))))) &&& (\<And>dests sip. msg_fresh \<sigma> (Rerr dests sip) = (\<forall>ripc\<in>dom dests. ripc \<in> kD (rt (\<sigma> sip)) \<and> the (dests ripc) - 1 \<le> nsqn (rt (\<sigma> sip)) ripc)) &&& (\<And>d dip. msg_fresh \<sigma> (Newpkt d dip) = True) &&& (\<And>d dip sip. msg_fresh \<sigma> (Pkt d dip sip) = True)
[PROOF STEP]
unfolding msg_fresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip handled. (case Rreq hops rreqid dip dsn dsk oip osn sip handled of Rreq hopsc x xa xb xc oipc osnc sipc xd \<Rightarrow> 1 \<le> osnc \<and> (sipc \<noteq> oipc \<longrightarrow> oipc \<in> kD (rt (\<sigma> sipc)) \<and> osnc \<le> nsqn (rt (\<sigma> sipc)) oipc \<and> (nsqn (rt (\<sigma> sipc)) oipc = osnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) oipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) oipc) = Aodv_Basic.inv)) | Rrep hopsc dipc dsnc x sipc \<Rightarrow> 1 \<le> dsnc \<and> (sipc \<noteq> dipc \<longrightarrow> dipc \<in> kD (rt (\<sigma> sipc)) \<and> dsnc \<le> nsqn (rt (\<sigma> sipc)) dipc \<and> (nsqn (rt (\<sigma> sipc)) dipc = dsnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) dipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) dipc) = Aodv_Basic.inv)) | Rerr destsc sipc \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> kD (rt (\<sigma> sipc)) \<and> the (destsc ripc) - 1 \<le> nsqn (rt (\<sigma> sipc)) ripc | _ \<Rightarrow> True) = (1 \<le> osn \<and> (sip \<noteq> oip \<longrightarrow> oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)))) &&& (\<And>hops dip dsn oip sip. (case Rrep hops dip dsn oip sip of Rreq hopsc x xa xb xc oipc osnc sipc xd \<Rightarrow> 1 \<le> osnc \<and> (sipc \<noteq> oipc \<longrightarrow> oipc \<in> kD (rt (\<sigma> sipc)) \<and> osnc \<le> nsqn (rt (\<sigma> sipc)) oipc \<and> (nsqn (rt (\<sigma> sipc)) oipc = osnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) oipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) oipc) = Aodv_Basic.inv)) | Rrep hopsc dipc dsnc x sipc \<Rightarrow> 1 \<le> dsnc \<and> (sipc \<noteq> dipc \<longrightarrow> dipc \<in> kD (rt (\<sigma> sipc)) \<and> dsnc \<le> nsqn (rt (\<sigma> sipc)) dipc \<and> (nsqn (rt (\<sigma> sipc)) dipc = dsnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) dipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) dipc) = Aodv_Basic.inv)) | Rerr destsc sipc \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> kD (rt (\<sigma> sipc)) \<and> the (destsc ripc) - 1 \<le> nsqn (rt (\<sigma> sipc)) ripc | _ \<Rightarrow> True) = (1 \<le> dsn \<and> (sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv))))) &&& (\<And>dests sip. (case Rerr dests sip of Rreq hopsc x xa xb xc oipc osnc sipc xd \<Rightarrow> 1 \<le> osnc \<and> (sipc \<noteq> oipc \<longrightarrow> oipc \<in> kD (rt (\<sigma> sipc)) \<and> osnc \<le> nsqn (rt (\<sigma> sipc)) oipc \<and> (nsqn (rt (\<sigma> sipc)) oipc = osnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) oipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) oipc) = Aodv_Basic.inv)) | Rrep hopsc dipc dsnc x sipc \<Rightarrow> 1 \<le> dsnc \<and> (sipc \<noteq> dipc \<longrightarrow> dipc \<in> kD (rt (\<sigma> sipc)) \<and> dsnc \<le> nsqn (rt (\<sigma> sipc)) dipc \<and> (nsqn (rt (\<sigma> sipc)) dipc = dsnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) dipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) dipc) = Aodv_Basic.inv)) | Rerr destsc sipc \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> kD (rt (\<sigma> sipc)) \<and> the (destsc ripc) - 1 \<le> nsqn (rt (\<sigma> sipc)) ripc | _ \<Rightarrow> True) = (\<forall>ripc\<in>dom dests. ripc \<in> kD (rt (\<sigma> sip)) \<and> the (dests ripc) - 1 \<le> nsqn (rt (\<sigma> sip)) ripc)) &&& (\<And>d dip. (case Newpkt d dip of Rreq hopsc x xa xb xc oipc osnc sipc xd \<Rightarrow> 1 \<le> osnc \<and> (sipc \<noteq> oipc \<longrightarrow> oipc \<in> kD (rt (\<sigma> sipc)) \<and> osnc \<le> nsqn (rt (\<sigma> sipc)) oipc \<and> (nsqn (rt (\<sigma> sipc)) oipc = osnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) oipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) oipc) = Aodv_Basic.inv)) | Rrep hopsc dipc dsnc x sipc \<Rightarrow> 1 \<le> dsnc \<and> (sipc \<noteq> dipc \<longrightarrow> dipc \<in> kD (rt (\<sigma> sipc)) \<and> dsnc \<le> nsqn (rt (\<sigma> sipc)) dipc \<and> (nsqn (rt (\<sigma> sipc)) dipc = dsnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) dipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) dipc) = Aodv_Basic.inv)) | Rerr destsc sipc \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> kD (rt (\<sigma> sipc)) \<and> the (destsc ripc) - 1 \<le> nsqn (rt (\<sigma> sipc)) ripc | _ \<Rightarrow> True) = True) &&& (\<And>d dip sip. (case Pkt d dip sip of Rreq hopsc x xa xb xc oipc osnc sipc xd \<Rightarrow> 1 \<le> osnc \<and> (sipc \<noteq> oipc \<longrightarrow> oipc \<in> kD (rt (\<sigma> sipc)) \<and> osnc \<le> nsqn (rt (\<sigma> sipc)) oipc \<and> (nsqn (rt (\<sigma> sipc)) oipc = osnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) oipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) oipc) = Aodv_Basic.inv)) | Rrep hopsc dipc dsnc x sipc \<Rightarrow> 1 \<le> dsnc \<and> (sipc \<noteq> dipc \<longrightarrow> dipc \<in> kD (rt (\<sigma> sipc)) \<and> dsnc \<le> nsqn (rt (\<sigma> sipc)) dipc \<and> (nsqn (rt (\<sigma> sipc)) dipc = dsnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) dipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) dipc) = Aodv_Basic.inv)) | Rerr destsc sipc \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> kD (rt (\<sigma> sipc)) \<and> the (destsc ripc) - 1 \<le> nsqn (rt (\<sigma> sipc)) ripc | _ \<Rightarrow> True) = True)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma msg_fresh_inc_sn [simp, elim]:
  "msg_fresh \<sigma> m \<Longrightarrow> rreq_rrep_sn m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msg_fresh \<sigma> m \<Longrightarrow> rreq_rrep_sn m
[PROOF STEP]
by (cases m) simp_all


[STATEMENT]
lemma recv_msg_fresh_inc_sn [simp, elim]:
  "orecvmsg (msg_fresh) \<sigma> m \<Longrightarrow> recvmsg rreq_rrep_sn m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orecvmsg msg_fresh \<sigma> m \<Longrightarrow> recvmsg rreq_rrep_sn m
[PROOF STEP]
by (cases m) simp_all


[STATEMENT]
lemma rreq_nsqn_is_fresh [simp]:
  fixes \<sigma> msg hops rreqid dip dsn dsk oip osn sip handled
  assumes "rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)"
      and "rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip handled)"
  shows "msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled)"
        (is "msg_fresh \<sigma> ?msg")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled)
[PROOF STEP]
let ?rt = "rt (\<sigma> sip)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip handled)
[PROOF STEP]
have "1 \<le> osn"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip handled)

goal (1 subgoal):
 1. 1 \<le> osn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> osn

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> osn

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled)
[PROOF STEP]
unfolding msg_fresh_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> osn

goal (1 subgoal):
 1. case Rreq hops rreqid dip dsn dsk oip osn sip handled of Rreq hopsc x xa xb xc oipc osnc sipc xd \<Rightarrow> 1 \<le> osnc \<and> (sipc \<noteq> oipc \<longrightarrow> oipc \<in> kD (rt (\<sigma> sipc)) \<and> osnc \<le> nsqn (rt (\<sigma> sipc)) oipc \<and> (nsqn (rt (\<sigma> sipc)) oipc = osnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) oipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) oipc) = Aodv_Basic.inv)) | Rrep hopsc dipc dsnc x sipc \<Rightarrow> 1 \<le> dsnc \<and> (sipc \<noteq> dipc \<longrightarrow> dipc \<in> kD (rt (\<sigma> sipc)) \<and> dsnc \<le> nsqn (rt (\<sigma> sipc)) dipc \<and> (nsqn (rt (\<sigma> sipc)) dipc = dsnc \<longrightarrow> the (dhops (rt (\<sigma> sipc)) dipc) \<le> hopsc \<or> the (flag (rt (\<sigma> sipc)) dipc) = Aodv_Basic.inv)) | Rerr destsc sipc \<Rightarrow> \<forall>ripc\<in>dom destsc. ripc \<in> kD (rt (\<sigma> sipc)) \<and> the (destsc ripc) - 1 \<le> nsqn (rt (\<sigma> sipc)) ripc | _ \<Rightarrow> True
[PROOF STEP]
proof (simp only: msg.case, intro conjI impI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> oip \<in> kD (rt (\<sigma> sip))
 3. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 4. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip; nsqn (rt (\<sigma> sip)) oip = osn\<rbrakk> \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
assume "sip \<noteq> oip"
[PROOF STATE]
proof (state)
this:
sip \<noteq> oip

goal (4 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> oip \<in> kD (rt (\<sigma> sip))
 3. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 4. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip; nsqn (rt (\<sigma> sip)) oip = osn\<rbrakk> \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip
[PROOF STEP]
show "oip \<in> kD(?rt)"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
oip \<in> kD (rt (\<sigma> sip))

goal (3 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 3. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip; nsqn (rt (\<sigma> sip)) oip = osn\<rbrakk> \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 3. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip; nsqn (rt (\<sigma> sip)) oip = osn\<rbrakk> \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
assume "sip \<noteq> oip"
         and "nsqn ?rt oip = osn"
[PROOF STATE]
proof (state)
this:
sip \<noteq> oip
nsqn (rt (\<sigma> sip)) oip = osn

goal (3 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 3. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip; nsqn (rt (\<sigma> sip)) oip = osn\<rbrakk> \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
show "the (dhops ?rt oip) \<le> hops \<or> the (flag ?rt oip) = inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
proof (cases "oip\<in>vD(?rt)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. oip \<in> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
 2. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
assume "oip\<in>vD(?rt)"
[PROOF STATE]
proof (state)
this:
oip \<in> vD (rt (\<sigma> sip))

goal (2 subgoals):
 1. oip \<in> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
 2. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
hence "nsqn ?rt oip = sqn ?rt oip"
[PROOF STATE]
proof (prove)
using this:
oip \<in> vD (rt (\<sigma> sip))

goal (1 subgoal):
 1. nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip

goal (2 subgoals):
 1. oip \<in> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
 2. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
with \<open>nsqn ?rt oip = osn\<close>
[PROOF STATE]
proof (chain)
picking this:
nsqn (rt (\<sigma> sip)) oip = osn
nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip
[PROOF STEP]
have "sqn ?rt oip = osn"
[PROOF STATE]
proof (prove)
using this:
nsqn (rt (\<sigma> sip)) oip = osn
nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. sqn (rt (\<sigma> sip)) oip = osn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqn (rt (\<sigma> sip)) oip = osn

goal (2 subgoals):
 1. oip \<in> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
 2. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
with assms(1) and \<open>sip \<noteq> oip\<close>
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip
sqn (rt (\<sigma> sip)) oip = osn
[PROOF STEP]
have "the (dhops ?rt oip) \<le> hops"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip
sqn (rt (\<sigma> sip)) oip = osn

goal (1 subgoal):
 1. the (dhops (rt (\<sigma> sip)) oip) \<le> hops
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (dhops (rt (\<sigma> sip)) oip) \<le> hops

goal (2 subgoals):
 1. oip \<in> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
 2. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
the (dhops (rt (\<sigma> sip)) oip) \<le> hops

goal (1 subgoal):
 1. the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv

goal (1 subgoal):
 1. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
assume "oip\<notin>vD(?rt)"
[PROOF STATE]
proof (state)
this:
oip \<notin> vD (rt (\<sigma> sip))

goal (1 subgoal):
 1. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
oip \<notin> vD (rt (\<sigma> sip))

goal (1 subgoal):
 1. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
from assms(1) and \<open>sip \<noteq> oip\<close>
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip
[PROOF STEP]
have "oip\<in>kD(?rt)"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
oip \<in> kD (rt (\<sigma> sip))

goal (1 subgoal):
 1. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
oip \<notin> vD (rt (\<sigma> sip))
oip \<in> kD (rt (\<sigma> sip))
[PROOF STEP]
have "oip\<in>iD(?rt)"
[PROOF STATE]
proof (prove)
using this:
oip \<notin> vD (rt (\<sigma> sip))
oip \<in> kD (rt (\<sigma> sip))

goal (1 subgoal):
 1. oip \<in> iD (rt (\<sigma> sip))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
oip \<in> iD (rt (\<sigma> sip))

goal (1 subgoal):
 1. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
hence "the (flag ?rt oip) = inv"
[PROOF STATE]
proof (prove)
using this:
oip \<in> iD (rt (\<sigma> sip))

goal (1 subgoal):
 1. the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv

goal (1 subgoal):
 1. oip \<notin> vD (rt (\<sigma> sip)) \<Longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv

goal (1 subgoal):
 1. the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv

goal (2 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
assume "sip \<noteq> oip"
[PROOF STATE]
proof (state)
this:
sip \<noteq> oip

goal (2 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip
[PROOF STEP]
have "osn \<le> sqn ?rt oip"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip

goal (1 subgoal):
 1. osn \<le> sqn (rt (\<sigma> sip)) oip
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
osn \<le> sqn (rt (\<sigma> sip)) oip

goal (2 subgoals):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>1 \<le> osn; 1 \<le> osn; sip \<noteq> oip\<rbrakk> \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
thus "osn \<le> nsqn (rt (\<sigma> sip)) oip"
[PROOF STATE]
proof (prove)
using this:
osn \<le> sqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
proof (rule nat_le_eq_or_lt)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 2. osn < sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
assume "osn < sqn ?rt oip"
[PROOF STATE]
proof (state)
this:
osn < sqn (rt (\<sigma> sip)) oip

goal (2 subgoals):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 2. osn < sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
hence "osn \<le> sqn ?rt oip - 1"
[PROOF STATE]
proof (prove)
using this:
osn < sqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. osn \<le> sqn (rt (\<sigma> sip)) oip - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
osn \<le> sqn (rt (\<sigma> sip)) oip - 1

goal (2 subgoals):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 2. osn < sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
osn \<le> sqn (rt (\<sigma> sip)) oip - 1

goal (2 subgoals):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 2. osn < sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
have "... \<le> nsqn ?rt oip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn (rt (\<sigma> sip)) oip - 1 \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
by (rule sqn_nsqn)
[PROOF STATE]
proof (state)
this:
sqn (rt (\<sigma> sip)) oip - 1 \<le> nsqn (rt (\<sigma> sip)) oip

goal (2 subgoals):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
 2. osn < sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
show "osn \<le> nsqn ?rt oip"
[PROOF STATE]
proof (prove)
using this:
osn \<le> nsqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
osn \<le> nsqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
assume "osn = sqn ?rt oip"
[PROOF STATE]
proof (state)
this:
osn = sqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
with assms(1) and \<open>sip \<noteq> oip\<close>
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip
osn = sqn (rt (\<sigma> sip)) oip
[PROOF STEP]
have "oip\<in>kD(?rt)"
                                       and "the (flag ?rt oip) = val"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rreq hops rreqid dip dsn dsk oip osn sip handled)
sip \<noteq> oip
osn = sqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip)) &&& the (flag (rt (\<sigma> sip)) oip) = val
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
oip \<in> kD (rt (\<sigma> sip))
the (flag (rt (\<sigma> sip)) oip) = val

goal (1 subgoal):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
hence "nsqn ?rt oip = sqn ?rt oip"
[PROOF STATE]
proof (prove)
using this:
oip \<in> kD (rt (\<sigma> sip))
the (flag (rt (\<sigma> sip)) oip) = val

goal (1 subgoal):
 1. nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
with \<open>osn = sqn ?rt oip\<close>
[PROOF STATE]
proof (chain)
picking this:
osn = sqn (rt (\<sigma> sip)) oip
nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip
[PROOF STEP]
have "nsqn ?rt oip = osn"
[PROOF STATE]
proof (prove)
using this:
osn = sqn (rt (\<sigma> sip)) oip
nsqn (rt (\<sigma> sip)) oip = sqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. nsqn (rt (\<sigma> sip)) oip = osn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nsqn (rt (\<sigma> sip)) oip = osn

goal (1 subgoal):
 1. osn = sqn (rt (\<sigma> sip)) oip \<Longrightarrow> osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
thus "osn \<le> nsqn ?rt oip"
[PROOF STATE]
proof (prove)
using this:
nsqn (rt (\<sigma> sip)) oip = osn

goal (1 subgoal):
 1. osn \<le> nsqn (rt (\<sigma> sip)) oip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
osn \<le> nsqn (rt (\<sigma> sip)) oip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
osn \<le> nsqn (rt (\<sigma> sip)) oip

goal (1 subgoal):
 1. \<lbrakk>1 \<le> osn; 1 \<le> osn\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma> (Rreq hops rreqid dip dsn dsk oip osn sip handled)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rrep_nsqn_is_fresh [simp]:
  fixes \<sigma> msg hops dip dsn oip sip
  assumes "rreq_rrep_fresh (rt (\<sigma> sip)) (Rrep hops dip dsn oip sip)"
      and "rreq_rrep_sn (Rrep hops dip dsn oip sip)"
  shows "msg_fresh \<sigma> (Rrep hops dip dsn oip sip)"
        (is "msg_fresh \<sigma> ?msg")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rrep hops dip dsn oip sip)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rrep hops dip dsn oip sip)
[PROOF STEP]
let ?rt = "rt (\<sigma> sip)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rrep hops dip dsn oip sip)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rrep hops dip dsn oip sip)
rreq_rrep_sn (Rrep hops dip dsn oip sip)
[PROOF STEP]
have "sip \<noteq> dip \<longrightarrow> dip\<in>kD(?rt) \<and> sqn ?rt dip = dsn \<and> the (flag ?rt dip) = val"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rrep hops dip dsn oip sip)
rreq_rrep_sn (Rrep hops dip dsn oip sip)

goal (1 subgoal):
 1. sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> sqn (rt (\<sigma> sip)) dip = dsn \<and> the (flag (rt (\<sigma> sip)) dip) = val
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> sqn (rt (\<sigma> sip)) dip = dsn \<and> the (flag (rt (\<sigma> sip)) dip) = val

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rrep hops dip dsn oip sip)
[PROOF STEP]
hence "sip \<noteq> dip \<longrightarrow> dip\<in>kD(?rt) \<and> nsqn ?rt dip \<ge> dsn"
[PROOF STATE]
proof (prove)
using this:
sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> sqn (rt (\<sigma> sip)) dip = dsn \<and> the (flag (rt (\<sigma> sip)) dip) = val

goal (1 subgoal):
 1. sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rrep hops dip dsn oip sip)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rrep hops dip dsn oip sip)
rreq_rrep_sn (Rrep hops dip dsn oip sip)
sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip
[PROOF STEP]
show "msg_fresh \<sigma> ?msg"
[PROOF STATE]
proof (prove)
using this:
rreq_rrep_fresh (rt (\<sigma> sip)) (Rrep hops dip dsn oip sip)
rreq_rrep_sn (Rrep hops dip dsn oip sip)
sip \<noteq> dip \<longrightarrow> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rrep hops dip dsn oip sip)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma> (Rrep hops dip dsn oip sip)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rerr_nsqn_is_fresh [simp]:
  fixes \<sigma> msg dests sip
  assumes "rerr_invalid (rt (\<sigma> sip)) (Rerr dests sip)"
  shows "msg_fresh \<sigma> (Rerr dests sip)"
        (is "msg_fresh \<sigma> ?msg")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rerr dests sip)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rerr dests sip)
[PROOF STEP]
let ?rt = "rt (\<sigma> sip)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msg_fresh \<sigma> (Rerr dests sip)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
rerr_invalid (rt (\<sigma> sip)) (Rerr dests sip)
[PROOF STEP]
have *: "(\<forall>rip\<in>dom(dests). (rip\<in>iD(rt (\<sigma> sip))
                                     \<and> the (dests rip) = sqn (rt (\<sigma> sip)) rip))"
[PROOF STATE]
proof (prove)
using this:
rerr_invalid (rt (\<sigma> sip)) (Rerr dests sip)

goal (1 subgoal):
 1. \<forall>rip\<in>dom dests. rip \<in> iD (rt (\<sigma> sip)) \<and> the (dests rip) = sqn (rt (\<sigma> sip)) rip
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<forall>rip\<in>dom dests. rip \<in> iD (rt (\<sigma> sip)) \<and> the (dests rip) = sqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rerr dests sip)
[PROOF STEP]
have "(\<forall>rip\<in>dom(dests). (rip\<in>kD(rt (\<sigma> sip))
                                     \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
fix rip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
assume "rip \<in> dom dests"
[PROOF STATE]
proof (state)
this:
rip \<in> dom dests

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>rip\<in>dom dests. rip \<in> iD (rt (\<sigma> sip)) \<and> the (dests rip) = sqn (rt (\<sigma> sip)) rip
rip \<in> dom dests
[PROOF STEP]
have "rip\<in>iD(rt (\<sigma> sip))" and "the (dests rip) = sqn (rt (\<sigma> sip)) rip"
[PROOF STATE]
proof (prove)
using this:
\<forall>rip\<in>dom dests. rip \<in> iD (rt (\<sigma> sip)) \<and> the (dests rip) = sqn (rt (\<sigma> sip)) rip
rip \<in> dom dests

goal (1 subgoal):
 1. rip \<in> iD (rt (\<sigma> sip)) &&& the (dests rip) = sqn (rt (\<sigma> sip)) rip
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rip \<in> iD (rt (\<sigma> sip))
the (dests rip) = sqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
the (dests rip) = sqn (rt (\<sigma> sip)) rip
[PROOF STEP]
have "the (dests rip) - 1 = sqn (rt (\<sigma> sip)) rip - 1"
[PROOF STATE]
proof (prove)
using this:
the (dests rip) = sqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. the (dests rip) - 1 = sqn (rt (\<sigma> sip)) rip - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (dests rip) - 1 = sqn (rt (\<sigma> sip)) rip - 1

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
the (dests rip) - 1 = sqn (rt (\<sigma> sip)) rip - 1

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
have "... \<le> nsqn (rt (\<sigma> sip)) rip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn (rt (\<sigma> sip)) rip - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
by (rule sqn_nsqn)
[PROOF STATE]
proof (state)
this:
sqn (rt (\<sigma> sip)) rip - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
have "the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip"
[PROOF STATE]
proof (prove)
using this:
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
with \<open>rip\<in>iD(rt (\<sigma> sip))\<close>
[PROOF STATE]
proof (chain)
picking this:
rip \<in> iD (rt (\<sigma> sip))
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
show "rip\<in>kD(rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip"
[PROOF STATE]
proof (prove)
using this:
rip \<in> iD (rt (\<sigma> sip))
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rerr dests sip)
[PROOF STEP]
thus "msg_fresh \<sigma> ?msg"
[PROOF STATE]
proof (prove)
using this:
\<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. msg_fresh \<sigma> (Rerr dests sip)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma> (Rerr dests sip)

goal:
No subgoals!
[PROOF STEP]
qed