[STATEMENT]
lemma LBex:
 "\<lbrakk> nqfree f; R.I f (x#xs); \<not>R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs \<rbrakk>
  \<Longrightarrow> \<exists>l\<in> LB f xs. l < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x
[PROOF STEP]
apply(induct f)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>nqfree TrueF; R.I TrueF (x # xs); \<not> R.I (inf\<^sub>- TrueF) xs; x \<notin> EQ TrueF xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 TrueF) \<and> 0 < c}. l < x
 2. \<lbrakk>nqfree FalseF; R.I FalseF (x # xs); \<not> R.I (inf\<^sub>- FalseF) xs; x \<notin> EQ FalseF xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 FalseF) \<and> 0 < c}. l < x
 3. \<And>xa. \<lbrakk>nqfree (Atom xa); R.I (Atom xa) (x # xs); \<not> R.I (inf\<^sub>- (Atom xa)) xs; x \<notin> EQ (Atom xa) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Atom xa)) \<and> 0 < c}. l < x
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (And f1 f2)) \<and> 0 < c}. l < x
 5. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Or f1 f2)) \<and> 0 < c}. l < x
 6. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>- (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Neg f)) \<and> 0 < c}. l < x
 7. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>- (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (ExQ f)) \<and> 0 < c}. l < x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>nqfree FalseF; R.I FalseF (x # xs); \<not> R.I (inf\<^sub>- FalseF) xs; x \<notin> EQ FalseF xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 FalseF) \<and> 0 < c}. l < x
 2. \<And>xa. \<lbrakk>nqfree (Atom xa); R.I (Atom xa) (x # xs); \<not> R.I (inf\<^sub>- (Atom xa)) xs; x \<notin> EQ (Atom xa) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Atom xa)) \<and> 0 < c}. l < x
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (And f1 f2)) \<and> 0 < c}. l < x
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Or f1 f2)) \<and> 0 < c}. l < x
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>- (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Neg f)) \<and> 0 < c}. l < x
 6. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>- (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (ExQ f)) \<and> 0 < c}. l < x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>nqfree (Atom xa); R.I (Atom xa) (x # xs); \<not> R.I (inf\<^sub>- (Atom xa)) xs; x \<notin> EQ (Atom xa) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Atom xa)) \<and> 0 < c}. l < x
 2. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (And f1 f2)) \<and> 0 < c}. l < x
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Or f1 f2)) \<and> 0 < c}. l < x
 4. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>- (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Neg f)) \<and> 0 < c}. l < x
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>- (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (ExQ f)) \<and> 0 < c}. l < x
[PROOF STEP]
apply(rename_tac a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>nqfree (Atom a); R.I (Atom a) (x # xs); \<not> R.I (inf\<^sub>- (Atom a)) xs; x \<notin> EQ (Atom a) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Atom a)) \<and> 0 < c}. l < x
 2. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (And f1 f2)) \<and> 0 < c}. l < x
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Or f1 f2)) \<and> 0 < c}. l < x
 4. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>- (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Neg f)) \<and> 0 < c}. l < x
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>- (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (ExQ f)) \<and> 0 < c}. l < x
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a x11 x12. \<lbrakk>nqfree (Atom a); R.I (Atom a) (x # xs); \<not> R.I (inf\<^sub>- (Atom a)) xs; x \<notin> EQ (Atom a) xs; a = Less x11 x12\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Atom a)) \<and> 0 < c}. l < x
 2. \<And>a x21 x22. \<lbrakk>nqfree (Atom a); R.I (Atom a) (x # xs); \<not> R.I (inf\<^sub>- (Atom a)) xs; x \<notin> EQ (Atom a) xs; a = Eq x21 x22\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Atom a)) \<and> 0 < c}. l < x
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (And f1 f2)) \<and> 0 < c}. l < x
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>- f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c}. l < x; \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c}. l < x; nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>- (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Or f1 f2)) \<and> 0 < c}. l < x
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>- (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (Neg f)) \<and> 0 < c}. l < x
 6. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>- f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}. l < x; nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>- (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> \<exists>l\<in>{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 (ExQ f)) \<and> 0 < c}. l < x
[PROOF STEP]
apply(auto simp add: depends\<^sub>R_def field_simps split:if_splits list.splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>f1 f2. \<lbrakk>\<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c) \<and> l < x; \<lbrakk>\<not> R.I (inf\<^sub>- f2) xs; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c) \<and> l < x; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; R.I f1 (x # xs); R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f1) xs\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> 0 < c) \<and> l < x
 2. \<And>f1 f2. \<lbrakk>\<lbrakk>\<not> R.I (inf\<^sub>- f1) xs; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c) \<and> l < x; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c) \<and> l < x; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; R.I f1 (x # xs); R.I f2 (x # xs); \<not> R.I (inf\<^sub>- f2) xs\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> 0 < c) \<and> l < x
 3. \<And>f1 f2. \<lbrakk>\<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c) \<and> l < x; \<lbrakk>R.I f2 (x # xs); \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c) \<and> l < x; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; \<not> R.I (inf\<^sub>- f1) xs; \<not> R.I (inf\<^sub>- f2) xs; R.I f1 (x # xs)\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> 0 < c) \<and> l < x
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>R.I f1 (x # xs); \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> 0 < c) \<and> l < x; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> 0 < c) \<and> l < x; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; \<not> R.I (inf\<^sub>- f1) xs; \<not> R.I (inf\<^sub>- f2) xs; R.I f2 (x # xs)\<rbrakk> \<Longrightarrow> \<exists>l. (\<exists>r c cs. l = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> 0 < c) \<and> l < x
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma UBex:
 "\<lbrakk> nqfree f; R.I f (x#xs); \<not>R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs \<rbrakk>
  \<Longrightarrow> \<exists>u\<in> UB f xs. x < u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> \<exists>u\<in>UB f xs. x < u
[PROOF STEP]
apply(induct f)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>nqfree TrueF; R.I TrueF (x # xs); \<not> R.I (inf\<^sub>+ TrueF) xs; x \<notin> EQ TrueF xs\<rbrakk> \<Longrightarrow> Bex (UB TrueF xs) ((<) x)
 2. \<lbrakk>nqfree FalseF; R.I FalseF (x # xs); \<not> R.I (inf\<^sub>+ FalseF) xs; x \<notin> EQ FalseF xs\<rbrakk> \<Longrightarrow> Bex (UB FalseF xs) ((<) x)
 3. \<And>xa. \<lbrakk>nqfree (Atom xa); R.I (Atom xa) (x # xs); \<not> R.I (inf\<^sub>+ (Atom xa)) xs; x \<notin> EQ (Atom xa) xs\<rbrakk> \<Longrightarrow> Bex (UB (Atom xa) xs) ((<) x)
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (And f1 f2) xs) ((<) x)
 5. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (Or f1 f2) xs) ((<) x)
 6. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>+ (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> Bex (UB (Neg f) xs) ((<) x)
 7. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>+ (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> Bex (UB (ExQ f) xs) ((<) x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>nqfree FalseF; R.I FalseF (x # xs); \<not> R.I (inf\<^sub>+ FalseF) xs; x \<notin> EQ FalseF xs\<rbrakk> \<Longrightarrow> Bex (UB FalseF xs) ((<) x)
 2. \<And>xa. \<lbrakk>nqfree (Atom xa); R.I (Atom xa) (x # xs); \<not> R.I (inf\<^sub>+ (Atom xa)) xs; x \<notin> EQ (Atom xa) xs\<rbrakk> \<Longrightarrow> Bex (UB (Atom xa) xs) ((<) x)
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (And f1 f2) xs) ((<) x)
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (Or f1 f2) xs) ((<) x)
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>+ (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> Bex (UB (Neg f) xs) ((<) x)
 6. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>+ (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> Bex (UB (ExQ f) xs) ((<) x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>nqfree (Atom xa); R.I (Atom xa) (x # xs); \<not> R.I (inf\<^sub>+ (Atom xa)) xs; x \<notin> EQ (Atom xa) xs\<rbrakk> \<Longrightarrow> Bex (UB (Atom xa) xs) ((<) x)
 2. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (And f1 f2) xs) ((<) x)
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (Or f1 f2) xs) ((<) x)
 4. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>+ (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> Bex (UB (Neg f) xs) ((<) x)
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>+ (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> Bex (UB (ExQ f) xs) ((<) x)
[PROOF STEP]
apply(rename_tac a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>nqfree (Atom a); R.I (Atom a) (x # xs); \<not> R.I (inf\<^sub>+ (Atom a)) xs; x \<notin> EQ (Atom a) xs\<rbrakk> \<Longrightarrow> Bex (UB (Atom a) xs) ((<) x)
 2. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (And f1 f2) xs) ((<) x)
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (Or f1 f2) xs) ((<) x)
 4. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>+ (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> Bex (UB (Neg f) xs) ((<) x)
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>+ (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> Bex (UB (ExQ f) xs) ((<) x)
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a x11 x12. \<lbrakk>nqfree (Atom a); R.I (Atom a) (x # xs); \<not> R.I (inf\<^sub>+ (Atom a)) xs; x \<notin> EQ (Atom a) xs; a = Less x11 x12\<rbrakk> \<Longrightarrow> Bex (UB (Atom a) xs) ((<) x)
 2. \<And>a x21 x22. \<lbrakk>nqfree (Atom a); R.I (Atom a) (x # xs); \<not> R.I (inf\<^sub>+ (Atom a)) xs; x \<notin> EQ (Atom a) xs; a = Eq x21 x22\<rbrakk> \<Longrightarrow> Bex (UB (Atom a) xs) ((<) x)
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (And f1 f2); R.I (And f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (And f1 f2)) xs; x \<notin> EQ (And f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (And f1 f2) xs) ((<) x)
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>nqfree f1; R.I f1 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs; x \<notin> EQ f1 xs\<rbrakk> \<Longrightarrow> Bex (UB f1 xs) ((<) x); \<lbrakk>nqfree f2; R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs; x \<notin> EQ f2 xs\<rbrakk> \<Longrightarrow> Bex (UB f2 xs) ((<) x); nqfree (Or f1 f2); R.I (Or f1 f2) (x # xs); \<not> R.I (inf\<^sub>+ (Or f1 f2)) xs; x \<notin> EQ (Or f1 f2) xs\<rbrakk> \<Longrightarrow> Bex (UB (Or f1 f2) xs) ((<) x)
 5. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (Neg f); R.I (Neg f) (x # xs); \<not> R.I (inf\<^sub>+ (Neg f)) xs; x \<notin> EQ (Neg f) xs\<rbrakk> \<Longrightarrow> Bex (UB (Neg f) xs) ((<) x)
 6. \<And>f. \<lbrakk>\<lbrakk>nqfree f; R.I f (x # xs); \<not> R.I (inf\<^sub>+ f) xs; x \<notin> EQ f xs\<rbrakk> \<Longrightarrow> Bex (UB f xs) ((<) x); nqfree (ExQ f); R.I (ExQ f) (x # xs); \<not> R.I (inf\<^sub>+ (ExQ f)) xs; x \<notin> EQ (ExQ f) xs\<rbrakk> \<Longrightarrow> Bex (UB (ExQ f) xs) ((<) x)
[PROOF STEP]
apply(auto simp add: depends\<^sub>R_def field_simps split:if_splits list.splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>f1 f2. \<lbrakk>\<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> c < 0) \<and> x < xa; \<lbrakk>\<not> R.I (inf\<^sub>+ f2) xs; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> c < 0) \<and> x < xa; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; R.I f1 (x # xs); R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f1) xs\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> c < 0) \<and> x < xa
 2. \<And>f1 f2. \<lbrakk>\<lbrakk>\<not> R.I (inf\<^sub>+ f1) xs; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> c < 0) \<and> x < xa; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> c < 0) \<and> x < xa; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; R.I f1 (x # xs); R.I f2 (x # xs); \<not> R.I (inf\<^sub>+ f2) xs\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> c < 0) \<and> x < xa
 3. \<And>f1 f2. \<lbrakk>\<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> c < 0) \<and> x < xa; \<lbrakk>R.I f2 (x # xs); \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> c < 0) \<and> x < xa; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; \<not> R.I (inf\<^sub>+ f1) xs; \<not> R.I (inf\<^sub>+ f2) xs; R.I f1 (x # xs)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> c < 0) \<and> x < xa
 4. \<And>f1 f2. \<lbrakk>\<lbrakk>R.I f1 (x # xs); \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f1) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<and> c < 0) \<and> x < xa; \<forall>r c cs. Eq r (c # cs) \<in> set (atoms\<^sub>0 f2) \<longrightarrow> x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> c = 0 \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> Less r (c # cs) \<in> set (atoms\<^sub>0 f2) \<and> c < 0) \<and> x < xa; \<forall>r c cs. x = (r - \<langle>cs,xs\<rangle>) / c \<longrightarrow> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f1) \<and> Eq r (c # cs) \<notin> set (atoms\<^sub>0 f2) \<or> c = 0; nqfree f1; nqfree f2; \<not> R.I (inf\<^sub>+ f1) xs; \<not> R.I (inf\<^sub>+ f2) xs; R.I f2 (x # xs)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>r c cs. xa = (r - \<langle>cs,xs\<rangle>) / c \<and> (Less r (c # cs) \<in> set (atoms\<^sub>0 f1) \<or> Less r (c # cs) \<in> set (atoms\<^sub>0 f2)) \<and> c < 0) \<and> x < xa
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_LB: "finite(LB f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}
[PROOF STEP]
have "LB f xs = (\<lambda>(r,cs). r + \<langle>cs,xs\<rangle>) ` set(lbounds(R.atoms\<^sub>0 f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c} = (\<lambda>(r, cs). r + \<langle>cs,xs\<rangle>) ` set (lbounds (atoms\<^sub>0 f))
[PROOF STEP]
by (force simp:set_lbounds image_def field_simps)
[PROOF STATE]
proof (state)
this:
{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c} = (\<lambda>(r, cs). r + \<langle>cs,xs\<rangle>) ` set (lbounds (atoms\<^sub>0 f))

goal (1 subgoal):
 1. finite {(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c} = (\<lambda>(r, cs). r + \<langle>cs,xs\<rangle>) ` set (lbounds (atoms\<^sub>0 f))

goal (1 subgoal):
 1. finite {(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {(r - \<langle>cs,xs\<rangle>) / c |r c cs. Less r (c # cs) \<in> set (atoms\<^sub>0 f) \<and> 0 < c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_UB: "finite(UB f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (UB f xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (UB f xs)
[PROOF STEP]
have "UB f xs = (\<lambda>(r,cs). r + \<langle>cs,xs\<rangle>) ` set(ubounds(R.atoms\<^sub>0 f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UB f xs = (\<lambda>(r, cs). r + \<langle>cs,xs\<rangle>) ` set (ubounds (atoms\<^sub>0 f))
[PROOF STEP]
by (force simp:set_ubounds image_def field_simps)
[PROOF STATE]
proof (state)
this:
UB f xs = (\<lambda>(r, cs). r + \<langle>cs,xs\<rangle>) ` set (ubounds (atoms\<^sub>0 f))

goal (1 subgoal):
 1. finite (UB f xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
UB f xs = (\<lambda>(r, cs). r + \<langle>cs,xs\<rangle>) ` set (ubounds (atoms\<^sub>0 f))

goal (1 subgoal):
 1. finite (UB f xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (UB f xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst_BNFs[simp]:
  "a \<in> Basic_BNFs.fsts (a,b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> Basic_BNFs.fsts (a, b)
[PROOF STEP]
using fsts.intros
[PROOF STATE]
proof (prove)
using this:
fst ?p \<in> Basic_BNFs.fsts ?p

goal (1 subgoal):
 1. a \<in> Basic_BNFs.fsts (a, b)
[PROOF STEP]
by auto


[STATEMENT]
lemma "\<not>pre_par c  \<Longrightarrow> pre c \<in> pre_set c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> pre_par c \<Longrightarrow> pre c \<in> pre_set c
[PROOF STEP]
by (induct c; simp)


[STATEMENT]
lemma pre_set:
  "pre c = \<Inter> (pre_set c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre c = \<Inter> (pre_set c)
[PROOF STEP]
by (induct c; fastforce)


[STATEMENT]
lemma pre_imp_pre_set:
  "s \<in> pre c \<Longrightarrow> a \<in> pre_set c \<Longrightarrow> s \<in> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> pre c; a \<in> pre_set c\<rbrakk> \<Longrightarrow> s \<in> a
[PROOF STEP]
by (simp add: pre_set)


[STATEMENT]
lemma weaken_pre_empty[simp]:
  "weaken_pre r {} = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weaken_pre r {} = r
[PROOF STEP]
by (induct r) auto


[STATEMENT]
lemma (in PolynRg) lcf_val_0:"lcf R S X \<zero> = \<zero>\<^bsub>S\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lcf R S X \<zero> = \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
by (simp add:lcf_def s_cf_def)


[STATEMENT]
lemma (in PolynRg) lcf_val:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero> \<rbrakk> \<Longrightarrow>
                    lcf R S X p = (snd (s_cf R S X p)) (fst (s_cf R S X p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> lcf R S X p = snd (s_cf R S X p) (fst (s_cf R S X p))
[PROOF STEP]
by (simp add:lcf_def)


[STATEMENT]
lemma (in PolynRg) lcf_mem:"p \<in> carrier R \<Longrightarrow> (lcf R S X p) \<in> carrier S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> lcf R S X p \<in> carrier S
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> lcf R S X p \<in> carrier S
[PROOF STEP]
apply (simp add:lcf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S
[PROOF STEP]
apply (cut_tac pol_coeff_mem[of "s_cf R S X p" "fst (s_cf R S X p)"],
          assumption,
        rule s_cf_pol_coeff, assumption, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) s_cf_expr0:"p \<in> carrier R \<Longrightarrow>
      pol_coeff S (s_cf R S X p) \<and>
      p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> pol_coeff S (s_cf R S X p) \<and> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p) \<and> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)
[PROOF STEP]
apply (simp add:s_cf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>) \<and> \<zero> = polyn_expr R X 0 (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> p = polyn_expr R X (fst (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)) (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<zero> \<in> carrier R; Subring R S; Ring S; p = \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>) \<and> \<zero> = polyn_expr R X 0 (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>) \<and> \<zero> = polyn_expr R X 0 (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> p = polyn_expr R X (fst (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)) (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply (rule conjI, simp add:pol_coeff_def, simp add:Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<zero> \<in> carrier R; Subring R S; Ring S; p = \<zero>\<rbrakk> \<Longrightarrow> \<zero> = polyn_expr R X 0 (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>) \<and> \<zero> = polyn_expr R X 0 (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> p = polyn_expr R X (fst (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)) (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply (simp add:polyn_expr_def,
        simp add:Subring_zero_ring_zero, simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>) \<and> \<zero> = polyn_expr R X 0 (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> p = polyn_expr R X (fst (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)) (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> p = polyn_expr R X (fst (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)) (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (rule someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (frule ex_polyn_expr[of p], erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (frule_tac c = c in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (frule_tac c = c and n = "c_max S c" in pol_coeff_le, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (subgoal_tac "p = polyn_expr R X (fst (c_max S c, snd c))
                                                  (c_max S c, snd c) \<and>
                     snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>",
        blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (c_max S c, snd c)) (c_max S c, snd c) \<and> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (rule conjI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; Subring R S; Ring S; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) (c_max S c, snd c)
 2. \<And>c. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (subst polyn_expr_short[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; Subring R S; Ring S; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c
 2. \<And>c. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (simp add:polyn_c_max)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; Subring R S; Ring S; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (rule coeff_max_nonzeroTr, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; Subring R S; Ring S; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst c. snd c j \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply (simp add:coeff_0_pol_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p \<in> carrier R; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pos_deg_nonzero:"\<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow>
                     p \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac s_cf_expr0[of p], (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
 2. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<in> carrier R
[PROOF STEP]
apply (frule pol_deg_eq_c_max[of p "s_cf R S X p"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); deg_n R S X p = c_max S (s_cf R S X p)\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
 2. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<in> carrier R
[PROOF STEP]
apply (simp, thin_tac "deg_n R S X p = c_max S (s_cf R S X p)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; 0 < c_max S (s_cf R S X p); pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
 2. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<in> carrier R
[PROOF STEP]
apply (simp add:c_max_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; 0 < (if \<forall>x\<le>fst (s_cf R S X p). snd (s_cf R S X p) x = \<zero>\<^bsub>S\<^esub> then 0 else n_max {j. j \<le> fst (s_cf R S X p) \<and> snd (s_cf R S X p) j \<noteq> \<zero>\<^bsub>S\<^esub>}); pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
 2. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<in> carrier R
[PROOF STEP]
apply (case_tac "\<forall>x\<le>fst (s_cf R S X p). snd (s_cf R S X p) x = \<zero>\<^bsub>S\<^esub> ", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; 0 < (if \<forall>x\<le>fst (s_cf R S X p). snd (s_cf R S X p) x = \<zero>\<^bsub>S\<^esub> then 0 else n_max {j. j \<le> fst (s_cf R S X p) \<and> snd (s_cf R S X p) j \<noteq> \<zero>\<^bsub>S\<^esub>}); pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); \<not> (\<forall>x\<le>fst (s_cf R S X p). snd (s_cf R S X p) x = \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
 2. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<in> carrier R
[PROOF STEP]
apply (thin_tac "0 < (if \<forall>x\<le>fst (s_cf R S X p). snd (s_cf R S X p) x = \<zero>\<^bsub>S\<^esub>
   then 0 else n_max
                {j. j \<le> fst (s_cf R S X p) \<and> snd (s_cf R S X p) j \<noteq> \<zero>\<^bsub>S\<^esub>})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); \<not> (\<forall>x\<le>fst (s_cf R S X p). snd (s_cf R S X p) x = \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
 2. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<in> carrier R
[PROOF STEP]
apply (simp add:coeff_0_pol_0[of "s_cf R S X p" "fst (s_cf R S X p)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> p \<in> carrier R
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) s_cf_expr:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
      pol_coeff S (s_cf R S X p) \<and>
      p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<and>
      (snd (s_cf R S X p)) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p) \<and> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<and> snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:s_cf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> p = polyn_expr R X (fst (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)) (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> snd (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>) (fst (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (rule someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule ex_polyn_expr[of p], erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule_tac c = c in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule_tac c = c and n = "c_max S c" in pol_coeff_le, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (subgoal_tac "p = polyn_expr R X (fst (c_max S c, snd c))
                                                  (c_max S c, snd c) \<and>
                     snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>",
        blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (c_max S c, snd c)) (c_max S c, snd c) \<and> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (rule conjI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) (c_max S c, snd c)
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (subst polyn_expr_short[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:polyn_c_max)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (rule coeff_max_nonzeroTr, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst c. snd c j \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:coeff_0_pol_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S x \<and> p = polyn_expr R X (fst x) x \<and> snd x (fst x) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) lcf_nonzero:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero> \<rbrakk> \<Longrightarrow>
                                          lcf R S X p \<noteq> \<zero>\<^bsub>S\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> lcf R S X p \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p) \<and> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<and> snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> lcf R S X p \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:lcf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) s_cf_deg:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                  deg_n R S X p = fst (s_cf R S X p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg_n R S X p = fst (s_cf R S X p)
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> deg_n R S X p = fst (s_cf R S X p)
[PROOF STEP]
apply (simp add:pol_deg_n[of p "s_cf R S X p" "fst (s_cf R S X p)"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done