[STATEMENT]
lemma Qw_cmpser:"\<lbrakk>Group G; w_cmpser G (Suc n) f \<rbrakk> \<Longrightarrow> 
                               Gchain n (Qw_cmpser G f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; w_cmpser G (Suc n) f\<rbrakk> \<Longrightarrow> Gchain n (Qw_cmpser G f)
[PROOF STEP]
apply (simp add:Gchain_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; w_cmpser G (Suc n) f\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. Group (Qw_cmpser G f l)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; w_cmpser G (Suc n) f; l \<le> n\<rbrakk> \<Longrightarrow> Group (Qw_cmpser G f l)
[PROOF STEP]
apply (simp  add:Qw_cmpser_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; w_cmpser G (Suc n) f; l \<le> n\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (simp add:w_cmpser_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; d_gchain G (Suc n) f \<and> (\<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)); l \<le> n\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; d_gchain G (Suc n) f; \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (simp add:d_gchain_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (cut_tac c = l in subsetD[of "{i. i \<le> n}" "{i. i \<le> (Suc n)}"], 
        rule subsetI, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); l \<in> {i. i \<le> Suc n}\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (frule_tac H = "f l" in Group.Group_Gp[of "G"],
        frule_tac a = l in forall_spec, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l)\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (frule_tac G = "Gp G (f l)" and N = "f (Suc l)" in Group.Group_Qg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l)\<rbrakk> \<Longrightarrow> \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)
 2. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l); Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l); Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done