[STATEMENT]
lemma nsqn_invalidate_eq:
  assumes "dip \<in> kD(rt)"
      and "dests dip = Some rsn"
    shows "nsqn (invalidate rt dests) dip = rsn - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dests dip = Some rsn
[PROOF STEP]
obtain dsk hops nhip pre
      where "invalidate rt dests dip = Some (rsn, dsk, inv, hops, nhip, pre)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. (\<And>dsk hops nhip pre. invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding invalidate_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. (\<And>dsk hops nhip pre. (case (rt 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 (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
from \<open>dip \<in> kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
[PROOF STEP]
have "dip \<in> kD(invalidate rt dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. dip \<in> kD (invalidate rt dests)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
using \<open>dests dip = Some rsn\<close>
[PROOF STATE]
proof (prove)
using this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)
dests dip = Some rsn

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nsqn (invalidate rt dests) dip = rsn - 1

goal:
No subgoals!
[PROOF STEP]
qed