[STATEMENT]
lemma rreq_rrep_fresh_any_step_invariant:
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), a, _). anycast (rreq_rrep_fresh (rt \<xi>)) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rreq_rrep_fresh (rt \<xi>)) a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rreq_rrep_fresh (rt \<xi>)) a)
[PROOF STEP]
have rreq_oip: "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
                       (l \<in> {PRreq-:3, PRreq-:4, PRreq-:13, PRreq-:21}
                               \<longrightarrow> oip \<xi> \<in> kD(rt \<xi>)
                                 \<and> (sqn (rt \<xi>) (oip \<xi>) > (osn \<xi>)
                                     \<or> (sqn (rt \<xi>) (oip \<xi>) = (osn \<xi>)
                                        \<and> the (dhops (rt \<xi>) (oip \<xi>)) \<le> Suc (hops \<xi>)
                                        \<and> the (flag (rt \<xi>) (oip \<xi>)) = val))))"
[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-:3, PRreq-:4, PRreq-:13, PRreq-:21} \<longrightarrow> oip \<xi> \<in> kD (rt \<xi>) \<and> (osn \<xi> < sqn (rt \<xi>) (oip \<xi>) \<or> sqn (rt \<xi>) (oip \<xi>) = osn \<xi> \<and> the (dhops (rt \<xi>) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (rt \<xi>) (oip \<xi>)) = val))
[PROOF STEP]
proof inv_cterms
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRreq-:2; ((\<xi>, {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:3 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) TT; p = {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRreq-:3; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> osn \<xi> < sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) \<or> sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) = osn \<xi> \<and> the (dhops (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) = val
[PROOF STEP]
fix l \<xi> l' pp p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRreq-:2; ((\<xi>, {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:3 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) TT; p = {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRreq-:3; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> osn \<xi> < sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) \<or> sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) = osn \<xi> \<and> the (dhops (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) = val
[PROOF STEP]
assume "(\<xi>, pp) \<in> reachable (paodv i) TT"
           and "{PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt :=
                update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk> p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp"
           and "l' = PRreq-:3"
[PROOF STATE]
proof (state)
this:
(\<xi>, pp) \<in> reachable (paodv i) TT
{PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp
l' = PRreq-:3

goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRreq-:2; ((\<xi>, {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:3 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) TT; {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) TT; p = {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRreq-:3; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> osn \<xi> < sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) \<or> sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) = osn \<xi> \<and> the (dhops (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) = val
[PROOF STEP]
show "osn \<xi> < sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)
           \<or> (sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) = osn \<xi>
             \<and> the (dhops (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>))
                                                                            \<le> Suc (hops \<xi>)
             \<and> the (flag (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>))
                                                                            = val)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. osn \<xi> < sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) \<or> sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) = osn \<xi> \<and> the (dhops (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) = val
[PROOF STEP]
unfolding update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. osn \<xi> < sqn (case rt \<xi> (oip \<xi>) of None \<Rightarrow> rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) \<and> (\<pi>\<^sub>5 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>3 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) = unk then rt \<xi>(oip \<xi> \<mapsto> (\<pi>\<^sub>2 s, snd (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>))) else rt \<xi>(oip \<xi> \<mapsto> s)) (oip \<xi>) \<or> sqn (case rt \<xi> (oip \<xi>) of None \<Rightarrow> rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) \<and> (\<pi>\<^sub>5 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>3 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) = unk then rt \<xi>(oip \<xi> \<mapsto> (\<pi>\<^sub>2 s, snd (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>))) else rt \<xi>(oip \<xi> \<mapsto> s)) (oip \<xi>) = osn \<xi> \<and> the (dhops (case rt \<xi> (oip \<xi>) of None \<Rightarrow> rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) \<and> (\<pi>\<^sub>5 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>3 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) = unk then rt \<xi>(oip \<xi> \<mapsto> (\<pi>\<^sub>2 s, snd (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>))) else rt \<xi>(oip \<xi> \<mapsto> s)) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (case rt \<xi> (oip \<xi>) of None \<Rightarrow> rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) \<and> (\<pi>\<^sub>5 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt \<xi>(oip \<xi> \<mapsto> (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) else if \<pi>\<^sub>3 (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>) = unk then rt \<xi>(oip \<xi> \<mapsto> (\<pi>\<^sub>2 s, snd (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>))) else rt \<xi>(oip \<xi> \<mapsto> s)) (oip \<xi>)) = val
[PROOF STEP]
by (clarsimp split: option.split)
                                  (metis linorder_neqE_nat not_less)
[PROOF STATE]
proof (state)
this:
osn \<xi> < sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) \<or> sqn (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>) = osn \<xi> \<and> the (dhops (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)) (oip \<xi>)) = val

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PRreq-:3, PRreq-:4, PRreq-:13, PRreq-:21} \<longrightarrow> oip \<xi> \<in> kD (rt \<xi>) \<and> (osn \<xi> < sqn (rt \<xi>) (oip \<xi>) \<or> sqn (rt \<xi>) (oip \<xi>) = osn \<xi> \<and> the (dhops (rt \<xi>) (oip \<xi>)) \<le> Suc (hops \<xi>) \<and> the (flag (rt \<xi>) (oip \<xi>)) = val))

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rreq_rrep_fresh (rt \<xi>)) a)
[PROOF STEP]
have rrep_prrep: "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l).
          (l \<in> {PRrep-:2..PRrep-:5} \<longrightarrow> (dip \<xi> \<in> kD(rt \<xi>)
                                        \<and> sqn (rt \<xi>) (dip \<xi>) = dsn \<xi>
                                        \<and> the (dhops (rt \<xi>) (dip \<xi>)) = Suc (hops \<xi>)
                                        \<and> the (flag (rt \<xi>) (dip \<xi>)) = val
                                        \<and> the (nhop (rt \<xi>) (dip \<xi>)) \<in> kD (rt \<xi>))))"
[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> {PRrep-:2..PRrep-:5} \<longrightarrow> dip \<xi> \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) (dip \<xi>) = dsn \<xi> \<and> the (dhops (rt \<xi>) (dip \<xi>)) = Suc (hops \<xi>) \<and> the (flag (rt \<xi>) (dip \<xi>)) = val \<and> the (nhop (rt \<xi>) (dip \<xi>)) \<in> kD (rt \<xi>))
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rrep_1_update_changes]
                              onl_invariant_sterms [OF aodv_wf sip_in_kD])
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PRrep-:2..PRrep-:5} \<longrightarrow> dip \<xi> \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) (dip \<xi>) = dsn \<xi> \<and> the (dhops (rt \<xi>) (dip \<xi>)) = Suc (hops \<xi>) \<and> the (flag (rt \<xi>) (dip \<xi>)) = val \<and> the (nhop (rt \<xi>) (dip \<xi>)) \<in> kD (rt \<xi>))

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rreq_rrep_fresh (rt \<xi>)) a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rreq_rrep_fresh (rt \<xi>)) a)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rreq_oip]
                              onl_invariant_sterms [OF aodv_wf rreq_dip_in_vD_dip_eq_ip]
                              onl_invariant_sterms [OF aodv_wf rrep_prrep])
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rreq_rrep_fresh (rt \<xi>)) a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rerr_invalid_any_step_invariant:
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), a, _). anycast (rerr_invalid (rt \<xi>)) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rerr_invalid (rt \<xi>)) a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rerr_invalid (rt \<xi>)) a)
[PROOF STEP]
have dests_inv: "paodv i \<TTurnstile>
                      onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:15, PPkt-:7, PRreq-:9,
                                            PRreq-:17, PRrep-:8, PRerr-:1}
                          \<longrightarrow> (\<forall>ip\<in>dom(dests \<xi>). ip\<in>vD(rt \<xi>)))
                         \<and> (l \<in> {PAodv-:16..PAodv-:17}
                              \<union> {PPkt-:8..PPkt-:9}
                              \<union> {PRreq-:10..PRreq-:11}
                              \<union> {PRreq-:18..PRreq-:19}
                              \<union> {PRrep-:9..PRrep-:10}
                              \<union> {PRerr-:2..PRerr-:4} \<longrightarrow> (\<forall>ip\<in>dom(dests \<xi>). ip\<in>iD(rt \<xi>)
                                                          \<and> the (dests \<xi> ip) = sqn (rt \<xi>) ip))
                         \<and> (l = PPkt-:12 \<longrightarrow> dip \<xi>\<in>iD(rt \<xi>)))"
[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> {PAodv-:15, PPkt-:7, PRreq-:9, PRreq-:17, PRrep-:8, PRerr-:1} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> vD (rt \<xi>))) \<and> (l \<in> {PAodv-:16..PAodv-:17} \<union> {PPkt-:8..PPkt-:9} \<union> {PRreq-:10..PRreq-:11} \<union> {PRreq-:18..PRreq-:19} \<union> {PRrep-:9..PRrep-:10} \<union> {PRerr-:2..PRerr-:4} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> iD (rt \<xi>) \<and> the (dests \<xi> ip) = sqn (rt \<xi>) ip)) \<and> (l = PPkt-:12 \<longrightarrow> dip \<xi> \<in> iD (rt \<xi>)))
[PROOF STEP]
by inv_cterms (clarsimp split: if_split_asm option.split_asm simp: domIff)+
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:15, PPkt-:7, PRreq-:9, PRreq-:17, PRrep-:8, PRerr-:1} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> vD (rt \<xi>))) \<and> (l \<in> {PAodv-:16..PAodv-:17} \<union> {PPkt-:8..PPkt-:9} \<union> {PRreq-:10..PRreq-:11} \<union> {PRreq-:18..PRreq-:19} \<union> {PRrep-:9..PRrep-:10} \<union> {PRerr-:2..PRerr-:4} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> iD (rt \<xi>) \<and> the (dests \<xi> ip) = sqn (rt \<xi>) ip)) \<and> (l = PPkt-:12 \<longrightarrow> dip \<xi> \<in> iD (rt \<xi>)))

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rerr_invalid (rt \<xi>)) a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rerr_invalid (rt \<xi>)) a)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf dests_inv])
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (rerr_invalid (rt \<xi>)) a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dests_vD_inc_sqn:
  "paodv i \<TTurnstile>
        onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PAodv-:15, PPkt-:7, PRreq-:9, PRreq-:17, PRrep-:8}
             \<longrightarrow> (\<forall>ip\<in>dom(dests \<xi>). ip\<in>vD(rt \<xi>) \<and> the (dests \<xi> ip) = inc (sqn (rt \<xi>) ip)))
           \<and> (l = PRerr-:1
             \<longrightarrow> (\<forall>ip\<in>dom(dests \<xi>). ip\<in>vD(rt \<xi>) \<and> the (dests \<xi> ip) > sqn (rt \<xi>) ip)))"
[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> {PAodv-:15, PPkt-:7, PRreq-:9, PRreq-:17, PRrep-:8} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> vD (rt \<xi>) \<and> the (dests \<xi> ip) = inc (sqn (rt \<xi>) ip))) \<and> (l = PRerr-:1 \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> vD (rt \<xi>) \<and> sqn (rt \<xi>) ip < the (dests \<xi> ip))))
[PROOF STEP]
by inv_cterms (clarsimp split: if_split_asm option.split_asm)+


[STATEMENT]
lemma route_tables_fresher:
  "paodv i \<TTurnstile>\<^sub>A (recvmsg rreq_rrep_sn \<rightarrow>) onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), _, (\<xi>', _)).
                                                                \<forall>dip\<in>kD(rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>')"
[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>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>dip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>')
[PROOF STEP]
proof (inv_cterms inv add:
           onl_invariant_sterms [OF aodv_wf dests_vD_inc_sqn [THEN invariant_restrict_inD]]
           onl_invariant_sterms [OF aodv_wf hop_count_positive [THEN invariant_restrict_inD]]
           onl_invariant_sterms [OF aodv_wf osn_rreq]
           onl_invariant_sterms [OF aodv_wf dsn_rrep]
           onl_invariant_sterms [OF aodv_wf invariant_restrict_inD])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRreq-:2; ((\<xi>, {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:3 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> osn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRreq-:3; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
 2. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRrep-:1; ((\<xi>, {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRrep-:2 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> dsn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRrep-:2; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dipa\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dipa\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
fix \<xi> pp p'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRreq-:2; ((\<xi>, {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:3 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> osn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRreq-:3; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
 2. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRrep-:1; ((\<xi>, {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRrep-:2 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> dsn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRrep-:2; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dipa\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dipa\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
assume "(\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn)"
       and "{PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
               p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp"
       and "Suc 0 \<le> osn \<xi>"
       and *: "\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)"
[PROOF STATE]
proof (state)
this:
(\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn)
{PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp
Suc 0 \<le> osn \<xi>
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)

goal (2 subgoals):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRreq-:2; ((\<xi>, {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRreq-:3 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> osn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRreq-:2}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRreq-:3; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
 2. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRrep-:1; ((\<xi>, {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRrep-:2 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> dsn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRrep-:2; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dipa\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dipa\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
show "\<forall>ip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
fix ip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
assume "ip\<in>kD (rt \<xi>)"
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)
ip \<in> kD (rt \<xi>)
[PROOF STEP]
have "1 \<le> the (dhops (rt \<xi>) ip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)
ip \<in> kD (rt \<xi>)

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

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> the (dhops (rt \<xi>) ip)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
from \<open>Suc 0 \<le> osn \<xi>\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc 0 \<le> osn \<xi>
[PROOF STEP]
have "update_arg_wf (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)"
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> osn \<xi>

goal (1 subgoal):
 1. update_arg_wf (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
update_arg_wf (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt \<xi>)
1 \<le> the (dhops (rt \<xi>) ip)
update_arg_wf (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
show "rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt \<xi>)
1 \<le> the (dhops (rt \<xi>) ip)
update_arg_wf (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal (1 subgoal):
 1. rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
by (rule rt_fresher_update)
[PROOF STATE]
proof (state)
this:
rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>ip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (oip \<xi>) (osn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRrep-:1; ((\<xi>, {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRrep-:2 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> dsn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRrep-:2; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dipa\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dipa\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRrep-:1; ((\<xi>, {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRrep-:2 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> dsn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRrep-:2; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dipa\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dipa\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
fix \<xi> pp p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRrep-:1; ((\<xi>, {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRrep-:2 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> dsn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRrep-:2; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dipa\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dipa\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
assume "(\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn)"
       and "{PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
            p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp"
       and "Suc 0 \<le> dsn \<xi>"
       and *: "\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)"
[PROOF STATE]
proof (state)
this:
(\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn)
{PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp
Suc 0 \<le> dsn \<xi>
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)

goal (1 subgoal):
 1. \<And>p l \<xi> a q l' \<xi>' pp p'. \<lbrakk>l = PRrep-:1; ((\<xi>, {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'), \<tau>\<^sub>s, \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V; PRrep-:2 \<in> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p'; (\<xi>, pp) \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p' \<in> sterms \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V pp; (\<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>, p') \<in> reachable (paodv i) (recvmsg rreq_rrep_sn); Suc 0 \<le> dsn \<xi>; \<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip); p = {PRrep-:1}\<lbrakk>\<lambda>\<xi>. \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>\<rbrakk>
p'; l' = PRrep-:2; a = \<tau>\<^sub>s; \<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)\<rparr>; q = p'\<rbrakk> \<Longrightarrow> \<forall>dipa\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>dipa\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
show "\<forall>ip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
fix ip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
assume "ip\<in>kD (rt \<xi>)"
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ip \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)
ip \<in> kD (rt \<xi>)
[PROOF STEP]
have "1 \<le> the (dhops (rt \<xi>) ip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip\<in>kD (rt \<xi>). Suc 0 \<le> the (dhops (rt \<xi>) ip)
ip \<in> kD (rt \<xi>)

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

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> the (dhops (rt \<xi>) ip)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
from \<open>Suc 0 \<le> dsn \<xi>\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc 0 \<le> dsn \<xi>
[PROOF STEP]
have "update_arg_wf (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)"
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> dsn \<xi>

goal (1 subgoal):
 1. update_arg_wf (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
update_arg_wf (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal (1 subgoal):
 1. \<And>ip. ip \<in> kD (rt \<xi>) \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ip \<in> kD (rt \<xi>)
1 \<le> the (dhops (rt \<xi>) ip)
update_arg_wf (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
show "rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)"
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD (rt \<xi>)
1 \<le> the (dhops (rt \<xi>) ip)
update_arg_wf (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal (1 subgoal):
 1. rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)
[PROOF STEP]
by (rule rt_fresher_update)
[PROOF STATE]
proof (state)
this:
rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>ip\<in>kD (rt \<xi>). rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, Suc (hops \<xi>), sip \<xi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma genPolyTame_spec:
 "generatePolygonTame n v f g = [g' \<leftarrow> generatePolygon n v f g . \<not> notame g']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. generatePolygonTame n v f g = filter (\<lambda>g'. \<not> notame g') (generatePolygon n v f g)
[PROOF STEP]
by(simp add:generatePolygonTame_def generatePolygon_def enum_enumerator)


[STATEMENT]
lemma genPolyTame_subset_genPoly:
 "g' \<in> set(generatePolygonTame i v f g) \<Longrightarrow>
  g' \<in> set(generatePolygon i v f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' \<in> set (generatePolygonTame i v f g) \<Longrightarrow> g' \<in> set (generatePolygon i v f g)
[PROOF STEP]
by(auto simp add:generatePolygon_def generatePolygonTame_def enum_enumerator)


[STATEMENT]
lemma next_tame0_subset_plane:
 "set(next_tame0 p g) \<subseteq> set(next_plane p g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (next_tame0\<^bsub>p\<^esub> g) \<subseteq> set (next_plane\<^bsub>p\<^esub> g)
[PROOF STEP]
by(auto simp add:next_tame0_def next_plane_def polysizes_def
           elim!:genPolyTame_subset_genPoly simp del:upt_Suc)


[STATEMENT]
lemma genPoly_new_face:
 "\<lbrakk>g' \<in> set (generatePolygon n v f g); minGraphProps g; f \<in> set (nonFinals g);
   v \<in> \<V> f; n \<ge> 3 \<rbrakk> \<Longrightarrow>
  \<exists>f \<in> set(finals g') - set(finals g). |vertices f| = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (generatePolygon n v f g); minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals g') - set (finals g). |vertices f| = n
[PROOF STEP]
apply(auto simp add:generatePolygon_def image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; x \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v x; g' = subdivFace g f (indexToVertexList f v x)\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v x))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(rename_tac "is")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is)\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(frule enumerator_length2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is)\<rbrakk> \<Longrightarrow> 2 < n
 2. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(frule (4) pre_subdivFace_indexToVertexList)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n\<rbrakk> \<Longrightarrow> 2 < n
 2. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is)\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(arith)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is)\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(subgoal_tac "indexToVertexList f v is \<noteq> []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is); indexToVertexList f v is \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
 2. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is)\<rbrakk> \<Longrightarrow> indexToVertexList f v is \<noteq> []
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is)\<rbrakk> \<Longrightarrow> indexToVertexList f v is \<noteq> []
 2. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is); indexToVertexList f v is \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(subst length_0_conv[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is)\<rbrakk> \<Longrightarrow> |indexToVertexList f v is| \<noteq> 0
 2. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is); indexToVertexList f v is \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace g f (indexToVertexList f v is); |is| = n; pre_subdivFace g f v (indexToVertexList f v is); indexToVertexList f v is \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace g f (indexToVertexList f v is))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(simp add: subdivFace_subdivFace'_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; is \<in> set (enumerator n |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 (tl (indexToVertexList f v is)); |is| = n; pre_subdivFace g f v (indexToVertexList f v is); indexToVertexList f v is \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 (tl (indexToVertexList f v is)))) - set (finals g). |vertices f| = n
[PROOF STEP]
apply(clarsimp simp:neq_Nil_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is y ys. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ys; pre_subdivFace g f v (y # ys); n = |is|; indexToVertexList f v is = y # ys\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ys)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(rename_tac "ovs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is y ovs. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(subgoal_tac "|indexToVertexList f v is| = |ovs| + 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is y ovs. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
 2. \<And>is y ovs. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs\<rbrakk> \<Longrightarrow> |indexToVertexList f v is| = |ovs| + 1
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is y ovs. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs\<rbrakk> \<Longrightarrow> |indexToVertexList f v is| = |ovs| + 1
 2. \<And>is y ovs. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is y ovs. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(drule (1) pre_subdivFace_pre_subdivFace')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is y ovs. \<lbrakk>minGraphProps g; f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1; pre_subdivFace' g f v v 0 ovs\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(drule (1) final_subdivFace')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1; pre_subdivFace' g f v v 0 ovs\<rbrakk> \<Longrightarrow> f \<in> \<F> g
 2. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1; pre_subdivFace' g f v v 0 ovs\<rbrakk> \<Longrightarrow> ovs = [] \<longrightarrow> 0 = 0 \<and> v = last (verticesFrom f v)
 3. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1; pre_subdivFace' g f v v 0 ovs; \<exists>f'\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). (f\<^bsup>-1\<^esup> \<bullet> v, v) \<in> \<E> f' \<and> |vertices f'| = 0 + |ovs| + (if v = v then 1 else |between (vertices f) v v| + 2)\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(simp add:nonFinals_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1; pre_subdivFace' g f v v 0 ovs\<rbrakk> \<Longrightarrow> ovs = [] \<longrightarrow> 0 = 0 \<and> v = last (verticesFrom f v)
 2. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1; pre_subdivFace' g f v v 0 ovs; \<exists>f'\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). (f\<^bsup>-1\<^esup> \<bullet> v, v) \<in> \<E> f' \<and> |vertices f'| = 0 + |ovs| + (if v = v then 1 else |between (vertices f) v v| + 2)\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(simp add:pre_subdivFace'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |indexToVertexList f v is| = |ovs| + 1; pre_subdivFace' g f v v 0 ovs; \<exists>f'\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). (f\<^bsup>-1\<^esup> \<bullet> v, v) \<in> \<E> f' \<and> |vertices f'| = 0 + |ovs| + (if v = v then 1 else |between (vertices f) v v| + 2)\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply (simp (no_asm_use))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 3 \<le> |is|; is \<in> set (enumerator |is| |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = |is|; indexToVertexList f v is = y # ovs; |is| = Suc |ovs|; pre_subdivFace' g f v v 0 ovs; \<exists>f'\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). (f\<^bsup>-1\<^esup> \<bullet> v, v) \<in> \<E> f' \<and> |vertices f'| = Suc |ovs|\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = |is|
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is y ovs. \<lbrakk>f \<in> set (nonFinals g); 2 \<le> |ovs|; is \<in> set (enumerator (Suc |ovs|) |vertices f|); \<not> containsDuplicateEdge g f v is; g' = subdivFace' g f v 0 ovs; pre_subdivFace g f v (y # ovs); n = Suc |ovs|; indexToVertexList f v is = y # ovs; |is| = Suc |ovs|; pre_subdivFace' g f v v 0 ovs; \<exists>f'\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). (f\<^bsup>-1\<^esup> \<bullet> v, v) \<in> \<E> f' \<and> |vertices f'| = Suc |ovs|\<rbrakk> \<Longrightarrow> \<exists>f\<in>set (finals (subdivFace' g f v 0 ovs)) - set (finals g). |vertices f| = Suc |ovs|
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma genPoly_incr_facesquander_lb:
assumes "g' \<in> set (generatePolygon n v f g)" "inv g"
        "f \<in> set(nonFinals g)" "v \<in> \<V> f" "3 \<le> n"
shows "faceSquanderLowerBound g' \<ge> faceSquanderLowerBound g + \<d> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
from genPoly_new_face[OF assms(1) inv_mgp[OF assms(2)] assms(3-5)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f\<in>set (finals g') - set (finals g). |vertices f| = n
[PROOF STEP]
obtain f
    where f: "f \<in> set (finals g') - set(finals g)"
    and size: "|vertices f| = n"
[PROOF STATE]
proof (prove)
using this:
\<exists>f\<in>set (finals g') - set (finals g). |vertices f| = n

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> set (finals g') - set (finals g); |vertices f| = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> set (finals g') - set (finals g)
|vertices f| = n

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
have g': "g' \<in> set(next_plane0 (n - 3) g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' \<in> set (next_plane0\<^bsub>n - 3\<^esub> g)
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
3 \<le> n

goal (1 subgoal):
 1. g' \<in> set (next_plane0\<^bsub>n - 3\<^esub> g)
[PROOF STEP]
by(rule_tac in_next_plane0I[OF assms(1,3-5)]) simp
[PROOF STATE]
proof (state)
this:
g' \<in> set (next_plane0\<^bsub>n - 3\<^esub> g)

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
note dist = minGraphProps11'[OF inv_mgp[OF assms(2)]]
[PROOF STATE]
proof (state)
this:
distinct (faces g)

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
note inv' = invariantE[OF inv_inv_next_plane0, OF g' assms(2)]
[PROOF STATE]
proof (state)
this:
Invariants.inv g'

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
note dist' = minGraphProps11'[OF inv_mgp[OF inv']]
[PROOF STATE]
proof (state)
this:
distinct (faces g')

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
note subset = next_plane0_finals_subset[OF g']
[PROOF STATE]
proof (state)
this:
set (finals g) \<subseteq> set (finals g')

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
have "faceSquanderLowerBound g' \<ge>
        faceSquanderLowerBound g + \<d> |vertices f|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> |vertices f| \<le> faceSquanderLowerBound g'
[PROOF STEP]
proof(unfold faceSquanderLowerBound_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
have "(\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f| ) + \<d> |vertices f| =
          (\<Sum>f\<in>set(finals g). \<d> |vertices f| ) + \<d> |vertices f|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f|
[PROOF STEP]
using dist
[PROOF STATE]
proof (prove)
using this:
distinct (faces g)

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f|
[PROOF STEP]
by(simp add:finals_def ListSum_conv_sum)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f|

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f|

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
have "\<dots> = (\<Sum>f\<in>set(finals g) \<union> {f}. \<d> |vertices f| )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|)
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f \<in> set (finals g') - set (finals g)

goal (1 subgoal):
 1. (\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|)

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>f\<in>set (finals g). \<d> |vertices f|) + \<d> |vertices f| = (\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|)

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
have "\<dots> \<le> (\<Sum>f\<in>set(finals g'). \<d> |vertices f| )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|) \<le> (\<Sum>f\<in>set (finals g'). \<d> |vertices f|)
[PROOF STEP]
using f subset
[PROOF STATE]
proof (prove)
using this:
f \<in> set (finals g') - set (finals g)
set (finals g) \<subseteq> set (finals g')

goal (1 subgoal):
 1. (\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|) \<le> (\<Sum>f\<in>set (finals g'). \<d> |vertices f|)
[PROOF STEP]
by(fastforce intro!: sum_mono2)
[PROOF STATE]
proof (state)
this:
(\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|) \<le> (\<Sum>f\<in>set (finals g'). \<d> |vertices f|)

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>f\<in>set (finals g) \<union> {f}. \<d> |vertices f|) \<le> (\<Sum>f\<in>set (finals g'). \<d> |vertices f|)

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
have "\<dots> = (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f| )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>f\<in>set (finals g'). \<d> |vertices f|) = (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
using dist'
[PROOF STATE]
proof (prove)
using this:
distinct (faces g')

goal (1 subgoal):
 1. (\<Sum>f\<in>set (finals g'). \<d> |vertices f|) = (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
by(simp add:finals_def ListSum_conv_sum)
[PROOF STATE]
proof (state)
this:
(\<Sum>f\<in>set (finals g'). \<d> |vertices f|) = (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
show "(\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f| ) + \<d> |vertices f|
          \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f| )"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)

goal (1 subgoal):
 1. (\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^bsub>f\<in>finals g\<^esub> \<d> |vertices f|) + \<d> |vertices f| \<le> (\<Sum>\<^bsub>f\<in>finals g'\<^esub> \<d> |vertices f|)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
faceSquanderLowerBound g + \<d> |vertices f| \<le> faceSquanderLowerBound g'

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
with size
[PROOF STATE]
proof (chain)
picking this:
|vertices f| = n
faceSquanderLowerBound g + \<d> |vertices f| \<le> faceSquanderLowerBound g'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
|vertices f| = n
faceSquanderLowerBound g + \<d> |vertices f| \<le> faceSquanderLowerBound g'

goal (1 subgoal):
 1. faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delAround_def: "deleteAround g u ps = [p \<leftarrow> ps. \<not> close g u (fst p)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deleteAround g u ps = filter (\<lambda>p. \<not> close g u (fst p)) ps
[PROOF STEP]
by (induct ps) (auto simp: deleteAroundCons close_def)


[STATEMENT]
lemma close_sym: assumes mgp: "minGraphProps g" and ug: "u : \<V> g" and cl: "close g u v"
shows "close g v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. close g v u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. close g v u
[PROOF STEP]
obtain f where f: "f \<in> set(facesAt g u)" and
    "if": "if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> set (facesAt g u); if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cl
[PROOF STATE]
proof (prove)
using this:
close g u v

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> set (facesAt g u); if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (unfold close_def) blast
[PROOF STATE]
proof (state)
this:
f \<in> set (facesAt g u)
if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
note uf = minGraphProps6[OF mgp ug f]
[PROOF STATE]
proof (state)
this:
u \<in> \<V> f

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp ug f]]
[PROOF STATE]
proof (state)
this:
distinct (vertices f)

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. close g v u
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> close g v u
 2. \<not> ?P \<Longrightarrow> close g v u
[PROOF STEP]
assume 4: "|vertices f| = 4"
[PROOF STATE]
proof (state)
this:
|vertices f| = 4

goal (2 subgoals):
 1. ?P \<Longrightarrow> close g v u
 2. \<not> ?P \<Longrightarrow> close g v u
[PROOF STEP]
hence "v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)"
[PROOF STATE]
proof (prove)
using this:
|vertices f| = 4

goal (1 subgoal):
 1. v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)
[PROOF STEP]
using "if"
[PROOF STATE]
proof (prove)
using this:
|vertices f| = 4
if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u

goal (1 subgoal):
 1. v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)

goal (2 subgoals):
 1. ?P \<Longrightarrow> close g v u
 2. \<not> ?P \<Longrightarrow> close g v u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = f \<bullet> u \<Longrightarrow> close g v u
 2. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
assume "v = f \<bullet> u"
[PROOF STATE]
proof (state)
this:
v = f \<bullet> u

goal (2 subgoals):
 1. v = f \<bullet> u \<Longrightarrow> close g v u
 2. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = f \<bullet> u
[PROOF STEP]
obtain f' where "f' \<in> set(facesAt g v)" "f' \<bullet> v = u"
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); f' \<bullet> v = u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mgp_nextVertex_face_ex2[OF mgp ug f]
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u
\<exists>f'\<in>set (facesAt g (f \<bullet> u)). f' \<bullet> (f \<bullet> u) = u

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); f' \<bullet> v = u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f' \<in> set (facesAt g v)
f' \<bullet> v = u

goal (2 subgoals):
 1. v = f \<bullet> u \<Longrightarrow> close g v u
 2. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f' \<in> set (facesAt g v)
f' \<bullet> v = u

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
by(auto simp:close_def)
[PROOF STATE]
proof (state)
this:
close g v u

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
assume v: "v = f \<bullet> (f \<bullet> u)"
[PROOF STATE]
proof (state)
this:
v = f \<bullet> (f \<bullet> u)

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
hence "f \<bullet> (f \<bullet> v) = u"
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> (f \<bullet> u)

goal (1 subgoal):
 1. f \<bullet> (f \<bullet> v) = u
[PROOF STEP]
using quad_next4_id[OF 4 distf uf]
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> (f \<bullet> u)
f \<bullet> (f \<bullet> (f \<bullet> (f \<bullet> u))) = u

goal (1 subgoal):
 1. f \<bullet> (f \<bullet> v) = u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<bullet> (f \<bullet> v) = u

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<bullet> (f \<bullet> v) = u

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
have "f \<in> set(facesAt g v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> set (facesAt g v)
[PROOF STEP]
using v uf
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> (f \<bullet> u)
u \<in> \<V> f

goal (1 subgoal):
 1. f \<in> set (facesAt g v)
[PROOF STEP]
by(simp add: minGraphProps7[OF mgp minGraphProps5[OF mgp ug f]])
[PROOF STATE]
proof (state)
this:
f \<in> set (facesAt g v)

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> close g v u
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> (f \<bullet> v) = u
f \<in> set (facesAt g v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<bullet> (f \<bullet> v) = u
f \<in> set (facesAt g v)

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
f \<bullet> (f \<bullet> v) = u
f \<in> set (facesAt g v)
|vertices f| = 4

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
by(auto simp:close_def)
[PROOF STATE]
proof (state)
this:
close g v u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
close g v u

goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> close g v u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> close g v u
[PROOF STEP]
assume "|vertices f| \<noteq> 4"
[PROOF STATE]
proof (state)
this:
|vertices f| \<noteq> 4

goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> close g v u
[PROOF STEP]
hence "v = f \<bullet> u"
[PROOF STATE]
proof (prove)
using this:
|vertices f| \<noteq> 4

goal (1 subgoal):
 1. v = f \<bullet> u
[PROOF STEP]
using "if"
[PROOF STATE]
proof (prove)
using this:
|vertices f| \<noteq> 4
if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u

goal (1 subgoal):
 1. v = f \<bullet> u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = f \<bullet> u

goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> close g v u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = f \<bullet> u
[PROOF STEP]
obtain f' where "f' \<in> set(facesAt g v)" "f' \<bullet> v = u"
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); f' \<bullet> v = u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mgp_nextVertex_face_ex2[OF mgp ug f]
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u
\<exists>f'\<in>set (facesAt g (f \<bullet> u)). f' \<bullet> (f \<bullet> u) = u

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); f' \<bullet> v = u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f' \<in> set (facesAt g v)
f' \<bullet> v = u

goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> close g v u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f' \<in> set (facesAt g v)
f' \<bullet> v = u

goal (1 subgoal):
 1. close g v u
[PROOF STEP]
by(auto simp:close_def)
[PROOF STATE]
proof (state)
this:
close g v u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
close g v u

goal:
No subgoals!
[PROOF STEP]
qed