[STATEMENT]
lemma anycast_msg_zhops:
  "\<And>rreqid dip dsn dsk oip osn sip.
      paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(_, a, _). anycast msg_zhops a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rreqid dip dsn dsk oip osn sip. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(uu_, a, uu_). anycast msg_zhops a)
[PROOF STEP]
proof (inv_cterms inv add:
           onl_invariant_sterms [OF aodv_wf rreq_dip_in_vD_dip_eq_ip [THEN invariant_restrict_inD]]
           onl_invariant_sterms [OF aodv_wf hop_count_positive [THEN invariant_restrict_inD]],
         elim conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p' pp'. \<lbrakk>l = PRreq-:14; ((\<xi>, {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'), unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)), \<xi>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:15 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>, p') \<in> reachable (paodv i) TT; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'; l' = PRreq-:15; a = unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)); \<xi>' = \<xi>; q = p'; dip \<xi> \<in> vD (rt \<xi>); dip \<xi> \<noteq> ip \<xi>\<rbrakk> \<Longrightarrow> 0 < the (dhops (rt \<xi>) (dip \<xi>))
[PROOF STEP]
fix l \<xi> a pp p' pp'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p' pp'. \<lbrakk>l = PRreq-:14; ((\<xi>, {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'), unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)), \<xi>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:15 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>, p') \<in> reachable (paodv i) TT; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'; l' = PRreq-:15; a = unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)); \<xi>' = \<xi>; q = p'; dip \<xi> \<in> vD (rt \<xi>); dip \<xi> \<noteq> ip \<xi>\<rbrakk> \<Longrightarrow> 0 < the (dhops (rt \<xi>) (dip \<xi>))
[PROOF STEP]
assume "(\<xi>, pp) \<in> reachable (paodv i) TT"
       and "{PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)),
               \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)).
                     p' \<triangleright> pp' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp"
       and "l = PRreq-:14"
       and "a = unicast (the (nhop (rt \<xi>) (oip \<xi>)))
                 (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>))"
       and *: "\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)"
       and "dip \<xi> \<in> vD (rt \<xi>)"
[PROOF STATE]
proof (state)
this:
(\<xi>, pp) \<in> reachable (paodv i) TT
{PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp
l = PRreq-:14
a = unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>))
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)
dip \<xi> \<in> vD (rt \<xi>)

goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p' pp'. \<lbrakk>l = PRreq-:14; ((\<xi>, {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'), unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)), \<xi>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:15 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>, p') \<in> reachable (paodv i) TT; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'; l' = PRreq-:15; a = unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)); \<xi>' = \<xi>; q = p'; dip \<xi> \<in> vD (rt \<xi>); dip \<xi> \<noteq> ip \<xi>\<rbrakk> \<Longrightarrow> 0 < the (dhops (rt \<xi>) (dip \<xi>))
[PROOF STEP]
from \<open>dip \<xi> \<in> vD (rt \<xi>)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<xi> \<in> vD (rt \<xi>)
[PROOF STEP]
have "dip \<xi> \<in> kD (rt \<xi>)"
[PROOF STATE]
proof (prove)
using this:
dip \<xi> \<in> vD (rt \<xi>)

goal (1 subgoal):
 1. dip \<xi> \<in> kD (rt \<xi>)
[PROOF STEP]
by (rule vD_iD_gives_kD(1))
[PROOF STATE]
proof (state)
this:
dip \<xi> \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p' pp'. \<lbrakk>l = PRreq-:14; ((\<xi>, {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'), unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)), \<xi>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:15 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>, p') \<in> reachable (paodv i) TT; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'; l' = PRreq-:15; a = unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)); \<xi>' = \<xi>; q = p'; dip \<xi> \<in> vD (rt \<xi>); dip \<xi> \<noteq> ip \<xi>\<rbrakk> \<Longrightarrow> 0 < the (dhops (rt \<xi>) (dip \<xi>))
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)
dip \<xi> \<in> kD (rt \<xi>)
[PROOF STEP]
have "Suc 0 \<le> the (dhops (rt \<xi>) (dip \<xi>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)
dip \<xi> \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. Suc 0 \<le> the (dhops (rt \<xi>) (dip \<xi>))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> the (dhops (rt \<xi>) (dip \<xi>))

goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p' pp'. \<lbrakk>l = PRreq-:14; ((\<xi>, {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'), unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)), \<xi>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:15 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>, p') \<in> reachable (paodv i) TT; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:14}unicast(\<lambda>\<xi>. the (nhop (rt \<xi>) (oip \<xi>)), \<lambda>\<xi>. Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)) .
p' \<triangleright> pp'; l' = PRreq-:15; a = unicast (the (nhop (rt \<xi>) (oip \<xi>))) (Rrep (the (dhops (rt \<xi>) (dip \<xi>))) (dip \<xi>) (sqn (rt \<xi>) (dip \<xi>)) (oip \<xi>) (ip \<xi>)); \<xi>' = \<xi>; q = p'; dip \<xi> \<in> vD (rt \<xi>); dip \<xi> \<noteq> ip \<xi>\<rbrakk> \<Longrightarrow> 0 < the (dhops (rt \<xi>) (dip \<xi>))
[PROOF STEP]
thus "0 < the (dhops (rt \<xi>) (dip \<xi>))"
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> the (dhops (rt \<xi>) (dip \<xi>))

goal (1 subgoal):
 1. 0 < the (dhops (rt \<xi>) (dip \<xi>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < the (dhops (rt \<xi>) (dip \<xi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hop_count_zero_oip_dip_sip:
  "paodv i \<TTurnstile> (recvmsg msg_zhops \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                 (l\<in>{PAodv-:4..PAodv-:5} \<union> {PRreq-:n|n. True} \<longrightarrow>
                          (hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>))
                 \<and>
                 ((l\<in>{PAodv-:6..PAodv-:7} \<union> {PRrep-:n|n. True} \<longrightarrow>
                          (hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg msg_zhops \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>))
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) auto


[STATEMENT]
lemma osn_rreq:
  "paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                                    l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n|n. True} \<longrightarrow> 1 \<le> osn \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) clarsimp


[STATEMENT]
lemma osn_rreq':
  "paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                                    l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n|n. True} \<longrightarrow> 1 \<le> osn \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>)
[PROOF STEP]
proof (rule invariant_weakenE [OF osn_rreq])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg rreq_rrep_sn a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg rreq_rrep_sn a
[PROOF STEP]
assume "recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a"
[PROOF STATE]
proof (state)
this:
recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a

goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg rreq_rrep_sn a
[PROOF STEP]
thus "recvmsg rreq_rrep_sn a"
[PROOF STATE]
proof (prove)
using this:
recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a

goal (1 subgoal):
 1. recvmsg rreq_rrep_sn a
[PROOF STEP]
by (cases a) simp_all
[PROOF STATE]
proof (state)
this:
recvmsg rreq_rrep_sn a

goal (1 subgoal):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:4, PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> 1 \<le> osn \<xi>) s
[PROOF STEP]
qed


[STATEMENT]
lemma dsn_rrep:
  "paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                                    l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n|n. True} \<longrightarrow> 1 \<le> dsn \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) clarsimp


[STATEMENT]
lemma dsn_rrep':
  "paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>)  onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                                    l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n|n. True} \<longrightarrow> 1 \<le> dsn \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>)
[PROOF STEP]
proof (rule invariant_weakenE [OF dsn_rrep])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg rreq_rrep_sn a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg rreq_rrep_sn a
[PROOF STEP]
assume "recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a"
[PROOF STATE]
proof (state)
this:
recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a

goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg rreq_rrep_sn a
[PROOF STEP]
thus "recvmsg rreq_rrep_sn a"
[PROOF STATE]
proof (prove)
using this:
recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a

goal (1 subgoal):
 1. recvmsg rreq_rrep_sn a
[PROOF STEP]
by (cases a) simp_all
[PROOF STATE]
proof (state)
this:
recvmsg rreq_rrep_sn a

goal (1 subgoal):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:6, PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> 1 \<le> dsn \<xi>) s
[PROOF STEP]
qed


[STATEMENT]
lemma hop_count_zero_oip_dip_sip':
  "paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                 (l\<in>{PAodv-:4..PAodv-:5} \<union> {PRreq-:n|n. True} \<longrightarrow>
                          (hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>))
                 \<and>
                 ((l\<in>{PAodv-:6..PAodv-:7} \<union> {PRrep-:n|n. True} \<longrightarrow>
                          (hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>))
[PROOF STEP]
proof (rule invariant_weakenE [OF hop_count_zero_oip_dip_sip])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg msg_zhops a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg msg_zhops a
[PROOF STEP]
assume "recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a"
[PROOF STATE]
proof (state)
this:
recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a

goal (2 subgoals):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s
 2. \<And>a. recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a \<Longrightarrow> recvmsg msg_zhops a
[PROOF STEP]
thus "recvmsg msg_zhops a"
[PROOF STATE]
proof (prove)
using this:
recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) a

goal (1 subgoal):
 1. recvmsg msg_zhops a
[PROOF STEP]
by (cases a) simp_all
[PROOF STATE]
proof (state)
this:
recvmsg msg_zhops a

goal (1 subgoal):
 1. \<And>s. onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s \<Longrightarrow> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:4..PAodv-:5} \<union> {PRreq-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> oip \<xi> = sip \<xi>) \<and> (l \<in> {PAodv-:6..PAodv-:7} \<union> {PRrep-:n |n. True} \<longrightarrow> hops \<xi> = 0 \<longrightarrow> dip \<xi> = sip \<xi>)) s
[PROOF STEP]
qed


[STATEMENT]
lemma zero_seq_unk_hops_one':
  "paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, _).
                 \<forall>dip\<in>kD(rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk)
                              \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1)
                              \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
fix dip and \<xi> :: state and P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
assume "sqn (invalidate (rt \<xi>) (dests \<xi>)) dip = 0"
       and all: "\<forall>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip"
       and *: "sqn (rt \<xi>) dip = 0 \<Longrightarrow> P \<xi> dip"
[PROOF STATE]
proof (state)
this:
sqn (invalidate (rt \<xi>) (dests \<xi>)) dip = 0
\<forall>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip
sqn (rt \<xi>) dip = 0 \<Longrightarrow> P \<xi> dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
have "P \<xi> dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<xi> dip
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<xi> dip
[PROOF STEP]
from all
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip
[PROOF STEP]
have "sqn (rt \<xi>) dip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) dip"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip

goal (1 subgoal):
 1. sqn (rt \<xi>) dip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) dip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sqn (rt \<xi>) dip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) dip

goal (1 subgoal):
 1. P \<xi> dip
[PROOF STEP]
with \<open>sqn (invalidate (rt \<xi>) (dests \<xi>)) dip = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
sqn (invalidate (rt \<xi>) (dests \<xi>)) dip = 0
sqn (rt \<xi>) dip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) dip
[PROOF STEP]
have "sqn (rt \<xi>) dip = 0"
[PROOF STATE]
proof (prove)
using this:
sqn (invalidate (rt \<xi>) (dests \<xi>)) dip = 0
sqn (rt \<xi>) dip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) dip

goal (1 subgoal):
 1. sqn (rt \<xi>) dip = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqn (rt \<xi>) dip = 0

goal (1 subgoal):
 1. P \<xi> dip
[PROOF STEP]
thus "P \<xi> dip"
[PROOF STATE]
proof (prove)
using this:
sqn (rt \<xi>) dip = 0

goal (1 subgoal):
 1. P \<xi> dip
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
P \<xi> dip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<xi> dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ?dip2 = 0; \<forall>ip. sqn (rt ?\<xi>2) ip \<le> sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ip; sqn (rt ?\<xi>2) ?dip2 = 0 \<Longrightarrow> ?P2 ?\<xi>2 ?dip2\<rbrakk> \<Longrightarrow> ?P2 ?\<xi>2 ?dip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
note sqn_invalidate_zero [elim!] = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ?dip2 = 0; \<forall>ip. sqn (rt ?\<xi>2) ip \<le> sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ip; sqn (rt ?\<xi>2) ?dip2 = 0 \<Longrightarrow> ?P2 ?\<xi>2 ?dip2\<rbrakk> \<Longrightarrow> ?P2 ?\<xi>2 ?dip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ?dip2 = 0; \<forall>ip. sqn (rt ?\<xi>2) ip \<le> sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ip; sqn (rt ?\<xi>2) ?dip2 = 0 \<Longrightarrow> ?P2 ?\<xi>2 ?dip2\<rbrakk> \<Longrightarrow> ?P2 ?\<xi>2 ?dip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
fix dsn hops :: nat and sip oip rt and ip dip :: ip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
assume "\<forall>dip\<in>kD(rt).
                (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3(the (rt dip)) = unk) \<and>
                (\<pi>\<^sub>3(the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and>
                (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)"
       and "hops = 0 \<longrightarrow> sip = dip"
       and "Suc 0 \<le> dsn"
       and "ip \<noteq> dip \<longrightarrow> ip\<in>kD(rt)"
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)
hops = 0 \<longrightarrow> sip = dip
Suc 0 \<le> dsn
ip \<noteq> dip \<longrightarrow> ip \<in> kD rt

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
hence "the (dhops (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = Suc 0 \<longrightarrow>
           the (nhop (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = ip"
[PROOF STATE]
proof (prove)
using this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)
hops = 0 \<longrightarrow> sip = dip
Suc 0 \<le> dsn
ip \<noteq> dip \<longrightarrow> ip \<in> kD rt

goal (1 subgoal):
 1. the (dhops (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = Suc 0 \<longrightarrow> the (nhop (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = ip
[PROOF STEP]
by - (rule update_cases, auto simp add: sqn_def dest!: bspec)
[PROOF STATE]
proof (state)
this:
the (dhops (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = Suc 0 \<longrightarrow> the (nhop (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = ip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); ?hops2 = 0 \<longrightarrow> ?sip2 = ?dip2; Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> the (dhops (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = Suc 0 \<longrightarrow> the (nhop (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = ?ip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
note prreq_ok1 [simp] = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); ?hops2 = 0 \<longrightarrow> ?sip2 = ?dip2; Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> the (dhops (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = Suc 0 \<longrightarrow> the (nhop (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = ?ip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); ?hops2 = 0 \<longrightarrow> ?sip2 = ?dip2; Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> the (dhops (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = Suc 0 \<longrightarrow> the (nhop (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = ?ip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
fix ip dsn hops sip oip rt dip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
assume "\<forall>dip\<in>kD(rt).
                (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3(the (rt dip)) = unk) \<and>
                (\<pi>\<^sub>3(the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and>
                (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)"
       and "Suc 0 \<le> dsn"
       and "ip \<noteq> dip \<longrightarrow> ip\<in>kD(rt)"
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)
Suc 0 \<le> dsn
ip \<noteq> dip \<longrightarrow> ip \<in> kD rt

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
hence "\<pi>\<^sub>3(the (update rt dip (dsn, kno, val, Suc hops, sip) ip)) = unk \<longrightarrow>
           the (dhops (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = Suc 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)
Suc 0 \<le> dsn
ip \<noteq> dip \<longrightarrow> ip \<in> kD rt

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (update rt dip (dsn, kno, val, Suc hops, sip) ip)) = unk \<longrightarrow> the (dhops (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = Suc 0
[PROOF STEP]
by - (rule update_cases, auto simp add: sqn_def sqnf_def dest!: bspec)
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (update rt dip (dsn, kno, val, Suc hops, sip) ip)) = unk \<longrightarrow> the (dhops (update rt dip (dsn, kno, val, Suc hops, sip)) ip) = Suc 0

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2) ?ip2)) = unk \<longrightarrow> the (dhops (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = Suc 0

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
note prreq_ok2 [simp] = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2) ?ip2)) = unk \<longrightarrow> the (dhops (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = Suc 0

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2) ?ip2)) = unk \<longrightarrow> the (dhops (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = Suc 0

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
fix ip dsn hops sip oip rt dip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
assume "\<forall>dip\<in>kD(rt).
                (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3(the (rt dip)) = unk) \<and>
                (\<pi>\<^sub>3(the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and>
                (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)"
       and "Suc 0 \<le> dsn"
       and "ip \<noteq> dip \<longrightarrow> ip\<in>kD(rt)"
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)
Suc 0 \<le> dsn
ip \<noteq> dip \<longrightarrow> ip \<in> kD rt

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
hence "sqn (update rt dip (dsn, kno, val, Suc hops, sip)) ip = 0 \<longrightarrow>
           \<pi>\<^sub>3 (the (update rt dip (dsn, kno, val, Suc hops, sip) ip)) = unk"
[PROOF STATE]
proof (prove)
using this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)
Suc 0 \<le> dsn
ip \<noteq> dip \<longrightarrow> ip \<in> kD rt

goal (1 subgoal):
 1. sqn (update rt dip (dsn, kno, val, Suc hops, sip)) ip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update rt dip (dsn, kno, val, Suc hops, sip) ip)) = unk
[PROOF STEP]
by - (rule update_cases, auto simp add: sqn_def dest!: bspec)
[PROOF STATE]
proof (state)
this:
sqn (update rt dip (dsn, kno, val, Suc hops, sip)) ip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update rt dip (dsn, kno, val, Suc hops, sip) ip)) = unk

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> sqn (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2 = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2) ?ip2)) = unk

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
note prreq_ok3 [simp] = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> sqn (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2 = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2) ?ip2)) = unk

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip); Suc 0 \<le> ?dsn2; ?ip2 \<noteq> ?dip2 \<longrightarrow> ?ip2 \<in> kD ?rt2\<rbrakk> \<Longrightarrow> sqn (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2)) ?ip2 = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?dip2 (?dsn2, kno, val, Suc ?hops2, ?sip2) ?ip2)) = unk

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
fix rt sip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
assume "\<forall>dip\<in>kD rt.
              (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3(the (rt dip)) = unk) \<and>
              (\<pi>\<^sub>3(the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and>
              (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)"
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
hence "\<forall>dip\<in>kD rt.
          (sqn (update rt sip (0, unk, val, Suc 0, sip)) dip = 0 \<longrightarrow>
           \<pi>\<^sub>3(the (update rt sip (0, unk, val, Suc 0, sip) dip)) = unk)
        \<and> (\<pi>\<^sub>3(the (update rt sip (0, unk, val, Suc 0, sip) dip)) = unk \<longrightarrow>
           the (dhops (update rt sip (0, unk, val, Suc 0, sip)) dip) = Suc 0)
        \<and> (the (dhops (update rt sip (0, unk, val, Suc 0, sip)) dip) = Suc 0 \<longrightarrow>
           the (nhop (update rt sip (0, unk, val, Suc 0, sip)) dip) = dip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>dip\<in>kD rt. (sqn rt dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk) \<and> (\<pi>\<^sub>3 (the (rt dip)) = unk \<longrightarrow> the (dhops rt dip) = Suc 0) \<and> (the (dhops rt dip) = Suc 0 \<longrightarrow> the (nhop rt dip) = dip)

goal (1 subgoal):
 1. \<forall>dip\<in>kD rt. (sqn (update rt sip (0, unk, val, Suc 0, sip)) dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update rt sip (0, unk, val, Suc 0, sip) dip)) = unk) \<and> (\<pi>\<^sub>3 (the (update rt sip (0, unk, val, Suc 0, sip) dip)) = unk \<longrightarrow> the (dhops (update rt sip (0, unk, val, Suc 0, sip)) dip) = Suc 0) \<and> (the (dhops (update rt sip (0, unk, val, Suc 0, sip)) dip) = Suc 0 \<longrightarrow> the (nhop (update rt sip (0, unk, val, Suc 0, sip)) dip) = dip)
[PROOF STEP]
by - (rule update_cases, simp_all add: sqnf_def sqn_def)
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. (sqn (update rt sip (0, unk, val, Suc 0, sip)) dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update rt sip (0, unk, val, Suc 0, sip) dip)) = unk) \<and> (\<pi>\<^sub>3 (the (update rt sip (0, unk, val, Suc 0, sip) dip)) = unk \<longrightarrow> the (dhops (update rt sip (0, unk, val, Suc 0, sip)) dip) = Suc 0) \<and> (the (dhops (update rt sip (0, unk, val, Suc 0, sip)) dip) = Suc 0 \<longrightarrow> the (nhop (update rt sip (0, unk, val, Suc 0, sip)) dip) = dip)

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip) \<Longrightarrow> \<forall>dip\<in>kD ?rt2. (sqn (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2) dip)) = unk) \<and> (\<pi>\<^sub>3 (the (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2) dip)) = unk \<longrightarrow> the (dhops (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip) = Suc 0) \<and> (the (dhops (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip) = Suc 0 \<longrightarrow> the (nhop (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip) = dip)

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
note prreq_ok4 [simp] = this
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD ?rt2. (sqn ?rt2 dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (?rt2 dip)) = unk) \<and> (\<pi>\<^sub>3 (the (?rt2 dip)) = unk \<longrightarrow> the (dhops ?rt2 dip) = Suc 0) \<and> (the (dhops ?rt2 dip) = Suc 0 \<longrightarrow> the (nhop ?rt2 dip) = dip) \<Longrightarrow> \<forall>dip\<in>kD ?rt2. (sqn (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2) dip)) = unk) \<and> (\<pi>\<^sub>3 (the (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2) dip)) = unk \<longrightarrow> the (dhops (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip) = Suc 0) \<and> (the (dhops (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip) = Suc 0 \<longrightarrow> the (nhop (update ?rt2 ?sip2 (0, unk, val, Suc 0, ?sip2)) dip) = dip)

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
have prreq_ok5 [simp]: "\<And>sip rt.
    \<pi>\<^sub>3(the (update rt sip (0, unk, val, Suc 0, sip) sip)) = unk \<longrightarrow>
    the (dhops (update rt sip (0, unk, val, Suc 0, sip)) sip) = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sip rt. \<pi>\<^sub>3 (the (update rt sip (0, unk, val, Suc 0, sip) sip)) = unk \<longrightarrow> the (dhops (update rt sip (0, unk, val, Suc 0, sip)) sip) = Suc 0
[PROOF STEP]
by (rule update_cases) simp_all
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (update ?rt ?sip (0, unk, val, Suc 0, ?sip) ?sip)) = unk \<longrightarrow> the (dhops (update ?rt ?sip (0, unk, val, Suc 0, ?sip)) ?sip) = Suc 0

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
have prreq_ok6 [simp]: "\<And>sip rt.
    sqn (update rt sip (0, unk, val, Suc 0, sip)) sip = 0 \<longrightarrow>
    \<pi>\<^sub>3 (the (update rt sip (0, unk, val, Suc 0, sip) sip)) = unk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sip rt. sqn (update rt sip (0, unk, val, Suc 0, sip)) sip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update rt sip (0, unk, val, Suc 0, sip) sip)) = unk
[PROOF STEP]
by (rule update_cases) simp_all
[PROOF STATE]
proof (state)
this:
sqn (update ?rt ?sip (0, unk, val, Suc 0, ?sip)) ?sip = 0 \<longrightarrow> \<pi>\<^sub>3 (the (update ?rt ?sip (0, unk, val, Suc 0, ?sip) ?sip)) = unk

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf hop_count_zero_oip_dip_sip']
                            seq_step_invariant_sterms_TT [OF sqns_increase aodv_wf aodv_trans]
                            onl_invariant_sterms [OF aodv_wf osn_rreq']
                            onl_invariant_sterms [OF aodv_wf dsn_rrep']) clarsimp+
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk) \<and> (sqnf (rt \<xi>) dip = unk \<longrightarrow> the (dhops (rt \<xi>) dip) = 1) \<and> (the (dhops (rt \<xi>) dip) = 1 \<longrightarrow> the (nhop (rt \<xi>) dip) = dip))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_seq_unk_hops_one:
  "paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, _).
                 \<forall>dip\<in>kD(rt \<xi>). (sqn (rt \<xi>) dip = 0 \<longrightarrow> (sqnf (rt \<xi>) dip = unk
                                                         \<and> the (dhops (rt \<xi>) dip) = 1
                                                         \<and> the (nhop (rt \<xi>) dip) = dip)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. rreq_rrep_sn m \<and> msg_zhops m) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>dip\<in>kD (rt \<xi>). sqn (rt \<xi>) dip = 0 \<longrightarrow> sqnf (rt \<xi>) dip = unk \<and> the (dhops (rt \<xi>) dip) = 1 \<and> the (nhop (rt \<xi>) dip) = dip)
[PROOF STEP]
by (rule invariant_weakenE [OF zero_seq_unk_hops_one']) auto


[STATEMENT]
lemma kD_unk_or_atleast_one:
  "paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                               \<forall>dip\<in>kD(rt \<xi>). \<pi>\<^sub>3(the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2(the (rt \<xi> dip)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
fix sip rt dsn1 dsn2 dsk1 dsk2 flag1 flag2 hops1 hops2 nhip1 nhip2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
assume "dsk1 = unk \<or> Suc 0 \<le> dsn2"
[PROOF STATE]
proof (state)
this:
dsk1 = unk \<or> Suc 0 \<le> dsn2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
hence "\<pi>\<^sub>3(the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) sip)) = unk
            \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) sip"
[PROOF STATE]
proof (prove)
using this:
dsk1 = unk \<or> Suc 0 \<le> dsn2

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) sip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) sip
[PROOF STEP]
unfolding update_def
[PROOF STATE]
proof (prove)
using this:
dsk1 = unk \<or> Suc 0 \<le> dsn2

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the ((case rt sip of None \<Rightarrow> rt(sip \<mapsto> (dsn1, dsk1, flag1, hops1, nhip1)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn1, dsk1, flag1, hops1, nhip1) then rt(sip \<mapsto> (dsn1, dsk1, flag1, hops1, nhip1)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn1, dsk1, flag1, hops1, nhip1) \<and> (\<pi>\<^sub>5 (dsn1, dsk1, flag1, hops1, nhip1) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(sip \<mapsto> (dsn1, dsk1, flag1, hops1, nhip1)) else if \<pi>\<^sub>3 (dsn1, dsk1, flag1, hops1, nhip1) = unk then rt(sip \<mapsto> (\<pi>\<^sub>2 s, snd (dsn1, dsk1, flag1, hops1, nhip1))) else rt(sip \<mapsto> s)) sip)) = unk \<or> Suc 0 \<le> sqn (case rt sip of None \<Rightarrow> rt(sip \<mapsto> (dsn2, dsk2, flag2, hops2, nhip2)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn2, dsk2, flag2, hops2, nhip2) then rt(sip \<mapsto> (dsn2, dsk2, flag2, hops2, nhip2)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn2, dsk2, flag2, hops2, nhip2) \<and> (\<pi>\<^sub>5 (dsn2, dsk2, flag2, hops2, nhip2) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(sip \<mapsto> (dsn2, dsk2, flag2, hops2, nhip2)) else if \<pi>\<^sub>3 (dsn2, dsk2, flag2, hops2, nhip2) = unk then rt(sip \<mapsto> (\<pi>\<^sub>2 s, snd (dsn2, dsk2, flag2, hops2, nhip2))) else rt(sip \<mapsto> s)) sip
[PROOF STEP]
by (cases "dsk1 =unk") (clarsimp split: option.split)+
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) sip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) sip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?dsk1.2 = unk \<or> Suc 0 \<le> ?dsn2.2 \<Longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (?dsn1.2, ?dsk1.2, ?flag1.2, ?hops1.2, ?nhip1.2) ?sip2)) = unk \<or> Suc 0 \<le> sqn (update ?rt2 ?sip2 (?dsn2.2, ?dsk2.2, ?flag2.2, ?hops2.2, ?nhip2.2)) ?sip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
note fromsip [simp] = this
[PROOF STATE]
proof (state)
this:
?dsk1.2 = unk \<or> Suc 0 \<le> ?dsn2.2 \<Longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (?dsn1.2, ?dsk1.2, ?flag1.2, ?hops1.2, ?nhip1.2) ?sip2)) = unk \<or> Suc 0 \<le> sqn (update ?rt2 ?sip2 (?dsn2.2, ?dsk2.2, ?flag2.2, ?hops2.2, ?nhip2.2)) ?sip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?dsk1.2 = unk \<or> Suc 0 \<le> ?dsn2.2 \<Longrightarrow> \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (?dsn1.2, ?dsk1.2, ?flag1.2, ?hops1.2, ?nhip1.2) ?sip2)) = unk \<or> Suc 0 \<le> sqn (update ?rt2 ?sip2 (?dsn2.2, ?dsk2.2, ?flag2.2, ?hops2.2, ?nhip2.2)) ?sip2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
fix dip sip rt dsn1 dsn2 dsk1 dsk2 flag1 flag2 hops1 hops2 nhip1 nhip2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
assume allkd: "\<forall>dip\<in>kD(rt). \<pi>\<^sub>3(the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip"
         and    **: "dsk1 = unk \<or> Suc 0 \<le> dsn2"
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip
dsk1 = unk \<or> Suc 0 \<le> dsn2

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
have "\<forall>dip\<in>kD(rt). \<pi>\<^sub>3(the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk
            \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip"
        (is "\<forall>dip\<in>kD(rt). ?prop dip")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>dip\<in>kD rt. \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dip. dip \<in> kD rt \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
fix dip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dip. dip \<in> kD rt \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
assume "dip\<in>kD(rt)"
[PROOF STATE]
proof (state)
this:
dip \<in> kD rt

goal (1 subgoal):
 1. \<And>dip. dip \<in> kD rt \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
thus "?prop dip"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
proof (cases "dip = sip")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>dip \<in> kD rt; dip = sip\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
 2. \<lbrakk>dip \<in> kD rt; dip \<noteq> sip\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
assume "dip = sip"
[PROOF STATE]
proof (state)
this:
dip = sip

goal (2 subgoals):
 1. \<lbrakk>dip \<in> kD rt; dip = sip\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
 2. \<lbrakk>dip \<in> kD rt; dip \<noteq> sip\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
with **
[PROOF STATE]
proof (chain)
picking this:
dsk1 = unk \<or> Suc 0 \<le> dsn2
dip = sip
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dsk1 = unk \<or> Suc 0 \<le> dsn2
dip = sip

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dip \<noteq> sip\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dip \<noteq> sip\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
assume "dip \<noteq> sip"
[PROOF STATE]
proof (state)
this:
dip \<noteq> sip

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dip \<noteq> sip\<rbrakk> \<Longrightarrow> \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
with \<open>dip\<in>kD(rt)\<close> allkd
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
\<forall>dip\<in>kD rt. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip
dip \<noteq> sip
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
\<forall>dip\<in>kD rt. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip
dip \<noteq> sip

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. \<pi>\<^sub>3 (the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1) dip)) = unk \<or> Suc 0 \<le> sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2)) dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (?rt2 dip)) = unk \<or> Suc 0 \<le> sqn ?rt2 dip; ?dsk1.2 = unk \<or> Suc 0 \<le> ?dsn2.2\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (?dsn1.2, ?dsk1.2, ?flag1.2, ?hops1.2, ?nhip1.2) dip)) = unk \<or> Suc 0 \<le> sqn (update ?rt2 ?sip2 (?dsn2.2, ?dsk2.2, ?flag2.2, ?hops2.2, ?nhip2.2)) dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
note solve_update [simp] = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (?rt2 dip)) = unk \<or> Suc 0 \<le> sqn ?rt2 dip; ?dsk1.2 = unk \<or> Suc 0 \<le> ?dsn2.2\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (?dsn1.2, ?dsk1.2, ?flag1.2, ?hops1.2, ?nhip1.2) dip)) = unk \<or> Suc 0 \<le> sqn (update ?rt2 ?sip2 (?dsn2.2, ?dsk2.2, ?flag2.2, ?hops2.2, ?nhip2.2)) dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (?rt2 dip)) = unk \<or> Suc 0 \<le> sqn ?rt2 dip; ?dsk1.2 = unk \<or> Suc 0 \<le> ?dsn2.2\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (update ?rt2 ?sip2 (?dsn1.2, ?dsk1.2, ?flag1.2, ?hops1.2, ?nhip1.2) dip)) = unk \<or> Suc 0 \<le> sqn (update ?rt2 ?sip2 (?dsn2.2, ?dsk2.2, ?flag2.2, ?hops2.2, ?nhip2.2)) dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
fix dip rt dests
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
assume  *: "\<forall>ip\<in>dom(dests). ip\<in>kD(rt) \<and> sqn rt ip \<le> the (dests ip)"
         and **: "\<forall>ip\<in>kD(rt). \<pi>\<^sub>3(the (rt ip)) = unk \<or> Suc 0 \<le> sqn rt ip"
[PROOF STATE]
proof (state)
this:
\<forall>ip\<in>dom dests. ip \<in> kD rt \<and> sqn rt ip \<le> the (dests ip)
\<forall>ip\<in>kD rt. \<pi>\<^sub>3 (the (rt ip)) = unk \<or> Suc 0 \<le> sqn rt ip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
have "\<forall>dip\<in>kD(rt). \<pi>\<^sub>3(the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>dip\<in>kD rt. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dip. dip \<in> kD rt \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
fix dip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dip. dip \<in> kD rt \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
assume "dip\<in>kD(rt)"
[PROOF STATE]
proof (state)
this:
dip \<in> kD rt

goal (1 subgoal):
 1. \<And>dip. dip \<in> kD rt \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
with **
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip\<in>kD rt. \<pi>\<^sub>3 (the (rt ip)) = unk \<or> Suc 0 \<le> sqn rt ip
dip \<in> kD rt
[PROOF STEP]
have "\<pi>\<^sub>3(the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip\<in>kD rt. \<pi>\<^sub>3 (the (rt ip)) = unk \<or> Suc 0 \<le> sqn rt ip
dip \<in> kD rt

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip

goal (1 subgoal):
 1. \<And>dip. dip \<in> kD rt \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
thus "\<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip"
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn rt dip

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<pi>\<^sub>3 (the (rt dip)) = unk \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
 2. Suc 0 \<le> sqn rt dip \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
assume "\<pi>\<^sub>3(the (rt dip)) = unk"
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (rt dip)) = unk

goal (2 subgoals):
 1. \<pi>\<^sub>3 (the (rt dip)) = unk \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
 2. Suc 0 \<le> sqn rt dip \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^sub>3 (the (rt dip)) = unk

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip

goal (1 subgoal):
 1. Suc 0 \<le> sqn rt dip \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc 0 \<le> sqn rt dip \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
assume "Suc 0 \<le> sqn rt dip"
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> sqn rt dip

goal (1 subgoal):
 1. Suc 0 \<le> sqn rt dip \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
have "Suc 0 \<le> sqn (invalidate rt dests) dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
proof (cases "dip\<in>dom(dests)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
 2. dip \<notin> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
assume "dip\<in>dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<in> dom dests

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
 2. dip \<notin> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip\<in>dom dests. ip \<in> kD rt \<and> sqn rt ip \<le> the (dests ip)
dip \<in> dom dests
[PROOF STEP]
have "sqn rt dip \<le> the (dests dip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip\<in>dom dests. ip \<in> kD rt \<and> sqn rt ip \<le> the (dests ip)
dip \<in> dom dests

goal (1 subgoal):
 1. sqn rt dip \<le> the (dests dip)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqn rt dip \<le> the (dests dip)

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
 2. dip \<notin> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
with \<open>Suc 0 \<le> sqn rt dip\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc 0 \<le> sqn rt dip
sqn rt dip \<le> the (dests dip)
[PROOF STEP]
have "Suc 0 \<le> the (dests dip)"
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> sqn rt dip
sqn rt dip \<le> the (dests dip)

goal (1 subgoal):
 1. Suc 0 \<le> the (dests dip)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> the (dests dip)

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
 2. dip \<notin> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
with \<open>dip\<in>dom(dests)\<close> \<open>dip\<in>kD(rt)\<close> [THEN kD_Some]
[PROOF STATE]
proof (chain)
picking this:
dip \<in> dom dests
\<exists>dsn dsk flag hops nhip. rt dip = Some (dsn, dsk, flag, hops, nhip)
Suc 0 \<le> the (dests dip)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests
\<exists>dsn dsk flag hops nhip. rt dip = Some (dsn, dsk, flag, hops, nhip)
Suc 0 \<le> the (dests dip)

goal (1 subgoal):
 1. Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
unfolding invalidate_def sqn_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests
\<exists>dsn dsk flag hops nhip. rt dip = Some (dsn, dsk, flag, hops, nhip)
Suc 0 \<le> the (dests dip)

goal (1 subgoal):
 1. Suc 0 \<le> (case case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, bb), None) \<Rightarrow> Some (a, ab, ad, af, bb) | (Some (a, ab, ad, af, bb), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, bb) of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> sqn (invalidate rt dests) dip

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
assume "dip\<notin>dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<notin> dom dests

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
with \<open>Suc 0 \<le> sqn rt dip\<close> \<open>dip\<in>kD(rt)\<close> [THEN kD_Some]
[PROOF STATE]
proof (chain)
picking this:
Suc 0 \<le> sqn rt dip
\<exists>dsn dsk flag hops nhip. rt dip = Some (dsn, dsk, flag, hops, nhip)
dip \<notin> dom dests
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> sqn rt dip
\<exists>dsn dsk flag hops nhip. rt dip = Some (dsn, dsk, flag, hops, nhip)
dip \<notin> dom dests

goal (1 subgoal):
 1. Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
unfolding invalidate_def sqn_def
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> (case rt dip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r)
\<exists>dsn dsk flag hops nhip. rt dip = Some (dsn, dsk, flag, hops, nhip)
dip \<notin> dom dests

goal (1 subgoal):
 1. Suc 0 \<le> (case case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, bb), None) \<Rightarrow> Some (a, ab, ad, af, bb) | (Some (a, ab, ad, af, bb), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, bb) of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> sqn (invalidate rt dests) dip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> sqn (invalidate rt dests) dip

goal (1 subgoal):
 1. Suc 0 \<le> sqn rt dip \<Longrightarrow> \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> sqn (invalidate rt dests) dip

goal (1 subgoal):
 1. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip
[PROOF STEP]
by (rule disjI2)
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD rt. \<pi>\<^sub>3 (the (rt dip)) = unk \<or> Suc 0 \<le> sqn (invalidate rt dests) dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>ip\<in>dom ?dests2. ip \<in> kD ?rt2 \<and> sqn ?rt2 ip \<le> the (?dests2 ip); \<forall>ip\<in>kD ?rt2. \<pi>\<^sub>3 (the (?rt2 ip)) = unk \<or> Suc 0 \<le> sqn ?rt2 ip\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (?rt2 dip)) = unk \<or> Suc 0 \<le> sqn (invalidate ?rt2 ?dests2) dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
note solve_invalidate [simp] = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>ip\<in>dom ?dests2. ip \<in> kD ?rt2 \<and> sqn ?rt2 ip \<le> the (?dests2 ip); \<forall>ip\<in>kD ?rt2. \<pi>\<^sub>3 (the (?rt2 ip)) = unk \<or> Suc 0 \<le> sqn ?rt2 ip\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD ?rt2. \<pi>\<^sub>3 (the (?rt2 dip)) = unk \<or> Suc 0 \<le> sqn (invalidate ?rt2 ?dests2) dip

goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf dests_bigger_than_sqn
                                                               [THEN invariant_restrict_inD]]
                              onl_invariant_sterms [OF aodv_wf osn_rreq]
                              onl_invariant_sterms [OF aodv_wf dsn_rrep]
                    simp add: proj3_inv proj2_eq_sqn)
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> (recvmsg rreq_rrep_sn \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). \<pi>\<^sub>3 (the (rt \<xi> dip)) = unk \<or> 1 \<le> \<pi>\<^sub>2 (the (rt \<xi> dip)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rreq_rrep_sn_any_step_invariant:
  "paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(_, a, _). anycast rreq_rrep_sn a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(uu_, a, uu_). anycast rreq_rrep_sn a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(uu_, a, uu_). anycast rreq_rrep_sn a)
[PROOF STEP]
(* due to lack of addpreRT_welldefined, sqnf_know needed some small adaption [adding dip \<xi> \<in> kD (rt \<xi>)] *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(uu_, a, uu_). anycast rreq_rrep_sn a)
[PROOF STEP]
have sqnf_kno: "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                                      (l \<in> {PRreq-:14} \<longrightarrow> dip \<xi> \<in> kD (rt \<xi>) \<and> sqnf (rt \<xi>) (dip \<xi>) = kno))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PRreq-:14} \<longrightarrow> dip \<xi> \<in> kD (rt \<xi>) \<and> sqnf (rt \<xi>) (dip \<xi>) = kno)
[PROOF STEP]
by (inv_cterms)
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PRreq-:14} \<longrightarrow> dip \<xi> \<in> kD (rt \<xi>) \<and> sqnf (rt \<xi>) (dip \<xi>) = kno)

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(uu_, a, uu_). anycast rreq_rrep_sn a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(uu_, a, uu_). anycast rreq_rrep_sn a)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf sequence_number_one_or_bigger
                                                               [THEN invariant_restrict_inD]]
                              onl_invariant_sterms [OF aodv_wf kD_unk_or_atleast_one]
                              onl_invariant_sterms_TT [OF aodv_wf sqnf_kno]
                              onl_invariant_sterms [OF aodv_wf osn_rreq]
                              onl_invariant_sterms [OF aodv_wf dsn_rrep])
         (auto simp: proj2_eq_sqn)
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(uu_, a, uu_). anycast rreq_rrep_sn a)

goal:
No subgoals!
[PROOF STEP]
qed