你需要这个来获得我的进口：
(* tested with Isabelle2013-2 *)
theory Notepad
imports
Main
"~~/src/HOL/Library/Polynomial"
begin
notepad
begin
我有三个几乎相同的引理。
版本1：
{
fix a :: "('a:: comm_ring_1) poly"
have "degree((monom 1 1) -CONST pCons a 0) =1" sledgehammer
版本2：
{
fix a :: "('a:: comm_ring_1) poly"
def p ≡ "(monom 1 1) - CONST pCons a 0"
from p_def have "degree p = 1"
版本 3：
{
fix a :: "('a:: comm_ring_1) poly"
have "p ≡ (monom 1 1) - CONST pCons a 0 ⟹ degree p = 1"
这是运行大锤的结果，仅显示e定理证明器的结果；它显示了三个完全不同的结果：
(*
for instance, the three results of the prover e are:
"e": Try this: by (metis One_nat_def degree_1 degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one) (2.12 s).
"e": Try this: by (metis coeff_diff coeff_monom coeff_pCons_Suc degree_pCons_eq_if diff_0_right leading_coeff_0_iff pCons_cases zero_neq_one) (> 3 s).
"e": Try this: by (metis One_nat_def degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one) (214 ms).
*)
问： 为什么会这样？大锤是不确定的吗？还是伊莎贝尔的三个版本不同，所以大锤得到三个不同的输入？
(* tested with Isabelle2013-2 *)
theory Notepad
imports
Main
"~~/src/HOL/Library/Polynomial"
begin
notepad
begin
Here is the full code:
{
fix a :: "('a:: comm_ring_1) poly"
have "degree((monom 1 1) -CONST pCons a 0) =1"
(*
Sledgehammering...
"spass": Try this: by (metis One_nat_def degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one) (2.13 s).
"e": Try this: by (metis One_nat_def degree_1 degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one) (2.12 s).
To minimize: sledgehammer min (One_nat_def degree_1 degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one).
"z3": Timed out.
"remote_vampire": Timed out.
"remote_e_sine": Try this: by (smt Nat.add_0_right Nat.add_diff_inverse Nat.diff_cancel One_nat_def Suc_diff_1 Suc_diff_Suc Suc_diff_diff Suc_diff_eq_diff_pred Suc_eq_plus1 Suc_eq_plus1_left Suc_inject Suc_le_mono Suc_lessD Suc_lessE Suc_lessI Suc_less_SucD Suc_less_eq Suc_mono Suc_neq_Zero Suc_pred Suc_pred' Zero_neq_Suc Zero_not_Suc add_Suc add_Suc_right add_Suc_shift add_diff_cancel_left' add_diff_cancel_right add_diff_cancel_right' add_eq_if add_eq_self_zero add_gr_0 add_is_0 add_is_1 add_left_cancel add_lessD1 add_less_cancel_left add_less_cancel_right add_less_mono add_less_mono1 add_pCons add_pos_pos add_right_cancel bool.size(1) bool.size(2) bool.size(3) bool.size(4) coeff_0 coeff_1 coeff_add coeff_diff coeff_linear_power coeff_monom coeff_pCons_0 coeff_pCons_Suc comm_monoid_add_class.add.left_neutral comm_monoid_add_class.add.right_neutral comm_monoid_diff_class.add_diff_cancel_left comm_monoid_diff_class.diff_cancel comm_semiring_1_class.normalizing_semiring_rules(32) comm_semiring_1_class.normalizing_semiring_rules(33) degree_0 degree_1 degree_linear_power degree_monom_eq degree_pCons_0 degree_pCons_eq degree_pCons_eq_if degree_synthetic_div diff_0_eq_0 diff_0_right diff_Suc_1 diff_Suc_Suc diff_Suc_eq_diff_pred diff_Suc_less diff_add_0 diff_add_inverse diff_add_inverse2 diff_add_zero diff_cancel2 diff_commute diff_diff_cancel diff_diff_left diff_eq_diff_eq diff_induct diff_is_0_eq diff_is_0_eq' diff_less diff_less_Suc diff_less_iff(1) diff_less_iff(2) diff_less_iff(3) diff_less_iff(4) diff_less_mono2 diff_monom diff_pCons diff_right_commute diff_self diff_self_eq_0 diff_zero diffs0_imp_equal double_add_less_zero_iff_single_add_less_zero double_zero double_zero_sym dvd.dual_order.refl dvd.lift_Suc_mono_less dvd.lift_Suc_mono_less_iff dvd_1_iff_1 dvd_1_left dvd_diff_nat dvd_minus_self dvd_plusE dvd_plus_eq_left dvd_plus_eq_right dvd_pos_nat dvd_reduce eq_diff_eq' eq_iff_diff_eq_0 exists_least_lemma field_power_not_zero gcd_lcm_complete_lattice_nat.bot.extremum gcd_lcm_complete_lattice_nat.bot.extremum_strict gcd_lcm_complete_lattice_nat.bot.extremum_unique gcd_lcm_complete_lattice_nat.bot.extremum_uniqueI gcd_lcm_complete_lattice_nat.bot.not_eq_extremum gcd_lcm_complete_lattice_nat.top.extremum_strict gcd_lcm_complete_lattice_nat.top.extremum_unique gcd_lcm_complete_lattice_nat.top.extremum_uniqueI gcd_lcm_complete_lattice_nat.top.not_eq_extremum gcd_lcm_complete_lattice_nat.top_greatest gr0I gr0_conv_Suc gr0_implies_Suc gr_implies_not0 ind_euclid infinite_descent infinite_descent0 is_zero_null le0 le_0_eq le_add_diff_inverse le_add_diff_inverse2 leading_coeff_0_iff leading_coeff_neq_0 lessE lessI less_Suc0 less_SucE less_SucI less_Suc_eq less_Suc_eq_0_disj less_Suc_induct less_add_Suc1 less_add_Suc2 less_add_eq_less less_antisym less_diff_conv less_dvd_minus less_iff_Suc_add less_imp_Suc_add less_imp_add_positive less_imp_diff_less less_irrefl_nat less_nat_zero_code less_not_refl less_not_refl2 less_not_refl3 less_trans_Suc less_zeroE lift_Suc_mono_less lift_Suc_mono_less_iff linorder_neqE_nat list_decode.cases minus_nat.diff_0 minus_poly.rep_eq minus_real_def monoid_add_class.add.left_neutral monoid_add_class.add.right_neutral monom.rep_eq monom_0 monom_Suc monom_eq_0 monom_eq_0_iff monom_eq_iff n_not_Suc_n nat.inject nat.size(1) nat.size(2) nat.size(3) nat.size(4) nat_add_assoc nat_add_commute nat_add_left_cancel nat_add_left_cancel_le nat_add_left_cancel_less nat_add_left_commute nat_add_right_cancel nat_diff_split nat_diff_split_asm nat_dvd_not_less nat_induct nat_less_cases nat_less_induct nat_lt_two_imp_zero_or_one nat_neq_iff nat_power_eq_Suc_0_iff nat_power_less_imp_less nat_zero_less_power_iff neq0_conv not0_implies_Suc not_add_less1 not_add_less2 not_less0 not_less_eq not_less_less_Suc_eq one_is_add one_poly_def one_reorient order_root pCons_0_0 pCons_cases pCons_eq_0_iff pCons_eq_iff pCons_induct pcompose_0 plus_nat.add_0 poly_0 poly_1 poly_add poly_all_0_iff_0 poly_diff poly_gcd_0_0 poly_gcd_monic poly_gcd_zero_iff poly_minus_degree_zero_const poly_power pow_divides_eq_int pow_divides_eq_nat pow_divides_pow_int pow_divides_pow_nat power_0 power_0_Suc power_0_left power_Suc_0 power_eq_0_iff power_inject_exp power_one power_one_right power_strict_increasing_iff real_0_less_add_iff real_add_eq_0_iff real_add_less_0_iff real_add_minus_iff real_arch_pow real_arch_pow_inv real_lbound_gt_zero realpow_pos_nth realpow_pos_nth2 realpow_pos_nth_unique semiring_numeral_div_class.diff_zero size_bool strict_inc_induct synthetic_div_0 synthetic_div_eq_0_iff synthetic_div_pCons trans_less_add1 trans_less_add2 transitive_stepwise_gt transitive_stepwise_lt_eq triangle_0 triangle_Suc zero_diff zero_induct zero_induct_lemma zero_less_Suc zero_less_diff zero_less_double_add_iff_zero_less_single_add zero_less_power_nat_eq zero_neq_one zero_poly.rep_eq zero_reorient) (> 3 s).
To minimize: sledgehammer min [remote_e_sine] (Nat.add_0_right Nat.add_diff_inverse Nat.diff_cancel One_nat_def Suc_diff_1 Suc_diff_Suc Suc_diff_diff Suc_diff_eq_diff_pred Suc_eq_plus1 Suc_eq_plus1_left Suc_inject Suc_le_mono Suc_lessD Suc_lessE Suc_lessI Suc_less_SucD Suc_less_eq Suc_mono Suc_neq_Zero Suc_pred Suc_pred' Zero_neq_Suc Zero_not_Suc add_Suc add_Suc_right add_Suc_shift add_diff_cancel_left' add_diff_cancel_right add_diff_cancel_right' add_eq_if add_eq_self_zero add_gr_0 add_is_0 add_is_1 add_left_cancel add_lessD1 add_less_cancel_left add_less_cancel_right add_less_mono add_less_mono1 add_pCons add_pos_pos add_right_cancel bool.size(1) bool.size(2) bool.size(3) bool.size(4) coeff_0 coeff_1 coeff_add coeff_diff coeff_linear_power coeff_monom coeff_pCons_0 coeff_pCons_Suc comm_monoid_add_class.add.left_neutral comm_monoid_add_class.add.right_neutral comm_monoid_diff_class.add_diff_cancel_left comm_monoid_diff_class.diff_cancel comm_semiring_1_class.normalizing_semiring_rules(32) comm_semiring_1_class.normalizing_semiring_rules(33) degree_0 degree_1 degree_linear_power degree_monom_eq degree_pCons_0 degree_pCons_eq degree_pCons_eq_if degree_synthetic_div diff_0_eq_0 diff_0_right diff_Suc_1 diff_Suc_Suc diff_Suc_eq_diff_pred diff_Suc_less diff_add_0 diff_add_inverse diff_add_inverse2 diff_add_zero diff_cancel2 diff_commute diff_diff_cancel diff_diff_left diff_eq_diff_eq diff_induct diff_is_0_eq diff_is_0_eq' diff_less diff_less_Suc diff_less_iff(1) diff_less_iff(2) diff_less_iff(3) diff_less_iff(4) diff_less_mono2 diff_monom diff_pCons diff_right_commute diff_self diff_self_eq_0 diff_zero diffs0_imp_equal double_add_less_zero_iff_single_add_less_zero double_zero double_zero_sym dvd.dual_order.refl dvd.lift_Suc_mono_less dvd.lift_Suc_mono_less_iff dvd_1_iff_1 dvd_1_left dvd_diff_nat dvd_minus_self dvd_plusE dvd_plus_eq_left dvd_plus_eq_right dvd_pos_nat dvd_reduce eq_diff_eq' eq_iff_diff_eq_0 exists_least_lemma field_power_not_zero gcd_lcm_complete_lattice_nat.bot.extremum gcd_lcm_complete_lattice_nat.bot.extremum_strict gcd_lcm_complete_lattice_nat.bot.extremum_unique gcd_lcm_complete_lattice_nat.bot.extremum_uniqueI gcd_lcm_complete_lattice_nat.bot.not_eq_extremum gcd_lcm_complete_lattice_nat.top.extremum_strict gcd_lcm_complete_lattice_nat.top.extremum_unique gcd_lcm_complete_lattice_nat.top.extremum_uniqueI gcd_lcm_complete_lattice_nat.top.not_eq_extremum gcd_lcm_complete_lattice_nat.top_greatest gr0I gr0_conv_Suc gr0_implies_Suc gr_implies_not0 ind_euclid infinite_descent infinite_descent0 is_zero_null le0 le_0_eq le_add_diff_inverse le_add_diff_inverse2 leading_coeff_0_iff leading_coeff_neq_0 lessE lessI less_Suc0 less_SucE less_SucI less_Suc_eq less_Suc_eq_0_disj less_Suc_induct less_add_Suc1 less_add_Suc2 less_add_eq_less less_antisym less_diff_conv less_dvd_minus less_iff_Suc_add less_imp_Suc_add less_imp_add_positive less_imp_diff_less less_irrefl_nat less_nat_zero_code less_not_refl less_not_refl2 less_not_refl3 less_trans_Suc less_zeroE lift_Suc_mono_less lift_Suc_mono_less_iff linorder_neqE_nat list_decode.cases minus_nat.diff_0 minus_poly.rep_eq minus_real_def monoid_add_class.add.left_neutral monoid_add_class.add.right_neutral monom.rep_eq monom_0 monom_Suc monom_eq_0 monom_eq_0_iff monom_eq_iff n_not_Suc_n nat.inject nat.size(1) nat.size(2) nat.size(3) nat.size(4) nat_add_assoc nat_add_commute nat_add_left_cancel nat_add_left_cancel_le nat_add_left_cancel_less nat_add_left_commute nat_add_right_cancel nat_diff_split nat_diff_split_asm nat_dvd_not_less nat_induct nat_less_cases nat_less_induct nat_lt_two_imp_zero_or_one nat_neq_iff nat_power_eq_Suc_0_iff nat_power_less_imp_less nat_zero_less_power_iff neq0_conv not0_implies_Suc not_add_less1 not_add_less2 not_less0 not_less_eq not_less_less_Suc_eq one_is_add one_poly_def one_reorient order_root pCons_0_0 pCons_cases pCons_eq_0_iff pCons_eq_iff pCons_induct pcompose_0 plus_nat.add_0 poly_0 poly_1 poly_add poly_all_0_iff_0 poly_diff poly_gcd_0_0 poly_gcd_monic poly_gcd_zero_iff poly_minus_degree_zero_const poly_power pow_divides_eq_int pow_divides_eq_nat pow_divides_pow_int pow_divides_pow_nat power_0 power_0_Suc power_0_left power_Suc_0 power_eq_0_iff power_inject_exp power_one power_one_right power_strict_increasing_iff real_0_less_add_iff real_add_eq_0_iff real_add_less_0_iff real_add_minus_iff real_arch_pow real_arch_pow_inv real_lbound_gt_zero realpow_pos_nth realpow_pos_nth2 realpow_pos_nth_unique semiring_numeral_div_class.diff_zero size_bool strict_inc_induct synthetic_div_0 synthetic_div_eq_0_iff synthetic_div_pCons trans_less_add1 trans_less_add2 transitive_stepwise_gt transitive_stepwise_lt_eq triangle_0 triangle_Suc zero_diff zero_induct zero_induct_lemma zero_less_Suc zero_less_diff zero_less_double_add_iff_zero_less_single_add zero_less_power_nat_eq zero_neq_one zero_poly.rep_eq zero_reorient).
*)
{
fix a :: "('a:: comm_ring_1) poly"
def p ≡ "(monom 1 1) - CONST pCons a 0"
from p_def have "degree p = 1"
(*
Sledgehammering...
"spass": Try this: by (metis One_nat_def degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one) (227 ms).
"remote_e_sine": Timed out.
"z3": Timed out.
"remote_vampire": Timed out.
"e": Try this: by (metis coeff_diff coeff_monom coeff_pCons_Suc degree_pCons_eq_if diff_0_right leading_coeff_0_iff pCons_cases zero_neq_one) (> 3 s).
Structured proof (> 9.08 s):
proof -
have f1: "⋀x⇩1 x⇩2. coeff 0 x⇩1 = (x⇩2∷'a poly) ∨ x⇩2 ≠ 0"
using coeff_monom by simp
have f2: "⋀x⇩1 x⇩2. (coeff (esk6⇩1 x⇩1) x⇩2∷'a poly) = coeff x⇩1 (Suc x⇩2)"
by (metis coeff_pCons_Suc pCons_cases)
have f3: "⋀x⇩1. coeff (monom 1 1) (Suc x⇩1) = coeff p (Suc x⇩1)"
using p_def by fastforce
have f4: "⋀x⇩1. Suc (degree (esk6⇩1 x⇩1)) = degree x⇩1 ∨ esk6⇩1 x⇩1 = 0"
by (metis degree_pCons_eq_if pCons_cases)
have "⋀x⇩1. degree x⇩1 = 0 ∨ esk6⇩1 x⇩1 ≠ 0"
by (metis degree_pCons_eq_if pCons_cases)
hence "esk6⇩1 p ≠ 0"
using f1 f2 f3 by (metis coeff_monom leading_coeff_0_iff zero_neq_one)
thus "degree p = 1"
using f2 f3 f4 by (metis coeff_monom leading_coeff_0_iff)
qed
*)
{
fix a :: "('a:: comm_ring_1) poly"
have "p ≡ (monom 1 1) - CONST pCons a 0 ⟹ degree p = 1"
(*
Sledgehammering...
"spass": Try this: by (metis One_nat_def degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one) (210 ms).
"e": Try this: by (metis One_nat_def degree_pCons_eq_if diff_0_right diff_pCons monom_0 monom_Suc one_poly_def zero_neq_one) (214 ms).
"z3": Timed out.
"remote_e_sine": Try this: by (smt Nat.add_0_right Nat.add_diff_inverse Nat.diff_cancel One_nat_def Suc_diff_1 Suc_diff_Suc Suc_diff_diff Suc_diff_eq_diff_pred Suc_eq_plus1 Suc_eq_plus1_left Suc_inject Suc_le_mono Suc_lessD Suc_lessE Suc_lessI Suc_less_SucD Suc_less_eq Suc_mono Suc_neq_Zero Suc_pred Suc_pred' Zero_neq_Suc Zero_not_Suc add_Suc add_Suc_right add_Suc_shift add_diff_cancel_left' add_diff_cancel_right add_diff_cancel_right' add_eq_if add_eq_self_zero add_gr_0 add_is_0 add_is_1 add_left_cancel add_lessD1 add_less_cancel_left add_less_cancel_right add_less_mono add_less_mono1 add_pCons add_pos_pos add_right_cancel bool.size(1) bool.size(2) bool.size(3) bool.size(4) coeff_0 coeff_1 coeff_add coeff_diff coeff_linear_power coeff_monom coeff_pCons_0 coeff_pCons_Suc comm_monoid_add_class.add.left_neutral comm_monoid_add_class.add.right_neutral comm_monoid_diff_class.add_diff_cancel_left comm_monoid_diff_class.diff_cancel comm_semiring_1_class.normalizing_semiring_rules(32) comm_semiring_1_class.normalizing_semiring_rules(33) degree_0 degree_1 degree_linear_power degree_monom_eq degree_pCons_0 degree_pCons_eq degree_pCons_eq_if degree_synthetic_div diff_0_eq_0 diff_0_right diff_Suc_1 diff_Suc_Suc diff_Suc_eq_diff_pred diff_Suc_less diff_add_0 diff_add_inverse diff_add_inverse2 diff_add_zero diff_cancel2 diff_commute diff_diff_cancel diff_diff_left diff_eq_diff_eq diff_induct diff_is_0_eq diff_is_0_eq' diff_less diff_less_Suc diff_less_iff(1) diff_less_iff(2) diff_less_iff(3) diff_less_iff(4) diff_less_mono2 diff_monom diff_pCons diff_right_commute diff_self diff_self_eq_0 diff_zero diffs0_imp_equal double_add_less_zero_iff_single_add_less_zero double_zero double_zero_sym dvd.dual_order.refl dvd.lift_Suc_mono_less dvd.lift_Suc_mono_less_iff dvd_1_iff_1 dvd_1_left dvd_diff_nat dvd_minus_self dvd_plusE dvd_plus_eq_left dvd_plus_eq_right dvd_pos_nat dvd_reduce eq_diff_eq' eq_iff_diff_eq_0 exists_least_lemma field_power_not_zero gcd_lcm_complete_lattice_nat.bot.extremum gcd_lcm_complete_lattice_nat.bot.extremum_strict gcd_lcm_complete_lattice_nat.bot.extremum_unique gcd_lcm_complete_lattice_nat.bot.extremum_uniqueI gcd_lcm_complete_lattice_nat.bot.not_eq_extremum gcd_lcm_complete_lattice_nat.top.extremum_strict gcd_lcm_complete_lattice_nat.top.extremum_unique gcd_lcm_complete_lattice_nat.top.extremum_uniqueI gcd_lcm_complete_lattice_nat.top.not_eq_extremum gcd_lcm_complete_lattice_nat.top_greatest gr0I gr0_conv_Suc gr0_implies_Suc gr_implies_not0 ind_euclid infinite_descent infinite_descent0 is_zero_null le0 le_0_eq le_add_diff_inverse le_add_diff_inverse2 leading_coeff_0_iff leading_coeff_neq_0 lessE lessI less_Suc0 less_SucE less_SucI less_Suc_eq less_Suc_eq_0_disj less_Suc_induct less_add_Suc1 less_add_Suc2 less_add_eq_less less_antisym less_diff_conv less_dvd_minus less_iff_Suc_add less_imp_Suc_add less_imp_add_positive less_imp_diff_less less_irrefl_nat less_nat_zero_code less_not_refl less_not_refl2 less_not_refl3 less_trans_Suc less_zeroE lift_Suc_mono_less lift_Suc_mono_less_iff linorder_neqE_nat list_decode.cases minus_nat.diff_0 minus_poly.rep_eq minus_real_def monoid_add_class.add.left_neutral monoid_add_class.add.right_neutral monom.rep_eq monom_0 monom_Suc monom_eq_0 monom_eq_0_iff monom_eq_iff n_not_Suc_n nat.inject nat.size(1) nat.size(2) nat.size(3) nat.size(4) nat_add_assoc nat_add_commute nat_add_left_cancel nat_add_left_cancel_le nat_add_left_cancel_less nat_add_left_commute nat_add_right_cancel nat_diff_split nat_diff_split_asm nat_dvd_not_less nat_induct nat_less_cases nat_less_induct nat_lt_two_imp_zero_or_one nat_neq_iff nat_power_eq_Suc_0_iff nat_power_less_imp_less nat_zero_less_power_iff neq0_conv not0_implies_Suc not_add_less1 not_add_less2 not_less0 not_less_eq not_less_less_Suc_eq one_is_add one_poly_def one_reorient order_root pCons_0_0 pCons_cases pCons_eq_0_iff pCons_eq_iff pCons_induct pcompose_0 plus_nat.add_0 poly_0 poly_1 poly_add poly_all_0_iff_0 poly_diff poly_gcd_0_0 poly_gcd_monic poly_gcd_zero_iff poly_minus_degree_zero_const poly_power pow_divides_eq_int pow_divides_eq_nat pow_divides_pow_int pow_divides_pow_nat power_0 power_0_Suc power_0_left power_Suc_0 power_eq_0_iff power_inject_exp power_one power_one_right power_strict_increasing_iff real_0_less_add_iff real_add_eq_0_iff real_add_less_0_iff real_add_minus_iff real_arch_pow real_arch_pow_inv real_lbound_gt_zero realpow_pos_nth realpow_pos_nth2 realpow_pos_nth_unique semiring_numeral_div_class.diff_zero size_bool strict_inc_induct synthetic_div_0 synthetic_div_eq_0_iff synthetic_div_pCons trans_less_add1 trans_less_add2 transitive_stepwise_gt transitive_stepwise_lt_eq triangle_0 triangle_Suc zero_diff zero_induct zero_induct_lemma zero_less_Suc zero_less_diff zero_less_double_add_iff_zero_less_single_add zero_less_power_nat_eq zero_neq_one zero_poly.rep_eq zero_reorient) (> 3 s).
To minimize: sledgehammer min [remote_e_sine] (Nat.add_0_right Nat.add_diff_inverse Nat.diff_cancel One_nat_def Suc_diff_1 Suc_diff_Suc Suc_diff_diff Suc_diff_eq_diff_pred Suc_eq_plus1 Suc_eq_plus1_left Suc_inject Suc_le_mono Suc_lessD Suc_lessE Suc_lessI Suc_less_SucD Suc_less_eq Suc_mono Suc_neq_Zero Suc_pred Suc_pred' Zero_neq_Suc Zero_not_Suc add_Suc add_Suc_right add_Suc_shift add_diff_cancel_left' add_diff_cancel_right add_diff_cancel_right' add_eq_if add_eq_self_zero add_gr_0 add_is_0 add_is_1 add_left_cancel add_lessD1 add_less_cancel_left add_less_cancel_right add_less_mono add_less_mono1 add_pCons add_pos_pos add_right_cancel bool.size(1) bool.size(2) bool.size(3) bool.size(4) coeff_0 coeff_1 coeff_add coeff_diff coeff_linear_power coeff_monom coeff_pCons_0 coeff_pCons_Suc comm_monoid_add_class.add.left_neutral comm_monoid_add_class.add.right_neutral comm_monoid_diff_class.add_diff_cancel_left comm_monoid_diff_class.diff_cancel comm_semiring_1_class.normalizing_semiring_rules(32) comm_semiring_1_class.normalizing_semiring_rules(33) degree_0 degree_1 degree_linear_power degree_monom_eq degree_pCons_0 degree_pCons_eq degree_pCons_eq_if degree_synthetic_div diff_0_eq_0 diff_0_right diff_Suc_1 diff_Suc_Suc diff_Suc_eq_diff_pred diff_Suc_less diff_add_0 diff_add_inverse diff_add_inverse2 diff_add_zero diff_cancel2 diff_commute diff_diff_cancel diff_diff_left diff_eq_diff_eq diff_induct diff_is_0_eq diff_is_0_eq' diff_less diff_less_Suc diff_less_iff(1) diff_less_iff(2) diff_less_iff(3) diff_less_iff(4) diff_less_mono2 diff_monom diff_pCons diff_right_commute diff_self diff_self_eq_0 diff_zero diffs0_imp_equal double_add_less_zero_iff_single_add_less_zero double_zero double_zero_sym dvd.dual_order.refl dvd.lift_Suc_mono_less dvd.lift_Suc_mono_less_iff dvd_1_iff_1 dvd_1_left dvd_diff_nat dvd_minus_self dvd_plusE dvd_plus_eq_left dvd_plus_eq_right dvd_pos_nat dvd_reduce eq_diff_eq' eq_iff_diff_eq_0 exists_least_lemma field_power_not_zero gcd_lcm_complete_lattice_nat.bot.extremum gcd_lcm_complete_lattice_nat.bot.extremum_strict gcd_lcm_complete_lattice_nat.bot.extremum_unique gcd_lcm_complete_lattice_nat.bot.extremum_uniqueI gcd_lcm_complete_lattice_nat.bot.not_eq_extremum gcd_lcm_complete_lattice_nat.top.extremum_strict gcd_lcm_complete_lattice_nat.top.extremum_unique gcd_lcm_complete_lattice_nat.top.extremum_uniqueI gcd_lcm_complete_lattice_nat.top.not_eq_extremum gcd_lcm_complete_lattice_nat.top_greatest gr0I gr0_conv_Suc gr0_implies_Suc gr_implies_not0 ind_euclid infinite_descent infinite_descent0 is_zero_null le0 le_0_eq le_add_diff_inverse le_add_diff_inverse2 leading_coeff_0_iff leading_coeff_neq_0 lessE lessI less_Suc0 less_SucE less_SucI less_Suc_eq less_Suc_eq_0_disj less_Suc_induct less_add_Suc1 less_add_Suc2 less_add_eq_less less_antisym less_diff_conv less_dvd_minus less_iff_Suc_add less_imp_Suc_add less_imp_add_positive less_imp_diff_less less_irrefl_nat less_nat_zero_code less_not_refl less_not_refl2 less_not_refl3 less_trans_Suc less_zeroE lift_Suc_mono_less lift_Suc_mono_less_iff linorder_neqE_nat list_decode.cases minus_nat.diff_0 minus_poly.rep_eq minus_real_def monoid_add_class.add.left_neutral monoid_add_class.add.right_neutral monom.rep_eq monom_0 monom_Suc monom_eq_0 monom_eq_0_iff monom_eq_iff n_not_Suc_n nat.inject nat.size(1) nat.size(2) nat.size(3) nat.size(4) nat_add_assoc nat_add_commute nat_add_left_cancel nat_add_left_cancel_le nat_add_left_cancel_less nat_add_left_commute nat_add_right_cancel nat_diff_split nat_diff_split_asm nat_dvd_not_less nat_induct nat_less_cases nat_less_induct nat_lt_two_imp_zero_or_one nat_neq_iff nat_power_eq_Suc_0_iff nat_power_less_imp_less nat_zero_less_power_iff neq0_conv not0_implies_Suc not_add_less1 not_add_less2 not_less0 not_less_eq not_less_less_Suc_eq one_is_add one_poly_def one_reorient order_root pCons_0_0 pCons_cases pCons_eq_0_iff pCons_eq_iff pCons_induct pcompose_0 plus_nat.add_0 poly_0 poly_1 poly_add poly_all_0_iff_0 poly_diff poly_gcd_0_0 poly_gcd_monic poly_gcd_zero_iff poly_minus_degree_zero_const poly_power pow_divides_eq_int pow_divides_eq_nat pow_divides_pow_int pow_divides_pow_nat power_0 power_0_Suc power_0_left power_Suc_0 power_eq_0_iff power_inject_exp power_one power_one_right power_strict_increasing_iff real_0_less_add_iff real_add_eq_0_iff real_add_less_0_iff real_add_minus_iff real_arch_pow real_arch_pow_inv real_lbound_gt_zero realpow_pos_nth realpow_pos_nth2 realpow_pos_nth_unique semiring_numeral_div_class.diff_zero size_bool strict_inc_induct synthetic_div_0 synthetic_div_eq_0_iff synthetic_div_pCons trans_less_add1 trans_less_add2 transitive_stepwise_gt transitive_stepwise_lt_eq triangle_0 triangle_Suc zero_diff zero_induct zero_induct_lemma zero_less_Suc zero_less_diff zero_less_double_add_iff_zero_less_single_add zero_less_power_nat_eq zero_neq_one zero_poly.rep_eq zero_reorient).
Sledgehammer ran out of time.
*)