[STATEMENT]
lemma rt_fresher_if_Some [intro!]:
  assumes "the (rt dip) \<sqsubseteq> r"
    shows "rt \<sqsubseteq>\<^bsub>dip\<^esub> (\<lambda>ip. if ip = dip then Some r else rt ip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> (\<lambda>ip. if ip = dip then Some r else rt ip)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
the (rt dip) \<sqsubseteq> r

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> (\<lambda>ip. if ip = dip then Some r else rt ip)
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
the (rt dip) \<sqsubseteq> r

goal (1 subgoal):
 1. the (rt dip) \<sqsubseteq> the (if dip = dip then Some r else rt dip)
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresh_as_refl [simp]: "\<And>rt dip. rt \<approx>\<^bsub>dip\<^esub> rt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. rt \<approx>\<^bsub>dip\<^esub> rt
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt \<and> rt \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresh_as_trans [simp, intro, trans]:
  "\<And>rt1 rt2 rt3 dip. \<lbrakk> rt1 \<approx>\<^bsub>dip\<^esub> rt2; rt2 \<approx>\<^bsub>dip\<^esub> rt3 \<rbrakk> \<Longrightarrow> rt1 \<approx>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt1 rt2 rt3 dip. \<lbrakk>rt1 \<approx>\<^bsub>dip\<^esub> rt2; rt2 \<approx>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
unfolding rt_fresh_as_def rt_fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt1 rt2 rt3 dip. \<lbrakk>the (rt1 dip) \<sqsubseteq> the (rt2 dip) \<and> the (rt2 dip) \<sqsubseteq> the (rt1 dip); the (rt2 dip) \<sqsubseteq> the (rt3 dip) \<and> the (rt3 dip) \<sqsubseteq> the (rt2 dip)\<rbrakk> \<Longrightarrow> the (rt1 dip) \<sqsubseteq> the (rt3 dip) \<and> the (rt3 dip) \<sqsubseteq> the (rt1 dip)
[PROOF STEP]
by (metis (mono_tags) fresher_trans)


[STATEMENT]
lemma rt_fresh_asI [intro!]:
  assumes "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
      and "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
    shows "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresh_as_fresherI [intro]:
  assumes "dip\<in>kD(rt1)"
      and "dip\<in>kD(rt2)"
      and "the (rt1 dip) \<sqsubseteq> the (rt2 dip)"
      and "the (rt2 dip) \<sqsubseteq> the (rt1 dip)"
    shows "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt1
dip \<in> kD rt2
the (rt1 dip) \<sqsubseteq> the (rt2 dip)
the (rt2 dip) \<sqsubseteq> the (rt1 dip)

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt1
dip \<in> kD rt2
the (rt1 dip) \<sqsubseteq> the (rt2 dip)
the (rt2 dip) \<sqsubseteq> the (rt1 dip)

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by (clarsimp dest!: single_rt_fresher)


[STATEMENT]
lemma nsqn_rt_fresh_asI:
  assumes "dip \<in> kD(rt)"
      and "dip \<in> kD(rt')"
      and "nsqn rt dip = nsqn rt' dip"
      and "\<pi>\<^sub>5(the (rt dip)) = \<pi>\<^sub>5(the (rt' dip))"
    shows "rt \<approx>\<^bsub>dip\<^esub> rt'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<approx>\<^bsub>dip\<^esub> rt'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt'
 2. rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
from assms(1-2,4)
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dip \<in> kD rt'
\<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (rt' dip))
[PROOF STEP]
have dhops': "the (dhops rt' dip) \<le> the (dhops rt dip)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> kD rt'
\<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (rt' dip))

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

goal (2 subgoals):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt'
 2. rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
with assms(1-3)
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dip \<in> kD rt'
nsqn rt dip = nsqn rt' dip
the (dhops rt' dip) \<le> the (dhops rt dip)
[PROOF STEP]
show "rt \<sqsubseteq>\<^bsub>dip\<^esub> rt'"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> kD rt'
nsqn rt dip = nsqn rt' dip
the (dhops rt' dip) \<le> the (dhops rt dip)

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt'
[PROOF STEP]
by (rule rt_fresherI2)
[PROOF STATE]
proof (state)
this:
rt \<sqsubseteq>\<^bsub>dip\<^esub> rt'

goal (1 subgoal):
 1. rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
from assms(1-2,4)
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dip \<in> kD rt'
\<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (rt' dip))
[PROOF STEP]
have dhops: "the (dhops rt dip) \<le> the (dhops rt' dip)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> kD rt'
\<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (rt' dip))

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

goal (1 subgoal):
 1. rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
with assms(2,1) assms(3) [symmetric]
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt'
dip \<in> kD rt
nsqn rt' dip = nsqn rt dip
the (dhops rt dip) \<le> the (dhops rt' dip)
[PROOF STEP]
show "rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt'
dip \<in> kD rt
nsqn rt' dip = nsqn rt dip
the (dhops rt dip) \<le> the (dhops rt' dip)

goal (1 subgoal):
 1. rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
by (rule rt_fresherI2)
[PROOF STATE]
proof (state)
this:
rt' \<sqsubseteq>\<^bsub>dip\<^esub> rt

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_fresh_asE [elim]:
  assumes "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
      and "\<lbrakk> rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<rbrakk> \<Longrightarrow> P rt1 rt2 dip"
    shows "P rt1 rt2 dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P rt1 rt2 dip
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2
\<lbrakk>rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1\<rbrakk> \<Longrightarrow> P rt1 rt2 dip

goal (1 subgoal):
 1. P rt1 rt2 dip
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
\<lbrakk>rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1\<rbrakk> \<Longrightarrow> P rt1 rt2 dip

goal (1 subgoal):
 1. P rt1 rt2 dip
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresh_asD1 [dest]:
  assumes "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
    shows "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresh_asD2 [dest]:
  assumes "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
    shows "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresh_as_sym:
  assumes "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
    shows "rt2 \<approx>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt2 \<approx>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt2 \<approx>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<and> rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
by simp


[STATEMENT]
lemma not_rt_fresh_asI1 [intro]:
  assumes "\<not> (rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2)"
    shows "\<not> (rt1 \<approx>\<^bsub>dip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
assume "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (state)
this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
hence "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not> (rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. False
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_rt_fresh_asI2 [intro]:
  assumes "\<not> (rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)"
    shows "\<not> (rt1 \<approx>\<^bsub>dip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
assume "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (state)
this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
hence "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not> (rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. False
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_single_rt_fresher [elim]:
  assumes "\<not>(the (rt1 ip) \<sqsubseteq> the (rt2 ip))"
    shows "\<not>(rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
assume "rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2"
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
hence "the (rt1 ip) \<sqsubseteq> the (rt2 ip)"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not>(the (rt1 ip) \<sqsubseteq> the (rt2 ip))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> the (rt1 ip) \<sqsubseteq> the (rt2 ip)
the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> the (rt1 ip) \<sqsubseteq> the (rt2 ip)
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. False
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_rt_fresher_single [elim]:
  assumes "\<not>(rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2)"
    shows "\<not>(the (rt1 ip) \<sqsubseteq> the (rt2 ip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip) \<Longrightarrow> False
[PROOF STEP]
assume "the (rt1 ip) \<sqsubseteq> the (rt2 ip)"
[PROOF STATE]
proof (state)
this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip) \<Longrightarrow> False
[PROOF STEP]
hence "rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2"
[PROOF STATE]
proof (prove)
using this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip) \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not>(rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. False
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_fresh_as_nsqnr:
  assumes "dip \<in> kD(rt1)"
      and "dip \<in> kD(rt2)"
      and "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
    shows "nsqn\<^sub>r (the (rt2 dip)) = nsqn\<^sub>r (the (rt1 dip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r (the (rt2 dip)) = nsqn\<^sub>r (the (rt1 dip))
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. nsqn\<^sub>r (the (rt2 dip)) = nsqn\<^sub>r (the (rt1 dip))
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. nsqn\<^sub>r (the (rt2 dip)) = nsqn\<^sub>r (the (rt1 dip))
[PROOF STEP]
by (auto simp: rt_fresher_def2 [OF \<open>dip \<in> kD(rt1)\<close> \<open>dip \<in> kD(rt2)\<close>]
                 rt_fresher_def2 [OF \<open>dip \<in> kD(rt2)\<close> \<open>dip \<in> kD(rt1)\<close>]
                 kD_nsqn [OF \<open>dip \<in> kD(rt1)\<close>]
                 kD_nsqn [OF \<open>dip \<in> kD(rt2)\<close>])


[STATEMENT]
lemma rt_fresher_mapupd [intro!]:
  assumes "dip\<in>kD(rt)"
      and "the (rt dip) \<sqsubseteq> r"
    shows "rt \<sqsubseteq>\<^bsub>dip\<^esub> rt(dip \<mapsto> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt(dip \<mapsto> r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
the (rt dip) \<sqsubseteq> r

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt(dip \<mapsto> r)
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
the (rt dip) \<sqsubseteq> r

goal (1 subgoal):
 1. the (rt dip) \<sqsubseteq> the ((rt(dip \<mapsto> r)) dip)
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresher_map_update_other [intro!]:
  assumes "dip\<in>kD(rt)"
      and "dip \<noteq> ip"
    shows "rt \<sqsubseteq>\<^bsub>dip\<^esub> rt(ip \<mapsto> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt(ip \<mapsto> r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<noteq> ip

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt(ip \<mapsto> r)
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<noteq> ip

goal (1 subgoal):
 1. the (rt dip) \<sqsubseteq> the ((rt(ip \<mapsto> r)) dip)
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresher_update_other [simp]:
  assumes inkD: "dip\<in>kD(rt)"
     and "dip \<noteq> ip"
   shows "rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<noteq> ip

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
unfolding update_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<noteq> ip

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> (case rt ip of None \<Rightarrow> rt(ip \<mapsto> r) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 r then rt(ip \<mapsto> addpre r (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 r \<and> (\<pi>\<^sub>5 r < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(ip \<mapsto> addpre r (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>3 r = unk then rt(ip \<mapsto> (\<pi>\<^sub>2 s, snd (addpre r (\<pi>\<^sub>7 s)))) else rt(ip \<mapsto> addpre s (\<pi>\<^sub>7 r)))
[PROOF STEP]
by (clarsimp split: option.split) (fastforce)


[STATEMENT]
theorem rt_fresher_update [simp]:
  assumes "dip\<in>kD(rt)"
      and "the (dhops rt dip) \<ge> 1"
      and "update_arg_wf r"
   shows "rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
proof (cases "dip = ip")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
 2. dip \<noteq> ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
assume "dip \<noteq> ip"
[PROOF STATE]
proof (state)
this:
dip \<noteq> ip

goal (2 subgoals):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
 2. dip \<noteq> ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
with \<open>dip\<in>kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dip \<noteq> ip
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<noteq> ip

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
by (rule rt_fresher_update_other)
[PROOF STATE]
proof (state)
this:
rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r

goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
assume "dip = ip"
[PROOF STATE]
proof (state)
this:
dip = ip

goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
from \<open>dip\<in>kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
[PROOF STEP]
obtain dsn\<^sub>n dsk\<^sub>n f\<^sub>n hops\<^sub>n nhip\<^sub>n pre\<^sub>n
      where rtn [simp]: "the (rt dip) = (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. (\<And>dsn\<^sub>n dsk\<^sub>n f\<^sub>n hops\<^sub>n nhip\<^sub>n pre\<^sub>n. the (rt dip) = (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases6)
[PROOF STATE]
proof (state)
this:
the (rt dip) = (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)

goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
with \<open>the (dhops rt dip) \<ge> 1\<close> and \<open>dip\<in>kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> the (dhops rt dip)
dip \<in> kD rt
the (rt dip) = (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
[PROOF STEP]
have "hops\<^sub>n \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> the (dhops rt dip)
dip \<in> kD rt
the (rt dip) = (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)

goal (1 subgoal):
 1. 1 \<le> hops\<^sub>n
[PROOF STEP]
by (metis proj5_eq_dhops projs(4))
[PROOF STATE]
proof (state)
this:
1 \<le> hops\<^sub>n

goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
from \<open>dip\<in>kD(rt)\<close> rtn
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
the (rt dip) = (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
[PROOF STEP]
have [simp]: "sqn rt dip = dsn\<^sub>n"
                           and [simp]: "the (dhops rt dip) = hops\<^sub>n"
                           and [simp]: "the (flag rt dip) = f\<^sub>n"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
the (rt dip) = (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)

goal (1 subgoal):
 1. sqn rt dip = dsn\<^sub>n &&& the (dhops rt dip) = hops\<^sub>n &&& the (flag rt dip) = f\<^sub>n
[PROOF STEP]
by (simp add: sqn_def proj5_eq_dhops [symmetric]
                            proj4_eq_flag [symmetric])+
[PROOF STATE]
proof (state)
this:
sqn rt dip = dsn\<^sub>n
the (dhops rt dip) = hops\<^sub>n
the (flag rt dip) = f\<^sub>n

goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
from \<open>update_arg_wf r\<close>
[PROOF STATE]
proof (chain)
picking this:
update_arg_wf r
[PROOF STEP]
have "(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
                                  \<sqsubseteq> the ((update rt dip r) dip)"
[PROOF STATE]
proof (prove)
using this:
update_arg_wf r

goal (1 subgoal):
 1. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip r dip)
[PROOF STEP]
proof (rule wf_r_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>nhip pre. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)
 2. \<And>dsn hops nhip pre. 0 < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
fix nhip pre
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>nhip pre. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)
 2. \<And>dsn hops nhip pre. 0 < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
from \<open>hops\<^sub>n \<ge> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> hops\<^sub>n
[PROOF STEP]
have "\<And>pre'. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
                                        \<sqsubseteq> (dsn\<^sub>n, unk, val, Suc 0, nhip, pre')"
[PROOF STATE]
proof (prove)
using this:
1 \<le> hops\<^sub>n

goal (1 subgoal):
 1. \<And>pre'. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn\<^sub>n, unk, val, Suc 0, nhip, pre')
[PROOF STEP]
unfolding fresher_def sqn_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> hops\<^sub>n

goal (1 subgoal):
 1. \<And>pre'. nsqn\<^sub>r (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) < nsqn\<^sub>r (dsn\<^sub>n, unk, val, Suc 0, nhip, pre') \<or> nsqn\<^sub>r (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) = nsqn\<^sub>r (dsn\<^sub>n, unk, val, Suc 0, nhip, pre') \<and> \<pi>\<^sub>5 (dsn\<^sub>n, unk, val, Suc 0, nhip, pre') \<le> \<pi>\<^sub>5 (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
[PROOF STEP]
by (cases f\<^sub>n) auto
[PROOF STATE]
proof (state)
this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn\<^sub>n, unk, val, Suc 0, nhip, ?pre')

goal (2 subgoals):
 1. \<And>nhip pre. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)
 2. \<And>dsn hops nhip pre. 0 < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
thus "(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
               \<sqsubseteq> the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)"
[PROOF STATE]
proof (prove)
using this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn\<^sub>n, unk, val, Suc 0, nhip, ?pre')

goal (1 subgoal):
 1. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)
[PROOF STEP]
using \<open>dip\<in>kD(rt)\<close>
[PROOF STATE]
proof (prove)
using this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn\<^sub>n, unk, val, Suc 0, nhip, ?pre')
dip \<in> kD rt

goal (1 subgoal):
 1. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)
[PROOF STEP]
by - (rule update_cases_kD, simp_all)
[PROOF STATE]
proof (state)
this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)

goal (1 subgoal):
 1. \<And>dsn hops nhip pre. 0 < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dsn hops nhip pre. 0 < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
fix dsn :: sqn and hops nhip pre
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dsn hops nhip pre. 0 < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
assume "0 < dsn"
[PROOF STATE]
proof (state)
this:
0 < dsn

goal (1 subgoal):
 1. \<And>dsn hops nhip pre. 0 < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
show "(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
               \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)
[PROOF STEP]
proof (rule update_cases_kD [OF _ \<open>dip\<in>kD(rt)\<close>], simp_all add: \<open>0 < dsn\<close>)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. dsn\<^sub>n < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
 2. \<lbrakk>dsn\<^sub>n = dsn; hops < hops\<^sub>n\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
 3. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
assume "dsn\<^sub>n < dsn"
[PROOF STATE]
proof (state)
this:
dsn\<^sub>n < dsn

goal (3 subgoals):
 1. dsn\<^sub>n < dsn \<Longrightarrow> (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
 2. \<lbrakk>dsn\<^sub>n = dsn; hops < hops\<^sub>n\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
 3. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
thus "(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
                   \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)"
[PROOF STATE]
proof (prove)
using this:
dsn\<^sub>n < dsn

goal (1 subgoal):
 1. (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
using this:
dsn\<^sub>n < dsn

goal (1 subgoal):
 1. nsqn\<^sub>r (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) < nsqn\<^sub>r (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) \<or> nsqn\<^sub>r (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) = nsqn\<^sub>r (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) \<and> \<pi>\<^sub>5 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) \<le> \<pi>\<^sub>5 (dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)

goal (2 subgoals):
 1. \<lbrakk>dsn\<^sub>n = dsn; hops < hops\<^sub>n\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
 2. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>dsn\<^sub>n = dsn; hops < hops\<^sub>n\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
 2. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
assume "dsn\<^sub>n = dsn"
             and "hops < hops\<^sub>n"
[PROOF STATE]
proof (state)
this:
dsn\<^sub>n = dsn
hops < hops\<^sub>n

goal (2 subgoals):
 1. \<lbrakk>dsn\<^sub>n = dsn; hops < hops\<^sub>n\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
 2. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
thus "(dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
                   \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)"
[PROOF STATE]
proof (prove)
using this:
dsn\<^sub>n = dsn
hops < hops\<^sub>n

goal (1 subgoal):
 1. (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
unfolding fresher_def nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
using this:
dsn\<^sub>n = dsn
hops < hops\<^sub>n

goal (1 subgoal):
 1. (if \<pi>\<^sub>4 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) = val \<or> \<pi>\<^sub>2 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) = 0 then \<pi>\<^sub>2 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) else \<pi>\<^sub>2 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) - 1) < (if \<pi>\<^sub>4 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) = val \<or> \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) = 0 then \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) else \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) - 1) \<or> (if \<pi>\<^sub>4 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) = val \<or> \<pi>\<^sub>2 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) = 0 then \<pi>\<^sub>2 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) else \<pi>\<^sub>2 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) - 1) = (if \<pi>\<^sub>4 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) = val \<or> \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) = 0 then \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) else \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) - 1) \<and> \<pi>\<^sub>5 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) \<le> \<pi>\<^sub>5 (dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(dsn, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)

goal (1 subgoal):
 1. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
assume "dsn\<^sub>n = dsn"
[PROOF STATE]
proof (state)
this:
dsn\<^sub>n = dsn

goal (1 subgoal):
 1. \<lbrakk>dsn\<^sub>n = dsn; f\<^sub>n = Aodv_Basic.inv\<rbrakk> \<Longrightarrow> (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
with \<open>0 < dsn\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < dsn
dsn\<^sub>n = dsn
[PROOF STEP]
show "(dsn, dsk\<^sub>n, inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
                   \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)"
[PROOF STATE]
proof (prove)
using this:
0 < dsn
dsn\<^sub>n = dsn

goal (1 subgoal):
 1. (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
using this:
0 < dsn
dsn\<^sub>n = dsn

goal (1 subgoal):
 1. nsqn\<^sub>r (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) < nsqn\<^sub>r (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) \<or> nsqn\<^sub>r (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) = nsqn\<^sub>r (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) \<and> \<pi>\<^sub>5 (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n) \<le> \<pi>\<^sub>5 (dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(dsn, dsk\<^sub>n, Aodv_Basic.inv, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> (dsn, kno, val, hops, nhip, pre \<union> pre\<^sub>n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip r dip)

goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
hence "rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt dip r"
[PROOF STATE]
proof (prove)
using this:
(dsn\<^sub>n, dsk\<^sub>n, f\<^sub>n, hops\<^sub>n, nhip\<^sub>n, pre\<^sub>n) \<sqsubseteq> the (update rt dip r dip)

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt dip r
[PROOF STEP]
by - (rule single_rt_fresher, simp)
[PROOF STATE]
proof (state)
this:
rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt dip r

goal (1 subgoal):
 1. dip = ip \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
with \<open>dip = ip\<close>
[PROOF STATE]
proof (chain)
picking this:
dip = ip
rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt dip r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip = ip
rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt dip r

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rt \<sqsubseteq>\<^bsub>dip\<^esub> update rt ip r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem rt_fresher_invalidate [simp]:
  assumes "dip\<in>kD(rt)"
      and indests: "\<forall>rip\<in>dom(dests). rip\<in>vD(rt) \<and> sqn rt rip < the (dests rip)"
    shows "rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
proof (cases "dip\<in>dom(dests)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
 2. dip \<notin> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
assume "dip\<notin>dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<notin> dom dests

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
 2. dip \<notin> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<notin> dom dests

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
using \<open>dip\<in>kD(rt)\<close>
[PROOF STATE]
proof (prove)
using this:
dip \<notin> dom dests
dip \<in> kD rt

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
by - (rule single_rt_fresher, simp)
[PROOF STATE]
proof (state)
this:
rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
assume "dip\<in>dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
with indests
[PROOF STATE]
proof (chain)
picking this:
\<forall>rip\<in>dom dests. rip \<in> vD rt \<and> sqn rt rip < the (dests rip)
dip \<in> dom dests
[PROOF STEP]
have "dip\<in>vD(rt)"
                           and "sqn rt dip < the (dests dip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>rip\<in>dom dests. rip \<in> vD rt \<and> sqn rt rip < the (dests rip)
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<in> vD rt &&& sqn rt dip < the (dests dip)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dip \<in> vD rt
sqn rt dip < the (dests dip)

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dip \<in> dom dests
dip \<in> vD rt
sqn rt dip < the (dests dip)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests
dip \<in> vD rt
sqn rt dip < the (dests dip)

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
unfolding invalidate_def sqn_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests
dip \<in> vD rt
(case rt dip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r) < the (dests dip)

goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> (\<lambda>ip. case (rt ip, dests ip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))
[PROOF STEP]
by - (rule single_rt_fresher, auto simp: fresher_def)
[PROOF STATE]
proof (state)
this:
rt \<sqsubseteq>\<^bsub>dip\<^esub> invalidate rt dests

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nsqn\<^sub>r_invalidate [simp]:
  assumes "dip\<in>kD(rt)"
      and "dip\<in>dom(dests)"
    shows "nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> dom dests

goal (1 subgoal):
 1. nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1
[PROOF STEP]
unfolding invalidate_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> dom dests

goal (1 subgoal):
 1. nsqn\<^sub>r (the (case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))) = the (dests dip) - 1
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_fresh_as_inc_invalidate [simp]:
  assumes "dip\<in>kD(rt)"
      and "\<forall>rip\<in>dom(dests). rip\<in>vD(rt) \<and> the (dests rip) = inc (sqn rt rip)"
    shows "rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
proof (cases "dip\<in>dom(dests)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
 2. dip \<notin> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
assume "dip\<notin>dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<notin> dom dests

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
 2. dip \<notin> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
with \<open>dip\<in>kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dip \<notin> dom dests
[PROOF STEP]
have "dip\<in>kD(invalidate rt dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<notin> dom dests

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

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

goal (1 subgoal):
 1. rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
by rule (simp_all add: \<open>dip\<notin>dom(dests)\<close>)
[PROOF STATE]
proof (state)
this:
rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
assume "dip\<in>dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>rip\<in>dom dests. rip \<in> vD rt \<and> the (dests rip) = inc (sqn rt rip)
dip \<in> dom dests
[PROOF STEP]
have "dip\<in>vD(rt)"
                  and "the (dests dip) = inc (sqn rt dip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>rip\<in>dom dests. rip \<in> vD rt \<and> the (dests rip) = inc (sqn rt rip)
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<in> vD rt &&& the (dests dip) = inc (sqn rt dip)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dip \<in> vD rt
the (dests dip) = inc (sqn rt dip)

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
from \<open>dip\<in>vD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD rt
[PROOF STEP]
have "dip\<in>kD(rt)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD rt

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

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dip \<in> kD rt

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
[PROOF STEP]
have "dip\<in>kD(invalidate rt dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

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

goal (1 subgoal):
 1. dip \<in> dom dests \<Longrightarrow> rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dip \<in> kD (invalidate rt dests)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
proof (rule nsqn_rt_fresh_asI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nsqn rt dip = nsqn (invalidate rt dests) dip
 2. \<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (invalidate rt dests dip))
[PROOF STEP]
from \<open>dip\<in>vD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD rt
[PROOF STEP]
have "nsqn rt dip = sqn rt dip"
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD rt

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

goal (2 subgoals):
 1. nsqn rt dip = nsqn (invalidate rt dests) dip
 2. \<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (invalidate rt dests dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nsqn rt dip = sqn rt dip

goal (2 subgoals):
 1. nsqn rt dip = nsqn (invalidate rt dests) dip
 2. \<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (invalidate rt dests dip))
[PROOF STEP]
have "sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))
[PROOF STEP]
from \<open>dip\<in>kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
[PROOF STEP]
have "nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1
[PROOF STEP]
using \<open>dip\<in>dom(dests)\<close>
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> dom dests

goal (1 subgoal):
 1. nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1
[PROOF STEP]
by (rule nsqn\<^sub>r_invalidate)
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1

goal (1 subgoal):
 1. sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))
[PROOF STEP]
with \<open>the (dests dip) = inc (sqn rt dip)\<close>
[PROOF STATE]
proof (chain)
picking this:
the (dests dip) = inc (sqn rt dip)
nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1
[PROOF STEP]
show "sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))"
[PROOF STATE]
proof (prove)
using this:
the (dests dip) = inc (sqn rt dip)
nsqn\<^sub>r (the (invalidate rt dests dip)) = the (dests dip) - 1

goal (1 subgoal):
 1. sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))

goal (2 subgoals):
 1. nsqn rt dip = nsqn (invalidate rt dests) dip
 2. \<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (invalidate rt dests dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqn rt dip = nsqn\<^sub>r (the (invalidate rt dests dip))

goal (2 subgoals):
 1. nsqn rt dip = nsqn (invalidate rt dests) dip
 2. \<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (invalidate rt dests dip))
[PROOF STEP]
from \<open>dip\<in>kD(invalidate rt dests)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD (invalidate rt dests)
[PROOF STEP]
have "nsqn\<^sub>r (the (invalidate rt dests dip)) = nsqn (invalidate rt dests) dip"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. nsqn\<^sub>r (the (invalidate rt dests dip)) = nsqn (invalidate rt dests) dip
[PROOF STEP]
by (simp add: kD_nsqn)
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (invalidate rt dests dip)) = nsqn (invalidate rt dests) dip

goal (2 subgoals):
 1. nsqn rt dip = nsqn (invalidate rt dests) dip
 2. \<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (invalidate rt dests dip))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nsqn rt dip = nsqn (invalidate rt dests) dip
[PROOF STEP]
show "nsqn rt dip = nsqn (invalidate rt dests) dip"
[PROOF STATE]
proof (prove)
using this:
nsqn rt dip = nsqn (invalidate rt dests) dip

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

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt dip)) = \<pi>\<^sub>5 (the (invalidate rt dests dip))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_fresh_as_addpreRT [simp]:
  assumes "ip\<in>kD(rt)"
    shows "rt \<approx>\<^bsub>dip\<^esub> the (addpreRT rt ip npre)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<approx>\<^bsub>dip\<^esub> the (addpreRT rt ip npre)
[PROOF STEP]
using assms [THEN kD_Some]
[PROOF STATE]
proof (prove)
using this:
\<exists>dsn dsk flag hops nhip pre. rt ip = Some (dsn, dsk, flag, hops, nhip, pre)

goal (1 subgoal):
 1. rt \<approx>\<^bsub>dip\<^esub> the (addpreRT rt ip npre)
[PROOF STEP]
by (auto simp: addpreRT_def)


[STATEMENT]
lemma rt_strictly_fresher_def'':
  "rt1 \<sqsubset>\<^bsub>i\<^esub> rt2 = ((rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2) \<and> \<not>(rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rt1 \<sqsubset>\<^bsub>i\<^esub> rt2) = (rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1)
[PROOF STEP]
unfolding rt_strictly_fresher_def rt_fresh_as_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> (rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1)) = (rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1)
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_strictly_fresherI' [intro]:
  assumes "rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2"
      and "\<not>(rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1)"
    shows "rt1 \<sqsubset>\<^bsub>i\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>i\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2
\<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>i\<^esub> rt2
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2
\<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_strictly_fresherE' [elim]:
  assumes "rt1 \<sqsubset>\<^bsub>i\<^esub> rt2"
      and "\<lbrakk> rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2; \<not>(rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1) \<rbrakk> \<Longrightarrow> P rt1 rt2 i"
    shows "P rt1 rt2 i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P rt1 rt2 i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>i\<^esub> rt2
\<lbrakk>rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2; \<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1\<rbrakk> \<Longrightarrow> P rt1 rt2 i

goal (1 subgoal):
 1. P rt1 rt2 i
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1
\<lbrakk>rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2; \<not> rt2 \<sqsubseteq>\<^bsub>i\<^esub> rt1\<rbrakk> \<Longrightarrow> P rt1 rt2 i

goal (1 subgoal):
 1. P rt1 rt2 i
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_strictly_fresherI [intro]:
  assumes "rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2"
      and "\<not>(rt1 \<approx>\<^bsub>i\<^esub> rt2)"
    shows "rt1 \<sqsubset>\<^bsub>i\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>i\<^esub> rt2
[PROOF STEP]
unfolding rt_strictly_fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> rt1 \<approx>\<^bsub>i\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2
\<not> rt1 \<approx>\<^bsub>i\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> rt1 \<approx>\<^bsub>i\<^esub> rt2
[PROOF STEP]
..


[STATEMENT]
lemma rt_strictly_fresherE [elim]:
  assumes "rt1 \<sqsubset>\<^bsub>i\<^esub> rt2"
      and "\<lbrakk> rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2; \<not>(rt1 \<approx>\<^bsub>i\<^esub> rt2) \<rbrakk> \<Longrightarrow> P rt1 rt2 i"
    shows "P rt1 rt2 i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P rt1 rt2 i
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>i\<^esub> rt2

goal (1 subgoal):
 1. P rt1 rt2 i
[PROOF STEP]
unfolding rt_strictly_fresher_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>i\<^esub> rt2 \<and> \<not> rt1 \<approx>\<^bsub>i\<^esub> rt2

goal (1 subgoal):
 1. P rt1 rt2 i
[PROOF STEP]
by rule (erule(1) assms(2))


[STATEMENT]
lemma rt_strictly_fresher_def':
  "rt1 \<sqsubset>\<^bsub>i\<^esub> rt2 =
     (nsqn\<^sub>r (the (rt1 i)) < nsqn\<^sub>r (the (rt2 i))
       \<or> (nsqn\<^sub>r (the (rt1 i)) = nsqn\<^sub>r (the (rt2 i)) \<and> \<pi>\<^sub>5(the (rt1 i)) > \<pi>\<^sub>5(the (rt2 i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rt1 \<sqsubset>\<^bsub>i\<^esub> rt2) = (nsqn\<^sub>r (the (rt1 i)) < nsqn\<^sub>r (the (rt2 i)) \<or> nsqn\<^sub>r (the (rt1 i)) = nsqn\<^sub>r (the (rt2 i)) \<and> \<pi>\<^sub>5 (the (rt2 i)) < \<pi>\<^sub>5 (the (rt1 i)))
[PROOF STEP]
unfolding rt_strictly_fresher_def'' rt_fresher_def fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nsqn\<^sub>r (the (rt1 i)) < nsqn\<^sub>r (the (rt2 i)) \<or> nsqn\<^sub>r (the (rt1 i)) = nsqn\<^sub>r (the (rt2 i)) \<and> \<pi>\<^sub>5 (the (rt2 i)) \<le> \<pi>\<^sub>5 (the (rt1 i))) \<and> \<not> (nsqn\<^sub>r (the (rt2 i)) < nsqn\<^sub>r (the (rt1 i)) \<or> nsqn\<^sub>r (the (rt2 i)) = nsqn\<^sub>r (the (rt1 i)) \<and> \<pi>\<^sub>5 (the (rt1 i)) \<le> \<pi>\<^sub>5 (the (rt2 i)))) = (nsqn\<^sub>r (the (rt1 i)) < nsqn\<^sub>r (the (rt2 i)) \<or> nsqn\<^sub>r (the (rt1 i)) = nsqn\<^sub>r (the (rt2 i)) \<and> \<pi>\<^sub>5 (the (rt2 i)) < \<pi>\<^sub>5 (the (rt1 i)))
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_strictly_fresher_fresherD [dest]:
  assumes "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2"
    shows "the (rt1 dip) \<sqsubseteq> the (rt2 dip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (rt1 dip) \<sqsubseteq> the (rt2 dip)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. the (rt1 dip) \<sqsubseteq> the (rt2 dip)
[PROOF STEP]
unfolding rt_strictly_fresher_def rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
the (rt1 dip) \<sqsubseteq> the (rt2 dip) \<and> \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. the (rt1 dip) \<sqsubseteq> the (rt2 dip)
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_strictly_fresher_not_fresh_asD [dest]:
  assumes "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2"
    shows "\<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_strictly_fresher_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_strictly_fresher_trans [elim, trans]:
  assumes "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2"
      and "rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3"
    shows "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2\<close>
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
obtain "the (rt1 dip) \<sqsubseteq> the (rt2 dip)"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. (the (rt1 dip) \<sqsubseteq> the (rt2 dip) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (rt1 dip) \<sqsubseteq> the (rt2 dip)

goal (1 subgoal):
 1. \<lbrakk>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
the (rt1 dip) \<sqsubseteq> the (rt2 dip)

goal (1 subgoal):
 1. \<lbrakk>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<close>
[PROOF STATE]
proof (chain)
picking this:
rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
obtain "the (rt2 dip) \<sqsubseteq> the (rt3 dip)"
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. (the (rt2 dip) \<sqsubseteq> the (rt3 dip) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (rt2 dip) \<sqsubseteq> the (rt3 dip)

goal (1 subgoal):
 1. \<lbrakk>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
the (rt1 dip) \<sqsubseteq> the (rt3 dip)
[PROOF STEP]
have "the (rt1 dip) \<sqsubseteq> the (rt3 dip)"
[PROOF STATE]
proof (prove)
using this:
the (rt1 dip) \<sqsubseteq> the (rt3 dip)

goal (1 subgoal):
 1. the (rt1 dip) \<sqsubseteq> the (rt3 dip)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
the (rt1 dip) \<sqsubseteq> the (rt3 dip)

goal (1 subgoal):
 1. \<lbrakk>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the (rt1 dip) \<sqsubseteq> the (rt3 dip)

goal (1 subgoal):
 1. \<lbrakk>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
have "\<not> (rt1 \<approx>\<^bsub>dip\<^esub> rt3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2\<close>
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
obtain "\<not>(the (rt2 dip) \<sqsubseteq> the (rt1 dip))"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. (\<not> the (rt2 dip) \<sqsubseteq> the (rt1 dip) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> the (rt2 dip) \<sqsubseteq> the (rt1 dip)

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<not> the (rt2 dip) \<sqsubseteq> the (rt1 dip)

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<close>
[PROOF STATE]
proof (chain)
picking this:
rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
obtain "\<not>(the (rt3 dip) \<sqsubseteq> the (rt2 dip))"
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. (\<not> the (rt3 dip) \<sqsubseteq> the (rt2 dip) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> the (rt3 dip) \<sqsubseteq> the (rt2 dip)

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<not> the (rt3 dip) \<sqsubseteq> the (rt1 dip)
[PROOF STEP]
have "\<not>(the (rt3 dip) \<sqsubseteq> the (rt1 dip))"
[PROOF STATE]
proof (prove)
using this:
\<not> the (rt3 dip) \<sqsubseteq> the (rt1 dip)

goal (1 subgoal):
 1. \<not> the (rt3 dip) \<sqsubseteq> the (rt1 dip)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> the (rt3 dip) \<sqsubseteq> the (rt1 dip)

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> the (rt3 dip) \<sqsubseteq> the (rt1 dip)

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. \<lbrakk>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2; rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<rbrakk> \<Longrightarrow> rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the (rt1 dip) \<sqsubseteq> the (rt3 dip)
\<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
show "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
using this:
the (rt1 dip) \<sqsubseteq> the (rt3 dip)
\<not> rt1 \<approx>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_strictly_fresher_irefl [simp]: "\<not> (rt \<sqsubset>\<^bsub>dip\<^esub> rt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rt \<sqsubset>\<^bsub>dip\<^esub> rt
[PROOF STEP]
unfolding rt_strictly_fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (rt \<sqsubseteq>\<^bsub>dip\<^esub> rt \<and> \<not> rt \<approx>\<^bsub>dip\<^esub> rt)
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma rt_fresher_trans_rt_strictly_fresher [elim, trans]:
  assumes "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2"
      and "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
    shows "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2\<close>
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
have "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
                           and "\<not>(rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 &&& \<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> \<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 &&& \<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from this(1) and \<open>rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3\<close>
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
have "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>\<not>(rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
have "\<not>(rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)"
[PROOF STATE]
proof (prove)
using this:
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
proof (rule contrapos_nn)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<Longrightarrow> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
assume "rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (state)
this:
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<Longrightarrow> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
with \<open>rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3\<close>
[PROOF STATE]
proof (chain)
picking this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
show "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
show "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3 \<and> \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_fresher_trans_rt_strictly_fresher' [elim, trans]:
  assumes "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
      and "rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3"
    shows "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3\<close>
[PROOF STATE]
proof (chain)
picking this:
rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
have "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
                           and "\<not>(rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3 &&& \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3 \<and> \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3 &&& \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2\<close> and this(1)
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
have "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>\<not>(rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
have "\<not>(rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)"
[PROOF STATE]
proof (prove)
using this:
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
proof (rule contrapos_nn)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<Longrightarrow> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
assume "rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (state)
this:
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<Longrightarrow> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
thus "rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
using this:
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
using \<open>rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2\<close>
[PROOF STATE]
proof (prove)
using this:
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
show "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3 \<and> \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_fresher_imp_nsqn_le:
  assumes "rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2"
      and "ip \<in> kD rt1"
      and "ip \<in> kD rt2"
    shows "nsqn rt1 ip \<le> nsqn rt2 ip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt1 ip \<le> nsqn rt2 ip
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. nsqn rt1 ip \<le> nsqn rt2 ip
[PROOF STEP]
by (auto simp add: rt_fresher_def2 [OF assms(2-3)])


[STATEMENT]
lemma rt_strictly_fresher_ltI [intro]:
  assumes "dip \<in> kD(rt1)"
      and "dip \<in> kD(rt2)"
      and "nsqn rt1 dip < nsqn rt2 dip"
    shows "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
 2. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt1
dip \<in> kD rt2
nsqn rt1 dip < nsqn rt2 dip
[PROOF STEP]
show "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt1
dip \<in> kD rt2
nsqn rt1 dip < nsqn rt2 dip

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
show "\<not>(rt1 \<approx>\<^bsub>dip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
assume "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (state)
this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
hence "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (prove)
using this:
rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
hence "nsqn rt2 dip \<le> nsqn rt1 dip"
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. nsqn rt2 dip \<le> nsqn rt1 dip
[PROOF STEP]
using \<open>dip \<in> kD(rt2)\<close> \<open>dip \<in> kD(rt1)\<close>
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
dip \<in> kD rt2
dip \<in> kD rt1

goal (1 subgoal):
 1. nsqn rt2 dip \<le> nsqn rt1 dip
[PROOF STEP]
by (rule rt_fresher_imp_nsqn_le)
[PROOF STATE]
proof (state)
this:
nsqn rt2 dip \<le> nsqn rt1 dip

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2 \<Longrightarrow> False
[PROOF STEP]
with \<open>nsqn rt1 dip < nsqn rt2 dip\<close>
[PROOF STATE]
proof (chain)
picking this:
nsqn rt1 dip < nsqn rt2 dip
nsqn rt2 dip \<le> nsqn rt1 dip
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
nsqn rt1 dip < nsqn rt2 dip
nsqn rt2 dip \<le> nsqn rt1 dip

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> rt1 \<approx>\<^bsub>dip\<^esub> rt2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_strictly_fresher_eqI [intro]:
  assumes "i\<in>kD(rt1)"
      and "i\<in>kD(rt2)"
      and "nsqn rt1 i = nsqn rt2 i"
      and "\<pi>\<^sub>5(the (rt2 i)) < \<pi>\<^sub>5(the (rt1 i))"
    shows "rt1 \<sqsubset>\<^bsub>i\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>i\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> kD rt1
i \<in> kD rt2
nsqn rt1 i = nsqn rt2 i
\<pi>\<^sub>5 (the (rt2 i)) < \<pi>\<^sub>5 (the (rt1 i))

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>i\<^esub> rt2
[PROOF STEP]
unfolding rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
using this:
i \<in> kD rt1
i \<in> kD rt2
nsqn rt1 i = nsqn rt2 i
\<pi>\<^sub>5 (the (rt2 i)) < \<pi>\<^sub>5 (the (rt1 i))

goal (1 subgoal):
 1. nsqn\<^sub>r (the (rt1 i)) < nsqn\<^sub>r (the (rt2 i)) \<or> nsqn\<^sub>r (the (rt1 i)) = nsqn\<^sub>r (the (rt2 i)) \<and> \<pi>\<^sub>5 (the (rt2 i)) < \<pi>\<^sub>5 (the (rt1 i))
[PROOF STEP]
by (auto simp add: kD_nsqn)


[STATEMENT]
lemma invalidate_rtsf_left [simp]:
  "\<And>dests dip rt rt'. dests dip = None \<Longrightarrow> (invalidate rt dests \<sqsubset>\<^bsub>dip\<^esub> rt') = (rt \<sqsubset>\<^bsub>dip\<^esub> rt')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dests dip rt rt'. dests dip = None \<Longrightarrow> (invalidate rt dests \<sqsubset>\<^bsub>dip\<^esub> rt') = (rt \<sqsubset>\<^bsub>dip\<^esub> rt')
[PROOF STEP]
unfolding invalidate_def rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dests dip rt rt'. dests dip = None \<Longrightarrow> (nsqn\<^sub>r (the (case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))) < nsqn\<^sub>r (the (rt' dip)) \<or> nsqn\<^sub>r (the (case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))) = nsqn\<^sub>r (the (rt' dip)) \<and> \<pi>\<^sub>5 (the (rt' dip)) < \<pi>\<^sub>5 (the (case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)))) = (nsqn\<^sub>r (the (rt dip)) < nsqn\<^sub>r (the (rt' dip)) \<or> nsqn\<^sub>r (the (rt dip)) = nsqn\<^sub>r (the (rt' dip)) \<and> \<pi>\<^sub>5 (the (rt' dip)) < \<pi>\<^sub>5 (the (rt dip)))
[PROOF STEP]
by (rule iffI) (auto split: option.split_asm)


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

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
 2. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
hence "dip \<notin> vD(invalidate rt1 dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_strictly_fresher_update_other [elim!]:
  "\<And>dip ip rt r rt'. \<lbrakk> dip \<noteq> ip; rt \<sqsubset>\<^bsub>dip\<^esub> rt' \<rbrakk> \<Longrightarrow> update rt ip r \<sqsubset>\<^bsub>dip\<^esub> rt'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dip ip rt r rt'. \<lbrakk>dip \<noteq> ip; rt \<sqsubset>\<^bsub>dip\<^esub> rt'\<rbrakk> \<Longrightarrow> update rt ip r \<sqsubset>\<^bsub>dip\<^esub> rt'
[PROOF STEP]
unfolding rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dip ip rt r rt'. \<lbrakk>dip \<noteq> ip; nsqn\<^sub>r (the (rt dip)) < nsqn\<^sub>r (the (rt' dip)) \<or> nsqn\<^sub>r (the (rt dip)) = nsqn\<^sub>r (the (rt' dip)) \<and> \<pi>\<^sub>5 (the (rt' dip)) < \<pi>\<^sub>5 (the (rt dip))\<rbrakk> \<Longrightarrow> nsqn\<^sub>r (the (update rt ip r dip)) < nsqn\<^sub>r (the (rt' dip)) \<or> nsqn\<^sub>r (the (update rt ip r dip)) = nsqn\<^sub>r (the (rt' dip)) \<and> \<pi>\<^sub>5 (the (rt' dip)) < \<pi>\<^sub>5 (the (update rt ip r dip))
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma addpreRT_strictly_fresher [simp]:
  assumes "dip \<in> kD(rt)"
    shows "(the (addpreRT rt dip npre) \<sqsubset>\<^bsub>ip\<^esub> rt2) = (rt \<sqsubset>\<^bsub>ip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (the (addpreRT rt dip npre) \<sqsubset>\<^bsub>ip\<^esub> rt2) = (rt \<sqsubset>\<^bsub>ip\<^esub> rt2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. (the (addpreRT rt dip npre) \<sqsubset>\<^bsub>ip\<^esub> rt2) = (rt \<sqsubset>\<^bsub>ip\<^esub> rt2)
[PROOF STEP]
unfolding rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. (nsqn\<^sub>r (the (the (addpreRT rt dip npre) ip)) < nsqn\<^sub>r (the (rt2 ip)) \<or> nsqn\<^sub>r (the (the (addpreRT rt dip npre) ip)) = nsqn\<^sub>r (the (rt2 ip)) \<and> \<pi>\<^sub>5 (the (rt2 ip)) < \<pi>\<^sub>5 (the (the (addpreRT rt dip npre) ip))) = (nsqn\<^sub>r (the (rt ip)) < nsqn\<^sub>r (the (rt2 ip)) \<or> nsqn\<^sub>r (the (rt ip)) = nsqn\<^sub>r (the (rt2 ip)) \<and> \<pi>\<^sub>5 (the (rt2 ip)) < \<pi>\<^sub>5 (the (rt ip)))
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma lt_sqn_imp_update_strictly_fresher:
  assumes "dip \<in> vD (rt2 nhip)"
      and  *: "osn < sqn (rt2 nhip) dip"
      and **: "rt \<noteq> update rt dip (osn, kno, val, hops, nhip, {})"
    shows "update rt dip (osn, kno, val, hops, nhip, {}) \<sqsubset>\<^bsub>dip\<^esub> rt2 nhip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update rt dip (osn, kno, val, hops, nhip, {}) \<sqsubset>\<^bsub>dip\<^esub> rt2 nhip
[PROOF STEP]
unfolding rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip)) \<or> nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip)) \<and> \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, hops, nhip, {}) dip))
[PROOF STEP]
proof (rule disjI1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
from **
[PROOF STATE]
proof (chain)
picking this:
rt \<noteq> update rt dip (osn, kno, val, hops, nhip, {})
[PROOF STEP]
have "nsqn (update rt dip (osn, kno, val, hops, nhip, {})) dip = osn"
[PROOF STATE]
proof (prove)
using this:
rt \<noteq> update rt dip (osn, kno, val, hops, nhip, {})

goal (1 subgoal):
 1. nsqn (update rt dip (osn, kno, val, hops, nhip, {})) dip = osn
[PROOF STEP]
by (rule nsqn_update_changed_kno_val)
[PROOF STATE]
proof (state)
this:
nsqn (update rt dip (osn, kno, val, hops, nhip, {})) dip = osn

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
with \<open>dip\<in>vD(rt2 nhip)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD (rt2 nhip)
nsqn (update rt dip (osn, kno, val, hops, nhip, {})) dip = osn
[PROOF STEP]
have "nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) = osn"
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (rt2 nhip)
nsqn (update rt dip (osn, kno, val, hops, nhip, {})) dip = osn

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) = osn
[PROOF STEP]
by (simp add: kD_nsqn)
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) = osn

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) = osn

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
have "osn < sqn (rt2 nhip) dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. osn < sqn (rt2 nhip) dip
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
osn < sqn (rt2 nhip) dip

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
osn < sqn (rt2 nhip) dip

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
have "sqn (rt2 nhip) dip = nsqn\<^sub>r (the (rt2 nhip dip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn (rt2 nhip) dip = nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
unfolding nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn (rt2 nhip) dip = (if \<pi>\<^sub>4 (the (rt2 nhip dip)) = val \<or> \<pi>\<^sub>2 (the (rt2 nhip dip)) = 0 then \<pi>\<^sub>2 (the (rt2 nhip dip)) else \<pi>\<^sub>2 (the (rt2 nhip dip)) - 1)
[PROOF STEP]
using \<open>dip \<in> vD (rt2 nhip)\<close>
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (rt2 nhip)

goal (1 subgoal):
 1. sqn (rt2 nhip) dip = (if \<pi>\<^sub>4 (the (rt2 nhip dip)) = val \<or> \<pi>\<^sub>2 (the (rt2 nhip dip)) = 0 then \<pi>\<^sub>2 (the (rt2 nhip dip)) else \<pi>\<^sub>2 (the (rt2 nhip dip)) - 1)
[PROOF STEP]
by - (metis vD_flag_val proj2_eq_sqn proj4_eq_flag vD_iD_gives_kD(1))
[PROOF STATE]
proof (state)
this:
sqn (rt2 nhip) dip = nsqn\<^sub>r (the (rt2 nhip dip))

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
show "nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip))
                                                              < nsqn\<^sub>r (the (rt2 nhip dip))"
[PROOF STATE]
proof (prove)
using this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip))

goal:
No subgoals!
[PROOF STEP]
qed