[STATEMENT]
lemma in_kD_after_update [simp]:
  fixes rt nip dsn dsk flag hops nhip pre
  shows "kD (update rt nip (dsn, dsk, flag, hops, nhip, pre)) = insert nip (kD rt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kD (update rt nip (dsn, dsk, flag, hops, nhip, pre)) = insert nip (kD rt)
[PROOF STEP]
unfolding update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kD (case rt nip of None \<Rightarrow> rt(nip \<mapsto> (dsn, dsk, flag, hops, nhip, pre)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip, pre) then rt(nip \<mapsto> addpre (dsn, dsk, flag, hops, nhip, pre) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip, pre) \<and> (\<pi>\<^sub>5 (dsn, dsk, flag, hops, nhip, pre) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(nip \<mapsto> addpre (dsn, dsk, flag, hops, nhip, pre) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>3 (dsn, dsk, flag, hops, nhip, pre) = unk then rt(nip \<mapsto> (\<pi>\<^sub>2 s, snd (addpre (dsn, dsk, flag, hops, nhip, pre) (\<pi>\<^sub>7 s)))) else rt(nip \<mapsto> addpre s (\<pi>\<^sub>7 (dsn, dsk, flag, hops, nhip, pre)))) = insert nip (kD rt)
[PROOF STEP]
by (cases "rt nip") auto