[STATEMENT]
lemma (in PolynRg) decompos_p:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow>
                p = (ldeg_p R S X d p) \<plusminus> (hdeg_p R S X (Suc d) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p = ldeg_p R S X d p \<plusminus> hdeg_p R S X (Suc d) p
[PROOF STEP]
apply (frule scf_d_pol[of  p "Suc d"], assumption+, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d \<and> p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> p = ldeg_p R S X d p \<plusminus> hdeg_p R S X (Suc d) p
[PROOF STEP]
apply (cut_tac subring, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> p = ldeg_p R S X d p \<plusminus> hdeg_p R S X (Suc d) p
[PROOF STEP]
apply (cut_tac polyn_Suc[of d "scf_d R S X p (Suc d)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X (Suc d) (Suc d, snd (scf_d R S X p (Suc d))) = polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>\<rbrakk> \<Longrightarrow> p = ldeg_p R S X d p \<plusminus> hdeg_p R S X (Suc d) p
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> Suc d \<le> fst (scf_d R S X p (Suc d))
[PROOF STEP]
apply (simp only:ldeg_p_def hdeg_p_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X (Suc d) (Suc d, snd (scf_d R S X p (Suc d))) = polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> Suc d \<le> fst (scf_d R S X p (Suc d))
[PROOF STEP]
apply (rotate_tac -1, drule sym, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = polyn_expr R X (Suc d) (Suc d, snd (scf_d R S X p (Suc d)))\<rbrakk> \<Longrightarrow> p = polyn_expr R X (Suc d) (Suc d, snd (scf_d R S X p (Suc d)))
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> Suc d \<le> fst (scf_d R S X p (Suc d))
[PROOF STEP]
apply (thin_tac "polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus>
     snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R (Suc d)\<^esup> =
     polyn_expr R X (Suc d) (Suc d, snd (scf_d R S X p (Suc d)))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> p = polyn_expr R X (Suc d) (Suc d, snd (scf_d R S X p (Suc d)))
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); Subring R S; fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> Suc d \<le> fst (scf_d R S X p (Suc d))
[PROOF STEP]
apply (simp add:polyn_expr_split[of "Suc d" "scf_d R S X p (Suc d)"],
        simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_ldeg_p:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk>  \<Longrightarrow>
                deg R S X (ldeg_p R S X d p) \<le> an d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> deg R S X (ldeg_p R S X d p) \<le> an d
[PROOF STEP]
apply (cut_tac subring,
       frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S\<rbrakk> \<Longrightarrow> deg R S X (ldeg_p R S X d p) \<le> an d
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p = \<zero>\<rbrakk> \<Longrightarrow> deg R S X (ldeg_p R S X d p) \<le> an d
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (ldeg_p R S X d p) \<le> an d
[PROOF STEP]
apply (simp add:ldeg_p_zero, simp add:deg_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (ldeg_p R S X d p) \<le> an d
[PROOF STEP]
apply (frule scf_d_pol[of p "Suc d"], assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> deg R S X (ldeg_p R S X d p) \<le> an d
[PROOF STEP]
apply (simp only:ldeg_p_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X d (scf_d R S X p (Suc d))) \<le> an d
[PROOF STEP]
apply (case_tac "polyn_expr R X d (scf_d R S X p (Suc d)) = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) = \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X d (scf_d R S X p (Suc d))) \<le> an d
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X d (scf_d R S X p (Suc d))) \<le> an d
[PROOF STEP]
apply (simp add:deg_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X d (scf_d R S X p (Suc d))) \<le> an d
[PROOF STEP]
apply (simp add:deg_an)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; an (deg_n R S X p) \<le> an (Suc d); Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X d (scf_d R S X p (Suc d))) \<le> an d
[PROOF STEP]
apply (simp add:ale_natle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg_n R S X p \<le> Suc d; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X d (scf_d R S X p (Suc d))) \<le> an d
[PROOF STEP]
apply (cut_tac pol_deg_le_n1[of "polyn_expr R X d (scf_d R S X p (Suc d))"
       "scf_d R S X p (Suc d)" d], simp add:deg_def ale_natle)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg_n R S X p \<le> Suc d; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<in> carrier R
 2. \<lbrakk>p \<in> carrier R; deg_n R S X p \<le> Suc d; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X p (Suc d))
 3. \<lbrakk>p \<in> carrier R; deg_n R S X p \<le> Suc d; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> d \<le> fst (scf_d R S X p (Suc d))
 4. \<lbrakk>p \<in> carrier R; deg_n R S X p \<le> Suc d; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); polyn_expr R X d (scf_d R S X p (Suc d)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) = polyn_expr R X d (scf_d R S X p (Suc d))
[PROOF STEP]
apply (rule polyn_mem, assumption+, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_minus_eq:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                    deg_n R S X (-\<^sub>a p) = deg_n 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 (-\<^sub>a p) = deg_n R S X p
[PROOF STEP]
apply (cut_tac subring,
       cut_tac ring_is_ag,
       frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; aGroup R; Ring S\<rbrakk> \<Longrightarrow> deg_n R S X (-\<^sub>a p) = deg_n R S X p
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; aGroup R; Ring S; aGroup R\<rbrakk> \<Longrightarrow> deg_n R S X (-\<^sub>a p) = deg_n R S X p
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption, (erule conjE)+,
        frule polyn_minus_m_cf[of "s_cf R S X p" "fst (s_cf R S X p)"], simp,
        drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p))) = deg_n R S X p
[PROOF STEP]
apply (frule_tac x = p in aGroup.ag_mOp_closed, assumption+,
        frule m_cf_pol_coeff [of "s_cf R S X p"],
        frule pol_deg_n[of "-\<^sub>a p" "m_cf S (s_cf R S X p)"
              "fst (s_cf R S X p)"], assumption,
        simp add:m_cf_len, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; -\<^sub>a p \<in> carrier R; pol_coeff S (m_cf S (s_cf R S X p))\<rbrakk> \<Longrightarrow> snd (m_cf S (s_cf R S X p)) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; -\<^sub>a p \<in> carrier R; pol_coeff S (m_cf S (s_cf R S X p)); deg_n R S X (-\<^sub>a p) = fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p))) = deg_n R S X p
[PROOF STEP]
apply (simp add:m_cf_def,
        frule pol_coeff_mem[of "s_cf R S X p" "fst (s_cf R S X p)"], simp,
        frule Ring.ring_is_ag[of S])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) j); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) j) \<in> carrier R; pol_coeff S (fst (s_cf R S X p), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) j); snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; aGroup S\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; -\<^sub>a p \<in> carrier R; pol_coeff S (m_cf S (s_cf R S X p)); deg_n R S X (-\<^sub>a p) = fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p))) = deg_n R S X p
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) j); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; polyn_expr R X (fst (s_cf R S X p)) (fst (s_cf R S X p), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) j) \<in> carrier R; pol_coeff S (fst (s_cf R S X p), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) j); snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; aGroup S; -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p)) = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; -\<^sub>a p \<in> carrier R; pol_coeff S (m_cf S (s_cf R S X p)); deg_n R S X (-\<^sub>a p) = fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p))) = deg_n R S X p
[PROOF STEP]
apply (frule aGroup.ag_inv_inv[THEN sym,
          of S "snd (s_cf R S X p) (fst (s_cf R S X p))"], assumption,
        simp add:aGroup.ag_inv_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; pol_coeff S (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>; -\<^sub>a p = polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p; -\<^sub>a p \<in> carrier R; pol_coeff S (m_cf S (s_cf R S X p)); deg_n R S X (-\<^sub>a p) = fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p))) = deg_n R S X p
[PROOF STEP]
apply (drule sym, simp, simp add:s_cf_deg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_minus_eq1:"p \<in> carrier R \<Longrightarrow>
                       deg R S X (-\<^sub>a p) = deg R S X p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> deg R S X (-\<^sub>a p) = deg R S X p
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> deg R S X (-\<^sub>a p) = deg R S X p
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; aGroup R; p = \<zero>\<rbrakk> \<Longrightarrow> deg R S X (-\<^sub>a p) = deg R S X p
 2. \<lbrakk>p \<in> carrier R; aGroup R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (-\<^sub>a p) = deg R S X p
[PROOF STEP]
apply (simp add:aGroup.ag_inv_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; aGroup R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (-\<^sub>a p) = deg R S X p
[PROOF STEP]
apply (frule deg_minus_eq[of p], assumption+,
       frule aGroup.ag_inv_inj[of "R" "p" "\<zero>"], assumption,
       simp add:ring_zero, assumption, simp add:aGroup.ag_inv_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; aGroup R; p \<noteq> \<zero>; deg_n R S X (-\<^sub>a p) = deg_n R S X p; -\<^sub>a p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (-\<^sub>a p) = deg R S X p
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of R p], assumption,
       simp add:deg_an)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) ldeg_p_pOp:"\<lbrakk>p \<in> carrier R; q \<in> carrier R;
      deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d)\<rbrakk> \<Longrightarrow>
      (ldeg_p R S X d p) \<plusminus>\<^bsub>R\<^esub> (ldeg_p R S X d q) =
                              ldeg_p R S X d (p \<plusminus>\<^bsub>R\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d)\<rbrakk> \<Longrightarrow> ldeg_p R S X d p \<plusminus> ldeg_p R S X d q = ldeg_p R S X d (p \<plusminus> q)
[PROOF STEP]
apply (simp add:ldeg_p_def,
       cut_tac ring_is_ag, cut_tac subring, frule subring_Ring[of S],
       frule scf_d_pol[of p "Suc d"], assumption+,
       frule scf_d_pol[of q "Suc d"], assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); fst (scf_d R S X q (Suc d)) = Suc d; q = polyn_expr R X (Suc d) (scf_d R S X q (Suc d))\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (frule polyn_add1[of "scf_d R S X p (Suc d)" "scf_d R S X q (Suc d)"],
       assumption+,
       rotate_tac -2, drule sym,
       frule aGroup.ag_pOp_closed[of "R" "p" "q"], assumption+,
       frule polyn_deg_add4 [of p q "Suc d"], assumption+,
       rotate_tac -5, drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); polyn_expr R X (fst (scf_d R S X p (Suc d))) (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X (fst (scf_d R S X q (Suc d))) (scf_d R S X q (Suc d)) = polyn_expr R X (max (fst (scf_d R S X p (Suc d))) (fst (scf_d R S X q (Suc d)))) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) \<in> carrier R; deg R S X (polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) (Suc d))
[PROOF STEP]
apply (rotate_tac 4, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = p \<plusminus> q\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (rotate_tac -1, drule sym,
       frule scf_d_pol[of "p \<plusminus> q" "Suc d"], assumption+, (erule conjE)+,
       frule box_equation[of "p \<plusminus> q" "polyn_expr R X (Suc d)
        (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))"
        "polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))"], assumption+,
       thin_tac "p \<plusminus> q =
        polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (frule add_cf_pol_coeff[of "scf_d R S X p (Suc d)"
                   "scf_d R S X q (Suc d)"],  assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (frule pol_expr_unique2[of "add_cf S (scf_d R S X p (Suc d))
       (scf_d R S X q (Suc d))" "scf_d R S X (p \<plusminus> q) (Suc d)"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); (polyn_expr R X (fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (fst (scf_d R S X (p \<plusminus> q) (Suc d))) (scf_d R S X (p \<plusminus> q) (Suc d))) = (\<forall>j\<le>fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))). snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j)\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (subst add_cf_len[of "scf_d R S X p (Suc d)" "scf_d R S X q (Suc d)"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> max (fst (scf_d R S X p (Suc d))) (fst (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); (polyn_expr R X (fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (fst (scf_d R S X (p \<plusminus> q) (Suc d))) (scf_d R S X (p \<plusminus> q) (Suc d))) = (\<forall>j\<le>fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))). snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j)\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (thin_tac "polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p",
        thin_tac "polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q",
        thin_tac "p \<plusminus> q = polyn_expr R X (Suc d)
          (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))",
        thin_tac "polyn_expr R X (Suc d)
          (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) =
           polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> max (fst (scf_d R S X p (Suc d))) (fst (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); (polyn_expr R X (fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (fst (scf_d R S X (p \<plusminus> q) (Suc d))) (scf_d R S X (p \<plusminus> q) (Suc d))) = (\<forall>j\<le>fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))). snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j)\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); (polyn_expr R X (fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (fst (scf_d R S X (p \<plusminus> q) (Suc d))) (scf_d R S X (p \<plusminus> q) (Suc d))) = (\<forall>j\<le>fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))). snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j)\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (thin_tac "polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p",
        thin_tac "polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q",
        thin_tac "p \<plusminus> q = polyn_expr R X (Suc d)
          (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); (polyn_expr R X (fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (fst (scf_d R S X (p \<plusminus> q) (Suc d))) (scf_d R S X (p \<plusminus> q) (Suc d))) = (\<forall>j\<le>fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))). snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j)\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (simp add:add_cf_len,
       thin_tac "polyn_expr R X (Suc d)
      (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) =
     polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (subst  polyn_expr_short[of "scf_d R S X p (Suc d)" d], assumption,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> polyn_expr R X d (d, snd (scf_d R S X p (Suc d))) \<plusminus> polyn_expr R X d (scf_d R S X q (Suc d)) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (subst  polyn_expr_short[of "scf_d R S X q (Suc d)" d], assumption,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> polyn_expr R X d (d, snd (scf_d R S X p (Suc d))) \<plusminus> polyn_expr R X d (d, snd (scf_d R S X q (Suc d))) = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (subst polyn_add_n[of d "snd (scf_d R S X p (Suc d))"
               "snd (scf_d R S X q (Suc d))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (d, snd (scf_d R S X p (Suc d)))
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (d, snd (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>j. (snd (scf_d R S X p (Suc d)) j \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) j) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) d = polyn_expr R X d (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (simp add:split_pol_coeff, simp add:split_pol_coeff,
        subst polyn_expr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>j. (snd (scf_d R S X p (Suc d)) j \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) j) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) d = \<Sigma>\<^sub>e R (\<lambda>j. snd (scf_d R S X (p \<plusminus> q) (Suc d)) j \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) d
[PROOF STEP]
apply (rule aGroup.nsum_eq, assumption+,
        rule allI, rule impI,
        frule_tac j = j in pol_coeff_mem[of "scf_d R S X p (Suc d)"],
               simp,
        frule_tac j = j in pol_coeff_mem[of "scf_d R S X q (Suc d)"],
               simp,
        cut_tac Ring, rule Ring.ring_tOp_closed, assumption+,
        rule Ring.mem_subring_mem_ring[of R S], assumption+,
        frule Ring.ring_is_ag[of S], rule aGroup.ag_pOp_closed[of S],
               assumption+,
        rule Ring.npClose, assumption, simp add:X_mem_R)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> \<forall>j\<le>d. snd (scf_d R S X (p \<plusminus> q) (Suc d)) j \<cdot>\<^sub>r X^\<^bsup>R j\<^esup> \<in> carrier R
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> \<forall>j\<le>d. (snd (scf_d R S X p (Suc d)) j \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) j) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup> = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>
[PROOF STEP]
apply (rule allI, rule impI,
        frule_tac j = j in pol_coeff_mem[of "scf_d R S X (p \<plusminus> q) (Suc d)"],
        simp, cut_tac Ring,
        subst Ring.ring_tOp_closed, assumption,
        rule Ring.mem_subring_mem_ring[of R S], assumption+,
        rule Ring.npClose, assumption, simp add:X_mem_R,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> \<forall>j\<le>d. (snd (scf_d R S X p (Suc d)) j \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) j) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup> = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>
[PROOF STEP]
apply (rule allI, rule impI,
        drule_tac a = j in forall_spec, simp,
        thin_tac " pol_coeff S
          (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; j \<le> d; snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> (snd (scf_d R S X p (Suc d)) j \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) j) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup> = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>
[PROOF STEP]
apply (simp add:add_cf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done