[STATEMENT]
lemma kth_obs_stable: assumes \<open>is_kth_obs \<pi> l j\<close> \<open>k < l\<close> shows \<open>\<exists> i. is_kth_obs \<pi> k i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> l j
k < l

goal (1 subgoal):
 1. \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
proof (induction \<open>l\<close> arbitrary: \<open>j\<close> rule: less_induct )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
case (less l j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < l; is_kth_obs \<pi> ?y1 ?j1; k < ?y1\<rbrakk> \<Longrightarrow> \<exists>a. is_kth_obs \<pi> k a
is_kth_obs \<pi> l j
k < l

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
have cardl: \<open>card (obs_ids \<pi> \<inter> {..<j}) = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<j}) = l
[PROOF STEP]
using less is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 < l; is_kth_obs \<pi> ?y1 ?j1; k < ?y1\<rbrakk> \<Longrightarrow> \<exists>a. is_kth_obs \<pi> k a
is_kth_obs \<pi> l j
k < l
is_kth_obs ?\<pi> ?k ?i = (card (obs_ids ?\<pi> \<inter> {..<?i}) = ?k \<and> local.att (?\<pi> ?i) \<noteq> None)

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<j}) = l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (obs_ids \<pi> \<inter> {..<j}) = l

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (obs_ids \<pi> \<inter> {..<j}) = l
[PROOF STEP]
obtain i where  ex: \<open>i \<in> obs_ids \<pi> \<inter> {..<j}\<close> (is \<open>?P i\<close>)
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<j}) = l

goal (1 subgoal):
 1. (\<And>i. i \<in> obs_ids \<pi> \<inter> {..<j} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less(3)
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<j}) = l
k < l

goal (1 subgoal):
 1. (\<And>i. i \<in> obs_ids \<pi> \<inter> {..<j} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis card.empty empty_iff less_irrefl subsetI subset_antisym zero_diff zero_less_diff)
[PROOF STATE]
proof (state)
this:
i \<in> obs_ids \<pi> \<inter> {..<j}

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
have bound: \<open>\<forall> i. i \<in> obs_ids \<pi> \<inter> {..<j} \<longrightarrow> i \<le> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i \<in> obs_ids \<pi> \<inter> {..<j} \<longrightarrow> i \<le> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<in> obs_ids \<pi> \<inter> {..<j} \<longrightarrow> i \<le> j

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
let \<open>?i\<close> = \<open>GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
have *: \<open>?i < j\<close> \<open>?i \<in> obs_ids \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) < j &&& (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<in> obs_ids \<pi>
[PROOF STEP]
using GreatestI_nat[of \<open>?P\<close> \<open>i\<close> \<open>j\<close>] ex bound
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in> obs_ids \<pi> \<inter> {..<j}; \<And>y. y \<in> obs_ids \<pi> \<inter> {..<j} \<Longrightarrow> y \<le> j\<rbrakk> \<Longrightarrow> (GREATEST a. a \<in> obs_ids \<pi> \<inter> {..<j}) \<in> obs_ids \<pi> \<inter> {..<j}
i \<in> obs_ids \<pi> \<inter> {..<j}
\<forall>i. i \<in> obs_ids \<pi> \<inter> {..<j} \<longrightarrow> i \<le> j

goal (1 subgoal):
 1. (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) < j &&& (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<in> obs_ids \<pi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) < j
(GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<in> obs_ids \<pi>

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
have **: \<open>\<forall> i. i \<in> obs_ids \<pi> \<and> i<j \<longrightarrow> i \<le> ?i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i \<in> obs_ids \<pi> \<and> i < j \<longrightarrow> i \<le> (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
using Greatest_le_nat[of \<open>?P\<close> _ \<open>j\<close>] ex bound
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k \<in> obs_ids \<pi> \<inter> {..<j}; \<And>y. y \<in> obs_ids \<pi> \<inter> {..<j} \<Longrightarrow> y \<le> j\<rbrakk> \<Longrightarrow> ?k \<le> (GREATEST a. a \<in> obs_ids \<pi> \<inter> {..<j})
i \<in> obs_ids \<pi> \<inter> {..<j}
\<forall>i. i \<in> obs_ids \<pi> \<inter> {..<j} \<longrightarrow> i \<le> j

goal (1 subgoal):
 1. \<forall>i. i \<in> obs_ids \<pi> \<and> i < j \<longrightarrow> i \<le> (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<in> obs_ids \<pi> \<and> i < j \<longrightarrow> i \<le> (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j})

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
have \<open>(obs_ids \<pi> \<inter> {..<?i}) \<union> {?i} = obs_ids \<pi> \<inter> {..<j}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} = obs_ids \<pi> \<inter> {..<j}
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<subseteq> obs_ids \<pi> \<inter> {..<j}
 2. obs_ids \<pi> \<inter> {..<j} \<subseteq> obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j) \<in> obs_ids \<pi>
 2. (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j) < j
 3. \<And>x. \<lbrakk>x \<in> obs_ids \<pi>; x < (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)\<rbrakk> \<Longrightarrow> x < j
 4. \<And>x. \<lbrakk>x \<in> obs_ids \<pi>; x < j; x \<noteq> (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)\<rbrakk> \<Longrightarrow> x < (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)
[PROOF STEP]
using *[simplified]
[PROOF STATE]
proof (prove)
using this:
(GREATEST i. i \<in> obs_ids \<pi> \<and> i < j) < j
(GREATEST i. i \<in> obs_ids \<pi> \<and> i < j) \<in> obs_ids \<pi>

goal (4 subgoals):
 1. (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j) \<in> obs_ids \<pi>
 2. (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j) < j
 3. \<And>x. \<lbrakk>x \<in> obs_ids \<pi>; x < (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)\<rbrakk> \<Longrightarrow> x < j
 4. \<And>x. \<lbrakk>x \<in> obs_ids \<pi>; x < j; x \<noteq> (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)\<rbrakk> \<Longrightarrow> x < (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> obs_ids \<pi>; x < j; x \<noteq> (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)\<rbrakk> \<Longrightarrow> x < (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)
[PROOF STEP]
using **[simplified]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i \<in> obs_ids \<pi> \<and> i < j \<longrightarrow> i \<le> (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> obs_ids \<pi>; x < j; x \<noteq> (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)\<rbrakk> \<Longrightarrow> x < (GREATEST i. i \<in> obs_ids \<pi> \<and> i < j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} = obs_ids \<pi> \<inter> {..<j}

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} = obs_ids \<pi> \<inter> {..<j}

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
have \<open>?i \<notin> (obs_ids \<pi> \<inter> {..<?i})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<notin> obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<notin> obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} = obs_ids \<pi> \<inter> {..<j}
(GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<notin> obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}
[PROOF STEP]
have \<open>Suc (card (obs_ids \<pi> \<inter> {..<?i})) = l\<close>
[PROOF STATE]
proof (prove)
using this:
obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} = obs_ids \<pi> \<inter> {..<j}
(GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<notin> obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}

goal (1 subgoal):
 1. Suc (card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}})) = l
[PROOF STEP]
using cardl
[PROOF STATE]
proof (prove)
using this:
obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} \<union> {GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}} = obs_ids \<pi> \<inter> {..<j}
(GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<notin> obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}
card (obs_ids \<pi> \<inter> {..<j}) = l

goal (1 subgoal):
 1. Suc (card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}})) = l
[PROOF STEP]
by (metis Un_empty_right Un_insert_right card_insert_disjoint finite_Int finite_lessThan)
[PROOF STATE]
proof (state)
this:
Suc (card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}})) = l

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
hence \<open>card (obs_ids \<pi> \<inter> {..<?i}) = l - 1\<close>
[PROOF STATE]
proof (prove)
using this:
Suc (card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}})) = l

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}) = l - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}) = l - 1

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
hence iko: \<open>is_kth_obs \<pi> (l - 1) ?i\<close>
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}) = l - 1

goal (1 subgoal):
 1. is_kth_obs \<pi> (l - 1) (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
using *(2)
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}}) = l - 1
(GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j}) \<in> obs_ids \<pi>

goal (1 subgoal):
 1. is_kth_obs \<pi> (l - 1) (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
unfolding is_kth_obs_def obs_ids_def
[PROOF STATE]
proof (prove)
using this:
card ({k. local.att (\<pi> k) \<noteq> None} \<inter> {..<GREATEST i. i \<in> {k. local.att (\<pi> k) \<noteq> None} \<inter> {..<j}}) = l - 1
(GREATEST i. i \<in> {k. local.att (\<pi> k) \<noteq> None} \<inter> {..<j}) \<in> {k. local.att (\<pi> k) \<noteq> None}

goal (1 subgoal):
 1. card ({k. local.att (\<pi> k) \<noteq> None} \<inter> {..<GREATEST i. i \<in> {k. local.att (\<pi> k) \<noteq> None} \<inter> {..<j}}) = l - 1 \<and> local.att (\<pi> (GREATEST i. i \<in> {k. local.att (\<pi> k) \<noteq> None} \<inter> {..<j})) \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> (l - 1) (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j})

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
have ll: \<open>l - 1 < l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l - 1 < l
[PROOF STEP]
by (metis One_nat_def diff_Suc_less less.prems(2) not_gr0 not_less0)
[PROOF STATE]
proof (state)
this:
l - 1 < l

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
note IV=less(1)[OF ll iko]
[PROOF STATE]
proof (state)
this:
k < l - 1 \<Longrightarrow> \<exists>a. is_kth_obs \<pi> k a

goal (1 subgoal):
 1. \<And>x j. \<lbrakk>\<And>y j. \<lbrakk>y < x; is_kth_obs \<pi> y j; k < y\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k); is_kth_obs \<pi> x j; k < x\<rbrakk> \<Longrightarrow> Ex (is_kth_obs \<pi> k)
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
 2. \<not> ?P \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
assume \<open>k < l - 1\<close>
[PROOF STATE]
proof (state)
this:
k < l - 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
 2. \<not> ?P \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
k < l - 1

goal (1 subgoal):
 1. \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
using IV
[PROOF STATE]
proof (prove)
using this:
k < l - 1
k < l - 1 \<Longrightarrow> \<exists>a. is_kth_obs \<pi> k a

goal (1 subgoal):
 1. \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>i. is_kth_obs \<pi> k i

goal (1 subgoal):
 1. \<not> k < l - 1 \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k < l - 1 \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
assume \<open>\<not> k < l - 1\<close>
[PROOF STATE]
proof (state)
this:
\<not> k < l - 1

goal (1 subgoal):
 1. \<not> k < l - 1 \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
hence \<open>k = l - 1\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> k < l - 1

goal (1 subgoal):
 1. k = l - 1
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<not> k < l - 1
\<lbrakk>?y1 < l; is_kth_obs \<pi> ?y1 ?j1; k < ?y1\<rbrakk> \<Longrightarrow> \<exists>a. is_kth_obs \<pi> k a
is_kth_obs \<pi> l j
k < l

goal (1 subgoal):
 1. k = l - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = l - 1

goal (1 subgoal):
 1. \<not> k < l - 1 \<Longrightarrow> \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
k = l - 1

goal (1 subgoal):
 1. \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
using iko
[PROOF STATE]
proof (prove)
using this:
k = l - 1
is_kth_obs \<pi> (l - 1) (GREATEST i. i \<in> obs_ids \<pi> \<inter> {..<j})

goal (1 subgoal):
 1. \<exists>i. is_kth_obs \<pi> k i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i. is_kth_obs \<pi> k i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i. is_kth_obs \<pi> k i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kth_obs_mono: assumes \<open>is_kth_obs \<pi> k i\<close> \<open>is_kth_obs \<pi> l j\<close> \<open>k < l\<close> shows \<open>i < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> i < j\<close>
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
hence \<open>{..<j} \<subseteq> {..<i}\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i < j

goal (1 subgoal):
 1. {..<j} \<subseteq> {..<i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{..<j} \<subseteq> {..<i}

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
hence \<open>obs_ids \<pi> \<inter> {..<j} \<subseteq> obs_ids \<pi> \<inter> {..<i}\<close>
[PROOF STATE]
proof (prove)
using this:
{..<j} \<subseteq> {..<i}

goal (1 subgoal):
 1. obs_ids \<pi> \<inter> {..<j} \<subseteq> obs_ids \<pi> \<inter> {..<i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
obs_ids \<pi> \<inter> {..<j} \<subseteq> obs_ids \<pi> \<inter> {..<i}

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
obs_ids \<pi> \<inter> {..<j} \<subseteq> obs_ids \<pi> \<inter> {..<i}

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
have \<open>finite (obs_ids \<pi> \<inter> {..<i})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (obs_ids \<pi> \<inter> {..<i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (obs_ids \<pi> \<inter> {..<i})

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
obs_ids \<pi> \<inter> {..<j} \<subseteq> obs_ids \<pi> \<inter> {..<i}
finite (obs_ids \<pi> \<inter> {..<i})
[PROOF STEP]
have \<open>card (obs_ids \<pi> \<inter> {..<j}) \<le> card (obs_ids \<pi> \<inter> {..<i})\<close>
[PROOF STATE]
proof (prove)
using this:
obs_ids \<pi> \<inter> {..<j} \<subseteq> obs_ids \<pi> \<inter> {..<i}
finite (obs_ids \<pi> \<inter> {..<i})

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<j}) \<le> card (obs_ids \<pi> \<inter> {..<i})
[PROOF STEP]
by (metis card_mono)
[PROOF STATE]
proof (state)
this:
card (obs_ids \<pi> \<inter> {..<j}) \<le> card (obs_ids \<pi> \<inter> {..<i})

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<j}) \<le> card (obs_ids \<pi> \<inter> {..<i})

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<j}) \<le> card (obs_ids \<pi> \<inter> {..<i})
is_kth_obs \<pi> k i
is_kth_obs \<pi> l j
k < l

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<j}) \<le> card (obs_ids \<pi> \<inter> {..<i})
card (obs_ids \<pi> \<inter> {..<i}) = k \<and> local.att (\<pi> i) \<noteq> None
card (obs_ids \<pi> \<inter> {..<j}) = l \<and> local.att (\<pi> j) \<noteq> None
k < l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kth_obs_le_iff: assumes \<open>is_kth_obs \<pi> k i\<close> \<open>is_kth_obs \<pi> l j\<close>  shows \<open>k < l \<longleftrightarrow> i < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k < l) = (i < j)
[PROOF STEP]
by (metis assms kth_obs_unique kth_obs_mono not_less_iff_gr_or_eq)


[STATEMENT]
lemma ret_obs_all_obs: assumes path: \<open>is_path \<pi>\<close> and iki: \<open>is_kth_obs \<pi> k i\<close> and ret: \<open>\<pi> i = return\<close> and kl: \<open>k < l\<close> obtains j where \<open>is_kth_obs \<pi> l j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. is_kth_obs \<pi> l j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>j. is_kth_obs \<pi> l j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using kl iki ret
[PROOF STATE]
proof (prove)
using this:
k < l
is_kth_obs \<pi> k i
\<pi> i = local.return

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (induction \<open>l - k\<close> arbitrary: \<open>k\<close> \<open>i\<close> rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (less k i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>l - ?k1 < l - k; ?k1 < l; is_kth_obs \<pi> ?k1 ?i1; \<pi> ?i1 = local.return\<rbrakk> \<Longrightarrow> thesis
k < l
is_kth_obs \<pi> k i
\<pi> i = local.return

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note kl = \<open>k < l\<close>
[PROOF STATE]
proof (state)
this:
k < l

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note iki = \<open>is_kth_obs \<pi> k i\<close>
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> k i

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note ret = \<open>\<pi> i = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> i = local.return

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have card: \<open>card (obs_ids \<pi> \<inter> {..<i}) = k\<close> and att_ret: \<open>att return \<noteq> None\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = k &&& local.att local.return \<noteq> None
[PROOF STEP]
using iki ret
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k i
\<pi> i = local.return

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = k &&& local.att local.return \<noteq> None
[PROOF STEP]
unfolding is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<i}) = k \<and> local.att (\<pi> i) \<noteq> None
\<pi> i = local.return

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = k &&& local.att local.return \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (obs_ids \<pi> \<inter> {..<i}) = k
local.att local.return \<noteq> None

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have rets: \<open>\<pi> (Suc i) = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc i) = local.return
[PROOF STEP]
using path ret term_path_stable
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> i = local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return

goal (1 subgoal):
 1. \<pi> (Suc i) = local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (Suc i) = local.return

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence attsuc: \<open>att (\<pi> (Suc i)) \<noteq> None\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc i) = local.return

goal (1 subgoal):
 1. local.att (\<pi> (Suc i)) \<noteq> None
[PROOF STEP]
using att_ret
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc i) = local.return
local.att local.return \<noteq> None

goal (1 subgoal):
 1. local.att (\<pi> (Suc i)) \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.att (\<pi> (Suc i)) \<noteq> None

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence *: \<open>i \<in> obs_ids \<pi>\<close>
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi> (Suc i)) \<noteq> None

goal (1 subgoal):
 1. i \<in> obs_ids \<pi>
[PROOF STEP]
using att_ret ret
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi> (Suc i)) \<noteq> None
local.att local.return \<noteq> None
\<pi> i = local.return

goal (1 subgoal):
 1. i \<in> obs_ids \<pi>
[PROOF STEP]
unfolding obs_ids_def
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi> (Suc i)) \<noteq> None
local.att local.return \<noteq> None
\<pi> i = local.return

goal (1 subgoal):
 1. i \<in> {k. local.att (\<pi> k) \<noteq> None}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> obs_ids \<pi>

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>{..< Suc i} = insert i {..<i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..<Suc i} = insert i {..<i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{..<Suc i} = insert i {..<i}

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence a: \<open>obs_ids \<pi> \<inter> {..< Suc i} = insert i (obs_ids \<pi> \<inter> {..<i})\<close>
[PROOF STATE]
proof (prove)
using this:
{..<Suc i} = insert i {..<i}

goal (1 subgoal):
 1. obs_ids \<pi> \<inter> {..<Suc i} = insert i (obs_ids \<pi> \<inter> {..<i})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
{..<Suc i} = insert i {..<i}
i \<in> obs_ids \<pi>

goal (1 subgoal):
 1. obs_ids \<pi> \<inter> {..<Suc i} = insert i (obs_ids \<pi> \<inter> {..<i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
obs_ids \<pi> \<inter> {..<Suc i} = insert i (obs_ids \<pi> \<inter> {..<i})

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have b: \<open>i \<notin> obs_ids \<pi> \<inter> {..<i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<notin> obs_ids \<pi> \<inter> {..<i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<notin> obs_ids \<pi> \<inter> {..<i}

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>finite (obs_ids \<pi> \<inter> {..<i})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (obs_ids \<pi> \<inter> {..<i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (obs_ids \<pi> \<inter> {..<i})

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>card (obs_ids \<pi> \<inter> {..<Suc i}) = Suc k\<close>
[PROOF STATE]
proof (prove)
using this:
finite (obs_ids \<pi> \<inter> {..<i})

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<Suc i}) = Suc k
[PROOF STEP]
by (metis card card_insert_disjoint a b)
[PROOF STATE]
proof (state)
this:
card (obs_ids \<pi> \<inter> {..<Suc i}) = Suc k

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence iksuc: \<open>is_kth_obs \<pi> (Suc k) (Suc i)\<close>
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<Suc i}) = Suc k

goal (1 subgoal):
 1. is_kth_obs \<pi> (Suc k) (Suc i)
[PROOF STEP]
using attsuc
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<Suc i}) = Suc k
local.att (\<pi> (Suc i)) \<noteq> None

goal (1 subgoal):
 1. is_kth_obs \<pi> (Suc k) (Suc i)
[PROOF STEP]
unfolding is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<Suc i}) = Suc k
local.att (\<pi> (Suc i)) \<noteq> None

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<Suc i}) = Suc k \<and> local.att (\<pi> (Suc i)) \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> (Suc k) (Suc i)

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have suckl: \<open>Suc k \<le> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k \<le> l
[PROOF STEP]
using kl
[PROOF STATE]
proof (prove)
using this:
k < l

goal (1 subgoal):
 1. Suc k \<le> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc k \<le> l

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note less
[PROOF STATE]
proof (state)
this:
\<lbrakk>l - ?k1 < l - k; ?k1 < l; is_kth_obs \<pi> ?k1 ?i1; \<pi> ?i1 = local.return\<rbrakk> \<Longrightarrow> thesis
k < l
is_kth_obs \<pi> k i
\<pi> i = local.return

goal (1 subgoal):
 1. \<And>k i. \<lbrakk>\<And>ka i. \<lbrakk>l - ka < l - k; ka < l; is_kth_obs \<pi> ka i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>l - ?k1 < l - k; ?k1 < l; is_kth_obs \<pi> ?k1 ?i1; \<pi> ?i1 = local.return\<rbrakk> \<Longrightarrow> thesis
k < l
is_kth_obs \<pi> k i
\<pi> i = local.return

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases \<open>Suc k < l\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; Suc k < l\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; \<not> Suc k < l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume skl: \<open>Suc k < l\<close>
[PROOF STATE]
proof (state)
this:
Suc k < l

goal (2 subgoals):
 1. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; Suc k < l\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; \<not> Suc k < l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from less(1)[OF _ skl iksuc rets] skl
[PROOF STATE]
proof (chain)
picking this:
l - Suc k < l - k \<Longrightarrow> thesis
Suc k < l
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
l - Suc k < l - k \<Longrightarrow> thesis
Suc k < l

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

goal (1 subgoal):
 1. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; \<not> Suc k < l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; \<not> Suc k < l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<not> Suc k < l\<close>
[PROOF STATE]
proof (state)
this:
\<not> Suc k < l

goal (1 subgoal):
 1. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; \<not> Suc k < l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>Suc k = l\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> Suc k < l

goal (1 subgoal):
 1. Suc k = l
[PROOF STEP]
using suckl
[PROOF STATE]
proof (prove)
using this:
\<not> Suc k < l
Suc k \<le> l

goal (1 subgoal):
 1. Suc k = l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc k = l

goal (1 subgoal):
 1. \<lbrakk>\<And>k i. \<lbrakk>l - k < l - k; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return\<rbrakk> \<Longrightarrow> thesis; k < l; is_kth_obs \<pi> k i; \<pi> i = local.return; \<not> Suc k < l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
Suc k = l

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using iksuc that
[PROOF STATE]
proof (prove)
using this:
Suc k = l
is_kth_obs \<pi> (Suc k) (Suc i)
is_kth_obs \<pi> l ?j1 \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_kth_obs_missing_cs: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and iki: \<open>is_kth_obs \<pi> k i\<close> and not_in_\<pi>': \<open>\<not>(\<exists>i'. is_kth_obs \<pi>' k i')\<close>  obtains  l j where \<open>is_kth_obs \<pi> l j\<close> \<open>\<not> (\<exists> j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence all_in_\<pi>': \<open>\<forall> l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists> j' . cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> thesis

goal (1 subgoal):
 1. \<forall>l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<not> thesis
\<lbrakk>is_kth_obs \<pi> ?l1 ?j1; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> ?j1 = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<forall>l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. \<lbrakk>\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
[PROOF STEP]
obtain i' where csi: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. (\<And>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
is_path \<pi>
is_path \<pi>'
is_kth_obs \<pi> k i
\<nexists>i'. is_kth_obs \<pi>' k i'

goal (1 subgoal):
 1. (\<And>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. \<lbrakk>\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>att(\<pi>' i') \<noteq> None\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. local.att (\<pi>' i') \<noteq> None
[PROOF STEP]
using iki
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> k i

goal (1 subgoal):
 1. local.att (\<pi>' i') \<noteq> None
[PROOF STEP]
by (metis is_kth_obs_def last_cs)
[PROOF STATE]
proof (state)
this:
local.att (\<pi>' i') \<noteq> None

goal (1 subgoal):
 1. \<lbrakk>\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.att (\<pi>' i') \<noteq> None
[PROOF STEP]
obtain k' where ik': \<open>is_kth_obs \<pi>' k' i'\<close>
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi>' i') \<noteq> None

goal (1 subgoal):
 1. (\<And>k'. is_kth_obs \<pi>' k' i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis not_none_is_obs)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi>' k' i'

goal (1 subgoal):
 1. \<lbrakk>\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence kk': \<open>k' < k\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' k' i'

goal (1 subgoal):
 1. k' < k
[PROOF STEP]
using not_in_\<pi>' kth_obs_stable
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' k' i'
\<nexists>i'. is_kth_obs \<pi>' k i'
\<lbrakk>is_kth_obs ?\<pi> ?l ?j; ?k < ?l\<rbrakk> \<Longrightarrow> \<exists>i. is_kth_obs ?\<pi> ?k i

goal (1 subgoal):
 1. k' < k
[PROOF STEP]
by (auto, metis not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
k' < k

goal (1 subgoal):
 1. \<lbrakk>\<And>l j. \<lbrakk>is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases \<open>\<pi> i = return\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<pi> i = local.return \<Longrightarrow> False
 2. \<pi> i \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<pi> i \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> i \<noteq> local.return

goal (2 subgoals):
 1. \<pi> i = local.return \<Longrightarrow> False
 2. \<pi> i \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return

goal (1 subgoal):
 1. False
[PROOF STEP]
using kk' ik' csi iki
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return
k' < k
is_kth_obs \<pi>' k' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> k i

goal (1 subgoal):
 1. False
[PROOF STEP]
proof (induction \<open>k\<close> arbitrary: \<open>i\<close> \<open>i'\<close> \<open>k'\<close> )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < 0; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> 0 i\<rbrakk> \<Longrightarrow> False
 2. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<pi> i \<noteq> local.return
k' < 0
is_kth_obs \<pi>' k' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> 0 i

goal (2 subgoals):
 1. \<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < 0; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> 0 i\<rbrakk> \<Longrightarrow> False
 2. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return
k' < 0
is_kth_obs \<pi>' k' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> 0 i

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

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Suc k i i' k')
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<pi> ?i1 \<noteq> local.return; ?k'1 < k; is_kth_obs \<pi>' ?k'1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; is_kth_obs \<pi> k ?i1\<rbrakk> \<Longrightarrow> False
\<pi> i \<noteq> local.return
k' < Suc k
is_kth_obs \<pi>' k' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> (Suc k) i

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<pi> ?i1 \<noteq> local.return; ?k'1 < k; is_kth_obs \<pi>' ?k'1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; is_kth_obs \<pi> k ?i1\<rbrakk> \<Longrightarrow> False
\<pi> i \<noteq> local.return
k' < Suc k
is_kth_obs \<pi>' k' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> (Suc k) i
[PROOF STEP]
obtain j where ikj: \<open>is_kth_obs \<pi> k j\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<pi> ?i1 \<noteq> local.return; ?k'1 < k; is_kth_obs \<pi>' ?k'1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; is_kth_obs \<pi> k ?i1\<rbrakk> \<Longrightarrow> False
\<pi> i \<noteq> local.return
k' < Suc k
is_kth_obs \<pi>' k' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> (Suc k) i

goal (1 subgoal):
 1. (\<And>j. is_kth_obs \<pi> k j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis kth_obs_stable lessI)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> k j

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_kth_obs \<pi> k j
[PROOF STEP]
obtain j' where csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k j

goal (1 subgoal):
 1. (\<And>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using all_in_\<pi>'
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k j
\<forall>l j. is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. (\<And>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>att(\<pi>' j') \<noteq> None\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. local.att (\<pi>' j') \<noteq> None
[PROOF STEP]
using ikj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
is_kth_obs \<pi> k j

goal (1 subgoal):
 1. local.att (\<pi>' j') \<noteq> None
[PROOF STEP]
by (metis is_kth_obs_def last_cs)
[PROOF STATE]
proof (state)
this:
local.att (\<pi>' j') \<noteq> None

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.att (\<pi>' j') \<noteq> None
[PROOF STEP]
obtain k2 where ik2: \<open>is_kth_obs \<pi>' k2 j'\<close>
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi>' j') \<noteq> None

goal (1 subgoal):
 1. (\<And>k2. is_kth_obs \<pi>' k2 j' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis not_none_is_obs)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi>' k2 j'

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ji: \<open>j < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < i
[PROOF STEP]
using kth_obs_mono [OF ikj \<open>is_kth_obs \<pi> (Suc k) i\<close>]
[PROOF STATE]
proof (prove)
using this:
k < Suc k \<Longrightarrow> j < i

goal (1 subgoal):
 1. j < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence nretj: \<open>\<pi> j \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. \<pi> j \<noteq> local.return
[PROOF STEP]
using Suc(2) term_path_stable less_imp_le path(1)
[PROOF STATE]
proof (prove)
using this:
j < i
\<pi> i \<noteq> local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return
?x < ?y \<Longrightarrow> ?x \<le> ?y
is_path \<pi>

goal (1 subgoal):
 1. \<pi> j \<noteq> local.return
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> j \<noteq> local.return

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ji': \<open>j' < i'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j' < i'
[PROOF STEP]
using cs_order[OF path _ _ nretj, of \<open>j'\<close> \<open>i\<close> \<open>i'\<close>] csj \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close>  ji
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; j < i\<rbrakk> \<Longrightarrow> j' < i'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
j < i

goal (1 subgoal):
 1. j' < i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j' < i'

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>k2 \<noteq> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k2 \<noteq> k'
[PROOF STEP]
using ik2 Suc(4) ji' kth_obs_unique[of \<open>\<pi>'\<close> \<open>k'\<close> \<open>i'\<close> \<open>j'\<close>]
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' k2 j'
is_kth_obs \<pi>' k' i'
j' < i'
\<lbrakk>is_kth_obs \<pi>' k' i'; is_kth_obs \<pi>' k' j'\<rbrakk> \<Longrightarrow> i' = j'

goal (1 subgoal):
 1. k2 \<noteq> k'
[PROOF STEP]
by (metis less_irrefl)
[PROOF STATE]
proof (state)
this:
k2 \<noteq> k'

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence k2k': \<open>k2 < k'\<close>
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> k'

goal (1 subgoal):
 1. k2 < k'
[PROOF STEP]
using kth_obs_mono[OF \<open>is_kth_obs \<pi>' k' i'\<close> ik2] ji'
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> k'
k' < k2 \<Longrightarrow> i' < j'
j' < i'

goal (1 subgoal):
 1. k2 < k'
[PROOF STEP]
by (metis not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
k2 < k'

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence k2k: \<open>k2 < k\<close>
[PROOF STATE]
proof (prove)
using this:
k2 < k'

goal (1 subgoal):
 1. k2 < k
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
k2 < k'
\<lbrakk>\<pi> ?i1 \<noteq> local.return; ?k'1 < k; is_kth_obs \<pi>' ?k'1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; is_kth_obs \<pi> k ?i1\<rbrakk> \<Longrightarrow> False
\<pi> i \<noteq> local.return
k' < Suc k
is_kth_obs \<pi>' k' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> (Suc k) i

goal (1 subgoal):
 1. k2 < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k2 < k

goal (1 subgoal):
 1. \<And>k i i' k'. \<lbrakk>\<And>i i' k'. \<lbrakk>\<pi> i \<noteq> local.return; k' < k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> k i\<rbrakk> \<Longrightarrow> False; \<pi> i \<noteq> local.return; k' < Suc k; is_kth_obs \<pi>' k' i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> (Suc k) i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from Suc.IH[OF nretj k2k ik2 csj ikj]
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<pi> i = local.return \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> i = local.return \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<pi> i = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> i = local.return

goal (1 subgoal):
 1. \<pi> i = local.return \<Longrightarrow> False
[PROOF STEP]
hence reti': \<open>\<pi>' i' = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> i = local.return

goal (1 subgoal):
 1. \<pi>' i' = local.return
[PROOF STEP]
by (metis csi last_cs)
[PROOF STATE]
proof (state)
this:
\<pi>' i' = local.return

goal (1 subgoal):
 1. \<pi> i = local.return \<Longrightarrow> False
[PROOF STEP]
from ret_obs_all_obs[OF path(2) ik' reti' kk', of \<open>False\<close>] not_in_\<pi>'
[PROOF STATE]
proof (chain)
picking this:
(\<And>j. is_kth_obs \<pi>' k j \<Longrightarrow> False) \<Longrightarrow> False
\<nexists>i'. is_kth_obs \<pi>' k i'
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>j. is_kth_obs \<pi>' k j \<Longrightarrow> False) \<Longrightarrow> False
\<nexists>i'. is_kth_obs \<pi>' k i'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed