[STATEMENT]
lemma closed_nlistsI:
  "closed S f \<Longrightarrow> closed (nlists n S) (map2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed S f \<Longrightarrow> closed (nlists n S) (map2 f)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed S f \<Longrightarrow> closed (nlists n S) (map2 f)
[PROOF STEP]
apply (unfold closed_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists 0 S. \<forall>y\<in>nlists 0 S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists 0 S
 2. \<And>n. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S\<rbrakk> \<Longrightarrow> \<forall>x\<in>nlists (Suc n) S. \<forall>y\<in>nlists (Suc n) S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists (Suc n) S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S\<rbrakk> \<Longrightarrow> \<forall>x\<in>nlists (Suc n) S. \<forall>y\<in>nlists (Suc n) S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists (Suc n) S
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; x \<in> nlists (Suc n) S; y \<in> nlists (Suc n) S\<rbrakk> \<Longrightarrow> x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists (Suc n) S
[PROOF STEP]
apply (simp add: in_nlists_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; \<exists>y\<in>S. \<exists>ys\<in>nlists n S. x = y # ys; \<exists>ya\<in>S. \<exists>ys\<in>nlists n S. y = ya # ys\<rbrakk> \<Longrightarrow> \<exists>ya\<in>S. \<exists>ys\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y = ya # ys
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y ya yb ys ysa. \<lbrakk>\<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; ya \<in> S; yb \<in> S; ys \<in> nlists n S; ysa \<in> nlists n S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. \<exists>ysb\<in>nlists n S. ya # ys [\<squnion>\<^bsub>f\<^esub>] (yb # ysa) = y # ysb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done