[STATEMENT]
lemma nths_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> nths xs inds = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>inds. length xs \<le> i \<Longrightarrow> nths xs inds = []
[PROOF STEP]
apply (induct xs arbitrary: inds)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>inds. Ball inds ((\<le>) (length [])) \<Longrightarrow> nths [] inds = []
 2. \<And>a xs inds. \<lbrakk>\<And>inds. Ball inds ((\<le>) (length xs)) \<Longrightarrow> nths xs inds = []; Ball inds ((\<le>) (length (a # xs)))\<rbrakk> \<Longrightarrow> nths (a # xs) inds = []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs inds. \<lbrakk>\<And>inds. Ball inds ((\<le>) (length xs)) \<Longrightarrow> nths xs inds = []; Ball inds ((\<le>) (length (a # xs)))\<rbrakk> \<Longrightarrow> nths (a # xs) inds = []
[PROOF STEP]
apply (simp add: nths_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs inds. \<lbrakk>\<And>inds. Ball inds ((\<le>) (length xs)) \<Longrightarrow> nths xs inds = []; Ball inds ((\<le>) (Suc (length xs)))\<rbrakk> \<Longrightarrow> 0 \<notin> inds \<and> (0 \<notin> inds \<longrightarrow> nths xs {j. Suc j \<in> inds} = [])
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs inds. \<lbrakk>\<And>inds. \<forall>x\<in>inds. length xs \<le> x \<Longrightarrow> nths xs inds = []; \<forall>x\<in>inds. Suc (length xs) \<le> x; 0 \<notin> inds\<rbrakk> \<Longrightarrow> nths xs {j. Suc j \<in> inds} = []
[PROOF STEP]
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs inds. \<lbrakk>\<forall>x\<in>inds. Suc (length xs) \<le> x; 0 \<notin> inds; \<forall>x\<in>{j. Suc j \<in> inds}. length xs \<le> x \<Longrightarrow> nths xs {j. Suc j \<in> inds} = []\<rbrakk> \<Longrightarrow> nths xs {j. Suc j \<in> inds} = []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done