[STATEMENT]
lemma seq_Lam_Arr_implies:
    shows "\<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
proof (induct U arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>seq [t] []; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam
 2. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show "\<And>t. \<lbrakk>seq [t] []; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>seq [t] []; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>seq [?t] []; \<Lambda>.is_Lam ?t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
fix u U t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume ind: "\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (state)
this:
\<lbrakk>seq [?t] U; \<Lambda>.is_Lam ?t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume uU: "seq [t] (u # U)"
[PROOF STATE]
proof (state)
this:
seq [t] (u # U)

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume t: "\<Lambda>.is_Lam t"
[PROOF STATE]
proof (state)
this:
\<Lambda>.is_Lam t

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show "set (u # U) \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
have "\<Lambda>.is_Lam u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Lambda>.is_Lam u
[PROOF STEP]
by (metis Trg_last_Src_hd_eqI \<Lambda>.Src.simps(1-2,4-5) \<Lambda>.Trg.simps(2) \<Lambda>.is_App_def
            \<Lambda>.is_Beta_def \<Lambda>.is_Lam_def \<Lambda>.is_Var_def \<Lambda>.lambda.disc(9) \<Lambda>.lambda.exhaust_disc
            last_ConsL list.sel(1) t uU)
[PROOF STATE]
proof (state)
this:
\<Lambda>.is_Lam u

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Lambda>.is_Lam u

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
have "set U \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
proof (cases "U = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. U = [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
 2. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show "U = [] \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U = [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U = [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume U: "U \<noteq> []"
[PROOF STATE]
proof (state)
this:
U \<noteq> []

goal (1 subgoal):
 1. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
have "seq [u] U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq [u] U
[PROOF STEP]
by (metis U append_Cons arr_append_imp_seq not_Cons_self2 self_append_conv2
                seqE uU)
[PROOF STATE]
proof (state)
this:
seq [u] U

goal (1 subgoal):
 1. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
seq [u] U

goal (1 subgoal):
 1. set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
using ind calculation
[PROOF STATE]
proof (prove)
using this:
seq [u] U
\<lbrakk>seq [?t] U; \<Lambda>.is_Lam ?t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
\<Lambda>.is_Lam u

goal (1 subgoal):
 1. set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set U \<subseteq> Collect \<Lambda>.is_Lam

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Lambda>.is_Lam u
set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Lambda>.is_Lam u
set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (u # U) \<subseteq> Collect \<Lambda>.is_Lam

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (u # U) \<subseteq> Collect \<Lambda>.is_Lam

goal:
No subgoals!
[PROOF STEP]
qed