[STATEMENT]
lemma newton_seq_props_induct:
shows "\<And>k. k \<le> n \<Longrightarrow> (ns k) \<in> carrier Zp
              \<and> val_Zp (f'\<bullet>(ns k)) = val_Zp ((f'\<bullet>a))
              \<and> val_Zp (f\<bullet>(ns k)) \<ge> 2*(val_Zp (f'\<bullet>a)) + (2^k)*t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof(induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. k \<le> 0 \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
k \<le> 0

goal (2 subgoals):
 1. \<And>k. k \<le> 0 \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<le> 0
[PROOF STEP]
have kz: "k = 0"
[PROOF STATE]
proof (prove)
using this:
k \<le> 0

goal (1 subgoal):
 1. k = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. \<And>k. k \<le> 0 \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have B0: "( ns k) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
using kz
[PROOF STATE]
proof (prove)
using this:
k = 0

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns k \<in> carrier Zp

goal (2 subgoals):
 1. \<And>k. k \<le> 0 \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have B1: "val_Zp (f' \<bullet> ns k) = (val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using kz newton_seq.simps(1)
[PROOF STATE]
proof (prove)
using this:
k = 0
ns 0 = a

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)

goal (2 subgoals):
 1. \<And>k. k \<le> 0 \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have B2: "val_Zp (f \<bullet> (ns k)) \<ge> (2 * (val_Zp (f'\<bullet>a))) + 2 ^ k * t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have B20: "(2 * (val_Zp (f'\<bullet>a))) + 2 ^ k * t = (2 * (val_Zp (f'\<bullet>a))) +  t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
have "(2 * (val_Zp (f'\<bullet>a))) + 2 ^ k * t = (2 * (val_Zp (f'\<bullet>a))) +  t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
using kz  one_eint_def
[PROOF STATE]
proof (prove)
using this:
k = 0
1 = eint 1

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t
[PROOF STEP]
have "(2 * (val_Zp (f'\<bullet>a))) + 2 ^ k * t = (2 * (val_Zp (f'\<bullet>a))) + val_Zp (f\<bullet>a) - 2*(val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + t

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
unfolding hensel_factor_def
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) = eint 2 * val_Zp (f' \<bullet> a) + (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) = eint 2 * val_Zp (f' \<bullet> a) + val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
by (simp add: val_Zp_def)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
have "(2 * (val_Zp (f'\<bullet>a))) + 2 ^ k * t =  val_Zp (f\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = eint 2 * val_Zp (f' \<bullet> a) + val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = val_Zp (f \<bullet> a)
[PROOF STEP]
by (metis add_diff_cancel_eint eint_ord_simps(6) hensel_hypothesis)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t = val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by (simp add: kz)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (2 subgoals):
 1. \<And>k. k \<le> 0 \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
using B0 B1
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
ns k \<in> carrier Zp
val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)
k \<le> Suc n

goal (1 subgoal):
 1. \<And>n k. \<lbrakk>\<And>k. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k); k \<le> Suc n\<rbrakk> \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof(cases "k \<le> n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k \<le> n

goal (2 subgoals):
 1. k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
 2. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<le> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<le> n

goal (1 subgoal):
 1. ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
k \<le> n
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> k \<le> n

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have F1: "(ns n) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n \<in> carrier Zp
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. ns n \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns n \<in> carrier Zp

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have F2: "val_Zp (f'\<bullet>(ns n)) = val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have F3: "val_Zp (f\<bullet>(ns n)) \<ge> 2*(val_Zp (f'\<bullet>a)) + (2^n)*t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have kval: "k = Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = Suc n
[PROOF STEP]
using False Suc.prems le_Suc_eq
[PROOF STATE]
proof (prove)
using this:
\<not> k \<le> n
k \<le> Suc n
(?m \<le> Suc ?n) = (?m \<le> ?n \<or> ?m = Suc ?n)

goal (1 subgoal):
 1. k = Suc n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k = Suc n

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have F6: "val_Zp (f\<bullet>(ns n)) \<ge> val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
have "2*(val_Zp (f'\<bullet>a))  \<ge> val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
using f'a_closed val_pos eint_mult_mono'[of "val_Zp (f'\<bullet>a)" 1 2]
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> a \<in> carrier Zp
?x \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp ?x
\<lbrakk>0 \<le> val_Zp (f' \<bullet> a) \<and> val_Zp (f' \<bullet> a) \<noteq> \<infinity>; 1 < eint 2\<rbrakk> \<Longrightarrow> 1 * val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
by (metis Groups.add_ac(2) add.right_neutral eSuc_eint eint_0_iff(2) eint_add_left_cancel_le
              eint_ord_simps(2) f'a_nonneg_val f'a_not_infinite infinity_ne_i1 linorder_not_less
              mult_one_left not_one_less_zero one_add_one one_eint_def order_less_le order_trans zero_one_eint_neq(1))
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
hence  "2*(val_Zp (f'\<bullet>a)) + (2^n)*t  \<ge> val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
[PROOF STEP]
using t_times_pow_pos[of n]
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a)
0 < eint (2 ^ n) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
[PROOF STEP]
by (metis (no_types, lifting) add.right_neutral eint_add_left_cancel_le order_less_le order_trans)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using F2 F3
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have F5: " divide (f\<bullet>(ns n))(f'\<bullet>(ns n)) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
have 00: "f \<bullet> ns n \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns n \<in> carrier Zp
[PROOF STEP]
by (simp add: F1 to_fun_closed)
[PROOF STATE]
proof (state)
this:
f \<bullet> ns n \<in> carrier Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
have "val_Zp ((f'\<bullet>a)) \<noteq> val_Zp \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>
[PROOF STEP]
by (simp add:  val_Zp_def)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>

goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>
[PROOF STEP]
have 01: "f' \<bullet> ns n \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
using F2 F1 Zp_x_is_UP_cring f'_closed nonzero_def
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
ns n \<in> carrier Zp
UP_cring Zp
f' \<in> carrier (UP Zp)
nonzero ?R = {a \<in> carrier ?R. a \<noteq> \<zero>\<^bsub>?R\<^esub>}

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>; val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a); ns n \<in> carrier Zp; UP_cring Zp; f' \<in> carrier (UP Zp); \<And>R. nonzero R = {a \<in> carrier R. a \<noteq> \<zero>\<^bsub>R\<^esub>}\<rbrakk> \<Longrightarrow> f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
have "f' \<bullet> ns n \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns n \<in> carrier Zp
[PROOF STEP]
using F1 Zp_continuous_is_Zp_closed f'_closed  polynomial_is_Zp_continuous
[PROOF STATE]
proof (prove)
using this:
ns n \<in> carrier Zp
is_Zp_continuous ?f \<Longrightarrow> ?f \<in> carrier (function_ring (carrier Zp) Zp)
f' \<in> carrier (UP Zp)
?f \<in> carrier (UP Zp) \<Longrightarrow> is_Zp_continuous ((\<bullet>) ?f)

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> carrier Zp
[PROOF STEP]
by (simp add: to_fun_closed)
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns n \<in> carrier Zp

goal (1 subgoal):
 1. \<lbrakk>val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>; val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a); ns n \<in> carrier Zp; UP_cring Zp; f' \<in> carrier (UP Zp); \<And>R. nonzero R = {a \<in> carrier R. a \<noteq> \<zero>\<^bsub>R\<^esub>}\<rbrakk> \<Longrightarrow> f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' \<bullet> ns n \<in> carrier Zp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns n \<in> carrier Zp

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
using F2 \<open>val_Zp (f'\<bullet>a) \<noteq> val_Zp \<zero>\<close> not_nonzero_Zp
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns n \<in> carrier Zp
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
val_Zp (f' \<bullet> a) \<noteq> val_Zp \<zero>
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns n \<in> nonzero Zp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns n \<in> nonzero Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns n \<in> nonzero Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
using F6
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns n \<in> nonzero Zp
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
by (metis "00" F2 \<open>val_Zp (f'\<bullet>a) \<noteq> val_Zp \<zero>\<close> divide_closed nonzero_closed)
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have F4:  "(ns k) \<ominus> (ns n) = (\<ominus> divide (f\<bullet>(ns n))(f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns k \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
using F1 F5 newton_seq.simps(2)[of n] kval
[PROOF STATE]
proof (prove)
using this:
ns n \<in> carrier Zp
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
ns (Suc n) = newton_step (ns n)
k = Suc n

goal (1 subgoal):
 1. ns k \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
unfolding newton_step_def
[PROOF STATE]
proof (prove)
using this:
ns n \<in> carrier Zp
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
ns (Suc n) = ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
k = Suc n

goal (1 subgoal):
 1. ns k \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
by (metis R.l_neg R.minus_closed R.minus_zero R.plus_diff_simp R.r_neg2 R.r_right_minus_eq
            a_minus_def local.a_closed minus_a_inv)
[PROOF STATE]
proof (state)
this:
ns k \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have F7: "val_Zp (divide (f\<bullet>(ns n))(f'\<bullet>(ns n))) = val_Zp (f\<bullet>(ns n)) - val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)
[PROOF STEP]
apply(rule val_of_divide)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. f \<bullet> ns n \<in> carrier Zp
 2. f' \<bullet> ns n \<in> nonzero Zp
 3. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
apply (simp add: F1 to_fun_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f' \<bullet> ns n \<in> nonzero Zp
 2. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using F1 f'_closed to_fun_closed F2 not_nonzero_Zp val_Zp_def
[PROOF STATE]
proof (prove)
using this:
ns n \<in> carrier Zp
f' \<in> carrier (UP Zp)
\<lbrakk>?f \<in> carrier (UP Zp); ?x \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?f \<bullet> ?x \<in> carrier Zp
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (2 subgoals):
 1. f' \<bullet> ns n \<in> nonzero Zp
 2. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by (simp add: F6)
[PROOF STATE]
proof (state)
this:
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)

goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns k \<in> carrier Zp
 2. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
show P0:"ns k \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A0: "ns k = ns n \<ominus> (divide (f\<bullet> (ns n)) (f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns k = ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
by (simp add: kval newton_step_def)
[PROOF STATE]
proof (state)
this:
ns k = ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A1: "val_Zp (f'\<bullet>(ns n)) = val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A2: "val_Zp (f\<bullet>(ns n)) \<ge>val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
have A20: "(2 * val_Zp (f'\<bullet>a)) + 2 ^ n * (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a)) \<ge>val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
have "val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
using hensel_hypothesis eint_minus_le
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
?b < ?c \<Longrightarrow> 0 < ?c - ?b

goal (1 subgoal):
 1. 0 < val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
have "  (2 ^ n) * (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a))
                        \<ge> (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
0 < val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a) \<le> eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
using eint_pos_int_times_ge
[PROOF STATE]
proof (prove)
using this:
0 < val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
\<lbrakk>0 \<le> ?c; 0 < ?n\<rbrakk> \<Longrightarrow> ?c \<le> eint ?n * ?c

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a) \<le> eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a) \<le> eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a) \<le> eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
have  "  ((2 * val_Zp (f'\<bullet>a)) + 2 ^ n * (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a)))
                        \<ge> (2 * val_Zp (f'\<bullet>a)) + (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a) \<le> eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
by (simp add: val_Zp_def)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
have  "  ((2 * val_Zp (f'\<bullet>a)) + 2 ^ n * (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a)))
                        \<ge> (val_Zp (f\<bullet>a) )"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
show  "  ((2 * val_Zp (f'\<bullet>a)) + 2 ^ n * (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a)))
                        \<ge> (val_Zp (f'\<bullet>a) )"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
using hensel_hypothesis_weakened
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
have A21:"val_Zp (f\<bullet>(ns n)) \<ge> (2 * val_Zp (f'\<bullet>a)) + 2 ^ n * (val_Zp (f\<bullet>a) - 2 * val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
unfolding hensel_factor_def
[PROOF STATE]
proof (prove)
using this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using A21 A20
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) \<le> val_Zp (f \<bullet> ns n)
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A3: "ns n \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n \<in> carrier Zp
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. ns n \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns n \<in> carrier Zp

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A4: "val_Zp (f\<bullet>(ns n)) \<ge>val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using A1 A2
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A5: "f\<bullet>(ns n) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns n \<in> carrier Zp
[PROOF STEP]
by (simp add: F1 UP_cring.to_fun_closed Zp_x_is_UP_cring)
[PROOF STATE]
proof (state)
this:
f \<bullet> ns n \<in> carrier Zp

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A6: "(f'\<bullet>(ns n)) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
have "(f'\<bullet>(ns n)) \<in> carrier  Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns n \<in> carrier Zp
[PROOF STEP]
by (simp add: F1 UP_cring.to_fun_closed Zp_x_is_UP_cring f'_closed)
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns n \<in> carrier Zp

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
have "val_Zp (f'\<bullet>(ns n)) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>
[PROOF STEP]
using A1
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>
[PROOF STEP]
by (simp add:  val_Zp_def)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
using \<open>f' \<bullet> ns n \<in> carrier Zp\<close> not_nonzero_Zp val_Zp_def
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>
f' \<bullet> ns n \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns n \<in> nonzero Zp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns n \<in> nonzero Zp

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
have A7: " (divide (f\<bullet> (ns n)) (f'\<bullet>(ns n))) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
using A5 A6 A4 A3 F5
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns n \<in> carrier Zp
f' \<bullet> ns n \<in> nonzero Zp
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
ns n \<in> carrier Zp
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
using A0 A3 cring.cring_simprules(4)
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
ns k = ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
ns n \<in> carrier Zp
\<lbrakk>cring ?R; ?x \<in> carrier ?R; ?y \<in> carrier ?R\<rbrakk> \<Longrightarrow> ?x \<ominus>\<^bsub>?R\<^esub> ?y \<in> carrier ?R

goal (1 subgoal):
 1. ns k \<in> carrier Zp
[PROOF STEP]
by (simp add: F1 F5 cring.cring_simprules(4))
[PROOF STATE]
proof (state)
this:
ns k \<in> carrier Zp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns k \<in> carrier Zp

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have P1: "val_Zp (f' \<bullet> ns k) = val_Zp (f'\<bullet>a) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
proof(cases "(f' \<bullet> ns k) = (f' \<bullet> ns n)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f' \<bullet> ns k = f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
 2. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns k = f' \<bullet> ns n

goal (2 subgoals):
 1. f' \<bullet> ns k = f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
 2. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' \<bullet> ns k = f' \<bullet> ns n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns k = f' \<bullet> ns n

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using  Suc.IH
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns k = f' \<bullet> ns n
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by (metis order_refl)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns k \<noteq> f' \<bullet> ns n

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
have "val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) \<ge> val_Zp ((ns k) \<ominus> (ns n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (ns k \<ominus> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using False P0 f'_closed  poly_diff_val  Suc.IH
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns k \<noteq> f' \<bullet> ns n
ns k \<in> carrier Zp
f' \<in> carrier (UP Zp)
\<lbrakk>?f \<in> carrier (UP Zp); ?a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> val_Zp (?a \<ominus> ?b) \<le> val_Zp (?f \<bullet> ?a \<ominus> ?f \<bullet> ?b)
?k2 \<le> n \<Longrightarrow> ns ?k2 \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k2) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k2) * t \<le> val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. val_Zp (ns k \<ominus> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (ns k \<ominus> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (ns k \<ominus> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
have "val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) \<ge> val_Zp (\<ominus> divide (f\<bullet>(ns n))(f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns k \<ominus> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (\<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using  F4
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns k \<ominus> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
ns k \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (\<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
val_Zp (\<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (\<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
have "val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) \<ge> val_Zp (divide (f\<bullet>(ns n))(f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (\<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using F5 val_Zp_of_minus
[PROOF STATE]
proof (prove)
using this:
val_Zp (\<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> val_Zp ?a = val_Zp (\<ominus> ?a)

goal (1 subgoal):
 1. val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
have P10: "val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) \<ge> val_Zp (f\<bullet>(ns n)) - val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using F7
[PROOF STATE]
proof (prove)
using this:
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
have P11: "val_Zp (f'\<bullet>(ns n)) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>
[PROOF STEP]
by (simp add: F2)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>
[PROOF STEP]
have "val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) \<ge> (2 * val_Zp (f'\<bullet>a)) + 2 ^ n * t -  val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using F3 P10
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by (smt eint_add_cancel_fact eint_add_left_cancel_le order_trans)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
have P12: "val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) \<ge> (2 *(val_Zp (f'\<bullet>a))) + 2 ^ n * t - (val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by (simp add: F2)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
have P13:"val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) \<ge> (val_Zp (f'\<bullet>a)) + 2 ^ n * t "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
have "(2 *(val_Zp (f'\<bullet>a))) + (2 ^ n * t) - (val_Zp (f'\<bullet>a)) =  (2 *(val_Zp (f'\<bullet>a))) - (val_Zp (f'\<bullet>a)) + (2 ^ n * t) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
[PROOF STEP]
using eint_minus_comm
[PROOF STATE]
proof (prove)
using this:
?d + ?b - ?c = ?d - ?c + ?b

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (2 ^ n) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (2 ^ n) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using P12
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using f'a_not_infinite
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (2 ^ n) * t
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
val_Zp (f' \<bullet> a) \<noteq> \<infinity>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
have P14: "val_Zp ((f' \<bullet> ns k) \<ominus> (f' \<bullet> ns n)) > (val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
using f'a_not_infinite ge_plus_pos_imp_gt t_times_pow_pos
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
val_Zp (f' \<bullet> a) \<noteq> \<infinity>
\<lbrakk>?c \<noteq> \<infinity>; 0 < ?b; ?c + ?b \<le> ?d\<rbrakk> \<Longrightarrow> ?c < ?d
0 < eint (2 ^ ?n) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (f' \<bullet> ns k \<ominus> f' \<bullet> ns n)

goal (1 subgoal):
 1. f' \<bullet> ns k \<noteq> f' \<bullet> ns n \<Longrightarrow> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by (meson F1 F2 P0 P14 equal_val_Zp f'_closed f'a_closed to_fun_closed)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have P2: "val_Zp (f\<bullet>(ns k)) \<ge> 2*(val_Zp (f'\<bullet>a)) + (2^k)*t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have P23: "2 * (val_Zp (f'\<bullet>a)) + ((2 ^ k) * t) \<le> val_Zp (f \<bullet> ns k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have 0: "ns n \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n \<in> carrier Zp
[PROOF STEP]
by (simp add: F1)
[PROOF STATE]
proof (state)
this:
ns n \<in> carrier Zp

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have 1: "local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
using F5
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have 2: "(poly_shift_iter 2 (taylor (ns n) f)) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
using F1 F5 shift_closed 1
[PROOF STATE]
proof (prove)
using this:
ns n \<in> carrier Zp
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
?f \<in> carrier (UP Zp) \<Longrightarrow> shift ?n ?f \<in> carrier (UP Zp)
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
[PROOF STEP]
by (simp add: taylor_closed to_fun_closed)
[PROOF STATE]
proof (state)
this:
shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have 3: "divide (f \<bullet> ns n) (f' \<bullet> ns n) \<otimes> deriv f (ns n) = f \<bullet> ns n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<otimes> deriv f (ns n) = f \<bullet> ns n
[PROOF STEP]
by (metis F1 F2 F6 divide_formula f'_closed f'a_not_infinite f_closed mult_comm pderiv_eval_deriv to_fun_closed val_Zp_def)
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<otimes> deriv f (ns n) = f \<bullet> ns n

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have 4: "f \<in> carrier Zp_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> carrier (UP Zp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<in> carrier (UP Zp)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
obtain c where c_def: "c = poly_shift_iter (2::nat) (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. c = shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c = shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
have c_def': "c \<in> carrier Zp \<and> f \<bullet> (ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] (2::nat)"
[PROOF STATE]
proof (prove)
using this:
c = shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)

goal (1 subgoal):
 1. c \<in> carrier Zp \<and> f \<bullet> (ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2
[PROOF STEP]
using 0 1 2 3 4 UP_cring.taylor_deg_1_eval'''[of Zp f "ns n" "(divide (f\<bullet>(ns n)) (f'\<bullet>(ns n)))" c]
                Zp_x_is_UP_cring
[PROOF STATE]
proof (prove)
using this:
c = shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
ns n \<in> carrier Zp
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<otimes> deriv f (ns n) = f \<bullet> ns n
f \<in> carrier (UP Zp)
\<lbrakk>UP_cring Zp; f \<in> carrier (UP Zp); ns n \<in> carrier Zp; local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp; c = shift 2 (taylor (ns n) f) \<bullet> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n); local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<otimes> deriv f (ns n) = f \<bullet> ns n\<rbrakk> \<Longrightarrow> f \<bullet> (ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2
UP_cring Zp

goal (1 subgoal):
 1. c \<in> carrier Zp \<and> f \<bullet> (ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c \<in> carrier Zp \<and> f \<bullet> (ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have P230: "f\<bullet>(ns k) =  (c \<otimes> (divide (f\<bullet>(ns n)) (f'\<bullet>(ns n)))[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns k = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2
[PROOF STEP]
using c_def'
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier Zp \<and> f \<bullet> (ns n \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)) = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2

goal (1 subgoal):
 1. f \<bullet> ns k = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2
[PROOF STEP]
by (simp add: kval newton_step_def)
[PROOF STATE]
proof (state)
this:
f \<bullet> ns k = c \<otimes> local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have P231: "val_Zp (f\<bullet>(ns k)) = val_Zp c + 2*(val_Zp (f\<bullet>(ns n)) - val_Zp(f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f \<bullet> ns k) = val_Zp c + eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f \<bullet> ns k) = val_Zp c + eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))
[PROOF STEP]
have P2310: "val_Zp (f\<bullet>(ns k)) =  val_Zp c + val_Zp ((divide (f\<bullet>(ns n)) (f'\<bullet>(ns n)))[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f \<bullet> ns k) = val_Zp c + val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2)
[PROOF STEP]
by (simp add: F5 P230 c_def' val_Zp_mult)
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> ns k) = val_Zp c + val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2)

goal (1 subgoal):
 1. val_Zp (f \<bullet> ns k) = val_Zp c + eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))
[PROOF STEP]
have P2311: "val_Zp ((divide (f\<bullet>(ns n)) (f'\<bullet>(ns n)))[^](2::nat))
                                                    =  2*(val_Zp (f\<bullet>(ns n)) - val_Zp(f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2) = eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))
[PROOF STEP]
by (metis  F5 F7 R.pow_zero mult.commute not_nonzero_Zp of_nat_numeral times_eint_simps(3) val_Zp_def val_Zp_pow' zero_less_numeral)
[PROOF STATE]
proof (state)
this:
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2) = eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))

goal (1 subgoal):
 1. val_Zp (f \<bullet> ns k) = val_Zp c + eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n) [^] 2) = eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))

goal (1 subgoal):
 1. val_Zp (f \<bullet> ns k) = val_Zp c + eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))
[PROOF STEP]
by (simp add: P2310)
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> ns k) = val_Zp c + eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> ns k) = val_Zp c + eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have P232: "val_Zp (f\<bullet>(ns k)) \<ge> 2*(val_Zp (f\<bullet>(ns n)) - val_Zp(f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by (simp add: P231 c_def' val_pos)
[PROOF STATE]
proof (state)
this:
eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have P236:  "val_Zp (f\<bullet>(ns k)) \<ge> 2*(2 *val_Zp (f'\<bullet>a) + 2 ^ n * t)  - 2* val_Zp(f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
using P232 F3 eint_minus_ineq''[of "val_Zp(f'\<bullet>(ns n))" "(2 *val_Zp (f'\<bullet>a)) + 2 ^ n * t" "val_Zp (f\<bullet>(ns n))" 2 ]
                       F2 eint_pow_int_is_pos
[PROOF STATE]
proof (prove)
using this:
eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)) \<le> val_Zp (f \<bullet> ns k)
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
\<lbrakk>val_Zp (f' \<bullet> ns n) \<noteq> \<infinity>; eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n); 0 < eint 2; eint 2 \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> eint 2 * (val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n))
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
0 < ?n \<Longrightarrow> 0 < eint ?n

goal (1 subgoal):
 1. eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
hence  P237:  "val_Zp (f\<bullet>(ns k)) \<ge>(4*val_Zp (f'\<bullet>a)) + (2*((2 ^ n)* t)) - 2* val_Zp(f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
using this:
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k) \<Longrightarrow> eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
have "2*(2*val_Zp (f'\<bullet>a) + 2 ^ n * t)  = (4*val_Zp (f'\<bullet>a)) + 2*(2 ^ n)* t "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) = eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t
[PROOF STEP]
using distrib_left[of 2 "2*val_Zp (f'\<bullet>a)" "2 ^ n * t"] mult.assoc mult_one_right one_eint_def plus_eint_simps(1)
                          hensel_factor_def val_Zp_def
[PROOF STATE]
proof (prove)
using this:
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) = eint 2 * (eint 2 * val_Zp (f' \<bullet> a)) + eint 2 * (eint (2 ^ n) * t)
?a * ?b * ?c = ?a * (?b * ?c)
?n * 1 = ?n
1 = eint 1
eint ?m + eint ?n = eint (?m + ?n)
t = val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (1 subgoal):
 1. eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) = eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) = eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t

goal (1 subgoal):
 1. eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k) \<Longrightarrow> eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) = eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) = eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t

goal (1 subgoal):
 1. eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
using P236
[PROOF STATE]
proof (prove)
using this:
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) = eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t
eint 2 * (eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by (metis mult.assoc)
[PROOF STATE]
proof (state)
this:
eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
hence P237:  "val_Zp (f\<bullet>(ns k)) \<ge> 4*val_Zp (f'\<bullet>a) + 2*(2 ^ n)* t - 2* val_Zp((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
eint 4 * val_Zp (f' \<bullet> a) + eint 2 * (eint (2 ^ n) * t) - eint 2 * val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t - eint 2 * val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by (metis F2 mult.assoc)
[PROOF STATE]
proof (state)
this:
eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t - eint 2 * val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
hence P238: "val_Zp (f\<bullet>(ns k)) \<ge> 2*val_Zp (f'\<bullet>a) + 2*(2 ^ n)* t"
[PROOF STATE]
proof (prove)
using this:
eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t - eint 2 * val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
using eint_minus_comm[of "4*val_Zp (f'\<bullet>a) " "2*(2 ^ n)* t" "2* val_Zp((f'\<bullet>a))"]
[PROOF STATE]
proof (prove)
using this:
eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t - eint 2 * val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns k)
eint 4 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t - eint 2 * val_Zp (f' \<bullet> a) = eint 4 * val_Zp (f' \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by (simp add: eint_int_minus_distr)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by (simp add: kval)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
show "val_Zp (to_fun f' (ns k)) = val_Zp (f'\<bullet>a) \<and>
                2 * val_Zp (f'\<bullet>a) + eint (2 ^ k) * t \<le> val_Zp (to_fun f (ns k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
using P1 P2
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma newton_seq_closed:
shows "ns m \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns m \<in> carrier Zp
[PROOF STEP]
using newton_seq_props_induct
[PROOF STATE]
proof (prove)
using this:
?k \<le> ?n \<Longrightarrow> ns ?k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k) * t \<le> val_Zp (f \<bullet> ns ?k)

goal (1 subgoal):
 1. ns m \<in> carrier Zp
[PROOF STEP]
by blast


[STATEMENT]
lemma f_of_newton_seq_closed:
shows "f \<bullet> ns m \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns m \<in> carrier Zp
[PROOF STEP]
by (simp add: to_fun_closed newton_seq_closed)


[STATEMENT]
lemma newton_seq_fact1[simp]:
" val_Zp (f'\<bullet>(ns k)) = val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using newton_seq_props_induct
[PROOF STATE]
proof (prove)
using this:
?k \<le> ?n \<Longrightarrow> ns ?k \<in> carrier Zp \<and> val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a) \<and> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k) * t \<le> val_Zp (f \<bullet> ns ?k)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns k) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by blast


[STATEMENT]
lemma newton_seq_fact2:
"\<And>k.  val_Zp (f\<bullet>(ns k)) \<ge> 2*(val_Zp (f'\<bullet>a)) + (2^k)*t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by (meson le_iff_add newton_seq_props_induct)


[STATEMENT]
lemma newton_seq_fact3:
"val_Zp (f\<bullet>(ns l)) \<ge> val_Zp (f'\<bullet>(ns l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
have "2*(val_Zp (f'\<bullet>a)) + (2^l)*t \<ge> (val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t
[PROOF STEP]
using f'a_closed ord_pos t_pos
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> a \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> ord_Zp ?x
0 < t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t
[PROOF STEP]
by (smt eint_pos_int_times_ge f'a_nonneg_val f'a_not_infinite ge_plus_pos_imp_gt linorder_not_less nat_mult_not_infty order_less_le t_times_pow_pos)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t
[PROOF STEP]
show "val_Zp (f \<bullet> ns l) \<ge> val_Zp (f' \<bullet> ns l) "
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
using  f'a_closed f'a_nonzero newton_seq_fact1[of l] newton_seq_fact2[of l]  val_Zp_def
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t
f' \<bullet> a \<in> carrier Zp
f' \<bullet> a \<noteq> \<zero>
val_Zp (f' \<bullet> ns l) = val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t \<le> val_Zp (f \<bullet> ns l)
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t; f' \<bullet> a \<in> carrier Zp; f' \<bullet> a \<noteq> \<zero>; val_Zp (f' \<bullet> ns l) = val_Zp (f' \<bullet> a); eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t \<le> val_Zp (f \<bullet> ns l); val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))\<rbrakk> \<Longrightarrow> val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
using \<open>eint 2 * val_Zp (f'\<bullet>a) + eint (2 ^ l) * t \<le> val_Zp (to_fun f (ns l))\<close> \<open>val_Zp (f'\<bullet>a) \<le> eint 2 * val_Zp (f'\<bullet>a) + eint (2 ^ l) * t\<close>
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t \<le> val_Zp (f \<bullet> ns l)
val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ l) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma newton_seq_fact4[simp]:
  assumes "f\<bullet>(ns l) \<noteq>\<zero>"
  shows "val_Zp (f\<bullet>(ns l)) \<ge> val_Zp (f'\<bullet>(ns l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
using newton_seq_fact3
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns ?l) \<le> val_Zp (f \<bullet> ns ?l)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
by blast


[STATEMENT]
lemma newton_seq_fact5:
"divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
[PROOF STEP]
apply(rule divide_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. f \<bullet> ns l \<in> carrier Zp
 2. f' \<bullet> ns l \<in> carrier Zp
 3. f' \<bullet> ns l \<noteq> \<zero>
[PROOF STEP]
apply (simp add: to_fun_closed newton_seq_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f' \<bullet> ns l \<in> carrier Zp
 2. f' \<bullet> ns l \<noteq> \<zero>
[PROOF STEP]
apply (simp add: f'_closed to_fun_closed newton_seq_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns l \<noteq> \<zero>
[PROOF STEP]
by (metis f'a_not_infinite newton_seq_fact1 val_Zp_def)


[STATEMENT]
lemma newton_seq_fact6:
"(f'\<bullet>(ns l)) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns l \<in> nonzero Zp
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns l \<notin> nonzero Zp \<Longrightarrow> False
[PROOF STEP]
using  nonzero_memI nonzero_memE
        f'a_nonzero newton_seq_fact1  val_Zp_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> carrier Zp; ?a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ?a \<in> nonzero Zp
?a \<in> nonzero Zp \<Longrightarrow> ?a \<in> carrier Zp
?a \<in> nonzero Zp \<Longrightarrow> ?a \<noteq> \<zero>
f' \<bullet> a \<noteq> \<zero>
val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a)
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (1 subgoal):
 1. f' \<bullet> ns l \<notin> nonzero Zp \<Longrightarrow> False
[PROOF STEP]
by (metis (no_types, lifting) divide_closed f'_closed f'a_closed fa_closed hensel_factor_id
      hensel_hypothesis_weakened mult_zero_l newton_seq_closed order_less_le to_fun_closed val_Zp_mult)