[STATEMENT]
lemma (in Corps) ring_n_prod_primesTr:"\<lbrakk>0 < n; distinct_pds K n P;
 ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow>
 \<forall>j \<le> n.(\<nu>\<^bsub>K (P j)\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) =
                   (\<nu>\<^bsub>K (P j)\<^esub>) (mIg\<^bsub>K n P I\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (simp add:mgenerator1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j) = (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (simp add:value_mI_gen1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); j \<le> n\<rbrakk> \<Longrightarrow> (\<nu>\<^bsub>K P j\<^esub>) (Zl_mI K P I j) = LI K (\<nu>\<^bsub>K P j\<^esub>) I
[PROOF STEP]
apply (simp add:value_Zl_mI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_prod_primesTr1:"\<lbrakk>0 < n; distinct_pds K n P;
      ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow>
       I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (subst n_eq_val_eq_ideal[of "n" "P" "mprod_exp K (mL K P I)
       (Kb\<^bsub>K n P\<^esub>) n" "mIg\<^bsub>K n P I\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> mIg\<^bsub> K n P I\<^esub> \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>)
 4. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (simp add:mgeneratorTr4)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> mIg\<^bsub> K n P I\<^esub> \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>)
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (frule mI_gen_in_I1[of "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>); mIg\<^bsub> K n P I\<^esub> \<in> I\<rbrakk> \<Longrightarrow> mIg\<^bsub> K n P I\<^esub> \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>)
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (simp add:Ring.ideal_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (\<nu>\<^bsub>K P j\<^esub>) (mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n) = (\<nu>\<^bsub>K P j\<^esub>) (mIg\<^bsub> K n P I\<^esub>)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (simp add:ring_n_prod_primesTr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> I = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (mIg\<^bsub> K n P I\<^esub>)
[PROOF STEP]
apply (simp add:mI_principal)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_prod_primes:"\<lbrakk>0 < n; distinct_pds K n P;
      ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>);
     \<forall>k \<le> n. J k = (P\<^bsub>K P n\<^esub> k)\<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat ((mL K P I) k))\<^esup>\<rbrakk> \<Longrightarrow>
       I = i\<Pi>\<^bsub>(O\<^bsub>K P n\<^esub>),n\<^esub> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (P\<^bsub>K P n\<^esub> k) \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>\<rbrakk> \<Longrightarrow> I = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp add:prime_n_pd_principal[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>\<rbrakk> \<Longrightarrow> I = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (subst ring_n_prod_primesTr1[of "n" "P" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (frule Ring.prod_n_principal_ideal[of "O\<^bsub>K P n\<^esub>" "nat o (mL K P I)" "n"
       "Kb\<^bsub>K n P\<^esub>" "J"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> nat \<circ> mL K P I \<in> {j. j \<le> n} \<rightarrow> {j. 0 \<le> j}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> Kb\<^bsub>K n P\<^esub> \<in> {j. j \<le> n} \<rightarrow> carrier (O\<^bsub>K P n\<^esub>)
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 4. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (frule Kbase_hom[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K\<rbrakk> \<Longrightarrow> nat \<circ> mL K P I \<in> {j. j \<le> n} \<rightarrow> {j. 0 \<le> j}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> Kb\<^bsub>K n P\<^esub> \<in> {j. j \<le> n} \<rightarrow> carrier (O\<^bsub>K P n\<^esub>)
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 4. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp add:nat_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> Kb\<^bsub>K n P\<^esub> \<in> {j. j \<le> n} \<rightarrow> carrier (O\<^bsub>K P n\<^esub>)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (subst ring_n_pd_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> Kb\<^bsub>K n P\<^esub> \<in> {j. j \<le> n} \<rightarrow> carrier (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x})
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp add:Sr_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> Kb\<^bsub>K n P\<^esub> \<in> {j. j \<le> n} \<rightarrow> {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (rule Pi_I, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); x \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) x \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) x))
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp add:Kbase_Kronecker[of  "n" "P"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); x \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) x \<in> carrier K \<and> (\<forall>j\<le>n. 0 \<le> \<delta>\<^bsub>j x\<^esub>)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); x \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) x \<in> carrier K \<and> 0 \<le> 1
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); x \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) x \<in> carrier K \<and> ant 0 \<le> ant 1
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp del:ant_1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); x \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) x \<in> carrier K
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply (simp add:Kbase_hom)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) k\<^esup>
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (frule ring_n_mprod_mprodR[of "n" "P" n "mL K P I"  "Kb\<^bsub>K n P\<^esub>"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. mL K P I j \<in> Zset
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> mL K P I j
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 4. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (rule allI, rule impI, simp add:Zset_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> mL K P I j
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> mL K P I j
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 3. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (simp add: Zleast_in_mI_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (O\<^bsub>K P n\<^esub>) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (subst ring_n_pd_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier (Sr K {x \<in> carrier K. \<forall>j\<le>n. 0 \<le> (\<nu>\<^bsub>K P j\<^esub>) x}) - {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (simp add:Sr_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n\<rbrakk> \<Longrightarrow> (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (\<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)) \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (frule Kbase_hom1[of  "n" "P"], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (\<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)) \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (simp add:zero_in_ring_n_pd_zero_K)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (frule Kbase_Kronecker[of  "n" "P"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = \<delta>\<^bsub>j l\<^esub>\<rbrakk> \<Longrightarrow> \<forall>ja\<le>n. 0 \<le> (\<nu>\<^bsub>K P ja\<^esub>) ((Kb\<^bsub>K n P\<^esub>) j)
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (simp add:Kronecker_delta_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then 1 else 0)\<rbrakk> \<Longrightarrow> 0 \<le> 1
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (simp only:ant_1[THEN sym], simp only:ant_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; j \<le> n; \<forall>j\<le>n. (Kb\<^bsub>K n P\<^esub>) j \<in> carrier K \<and> (Kb\<^bsub>K n P\<^esub>) j \<noteq> \<zero>; \<forall>j\<le>n. \<forall>l\<le>n. (\<nu>\<^bsub>K P j\<^esub>) ((Kb\<^bsub>K n P\<^esub>) l) = (if j = l then ant 1 else ant 0)\<rbrakk> \<Longrightarrow> ant 0 \<le> ant 1
 2. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply (simp del:ant_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; I \<noteq> {\<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>}; I \<noteq> carrier (O\<^bsub>K P n\<^esub>); \<forall>k\<le>n. J k = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p (Kb\<^bsub>K n P\<^esub>) k \<^bsup>\<diamondsuit>(O\<^bsub>K P n\<^esub>) nat (mL K P I k)\<^esup>; Ring (O\<^bsub>K P n\<^esub>); i\<Pi>\<^bsub>O\<^bsub>K P n\<^esub>,n\<^esub> J = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n; mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n\<rbrakk> \<Longrightarrow> (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_exp K (mL K P I) (Kb\<^bsub>K n P\<^esub>) n = (O\<^bsub>K P n\<^esub>) \<diamondsuit>\<^sub>p mprod_expR (O\<^bsub>K P n\<^esub>) (nat \<circ> mL K P I) (Kb\<^bsub>K n P\<^esub>) n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in imap) create_create_commute:
  shows "\<langle>Create i1 e1\<rangle> \<rhd> \<langle>Create i2 e2\<rangle> = \<langle>Create i2 e2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Create i1 e1\<rangle> \<rhd> \<langle>Create i2 e2\<rangle> = \<langle>Create i2 e2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)


[STATEMENT]
lemma (in imap) create_delete_commute:
  assumes "i \<notin> is"
  shows "\<langle>Create i e1\<rangle> \<rhd> \<langle>Delete is e2\<rangle> = \<langle>Delete is e2\<rangle> \<rhd> \<langle>Create i e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Create i e1\<rangle> \<rhd> \<langle>Delete is e2\<rangle> = \<langle>Delete is e2\<rangle> \<rhd> \<langle>Create i e1\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<notin> is

goal (1 subgoal):
 1. \<langle>Create i e1\<rangle> \<rhd> \<langle>Delete is e2\<rangle> = \<langle>Delete is e2\<rangle> \<rhd> \<langle>Create i e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)


[STATEMENT]
lemma (in imap) create_append_commute:
  shows "\<langle>Create i1 e1\<rangle> \<rhd> \<langle>Append i2 e2\<rangle> = \<langle>Append i2 e2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Create i1 e1\<rangle> \<rhd> \<langle>Append i2 e2\<rangle> = \<langle>Append i2 e2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)


[STATEMENT]
lemma (in imap) create_expunge_commute:
  shows "\<langle>Create i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle> = \<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Create i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle> = \<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)


[STATEMENT]
lemma (in imap) create_store_commute:
  shows "\<langle>Create i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle> = \<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Create i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle> = \<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Create i1 e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)


[STATEMENT]
lemma (in imap) delete_delete_commute:
  shows "\<langle>Delete i1 e1\<rangle> \<rhd> \<langle>Delete i2 e2\<rangle> = \<langle>Delete i2 e2\<rangle> \<rhd> \<langle>Delete i1 e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Delete i1 e1\<rangle> \<rhd> \<langle>Delete i2 e2\<rangle> = \<langle>Delete i2 e2\<rangle> \<rhd> \<langle>Delete i1 e1\<rangle>
[PROOF STEP]
by(unfold interpret_op_def op_elem_def kleisli_def, fastforce)


[STATEMENT]
lemma (in imap) delete_append_commute:
  assumes "i \<notin> is"
  shows "\<langle>Delete is e1\<rangle> \<rhd> \<langle>Append i e2\<rangle> = \<langle>Append i e2\<rangle> \<rhd> \<langle>Delete is e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Delete is e1\<rangle> \<rhd> \<langle>Append i e2\<rangle> = \<langle>Append i e2\<rangle> \<rhd> \<langle>Delete is e1\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<notin> is

goal (1 subgoal):
 1. \<langle>Delete is e1\<rangle> \<rhd> \<langle>Append i e2\<rangle> = \<langle>Append i e2\<rangle> \<rhd> \<langle>Delete is e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)


[STATEMENT]
lemma (in imap) delete_expunge_commute:
  assumes "i \<notin> is"
  shows "\<langle>Delete is e1\<rangle> \<rhd> \<langle>Expunge e2 mo i\<rangle> = \<langle>Expunge e2 mo i\<rangle> \<rhd> \<langle>Delete is e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Delete is e1\<rangle> \<rhd> \<langle>Expunge e2 mo i\<rangle> = \<langle>Expunge e2 mo i\<rangle> \<rhd> \<langle>Delete is e1\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<notin> is

goal (1 subgoal):
 1. \<langle>Delete is e1\<rangle> \<rhd> \<langle>Expunge e2 mo i\<rangle> = \<langle>Expunge e2 mo i\<rangle> \<rhd> \<langle>Delete is e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)


[STATEMENT]
lemma (in imap) delete_store_commute:
  assumes "i \<notin> is"
  shows "\<langle>Delete is e1\<rangle> \<rhd> \<langle>Store e2 mo i\<rangle> = \<langle>Store e2 mo i\<rangle> \<rhd> \<langle>Delete is e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Delete is e1\<rangle> \<rhd> \<langle>Store e2 mo i\<rangle> = \<langle>Store e2 mo i\<rangle> \<rhd> \<langle>Delete is e1\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<notin> is

goal (1 subgoal):
 1. \<langle>Delete is e1\<rangle> \<rhd> \<langle>Store e2 mo i\<rangle> = \<langle>Store e2 mo i\<rangle> \<rhd> \<langle>Delete is e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)


[STATEMENT]
lemma (in imap) append_append_commute:
  shows "\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Append i2 e2\<rangle> = \<langle>Append i2 e2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Append i1 e1\<rangle> \<rhd> \<langle>Append i2 e2\<rangle> = \<langle>Append i2 e2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>
[PROOF STEP]
by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)


[STATEMENT]
lemma (in imap) append_expunge_commute:
  assumes "i1 \<noteq> mo"
  shows "(\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle>) = (\<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle> = \<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle>) x = (\<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle>) x = (\<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
show "(\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle>) x = (\<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle>) x = (\<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> mo

goal (1 subgoal):
 1. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle>) x = (\<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
by(auto simp add: interpret_op_def kleisli_def op_elem_def)
[PROOF STATE]
proof (state)
this:
(\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Expunge e2 mo i2\<rangle>) x = (\<langle>Expunge e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in imap) append_store_commute:
  assumes "i1 \<noteq> mo"
  shows "(\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle>) = (\<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle> = \<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle>) x = (\<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle>) x = (\<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
show "(\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle>) x = (\<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle>) x = (\<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> mo

goal (1 subgoal):
 1. (\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle>) x = (\<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x
[PROOF STEP]
by(auto simp add: interpret_op_def kleisli_def op_elem_def)
[PROOF STATE]
proof (state)
this:
(\<langle>Append i1 e1\<rangle> \<rhd> \<langle>Store e2 mo i2\<rangle>) x = (\<langle>Store e2 mo i2\<rangle> \<rhd> \<langle>Append i1 e1\<rangle>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in imap) expunge_expunge_commute:
  shows "(\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Expunge e2 mo2 i2\<rangle>) = (\<langle>Expunge e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Expunge e2 mo2 i2\<rangle> = \<langle>Expunge e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Expunge e2 mo2 i2\<rangle>) x = (\<langle>Expunge e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Expunge e2 mo2 i2\<rangle>) x = (\<langle>Expunge e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x
[PROOF STEP]
show "(\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Expunge e2 mo2 i2\<rangle>) x
       = (\<langle>Expunge e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Expunge e2 mo2 i2\<rangle>) x = (\<langle>Expunge e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x
[PROOF STEP]
by(auto simp add: interpret_op_def kleisli_def op_elem_def)
[PROOF STATE]
proof (state)
this:
(\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Expunge e2 mo2 i2\<rangle>) x = (\<langle>Expunge e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in imap) expunge_store_commute:
  assumes "i1 \<noteq> mo2" and "i2 \<noteq> mo1"
  shows "(\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle> = \<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x
[PROOF STEP]
show "(\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x
[PROOF STEP]
unfolding  interpret_op_def kleisli_def op_elem_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let metadata = fst (x (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Expunge e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) = (let metadata = fst (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Expunge e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after)))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
i2 \<noteq> mo1

goal (1 subgoal):
 1. (let metadata = fst (x (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Expunge e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) = (let metadata = fst (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Expunge e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Expunge e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after)))
[PROOF STEP]
by (simp, fastforce)
[PROOF STATE]
proof (state)
this:
(\<langle>Expunge e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Expunge e1 mo1 i1\<rangle>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in imap) store_store_commute:
  assumes "i1 \<noteq> mo2" and "i2 \<noteq> mo1"
  shows "(\<langle>Store e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Store e1 mo1 i1\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Store e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle> = \<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Store e1 mo1 i1\<rangle>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Store e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Store e1 mo1 i1\<rangle>) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<langle>Store e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Store e1 mo1 i1\<rangle>) x
[PROOF STEP]
show "(\<langle>Store e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Store e1 mo1 i1\<rangle>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>Store e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Store e1 mo1 i1\<rangle>) x
[PROOF STEP]
unfolding  interpret_op_def kleisli_def op_elem_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let metadata = fst (x (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) = (let metadata = fst (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> mo2
i2 \<noteq> mo1

goal (1 subgoal):
 1. (let metadata = fst (x (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) = (let metadata = fst (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (x (case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e2 mo2 i2 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (x(case Store e2 mo2 i2 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after))) \<bind> (\<lambda>y. let metadata = fst (y (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); files = snd (y (case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e)); after = case Store e1 mo1 i1 of Create i e \<Rightarrow> (metadata \<union> {i}, files) | Delete is e \<Rightarrow> (metadata - is, files - is) | Append i e \<Rightarrow> (metadata, files \<union> {i}) | Expunge e mo i \<Rightarrow> (metadata \<union> {i}, files - {mo}) | Store e mo i \<Rightarrow> (metadata, insert i (files - {mo})) in Some (y(case Store e1 mo1 i1 of Create i e \<Rightarrow> e | Delete is e \<Rightarrow> e | Append i e \<Rightarrow> e | Expunge e mo i \<Rightarrow> e | Store e mo i \<Rightarrow> e := after)))
[PROOF STEP]
by (simp, fastforce)
[PROOF STATE]
proof (state)
this:
(\<langle>Store e1 mo1 i1\<rangle> \<rhd> \<langle>Store e2 mo2 i2\<rangle>) x = (\<langle>Store e2 mo2 i2\<rangle> \<rhd> \<langle>Store e1 mo1 i1\<rangle>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_lm_1: "p \<in> PrimRec2 \<Longrightarrow> fn_to_set p \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> PrimRec2 \<Longrightarrow> fn_to_set p \<in> ce_sets
[PROOF STEP]
by (auto simp add: ce_sets_def)


[STATEMENT]
lemma ce_set_lm_2: "\<lbrakk> p \<in> PrimRec2; \<forall> x. (x \<in> A) = (\<exists> y. p x y = 0)\<rbrakk> \<Longrightarrow> A \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec2; \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)\<rbrakk> \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec2; \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)\<rbrakk> \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
assume p_is_pr: "p \<in> PrimRec2"
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec2

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec2; \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)\<rbrakk> \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
assume "\<forall> x. (x \<in> A) = (\<exists> y. p x y = 0)"
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec2; \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)\<rbrakk> \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)
[PROOF STEP]
have "A = fn_to_set p"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)

goal (1 subgoal):
 1. A = fn_to_set p
[PROOF STEP]
by (unfold fn_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
A = fn_to_set p

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec2; \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)\<rbrakk> \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
with p_is_pr
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec2
A = fn_to_set p
[PROOF STEP]
show "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec2
A = fn_to_set p

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (simp add: ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_lm_3: "A \<in> ce_sets \<Longrightarrow> \<exists> p \<in> PrimRec2. A = fn_to_set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
assume "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "A \<in> { (fn_to_set p) | p. p \<in> PrimRec2 }"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. A \<in> {fn_to_set p |p. p \<in> PrimRec2}
[PROOF STEP]
by (simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
A \<in> {fn_to_set p |p. p \<in> PrimRec2}

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<in> {fn_to_set p |p. p \<in> PrimRec2}

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec2. A = fn_to_set p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_lm_4: "A \<in> ce_sets \<Longrightarrow> \<exists> p \<in> PrimRec2. \<forall> x. (x \<in> A) = (\<exists> y. p x y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)
[PROOF STEP]
assume "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> p \<in> PrimRec2. A = fn_to_set p"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
by (rule ce_set_lm_3)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec2. A = fn_to_set p

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
obtain p where p_is_pr: "p \<in> PrimRec2" and L1: "A = fn_to_set p"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>PrimRec2. A = fn_to_set p

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> PrimRec2; A = fn_to_set p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec2
A = fn_to_set p

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>p\<in>PrimRec2. \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)
[PROOF STEP]
from p_is_pr L1
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec2
A = fn_to_set p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec2
A = fn_to_set p

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec2. \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)
[PROOF STEP]
by (unfold fn_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec2. \<forall>x. (x \<in> A) = (\<exists>y. p x y = 0)

goal:
No subgoals!
[PROOF STEP]
qed