[STATEMENT]
lemma vD_invalidate_rt_strictly_fresher [simp]:
  assumes "dip \<in> vD(invalidate rt1 dests)"
    shows "(invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
proof (cases "dip \<in> dom(dests)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
 2. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[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> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
 2. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
hence "dip \<notin> vD(invalidate rt1 dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<notin> vD (invalidate rt1 dests)
[PROOF STEP]
unfolding invalidate_def vD_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<notin> {dip. map_option \<pi>\<^sub>4 (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)) = Some val}
[PROOF STEP]
by clarsimp (metis assms option.simps(3) vD_invalidate_vD_not_dests)
[PROOF STATE]
proof (state)
this:
dip \<notin> vD (invalidate rt1 dests)

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
 2. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
with \<open>dip \<in> vD(invalidate rt1 dests)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD (invalidate rt1 dests)
dip \<notin> vD (invalidate rt1 dests)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (invalidate rt1 dests)
dip \<notin> vD (invalidate rt1 dests)

goal (1 subgoal):
 1. (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[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> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
hence "dests dip = None"
[PROOF STATE]
proof (prove)
using this:
dip \<notin> dom dests

goal (1 subgoal):
 1. dests dip = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dests dip = None

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dests dip = None

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
with \<open>dip \<in> vD(invalidate rt1 dests)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD (invalidate rt1 dests)
dests dip = None
[PROOF STEP]
have "dip \<in> vD(rt1)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (invalidate rt1 dests)
dests dip = None

goal (1 subgoal):
 1. dip \<in> vD rt1
[PROOF STEP]
unfolding invalidate_def vD_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> {dip. map_option \<pi>\<^sub>4 (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)) = Some val}
dests dip = None

goal (1 subgoal):
 1. dip \<in> {dip. flag rt1 dip = Some val}
[PROOF STEP]
by clarsimp (metis (opaque_lifting, no_types) assms vD_Some vD_invalidate_vD_not_dests)
[PROOF STATE]
proof (state)
this:
dip \<in> vD rt1

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dests dip = None
dip \<in> vD rt1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dests dip = None
dip \<in> vD rt1

goal (1 subgoal):
 1. (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
unfolding invalidate_def rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
using this:
dests dip = None
dip \<in> vD rt1

goal (1 subgoal):
 1. (nsqn\<^sub>r (the (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))) < nsqn\<^sub>r (the (rt2 dip)) \<or> nsqn\<^sub>r (the (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))) = nsqn\<^sub>r (the (rt2 dip)) \<and> \<pi>\<^sub>5 (the (rt2 dip)) < \<pi>\<^sub>5 (the (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)))) = (nsqn\<^sub>r (the (rt1 dip)) < nsqn\<^sub>r (the (rt2 dip)) \<or> nsqn\<^sub>r (the (rt1 dip)) = nsqn\<^sub>r (the (rt2 dip)) \<and> \<pi>\<^sub>5 (the (rt2 dip)) < \<pi>\<^sub>5 (the (rt1 dip)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)

goal:
No subgoals!
[PROOF STEP]
qed