[STATEMENT]
lemma init_mapstate_Some_aodv_init [elim]:
  assumes "s \<in> init (pnet np p)"
      and "netmap s i = Some v"
    shows "v \<in> init (np i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np p)
netmap s i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
proof (induction p arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
fix ii R s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume "s \<in> init (pnet np \<langle>ii; R\<rangle>)"
       and "netmap s i = Some v"
[PROOF STATE]
proof (state)
this:
s \<in> init (pnet np \<langle>ii; R\<rangle>)
netmap s i = Some v

goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
s \<in> init (pnet np \<langle>ii; R\<rangle>)
[PROOF STEP]
obtain ns where s: "s = NodeS ii ns R"
      and ns: "ns \<in> init (np ii)"
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np \<langle>ii; R\<rangle>)

goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>s = NodeS ii ns R; ns \<in> init (np ii)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s = NodeS ii ns R
ns \<in> init (np ii)

goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from s and \<open>netmap s i = Some v\<close>
[PROOF STATE]
proof (chain)
picking this:
s = NodeS ii ns R
netmap s i = Some v
[PROOF STEP]
have "i = ii"
[PROOF STATE]
proof (prove)
using this:
s = NodeS ii ns R
netmap s i = Some v

goal (1 subgoal):
 1. i = ii
[PROOF STEP]
by simp (metis domI domIff)
[PROOF STATE]
proof (state)
this:
i = ii

goal (2 subgoals):
 1. \<And>ia R s. \<lbrakk>s \<in> init (pnet np \<langle>ia; R\<rangle>); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
 2. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
with s ns
[PROOF STATE]
proof (chain)
picking this:
s = NodeS ii ns R
ns \<in> init (np ii)
i = ii
[PROOF STEP]
show "v \<in> init (np i)"
[PROOF STATE]
proof (prove)
using this:
s = NodeS ii ns R
ns \<in> init (np ii)
i = ii

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
using \<open>netmap s i = Some v\<close>
[PROOF STATE]
proof (prove)
using this:
s = NodeS ii ns R
ns \<in> init (np ii)
i = ii
netmap s i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
fix p1 p2 s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume IH1: "\<And>s. s \<in> init (pnet np p1) \<Longrightarrow> netmap s i = Some v \<Longrightarrow> v \<in> init (np i)"
       and IH2: "\<And>s. s \<in> init (pnet np p2) \<Longrightarrow> netmap s i = Some v \<Longrightarrow> v \<in> init (np i)"
       and "s \<in> init (pnet np (p1 \<parallel> p2))"
       and "netmap s i = Some v"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s \<in> init (pnet np p1); netmap ?s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
\<lbrakk>?s \<in> init (pnet np p2); netmap ?s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
s \<in> init (pnet np (p1 \<parallel> p2))
netmap s i = Some v

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from this(3)
[PROOF STATE]
proof (chain)
picking this:
s \<in> init (pnet np (p1 \<parallel> p2))
[PROOF STEP]
obtain s1 s2 where "s = SubnetS s1 s2"
                                and "s1 \<in> init (pnet np p1)"
                                and "s2 \<in> init (pnet np p2)"
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np (p1 \<parallel> p2))

goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>s = SubnetS s1 s2; s1 \<in> init (pnet np p1); s2 \<in> init (pnet np p2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = SubnetS s1 s2
s1 \<in> init (pnet np p1)
s2 \<in> init (pnet np p2)

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
from this(1) and \<open>netmap s i = Some v\<close>
[PROOF STATE]
proof (chain)
picking this:
s = SubnetS s1 s2
netmap s i = Some v
[PROOF STEP]
have "netmap s1 i = Some v \<or> netmap s2 i = Some v"
[PROOF STATE]
proof (prove)
using this:
s = SubnetS s1 s2
netmap s i = Some v

goal (1 subgoal):
 1. netmap s1 i = Some v \<or> netmap s2 i = Some v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
netmap s1 i = Some v \<or> netmap s2 i = Some v

goal (1 subgoal):
 1. \<And>p1 p2 s. \<lbrakk>\<And>s. \<lbrakk>s \<in> init (pnet np p1); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); \<And>s. \<lbrakk>s \<in> init (pnet np p2); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i); s \<in> init (pnet np (p1 \<parallel> p2)); netmap s i = Some v\<rbrakk> \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
thus "v \<in> init (np i)"
[PROOF STATE]
proof (prove)
using this:
netmap s1 i = Some v \<or> netmap s2 i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. netmap s1 i = Some v \<Longrightarrow> v \<in> init (np i)
 2. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume "netmap s1 i = Some v"
[PROOF STATE]
proof (state)
this:
netmap s1 i = Some v

goal (2 subgoals):
 1. netmap s1 i = Some v \<Longrightarrow> v \<in> init (np i)
 2. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
with \<open>s1 \<in> init (pnet np p1)\<close>
[PROOF STATE]
proof (chain)
picking this:
s1 \<in> init (pnet np p1)
netmap s1 i = Some v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 \<in> init (pnet np p1)
netmap s1 i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
by (rule IH1)
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal (1 subgoal):
 1. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
assume "netmap s2 i = Some v"
[PROOF STATE]
proof (state)
this:
netmap s2 i = Some v

goal (1 subgoal):
 1. netmap s2 i = Some v \<Longrightarrow> v \<in> init (np i)
[PROOF STEP]
with \<open>s2 \<in> init (pnet np p2)\<close>
[PROOF STATE]
proof (chain)
picking this:
s2 \<in> init (pnet np p2)
netmap s2 i = Some v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s2 \<in> init (pnet np p2)
netmap s2 i = Some v

goal (1 subgoal):
 1. v \<in> init (np i)
[PROOF STEP]
by (rule IH2)
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<in> init (np i)

goal:
No subgoals!
[PROOF STEP]
qed