[STATEMENT]
lemma i_set_cont_min_eq: "i_set_cont = i_set_cont_min"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_set_cont = i_set_cont_min
[PROOF STEP]
apply (rule set_eqI, rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> i_set_cont \<Longrightarrow> x \<in> i_set_cont_min
 2. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply (rename_tac x, rule_tac a=x in i_set_cont.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. x \<in> i_set_cont \<Longrightarrow> x \<in> i_set_cont
 2. \<And>x n. \<lbrakk>x \<in> i_set_cont; x = [n\<dots>]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont_min
 3. \<And>x n. \<lbrakk>x \<in> i_set_cont; x = [\<dots>n]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont_min
 4. \<And>x n d. \<lbrakk>x \<in> i_set_cont; x = [n\<dots>,d]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont_min
 5. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply (fastforce simp: iIN_0_iTILL_conv[symmetric])+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply (rename_tac x, rule_tac a=x in i_set_cont_min.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont_min
 2. \<And>x n. \<lbrakk>x \<in> i_set_cont_min; x = [n\<dots>]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont
 3. \<And>x n d. \<lbrakk>x \<in> i_set_cont_min; x = [n\<dots>,d]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done