[STATEMENT]
lemma fag_single_additionTr4:"\<lbrakk>commute_bpp f (aug_pm_set z i {a});
      assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f;
      ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a});
      zeroA z i f {a} z \<rbrakk> \<Longrightarrow>
      \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n\<longrightarrow> s \<^sub>f+ t = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z
[PROOF STEP]
apply (cut_tac a_in_aug_pm_set[of a "{a}" z i], simp,
        cut_tac addition_inc_add0[of "aug_pm_set z i {a}" f],
        frule subsetD[of "aug_pm_set z i {a}"
                     "addition_set f (aug_pm_set z i {a})" a], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} 0 \<and> t \<in> add_set f {\<^sub>i- a} 0 \<longrightarrow> s \<^sub>f+ t = z
 2. \<And>n. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} (Suc n) \<and> t \<in> add_set f {\<^sub>i- a} (Suc n) \<longrightarrow> s \<^sub>f+ t = z
 3. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> a \<^sub>f+ \<^sub>i- a = z
 2. \<And>n. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} (Suc n) \<and> t \<in> add_set f {\<^sub>i- a} (Suc n) \<longrightarrow> s \<^sub>f+ t = z
 3. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule inv_aug_addition [of "f" "z" "i" "{a}"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>a\<in>addition_set f (aug_pm_set z i {a}). \<^sub>i- a \<^sub>f+ a = z\<rbrakk> \<Longrightarrow> a \<^sub>f+ \<^sub>i- a = z
 2. \<And>n. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} (Suc n) \<and> t \<in> add_set f {\<^sub>i- a} (Suc n) \<longrightarrow> s \<^sub>f+ t = z
 3. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule aug_ipp_closed [of "f" "z" "i" "{a}" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>a\<in>addition_set f (aug_pm_set z i {a}). \<^sub>i- a \<^sub>f+ a = z; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> a \<^sub>f+ \<^sub>i- a = z
 2. \<And>n. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} (Suc n) \<and> t \<in> add_set f {\<^sub>i- a} (Suc n) \<longrightarrow> s \<^sub>f+ t = z
 3. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule fag_single_additionTr2 [of "f" "z" "i" "a" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>a\<in>addition_set f (aug_pm_set z i {a}). \<^sub>i- a \<^sub>f+ a = z; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> a \<in> add_set f {a} 0
 2. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>a\<in>addition_set f (aug_pm_set z i {a}). \<^sub>i- a \<^sub>f+ a = z; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ \<^sub>i- a = z\<rbrakk> \<Longrightarrow> a \<^sub>f+ \<^sub>i- a = z
 3. \<And>n. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} (Suc n) \<and> t \<in> add_set f {\<^sub>i- a} (Suc n) \<longrightarrow> s \<^sub>f+ t = z
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (simp, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z\<rbrakk> \<Longrightarrow> \<forall>s t. s \<in> add_set f {a} (Suc n) \<and> t \<in> add_set f {\<^sub>i- a} (Suc n) \<longrightarrow> s \<^sub>f+ t = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply ((rule allI)+, rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s t. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z; s \<in> add_set f {a} (Suc n); t \<in> add_set f {\<^sub>i- a} (Suc n)\<rbrakk> \<Longrightarrow> s \<^sub>f+ t = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s t. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z; \<exists>sa\<in>add_set f {a} n. s = sa \<^sub>f+ a; \<exists>s\<in>add_set f {\<^sub>i- a} n. t = s \<^sub>f+ \<^sub>i- a\<rbrakk> \<Longrightarrow> s \<^sub>f+ t = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (erule bexE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z; sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a\<rbrakk> \<Longrightarrow> s \<^sub>f+ t = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule aug_ipp_closed [of "f" "z" "i" "{a}" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z; sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> s \<^sub>f+ t = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); \<forall>s t. s \<in> add_set f {a} n \<and> t \<in> add_set f {\<^sub>i- a} n \<longrightarrow> s \<^sub>f+ t = z; sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (drule_tac x = sa in spec,
        drule_tac a = sb in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z\<rbrakk> \<Longrightarrow> sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = z
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (cut_tac n = n in addition_inc_add[of f "{a}"],
        cut_tac addition_set_mono[of "{a}" "aug_pm_set z i {a}" f],
        frule_tac c = sa and A = "add_set f {a} n" in subsetD[of _
          "addition_set f {a}"], assumption+,
        frule_tac c = sa in subsetD[of "addition_set f {a}"
               "addition_set f (aug_pm_set z i {a})"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 3. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (cut_tac n = n in addition_inc_add[of f "{\<^sub>i- a}"],
        cut_tac addition_set_mono[of "{\<^sub>i- a}" "aug_pm_set z i {\<^sub>i- a}" f],
        frule_tac c = sb and A = "add_set f {\<^sub>i- a} n" in subsetD[of _
          "addition_set f {\<^sub>i- a}"], assumption+,
        frule_tac c = sb in subsetD[of "addition_set f {\<^sub>i- a}"
               "addition_set f (aug_pm_set z i {\<^sub>i- a})"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {\<^sub>i- a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {\<^sub>i- a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (simp add:aug_pm_aug_pm_minus[THEN sym])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x = sb in aug_bpp_closed [of z i "{a}" f _ " \<^sub>i- a"],
         assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x = sa and y = a and z = "sb \<^sub>f+ \<^sub>i- a" in
                 addition_assoc [of "aug_pm_set z i {a}" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a))\<rbrakk> \<Longrightarrow> sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a))\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (thin_tac "sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a))")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x1 = a and y1 = sb and z1 = "\<^sub>i- a" in
        addition_assoc [THEN sym, of "aug_pm_set z i {a}" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = a \<^sub>f+ sb \<^sub>f+ \<^sub>i- a\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = a \<^sub>f+ sb \<^sub>f+ \<^sub>i- a\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (a \<^sub>f+ sb \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac y = sb in aug_commute [of "f" "z" "i" "{a}" "a"],
        assumption+, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a; a \<^sub>f+ sb = sb \<^sub>f+ a\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x = sb and y = a and z = "\<^sub>i- a" in
                 addition_assoc [of "aug_pm_set z i {a}" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a; a \<^sub>f+ sb = sb \<^sub>f+ a; sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a = sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a); a \<^sub>f+ sb = sb \<^sub>f+ a; sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a = sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (thin_tac "a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ sb = sb \<^sub>f+ a; sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a = sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (thin_tac "a \<^sub>f+ sb = sb \<^sub>f+ a",
        thin_tac "sb \<^sub>f+ a \<^sub>f+ \<^sub>i- a = sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)",
        thin_tac "sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (a \<^sub>f+ \<^sub>i- a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac y = " \<^sub>i- a" in aug_commute [of "f" "z" "i" "{a}" "a"],
            assumption+, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ \<^sub>i- a = \<^sub>i- a \<^sub>f+ a\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (\<^sub>i- a \<^sub>f+ a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x = sa and y = a and z = "sb \<^sub>f+ \<^sub>i- a" in
                 addition_assoc [of "aug_pm_set z i {a}" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ \<^sub>i- a = \<^sub>i- a \<^sub>f+ a\<rbrakk> \<Longrightarrow> sb \<^sub>f+ \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a})
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ \<^sub>i- a = \<^sub>i- a \<^sub>f+ a; sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a))\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (\<^sub>i- a \<^sub>f+ a)) = z
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 4. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 5. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x = sb in aug_bpp_closed [of "z" "i" "{a}" "f" _ " \<^sub>i- a"],
  assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ \<^sub>i- a = \<^sub>i- a \<^sub>f+ a; sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a))\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (\<^sub>i- a \<^sub>f+ a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (thin_tac "sa \<^sub>f+ a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a) = sa \<^sub>f+ (a \<^sub>f+ (sb \<^sub>f+ \<^sub>i- a))")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); a \<^sub>f+ \<^sub>i- a = \<^sub>i- a \<^sub>f+ a\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (\<^sub>i- a \<^sub>f+ a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (thin_tac "a \<^sub>f+ \<^sub>i- a = \<^sub>i- a \<^sub>f+ a")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a})\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (\<^sub>i- a \<^sub>f+ a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule inv_aug_addition [of "f" "z" "i" "{a}" ], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); \<forall>a\<in>addition_set f (aug_pm_set z i {a}). \<^sub>i- a \<^sub>f+ a = z\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ (\<^sub>i- a \<^sub>f+ a)) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (drule_tac x = a in bspec, assumption, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); \<^sub>i- a \<^sub>f+ a = z\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ z) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x = sb and y = z in aug_commute [of "f" "z" "i" "{a}"],
             assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); \<^sub>i- a \<^sub>f+ a = z\<rbrakk> \<Longrightarrow> z \<in> addition_set f (aug_pm_set z i {a})
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); \<^sub>i- a \<^sub>f+ a = z; sb \<^sub>f+ z = z \<^sub>f+ sb\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ z) = z
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 4. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 5. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (simp add:addition_set_inc_z)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); \<^sub>i- a \<^sub>f+ a = z; sb \<^sub>f+ z = z \<^sub>f+ sb\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (sb \<^sub>f+ z) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (frule_tac x = sb and y = z in aug_commute [of "f" "z" "i" "{a}"],
       assumption+, simp add:addition_set_inc_z, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}; addition_set f {\<^sub>i- a} \<subseteq> addition_set f (aug_pm_set z i {a}); sb \<in> addition_set f {\<^sub>i- a}; sb \<in> addition_set f (aug_pm_set z i {a}); \<^sub>i- a \<^sub>f+ a = z; sb \<^sub>f+ z = z \<^sub>f+ sb\<rbrakk> \<Longrightarrow> sa \<^sub>f+ (z \<^sub>f+ sb) = z
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 3. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 4. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (simp add:zeroA_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}; addition_set f {a} \<subseteq> addition_set f (aug_pm_set z i {a}); sa \<in> addition_set f {a}; sa \<in> addition_set f (aug_pm_set z i {a}); add_set f {\<^sub>i- a} n \<subseteq> addition_set f {\<^sub>i- a}\<rbrakk> \<Longrightarrow> {\<^sub>i- a} \<subseteq> aug_pm_set z i {\<^sub>i- a}
 2. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 3. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (rule subsetI, simp add:aug_pm_set_def minus_set_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s t sa sb. \<lbrakk>assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z; a \<in> aug_pm_set z i {a}; aug_pm_set z i {a} \<subseteq> addition_set f (aug_pm_set z i {a}); a \<in> addition_set f (aug_pm_set z i {a}); sa \<in> add_set f {a} n; s = sa \<^sub>f+ a; sb \<in> add_set f {\<^sub>i- a} n; t = sb \<^sub>f+ \<^sub>i- a; \<^sub>i- a \<in> addition_set f (aug_pm_set z i {a}); sa \<^sub>f+ sb = z; add_set f {a} n \<subseteq> addition_set f {a}\<rbrakk> \<Longrightarrow> {a} \<subseteq> aug_pm_set z i {a}
 2. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply (simp add:aug_pm_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>commute_bpp f (aug_pm_set z i {a}); assoc_bpp (aug_pm_set z i {a}) f; ipp_cond1 {a} i; ipp_cond2 z {a} i f; ipp_cond3 z i; inv_ipp z i f {a}; commute_bpp f (aug_pm_set z i {a}); zeroA z i f {a} z\<rbrakk> \<Longrightarrow> a \<in> {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma TYRELI: "TYREL (R::(_\<times>'a) set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TYREL R
[PROOF STEP]
by simp


[STATEMENT]
lemma act_sup_distr: "\<alpha> (x \<squnion> y) p = (\<alpha> x p) \<squnion> (\<alpha> y p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
have "\<alpha> (x \<squnion> y) p  = \<alpha> (\<Squnion>{x,y}) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> (\<Squnion>{x, y}) p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> (x \<squnion> y) p = \<alpha> (\<Squnion>{x, y}) p

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> (x \<squnion> y) p = \<alpha> (\<Squnion>{x, y}) p

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
have "... = \<Squnion>{\<alpha> v p |v. v \<in> {x,y}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (\<Squnion>{x, y}) p = \<Squnion>{\<alpha> v p |v. v \<in> {x, y}}
[PROOF STEP]
by (rule act3)
[PROOF STATE]
proof (state)
this:
\<alpha> (\<Squnion>{x, y}) p = \<Squnion>{\<alpha> v p |v. v \<in> {x, y}}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> (\<Squnion>{x, y}) p = \<Squnion>{\<alpha> v p |v. v \<in> {x, y}}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
have "... = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>{\<alpha> v p |v. v \<in> {x, y}} = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}
[PROOF STEP]
by (metis empty_iff insert_iff)
[PROOF STATE]
proof (state)
this:
\<Squnion>{\<alpha> v p |v. v \<in> {x, y}} = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<alpha> (x \<squnion> y) p = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> (x \<squnion> y) p = \<Squnion>{v. v = \<alpha> x p \<or> v = \<alpha> y p}

goal (1 subgoal):
 1. \<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p
[PROOF STEP]
by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
[PROOF STATE]
proof (state)
this:
\<alpha> (x \<squnion> y) p = \<alpha> x p \<squnion> \<alpha> y p

goal:
No subgoals!
[PROOF STEP]
qed