[STATEMENT]
lemma  cart_prod_fst:"x \<in> A \<times> B \<Longrightarrow> fst x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<times> B \<Longrightarrow> fst x \<in> A
[PROOF STEP]
by auto


[STATEMENT]
lemma  cart_prod_snd:"x \<in> A \<times> B \<Longrightarrow> snd x \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<times> B \<Longrightarrow> snd x \<in> B
[PROOF STEP]
by auto


[STATEMENT]
lemma cart_prod_split:"((x,y) \<in> A \<times> B) = (x \<in> A \<and> y \<in> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> A \<times> B) = (x \<in> A \<and> y \<in> B)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in PolynRg) P_mod_diffxxx3:"\<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>;
   maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y;
   f \<in> carrier R; gh \<in> carrier R \<times> carrier R;
   deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R'
                            (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh));
   deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R'
         (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f;
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
                                           (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh));
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
       (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh));
  rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh))
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh));
  P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a ((fst gh) \<cdot>\<^sub>r (snd gh))); 0 < m\<rbrakk> \<Longrightarrow>
  \<exists>gh1. gh1 \<in>carrier R \<times> carrier R \<and>
       (deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
           (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1))) \<and>
   P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) ((fst gh) \<plusminus> -\<^sub>a (fst gh1)) \<and>
       (deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
           (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le>
                                                              deg R S X f) \<and>
        P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) ((snd gh) \<plusminus> -\<^sub>a (snd gh1)) \<and>
        P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc m)\<^esup>)) (f \<plusminus> (-\<^sub>a ((fst gh1) \<cdot>\<^sub>r (snd gh1))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; gh \<in> carrier R \<times> carrier R; deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh \<cdot>\<^sub>r snd gh); 0 < m\<rbrakk> \<Longrightarrow> \<exists>gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1)
[PROOF STEP]
apply (cases gh)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; gh \<in> carrier R \<times> carrier R; deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh \<cdot>\<^sub>r snd gh); 0 < m; gh = (a, b)\<rbrakk> \<Longrightarrow> \<exists>gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1)
[PROOF STEP]
apply (simp del: npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; a \<in> carrier R \<and> b \<in> carrier R; deg R S X a \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a); deg R S X b + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) b); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) b); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b); 0 < m; gh = (a, b)\<rbrakk> \<Longrightarrow> \<exists>aa. aa \<in> carrier R \<and> (\<exists>ba. ba \<in> carrier R \<and> deg R S X aa \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) aa) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (a \<plusminus> -\<^sub>a aa) \<and> deg R S X ba + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) aa) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (b \<plusminus> -\<^sub>a ba) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a aa \<cdot>\<^sub>r ba))
[PROOF STEP]
apply (rename_tac g h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g h. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R \<and> h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); 0 < m; gh = (g, h)\<rbrakk> \<Longrightarrow> \<exists>a. a \<in> carrier R \<and> (\<exists>b. b \<in> carrier R \<and> deg R S X a \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (g \<plusminus> -\<^sub>a a) \<and> deg R S X b + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (h \<plusminus> -\<^sub>a b) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b))
[PROOF STEP]
apply (erule conjE,
        frule_tac g = g and h = h and f = f in P_mod_diffxxx2[of t R' Y],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g h. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); 0 < m; gh = (g, h); g \<in> carrier R; h \<in> carrier R; \<exists>g1 h1. g1 \<in> carrier R \<and> h1 \<in> carrier R \<and> deg R S X g1 \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (g \<plusminus> -\<^sub>a g1) \<and> deg R S X h1 + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g1) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (h \<plusminus> -\<^sub>a h1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a g1 \<cdot>\<^sub>r h1)\<rbrakk> \<Longrightarrow> \<exists>a. a \<in> carrier R \<and> (\<exists>b. b \<in> carrier R \<and> deg R S X a \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (g \<plusminus> -\<^sub>a a) \<and> deg R S X b + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) a) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (h \<plusminus> -\<^sub>a b) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_diffxxx4:"\<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>;
      maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R;
      gh \<in> carrier R \<times> carrier R;
      deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
            (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh));
   deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R'
                (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f;
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
        (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh));
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
        (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh));
  rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh))
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh));
  P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a ((fst gh) \<cdot>\<^sub>r (snd gh))); 0 < m\<rbrakk> \<Longrightarrow>
  (Hen\<^bsub>R S X t R' Y f \<^esub> m gh) \<in> carrier R \<times> carrier R  \<and> (deg R S X
     (fst (Hen\<^bsub>R S X t R' Y f \<^esub> m gh)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
          (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))
                                   (fst (Hen\<^bsub>R S X t R' Y f \<^esub> m gh)))) \<and>
  P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) ((fst gh) \<plusminus> -\<^sub>a (fst (Hen\<^bsub>R S X t R' Y f \<^esub> m gh))) \<and>
  (deg R S X (snd (Hen\<^bsub>R S X t R' Y f \<^esub> m gh)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
   (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))
        (fst (Hen\<^bsub>R S X t R' Y f \<^esub> m gh))) \<le>  deg R S X f) \<and>
  P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) ((snd gh) \<plusminus> -\<^sub>a (snd (Hen\<^bsub>R S X t R' Y f \<^esub> m gh))) \<and>
    P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc m)\<^esup>)) (f \<plusminus> (-\<^sub>a ((fst (Hen\<^bsub>R S X t R' Y f \<^esub> m gh)) \<cdot>\<^sub>r
             (snd (Hen\<^bsub>R S X t R' Y f \<^esub> m gh)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; gh \<in> carrier R \<times> carrier R; deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh \<cdot>\<^sub>r snd gh); 0 < m\<rbrakk> \<Longrightarrow> Hen\<^bsub> R S X t R' Y f\<^esub> m gh \<in> carrier R \<times> carrier R \<and> deg R S X (fst (Hen\<^bsub> R S X t R' Y f\<^esub> m gh)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hen\<^bsub> R S X t R' Y f\<^esub> m gh))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst (Hen\<^bsub> R S X t R' Y f\<^esub> m gh)) \<and> deg R S X (snd (Hen\<^bsub> R S X t R' Y f\<^esub> m gh)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hen\<^bsub> R S X t R' Y f\<^esub> m gh))) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd (Hen\<^bsub> R S X t R' Y f\<^esub> m gh)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hen\<^bsub> R S X t R' Y f\<^esub> m gh) \<cdot>\<^sub>r snd (Hen\<^bsub> R S X t R' Y f\<^esub> m gh))
[PROOF STEP]
apply (unfold Hensel_next_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; gh \<in> carrier R \<times> carrier R; deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh \<cdot>\<^sub>r snd gh); 0 < m\<rbrakk> \<Longrightarrow> (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1)) \<in> carrier R \<times> carrier R \<and> deg R S X (fst (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1))) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1)))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1))) \<and> deg R S X (snd (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1))) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1)))) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1)) \<cdot>\<^sub>r snd (SOME gh1. gh1 \<in> carrier R \<times> carrier R \<and> deg R S X (fst gh1) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst gh1) \<and> deg R S X (snd gh1) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh1)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd gh1) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh1 \<cdot>\<^sub>r snd gh1)))
[PROOF STEP]
apply (rule someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; gh \<in> carrier R \<times> carrier R; deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh \<cdot>\<^sub>r snd gh); 0 < m\<rbrakk> \<Longrightarrow> \<exists>a. a \<in> carrier R \<times> carrier R \<and> deg R S X (fst a) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst a)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst a) \<and> deg R S X (snd a) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst a)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd a) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst a \<cdot>\<^sub>r snd a)
 2. \<And>x. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; gh \<in> carrier R \<times> carrier R; deg R S X (fst gh) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); deg R S X (snd gh) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst gh)) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd gh)); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (f \<plusminus> -\<^sub>a fst gh \<cdot>\<^sub>r snd gh); 0 < m; x \<in> carrier R \<times> carrier R \<and> deg R S X (fst x) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst x)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst x) \<and> deg R S X (snd x) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst x)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd x) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst x \<cdot>\<^sub>r snd x)\<rbrakk> \<Longrightarrow> x \<in> carrier R \<times> carrier R \<and> deg R S X (fst x) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst x)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (fst gh \<plusminus> -\<^sub>a fst x) \<and> deg R S X (snd x) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst x)) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S m\<^esup>)) (snd gh \<plusminus> -\<^sub>a snd x) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (f \<plusminus> -\<^sub>a fst x \<cdot>\<^sub>r snd x)
[PROOF STEP]
apply (rule P_mod_diffxxx3, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) fst_xxx:" \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t);
   \<forall>(n::nat). (F n) \<in> carrier R \<times> carrier R;
   \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a (fst (F (Suc m))))\<rbrakk> \<Longrightarrow>
       P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a (fst (F n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F 0))
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (drule_tac x = 0 in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; F 0 \<in> carrier R \<times> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F 0))
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (frule cart_prod_fst[of "F 0" "carrier R" "carrier R"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; F 0 \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F 0))
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; F 0 \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) \<zero>
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (frule_tac x = 0 in spec,
       frule_tac x = n in spec,
       drule_tac x = "Suc n" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (frule_tac x = "F 0" in cart_prod_fst[of _ "carrier R" "carrier R"],
        frule_tac x = "F n" in cart_prod_fst[of _ "carrier R" "carrier R"],
        frule_tac x = "F (Suc n)" in cart_prod_fst[of _ "carrier R"
                                                             "carrier R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F m) \<plusminus> -\<^sub>a fst (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (drule_tac x = n in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (frule_tac p = "fst (F 0) \<plusminus> -\<^sub>a (fst (F n))" and
                 q = "fst (F n) \<plusminus> -\<^sub>a (fst (F (Suc n)))" in
       P_mod_add[of  "S \<diamondsuit>\<^sub>p t"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)))\<rbrakk> \<Longrightarrow> fst (F 0) \<plusminus> -\<^sub>a fst (F n) \<in> carrier R
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)))\<rbrakk> \<Longrightarrow> fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)) \<in> carrier R
 3. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n))
 4. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)))
 5. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n))); P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n) \<plusminus> (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n))))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+, rule aGroup.ag_mOp_closed,
       assumption+)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n))); P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n) \<plusminus> (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n))))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (frule_tac x = "fst (F n)" in aGroup.ag_mOp_closed, assumption+,
       frule_tac x = "fst (F (Suc n))" in aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; fst (F 0) \<in> carrier R; fst (F n) \<in> carrier R; fst (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n))); P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F n) \<plusminus> (fst (F n) \<plusminus> -\<^sub>a fst (F (Suc n)))); -\<^sub>a fst (F n) \<in> carrier R; -\<^sub>a fst (F (Suc n)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (fst (F 0) \<plusminus> -\<^sub>a fst (F (Suc n)))
[PROOF STEP]
apply (simp add:aGroup.pOp_assocTr41[of "R", THEN sym],
       simp add:aGroup.pOp_assocTr42[of "R"],
       simp add:aGroup.ag_l_inv1,
       simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) snd_xxx:"\<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>;
   ideal S (S \<diamondsuit>\<^sub>p t);  \<forall>(n::nat). (F n) \<in> carrier R \<times> carrier R;
  \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a (snd (F (Suc m))))\<rbrakk> \<Longrightarrow>
   P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a (snd (F n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F 0))
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (drule_tac x = 0 in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; F 0 \<in> carrier R \<times> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F 0))
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (frule cart_prod_snd[of "F 0" "carrier R" "carrier R"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; F 0 \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F 0))
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; F 0 \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) \<zero>
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>n. F n \<in> carrier R \<times> carrier R; \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (frule_tac x = 0 in spec,
       frule_tac x = n in spec,
       drule_tac x = "Suc n" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (frule_tac x = "F 0" in cart_prod_snd[of _ "carrier R" "carrier R"],
        frule_tac x = "F n" in cart_prod_snd[of _ "carrier R" "carrier R"],
        frule_tac x = "F (Suc n)" in cart_prod_snd[of _ "carrier R"
                                                             "carrier R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); \<forall>m. P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F m) \<plusminus> -\<^sub>a snd (F (Suc m))); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (drule_tac x = n in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (frule_tac p = "snd (F 0) \<plusminus> -\<^sub>a (snd (F n))" and
                 q = "snd (F n) \<plusminus> -\<^sub>a (snd (F (Suc n)))" in
       P_mod_add[of  "S \<diamondsuit>\<^sub>p t"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)))\<rbrakk> \<Longrightarrow> snd (F 0) \<plusminus> -\<^sub>a snd (F n) \<in> carrier R
 2. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)))\<rbrakk> \<Longrightarrow> snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)) \<in> carrier R
 3. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n))
 4. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)))
 5. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n))); P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n) \<plusminus> (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n))))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+, rule aGroup.ag_mOp_closed,
       assumption+)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n))); P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n) \<plusminus> (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n))))\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (frule_tac x = "snd (F n)" in aGroup.ag_mOp_closed, assumption+,
       frule_tac x = "snd (F (Suc n))" in aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; ideal S (S \<diamondsuit>\<^sub>p t); Subring R S; Ring S; aGroup R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n)); F 0 \<in> carrier R \<times> carrier R; F n \<in> carrier R \<times> carrier R; F (Suc n) \<in> carrier R \<times> carrier R; snd (F 0) \<in> carrier R; snd (F n) \<in> carrier R; snd (F (Suc n)) \<in> carrier R; P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n))); P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F n) \<plusminus> (snd (F n) \<plusminus> -\<^sub>a snd (F (Suc n)))); -\<^sub>a snd (F n) \<in> carrier R; -\<^sub>a snd (F (Suc n)) \<in> carrier R\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (snd (F 0) \<plusminus> -\<^sub>a snd (F (Suc n)))
[PROOF STEP]
apply (simp add:aGroup.pOp_assocTr41[of "R", THEN sym],
       simp add:aGroup.pOp_assocTr42[of "R"],
       simp add:aGroup.ag_l_inv1,
       simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done