Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ B. ∀ p. ∀ a. (∀ x. Le(x,B) → ¬PowerDivides(p,x,a)) ∨ (∃ x. BoundedPowerValuation(p,a,B,x))Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
9 occurrences
Exact expanded native-PA statement
forall B p a. (forall f. (exists bpv_gap_search_none_bound. bpv_gap_search_none_bound + f = B) -> ~(exists bpv_result_search_property. ((exists ff_b_search_property_power ff_c_search_property_power. ((forall ff_i_search_property_power_repeat. (exists ff_lt_search_property_power_repeat_bound. ff_lt_search_property_power_repeat_bound + S ff_i_search_property_power_repeat = f) -> (((exists ff_h_search_property_power_repeat_decoded. ff_h_search_property_power_repeat_decoded + S (p) = S ((S (ff_i_search_property_power_repeat)) * ff_c_search_property_power)) /\ exists ff_q_search_property_power_repeat_decoded. ff_b_search_property_power = ff_q_search_property_power_repeat_decoded * S ((S (ff_i_search_property_power_repeat)) * ff_c_search_property_power) + (p)))) /\ (exists ff_u_search_property_power_product ff_v_search_property_power_product. ((((exists ff_h_search_property_power_product_start. ff_h_search_property_power_product_start + S (1) = S ((S (0)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_start. ff_u_search_property_power_product = ff_q_search_property_power_product_start * S ((S (0)) * ff_v_search_property_power_product) + (1))) /\ ((((exists ff_h_search_property_power_product_terminal. ff_h_search_property_power_product_terminal + S (bpv_result_search_property) = S ((S (f)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_terminal. ff_u_search_property_power_product = ff_q_search_property_power_product_terminal * S ((S (f)) * ff_v_search_property_power_product) + (bpv_result_search_property))) /\ forall ff_i_search_property_power_product. (exists ff_lt_search_property_power_product_bound. ff_lt_search_property_power_product_bound + S ff_i_search_property_power_product = f) -> exists ff_p_search_property_power_product ff_r_search_property_power_product ff_s_search_property_power_product. ((((exists ff_h_search_property_power_product_factor. ff_h_search_property_power_product_factor + S (ff_p_search_property_power_product) = S ((S (ff_i_search_property_power_product)) * ff_c_search_property_power)) /\ exists ff_q_search_property_power_product_factor. ff_b_search_property_power = ff_q_search_property_power_product_factor * S ((S (ff_i_search_property_power_product)) * ff_c_search_property_power) + (ff_p_search_property_power_product))) /\ ((((exists ff_h_search_property_power_product_partial. ff_h_search_property_power_product_partial + S (ff_r_search_property_power_product) = S ((S (ff_i_search_property_power_product)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_partial. ff_u_search_property_power_product = ff_q_search_property_power_product_partial * S ((S (ff_i_search_property_power_product)) * ff_v_search_property_power_product) + (ff_r_search_property_power_product))) /\ ((((exists ff_h_search_property_power_product_successor. ff_h_search_property_power_product_successor + S (ff_s_search_property_power_product) = S ((S (S ff_i_search_property_power_product)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_successor. ff_u_search_property_power_product = ff_q_search_property_power_product_successor * S ((S (S ff_i_search_property_power_product)) * ff_v_search_property_power_product) + (ff_s_search_property_power_product))) /\ ff_s_search_property_power_product = ff_r_search_property_power_product * ff_p_search_property_power_product)))))))) /\ (exists bpv_factor_search_property_divides. a = bpv_result_search_property * bpv_factor_search_property_divides)))) \/ (exists e. ((exists bpv_gap_search_selected_bound. bpv_gap_search_selected_bound + e = B) /\ (exists bpv_result_search_selected. ((exists ff_b_search_selected_power ff_c_search_selected_power. ((forall ff_i_search_selected_power_repeat. (exists ff_lt_search_selected_power_repeat_bound. ff_lt_search_selected_power_repeat_bound + S ff_i_search_selected_power_repeat = e) -> (((exists ff_h_search_selected_power_repeat_decoded. ff_h_search_selected_power_repeat_decoded + S (p) = S ((S (ff_i_search_selected_power_repeat)) * ff_c_search_selected_power)) /\ exists ff_q_search_selected_power_repeat_decoded. ff_b_search_selected_power = ff_q_search_selected_power_repeat_decoded * S ((S (ff_i_search_selected_power_repeat)) * ff_c_search_selected_power) + (p)))) /\ (exists ff_u_search_selected_power_product ff_v_search_selected_power_product. ((((exists ff_h_search_selected_power_product_start. ff_h_search_selected_power_product_start + S (1) = S ((S (0)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_start. ff_u_search_selected_power_product = ff_q_search_selected_power_product_start * S ((S (0)) * ff_v_search_selected_power_product) + (1))) /\ ((((exists ff_h_search_selected_power_product_terminal. ff_h_search_selected_power_product_terminal + S (bpv_result_search_selected) = S ((S (e)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_terminal. ff_u_search_selected_power_product = ff_q_search_selected_power_product_terminal * S ((S (e)) * ff_v_search_selected_power_product) + (bpv_result_search_selected))) /\ forall ff_i_search_selected_power_product. (exists ff_lt_search_selected_power_product_bound. ff_lt_search_selected_power_product_bound + S ff_i_search_selected_power_product = e) -> exists ff_p_search_selected_power_product ff_r_search_selected_power_product ff_s_search_selected_power_product. ((((exists ff_h_search_selected_power_product_factor. ff_h_search_selected_power_product_factor + S (ff_p_search_selected_power_product) = S ((S (ff_i_search_selected_power_product)) * ff_c_search_selected_power)) /\ exists ff_q_search_selected_power_product_factor. ff_b_search_selected_power = ff_q_search_selected_power_product_factor * S ((S (ff_i_search_selected_power_product)) * ff_c_search_selected_power) + (ff_p_search_selected_power_product))) /\ ((((exists ff_h_search_selected_power_product_partial. ff_h_search_selected_power_product_partial + S (ff_r_search_selected_power_product) = S ((S (ff_i_search_selected_power_product)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_partial. ff_u_search_selected_power_product = ff_q_search_selected_power_product_partial * S ((S (ff_i_search_selected_power_product)) * ff_v_search_selected_power_product) + (ff_r_search_selected_power_product))) /\ ((((exists ff_h_search_selected_power_product_successor. ff_h_search_selected_power_product_successor + S (ff_s_search_selected_power_product) = S ((S (S ff_i_search_selected_power_product)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_successor. ff_u_search_selected_power_product = ff_q_search_selected_power_product_successor * S ((S (S ff_i_search_selected_power_product)) * ff_v_search_selected_power_product) + (ff_s_search_selected_power_product))) /\ ff_s_search_selected_power_product = ff_r_search_selected_power_product * ff_p_search_selected_power_product)))))))) /\ (exists bpv_factor_search_selected_divides. a = bpv_result_search_selected * bpv_factor_search_selected_divides)))) /\ forall f. (exists bpv_gap_search_candidate_bound. bpv_gap_search_candidate_bound + f = B) -> (exists bpv_result_search_candidate. ((exists ff_b_search_candidate_power ff_c_search_candidate_power. ((forall ff_i_search_candidate_power_repeat. (exists ff_lt_search_candidate_power_repeat_bound. ff_lt_search_candidate_power_repeat_bound + S ff_i_search_candidate_power_repeat = f) -> (((exists ff_h_search_candidate_power_repeat_decoded. ff_h_search_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_search_candidate_power_repeat)) * ff_c_search_candidate_power)) /\ exists ff_q_search_candidate_power_repeat_decoded. ff_b_search_candidate_power = ff_q_search_candidate_power_repeat_decoded * S ((S (ff_i_search_candidate_power_repeat)) * ff_c_search_candidate_power) + (p)))) /\ (exists ff_u_search_candidate_power_product ff_v_search_candidate_power_product. ((((exists ff_h_search_candidate_power_product_start. ff_h_search_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_start. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_start * S ((S (0)) * ff_v_search_candidate_power_product) + (1))) /\ ((((exists ff_h_search_candidate_power_product_terminal. ff_h_search_candidate_power_product_terminal + S (bpv_result_search_candidate) = S ((S (f)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_terminal. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_terminal * S ((S (f)) * ff_v_search_candidate_power_product) + (bpv_result_search_candidate))) /\ forall ff_i_search_candidate_power_product. (exists ff_lt_search_candidate_power_product_bound. ff_lt_search_candidate_power_product_bound + S ff_i_search_candidate_power_product = f) -> exists ff_p_search_candidate_power_product ff_r_search_candidate_power_product ff_s_search_candidate_power_product. ((((exists ff_h_search_candidate_power_product_factor. ff_h_search_candidate_power_product_factor + S (ff_p_search_candidate_power_product) = S ((S (ff_i_search_candidate_power_product)) * ff_c_search_candidate_power)) /\ exists ff_q_search_candidate_power_product_factor. ff_b_search_candidate_power = ff_q_search_candidate_power_product_factor * S ((S (ff_i_search_candidate_power_product)) * ff_c_search_candidate_power) + (ff_p_search_candidate_power_product))) /\ ((((exists ff_h_search_candidate_power_product_partial. ff_h_search_candidate_power_product_partial + S (ff_r_search_candidate_power_product) = S ((S (ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_partial. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_partial * S ((S (ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product) + (ff_r_search_candidate_power_product))) /\ ((((exists ff_h_search_candidate_power_product_successor. ff_h_search_candidate_power_product_successor + S (ff_s_search_candidate_power_product) = S ((S (S ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_successor. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_successor * S ((S (S ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product) + (ff_s_search_candidate_power_product))) /\ ff_s_search_candidate_power_product = ff_r_search_candidate_power_product * ff_p_search_candidate_power_product)))))))) /\ (exists bpv_factor_search_candidate_divides. a = bpv_result_search_candidate * bpv_factor_search_candidate_divides))) -> (exists bpv_gap_search_maximal. bpv_gap_search_maximal + f = e))Proof neighborhood
Direct theorem prerequisites
BT00Q3 power_divides_decidable BT000Y le_zero BT000E le_refl BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT0018 le_succDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (6)
01Induction on BL1–3
02Establish hboundaryL4–8
Establish this local claim before using it. It is not an additional assumption.
- L4
have hboundary : PowerDivides(p,0,a) ∨ ¬PowerDivides(p,0,a)Definitions: PowerDivides(p,0,a)Original native command in the exact edition - L5
specialize power_divides_decidable p - L6
specialize power_divides_decidable 0 - L7
specialize power_divides_decidable a - L8
exact power_divides_decidable
03Separate the logical casesL9–10
04Construct an explicit witnessL11–11
Supply the displayed value, then prove that it has the required property.
- L11
exists 0
05Separate the logical casesL12–13
06Use earlier factsL14–16
07Fix variables and assumptionsL17–19
08Establish hf0L20–26
09Separate the logical casesL27–27
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L27
left
10Fix variables and assumptionsL28–30
11Establish hf0L31–40
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le zero.
12Fix variables and assumptionsL41–42
13Establish hboundaryL43–47
Establish this local claim before using it. It is not an additional assumption.
- L43
have hboundary : PowerDivides(p,S B,a) ∨ ¬PowerDivides(p,S B,a)Definitions: PowerDivides(p,S B,a)Original native command in the exact edition - L44
specialize power_divides_decidable p - L45
specialize power_divides_decidable (S B) - L46
specialize power_divides_decidable a - L47
exact power_divides_decidable
14Separate the logical casesL48–49
15Construct an explicit witnessL50–50
Supply the displayed value, then prove that it has the required property.
- L50
exists S B
16Separate the logical casesL51–52
17Use earlier factsL53–55
18Fix variables and assumptionsL56–58
19Use earlier factsL59–59
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L59
exact hf
20Establish hpreviousL60–63
Establish this local claim before using it. It is not an additional assumption.
- L60
have hprevious : (∀ x. Le(x,B) → ¬PowerDivides(p,x,a)) ∨ (∃ x. BoundedPowerValuation(p,a,B,x))Definitions: Le(x,B)PowerDivides(p,x,a)BoundedPowerValuation(p,a,B,x)Original native command in the exact edition - L61
specialize IH p - L62
specialize IH a - L63
exact IH
21Separate the logical casesL64–65
22Fix variables and assumptionsL66–68
23Establish hsplitL69–73
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
24Separate the logical casesL74–74
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L74
cases hsplit
25Use earlier factsL75–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L75
apply hboundary_right
26Calculate and transport equalitiesL76–79
27Use earlier factsL80–87
28Separate the logical casesL88–91
29Construct an explicit witnessL92–92
Supply the displayed value, then prove that it has the required property.
- L92
exists x
30Separate the logical casesL93–94
31Use earlier factsL95–99
32Fix variables and assumptionsL100–102
33Establish hsplitL103–107
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
34Separate the logical casesL108–109
35Use earlier factsL110–110
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L110
apply hboundary_right
36Calculate and transport equalitiesL111–114
37Use earlier factsL115–122
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 122 lines
- 0001
induction B - 0002
intro p - 0003
intro a - 0004
have hboundary : PowerDivides(p,0,a) ∨ ¬PowerDivides(p,0,a)Exact native replay line
have hboundary : (exists bpvi_result_search_base_boundary. ((exists bpvi_b_search_base_boundary_power bpvi_c_search_base_boundary_power. ((forall bpvi_i_search_base_boundary_power. (exists bpvi_repeat_gap_search_base_boundary_power. bpvi_repeat_gap_search_base_boundary_power + S bpvi_i_search_base_boundary_power = 0) -> (((exists bpvi_h_search_base_boundary_power_repeat. bpvi_h_search_base_boundary_power_repeat + S (p) = S ((S (bpvi_i_search_base_boundary_power)) * bpvi_c_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_repeat. bpvi_b_search_base_boundary_power = bpvi_q_search_base_boundary_power_repeat * S ((S (bpvi_i_search_base_boundary_power)) * bpvi_c_search_base_boundary_power) + (p)))) /\ (exists bpvi_u_search_base_boundary_power bpvi_v_search_base_boundary_power. ((((exists bpvi_h_search_base_boundary_power_start. bpvi_h_search_base_boundary_power_start + S (1) = S ((S (0)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_start. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_start * S ((S (0)) * bpvi_v_search_base_boundary_power) + (1))) /\ ((((exists bpvi_h_search_base_boundary_power_terminal. bpvi_h_search_base_boundary_power_terminal + S (bpvi_result_search_base_boundary) = S ((S (0)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_terminal. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_terminal * S ((S (0)) * bpvi_v_search_base_boundary_power) + (bpvi_result_search_base_boundary))) /\ forall bpvi_j_search_base_boundary_power. (exists bpvi_product_gap_search_base_boundary_power. bpvi_product_gap_search_base_boundary_power + S bpvi_j_search_base_boundary_power = 0) -> exists bpvi_factor_search_base_boundary_power bpvi_partial_search_base_boundary_power bpvi_successor_search_base_boundary_power. ((((exists bpvi_h_search_base_boundary_power_factor. bpvi_h_search_base_boundary_power_factor + S (bpvi_factor_search_base_boundary_power) = S ((S (bpvi_j_search_base_boundary_power)) * bpvi_c_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_factor. bpvi_b_search_base_boundary_power = bpvi_q_search_base_boundary_power_factor * S ((S (bpvi_j_search_base_boundary_power)) * bpvi_c_search_base_boundary_power) + (bpvi_factor_search_base_boundary_power))) /\ ((((exists bpvi_h_search_base_boundary_power_partial. bpvi_h_search_base_boundary_power_partial + S (bpvi_partial_search_base_boundary_power) = S ((S (bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_partial. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_partial * S ((S (bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power) + (bpvi_partial_search_base_boundary_power))) /\ ((((exists bpvi_h_search_base_boundary_power_successor. bpvi_h_search_base_boundary_power_successor + S (bpvi_successor_search_base_boundary_power) = S ((S (S bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_successor. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_successor * S ((S (S bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power) + (bpvi_successor_search_base_boundary_power))) /\ bpvi_successor_search_base_boundary_power = bpvi_partial_search_base_boundary_power * bpvi_factor_search_base_boundary_power)))))))) /\ exists bpvi_divisor_factor_search_base_boundary. a = bpvi_result_search_base_boundary * bpvi_divisor_factor_search_base_boundary)) \/ ~(exists bpvi_result_search_base_boundary. ((exists bpvi_b_search_base_boundary_power bpvi_c_search_base_boundary_power. ((forall bpvi_i_search_base_boundary_power. (exists bpvi_repeat_gap_search_base_boundary_power. bpvi_repeat_gap_search_base_boundary_power + S bpvi_i_search_base_boundary_power = 0) -> (((exists bpvi_h_search_base_boundary_power_repeat. bpvi_h_search_base_boundary_power_repeat + S (p) = S ((S (bpvi_i_search_base_boundary_power)) * bpvi_c_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_repeat. bpvi_b_search_base_boundary_power = bpvi_q_search_base_boundary_power_repeat * S ((S (bpvi_i_search_base_boundary_power)) * bpvi_c_search_base_boundary_power) + (p)))) /\ (exists bpvi_u_search_base_boundary_power bpvi_v_search_base_boundary_power. ((((exists bpvi_h_search_base_boundary_power_start. bpvi_h_search_base_boundary_power_start + S (1) = S ((S (0)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_start. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_start * S ((S (0)) * bpvi_v_search_base_boundary_power) + (1))) /\ ((((exists bpvi_h_search_base_boundary_power_terminal. bpvi_h_search_base_boundary_power_terminal + S (bpvi_result_search_base_boundary) = S ((S (0)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_terminal. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_terminal * S ((S (0)) * bpvi_v_search_base_boundary_power) + (bpvi_result_search_base_boundary))) /\ forall bpvi_j_search_base_boundary_power. (exists bpvi_product_gap_search_base_boundary_power. bpvi_product_gap_search_base_boundary_power + S bpvi_j_search_base_boundary_power = 0) -> exists bpvi_factor_search_base_boundary_power bpvi_partial_search_base_boundary_power bpvi_successor_search_base_boundary_power. ((((exists bpvi_h_search_base_boundary_power_factor. bpvi_h_search_base_boundary_power_factor + S (bpvi_factor_search_base_boundary_power) = S ((S (bpvi_j_search_base_boundary_power)) * bpvi_c_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_factor. bpvi_b_search_base_boundary_power = bpvi_q_search_base_boundary_power_factor * S ((S (bpvi_j_search_base_boundary_power)) * bpvi_c_search_base_boundary_power) + (bpvi_factor_search_base_boundary_power))) /\ ((((exists bpvi_h_search_base_boundary_power_partial. bpvi_h_search_base_boundary_power_partial + S (bpvi_partial_search_base_boundary_power) = S ((S (bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_partial. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_partial * S ((S (bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power) + (bpvi_partial_search_base_boundary_power))) /\ ((((exists bpvi_h_search_base_boundary_power_successor. bpvi_h_search_base_boundary_power_successor + S (bpvi_successor_search_base_boundary_power) = S ((S (S bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power)) /\ exists bpvi_q_search_base_boundary_power_successor. bpvi_u_search_base_boundary_power = bpvi_q_search_base_boundary_power_successor * S ((S (S bpvi_j_search_base_boundary_power)) * bpvi_v_search_base_boundary_power) + (bpvi_successor_search_base_boundary_power))) /\ bpvi_successor_search_base_boundary_power = bpvi_partial_search_base_boundary_power * bpvi_factor_search_base_boundary_power)))))))) /\ exists bpvi_divisor_factor_search_base_boundary. a = bpvi_result_search_base_boundary * bpvi_divisor_factor_search_base_boundary)) - 0005
specialize power_divides_decidable p - 0006
specialize power_divides_decidable 0 - 0007
specialize power_divides_decidable a - 0008
exact power_divides_decidable - 0009
cases hboundary - 0010
right - 0011
exists 0 - 0012
split - 0013
split - 0014
specialize le_refl 0 - 0015
exact le_refl - 0016
exact hboundary_left - 0017
intro f - 0018
intro hf - 0019
intro hproperty - 0020
have hf0 : f = 0 - 0021
specialize le_zero f - 0022
apply le_zero - 0023
exact hf - 0024
rewrite hf0 - 0025
specialize le_refl 0 - 0026
exact le_refl - 0027
left - 0028
intro f - 0029
intro hf - 0030
intro hproperty - 0031
have hf0 : f = 0 - 0032
specialize le_zero f - 0033
apply le_zero - 0034
exact hf - 0035
apply hboundary_right - 0036
rewrite hf0 at hproperty - 0037
rewrite hf0 at hproperty - 0038
rewrite hf0 at hproperty - 0039
rewrite hf0 at hproperty - 0040
exact hproperty - 0041
intro p - 0042
intro a - 0043
have hboundary : PowerDivides(p,S B,a) ∨ ¬PowerDivides(p,S B,a)Exact native replay line
have hboundary : (exists bpvi_result_search_succ_boundary. ((exists bpvi_b_search_succ_boundary_power bpvi_c_search_succ_boundary_power. ((forall bpvi_i_search_succ_boundary_power. (exists bpvi_repeat_gap_search_succ_boundary_power. bpvi_repeat_gap_search_succ_boundary_power + S bpvi_i_search_succ_boundary_power = S B) -> (((exists bpvi_h_search_succ_boundary_power_repeat. bpvi_h_search_succ_boundary_power_repeat + S (p) = S ((S (bpvi_i_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_repeat. bpvi_b_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_repeat * S ((S (bpvi_i_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power) + (p)))) /\ (exists bpvi_u_search_succ_boundary_power bpvi_v_search_succ_boundary_power. ((((exists bpvi_h_search_succ_boundary_power_start. bpvi_h_search_succ_boundary_power_start + S (1) = S ((S (0)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_start. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_start * S ((S (0)) * bpvi_v_search_succ_boundary_power) + (1))) /\ ((((exists bpvi_h_search_succ_boundary_power_terminal. bpvi_h_search_succ_boundary_power_terminal + S (bpvi_result_search_succ_boundary) = S ((S (S B)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_terminal. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_terminal * S ((S (S B)) * bpvi_v_search_succ_boundary_power) + (bpvi_result_search_succ_boundary))) /\ forall bpvi_j_search_succ_boundary_power. (exists bpvi_product_gap_search_succ_boundary_power. bpvi_product_gap_search_succ_boundary_power + S bpvi_j_search_succ_boundary_power = S B) -> exists bpvi_factor_search_succ_boundary_power bpvi_partial_search_succ_boundary_power bpvi_successor_search_succ_boundary_power. ((((exists bpvi_h_search_succ_boundary_power_factor. bpvi_h_search_succ_boundary_power_factor + S (bpvi_factor_search_succ_boundary_power) = S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_factor. bpvi_b_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_factor * S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power) + (bpvi_factor_search_succ_boundary_power))) /\ ((((exists bpvi_h_search_succ_boundary_power_partial. bpvi_h_search_succ_boundary_power_partial + S (bpvi_partial_search_succ_boundary_power) = S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_partial. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_partial * S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power) + (bpvi_partial_search_succ_boundary_power))) /\ ((((exists bpvi_h_search_succ_boundary_power_successor. bpvi_h_search_succ_boundary_power_successor + S (bpvi_successor_search_succ_boundary_power) = S ((S (S bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_successor. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_successor * S ((S (S bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power) + (bpvi_successor_search_succ_boundary_power))) /\ bpvi_successor_search_succ_boundary_power = bpvi_partial_search_succ_boundary_power * bpvi_factor_search_succ_boundary_power)))))))) /\ exists bpvi_divisor_factor_search_succ_boundary. a = bpvi_result_search_succ_boundary * bpvi_divisor_factor_search_succ_boundary)) \/ ~(exists bpvi_result_search_succ_boundary. ((exists bpvi_b_search_succ_boundary_power bpvi_c_search_succ_boundary_power. ((forall bpvi_i_search_succ_boundary_power. (exists bpvi_repeat_gap_search_succ_boundary_power. bpvi_repeat_gap_search_succ_boundary_power + S bpvi_i_search_succ_boundary_power = S B) -> (((exists bpvi_h_search_succ_boundary_power_repeat. bpvi_h_search_succ_boundary_power_repeat + S (p) = S ((S (bpvi_i_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_repeat. bpvi_b_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_repeat * S ((S (bpvi_i_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power) + (p)))) /\ (exists bpvi_u_search_succ_boundary_power bpvi_v_search_succ_boundary_power. ((((exists bpvi_h_search_succ_boundary_power_start. bpvi_h_search_succ_boundary_power_start + S (1) = S ((S (0)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_start. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_start * S ((S (0)) * bpvi_v_search_succ_boundary_power) + (1))) /\ ((((exists bpvi_h_search_succ_boundary_power_terminal. bpvi_h_search_succ_boundary_power_terminal + S (bpvi_result_search_succ_boundary) = S ((S (S B)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_terminal. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_terminal * S ((S (S B)) * bpvi_v_search_succ_boundary_power) + (bpvi_result_search_succ_boundary))) /\ forall bpvi_j_search_succ_boundary_power. (exists bpvi_product_gap_search_succ_boundary_power. bpvi_product_gap_search_succ_boundary_power + S bpvi_j_search_succ_boundary_power = S B) -> exists bpvi_factor_search_succ_boundary_power bpvi_partial_search_succ_boundary_power bpvi_successor_search_succ_boundary_power. ((((exists bpvi_h_search_succ_boundary_power_factor. bpvi_h_search_succ_boundary_power_factor + S (bpvi_factor_search_succ_boundary_power) = S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_factor. bpvi_b_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_factor * S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_c_search_succ_boundary_power) + (bpvi_factor_search_succ_boundary_power))) /\ ((((exists bpvi_h_search_succ_boundary_power_partial. bpvi_h_search_succ_boundary_power_partial + S (bpvi_partial_search_succ_boundary_power) = S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_partial. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_partial * S ((S (bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power) + (bpvi_partial_search_succ_boundary_power))) /\ ((((exists bpvi_h_search_succ_boundary_power_successor. bpvi_h_search_succ_boundary_power_successor + S (bpvi_successor_search_succ_boundary_power) = S ((S (S bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power)) /\ exists bpvi_q_search_succ_boundary_power_successor. bpvi_u_search_succ_boundary_power = bpvi_q_search_succ_boundary_power_successor * S ((S (S bpvi_j_search_succ_boundary_power)) * bpvi_v_search_succ_boundary_power) + (bpvi_successor_search_succ_boundary_power))) /\ bpvi_successor_search_succ_boundary_power = bpvi_partial_search_succ_boundary_power * bpvi_factor_search_succ_boundary_power)))))))) /\ exists bpvi_divisor_factor_search_succ_boundary. a = bpvi_result_search_succ_boundary * bpvi_divisor_factor_search_succ_boundary)) - 0044
specialize power_divides_decidable p - 0045
specialize power_divides_decidable (S B) - 0046
specialize power_divides_decidable a - 0047
exact power_divides_decidable - 0048
cases hboundary - 0049
right - 0050
exists S B - 0051
split - 0052
split - 0053
specialize le_refl (S B) - 0054
exact le_refl - 0055
exact hboundary_left - 0056
intro f - 0057
intro hf - 0058
intro hproperty - 0059
exact hf - 0060
have hprevious : (∀ x. Le(x,B) → ¬PowerDivides(p,x,a)) ∨ (∃ x. BoundedPowerValuation(p,a,B,x))Exact native replay line
have hprevious : (forall f. (exists bpv_gap_search_none_bound. bpv_gap_search_none_bound + f = B) -> ~(exists bpv_result_search_property. ((exists ff_b_search_property_power ff_c_search_property_power. ((forall ff_i_search_property_power_repeat. (exists ff_lt_search_property_power_repeat_bound. ff_lt_search_property_power_repeat_bound + S ff_i_search_property_power_repeat = f) -> (((exists ff_h_search_property_power_repeat_decoded. ff_h_search_property_power_repeat_decoded + S (p) = S ((S (ff_i_search_property_power_repeat)) * ff_c_search_property_power)) /\ exists ff_q_search_property_power_repeat_decoded. ff_b_search_property_power = ff_q_search_property_power_repeat_decoded * S ((S (ff_i_search_property_power_repeat)) * ff_c_search_property_power) + (p)))) /\ (exists ff_u_search_property_power_product ff_v_search_property_power_product. ((((exists ff_h_search_property_power_product_start. ff_h_search_property_power_product_start + S (1) = S ((S (0)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_start. ff_u_search_property_power_product = ff_q_search_property_power_product_start * S ((S (0)) * ff_v_search_property_power_product) + (1))) /\ ((((exists ff_h_search_property_power_product_terminal. ff_h_search_property_power_product_terminal + S (bpv_result_search_property) = S ((S (f)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_terminal. ff_u_search_property_power_product = ff_q_search_property_power_product_terminal * S ((S (f)) * ff_v_search_property_power_product) + (bpv_result_search_property))) /\ forall ff_i_search_property_power_product. (exists ff_lt_search_property_power_product_bound. ff_lt_search_property_power_product_bound + S ff_i_search_property_power_product = f) -> exists ff_p_search_property_power_product ff_r_search_property_power_product ff_s_search_property_power_product. ((((exists ff_h_search_property_power_product_factor. ff_h_search_property_power_product_factor + S (ff_p_search_property_power_product) = S ((S (ff_i_search_property_power_product)) * ff_c_search_property_power)) /\ exists ff_q_search_property_power_product_factor. ff_b_search_property_power = ff_q_search_property_power_product_factor * S ((S (ff_i_search_property_power_product)) * ff_c_search_property_power) + (ff_p_search_property_power_product))) /\ ((((exists ff_h_search_property_power_product_partial. ff_h_search_property_power_product_partial + S (ff_r_search_property_power_product) = S ((S (ff_i_search_property_power_product)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_partial. ff_u_search_property_power_product = ff_q_search_property_power_product_partial * S ((S (ff_i_search_property_power_product)) * ff_v_search_property_power_product) + (ff_r_search_property_power_product))) /\ ((((exists ff_h_search_property_power_product_successor. ff_h_search_property_power_product_successor + S (ff_s_search_property_power_product) = S ((S (S ff_i_search_property_power_product)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_successor. ff_u_search_property_power_product = ff_q_search_property_power_product_successor * S ((S (S ff_i_search_property_power_product)) * ff_v_search_property_power_product) + (ff_s_search_property_power_product))) /\ ff_s_search_property_power_product = ff_r_search_property_power_product * ff_p_search_property_power_product)))))))) /\ (exists bpv_factor_search_property_divides. a = bpv_result_search_property * bpv_factor_search_property_divides)))) \/ (exists e. ((exists bpv_gap_search_selected_bound. bpv_gap_search_selected_bound + e = B) /\ (exists bpv_result_search_selected. ((exists ff_b_search_selected_power ff_c_search_selected_power. ((forall ff_i_search_selected_power_repeat. (exists ff_lt_search_selected_power_repeat_bound. ff_lt_search_selected_power_repeat_bound + S ff_i_search_selected_power_repeat = e) -> (((exists ff_h_search_selected_power_repeat_decoded. ff_h_search_selected_power_repeat_decoded + S (p) = S ((S (ff_i_search_selected_power_repeat)) * ff_c_search_selected_power)) /\ exists ff_q_search_selected_power_repeat_decoded. ff_b_search_selected_power = ff_q_search_selected_power_repeat_decoded * S ((S (ff_i_search_selected_power_repeat)) * ff_c_search_selected_power) + (p)))) /\ (exists ff_u_search_selected_power_product ff_v_search_selected_power_product. ((((exists ff_h_search_selected_power_product_start. ff_h_search_selected_power_product_start + S (1) = S ((S (0)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_start. ff_u_search_selected_power_product = ff_q_search_selected_power_product_start * S ((S (0)) * ff_v_search_selected_power_product) + (1))) /\ ((((exists ff_h_search_selected_power_product_terminal. ff_h_search_selected_power_product_terminal + S (bpv_result_search_selected) = S ((S (e)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_terminal. ff_u_search_selected_power_product = ff_q_search_selected_power_product_terminal * S ((S (e)) * ff_v_search_selected_power_product) + (bpv_result_search_selected))) /\ forall ff_i_search_selected_power_product. (exists ff_lt_search_selected_power_product_bound. ff_lt_search_selected_power_product_bound + S ff_i_search_selected_power_product = e) -> exists ff_p_search_selected_power_product ff_r_search_selected_power_product ff_s_search_selected_power_product. ((((exists ff_h_search_selected_power_product_factor. ff_h_search_selected_power_product_factor + S (ff_p_search_selected_power_product) = S ((S (ff_i_search_selected_power_product)) * ff_c_search_selected_power)) /\ exists ff_q_search_selected_power_product_factor. ff_b_search_selected_power = ff_q_search_selected_power_product_factor * S ((S (ff_i_search_selected_power_product)) * ff_c_search_selected_power) + (ff_p_search_selected_power_product))) /\ ((((exists ff_h_search_selected_power_product_partial. ff_h_search_selected_power_product_partial + S (ff_r_search_selected_power_product) = S ((S (ff_i_search_selected_power_product)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_partial. ff_u_search_selected_power_product = ff_q_search_selected_power_product_partial * S ((S (ff_i_search_selected_power_product)) * ff_v_search_selected_power_product) + (ff_r_search_selected_power_product))) /\ ((((exists ff_h_search_selected_power_product_successor. ff_h_search_selected_power_product_successor + S (ff_s_search_selected_power_product) = S ((S (S ff_i_search_selected_power_product)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_successor. ff_u_search_selected_power_product = ff_q_search_selected_power_product_successor * S ((S (S ff_i_search_selected_power_product)) * ff_v_search_selected_power_product) + (ff_s_search_selected_power_product))) /\ ff_s_search_selected_power_product = ff_r_search_selected_power_product * ff_p_search_selected_power_product)))))))) /\ (exists bpv_factor_search_selected_divides. a = bpv_result_search_selected * bpv_factor_search_selected_divides)))) /\ forall f. (exists bpv_gap_search_candidate_bound. bpv_gap_search_candidate_bound + f = B) -> (exists bpv_result_search_candidate. ((exists ff_b_search_candidate_power ff_c_search_candidate_power. ((forall ff_i_search_candidate_power_repeat. (exists ff_lt_search_candidate_power_repeat_bound. ff_lt_search_candidate_power_repeat_bound + S ff_i_search_candidate_power_repeat = f) -> (((exists ff_h_search_candidate_power_repeat_decoded. ff_h_search_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_search_candidate_power_repeat)) * ff_c_search_candidate_power)) /\ exists ff_q_search_candidate_power_repeat_decoded. ff_b_search_candidate_power = ff_q_search_candidate_power_repeat_decoded * S ((S (ff_i_search_candidate_power_repeat)) * ff_c_search_candidate_power) + (p)))) /\ (exists ff_u_search_candidate_power_product ff_v_search_candidate_power_product. ((((exists ff_h_search_candidate_power_product_start. ff_h_search_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_start. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_start * S ((S (0)) * ff_v_search_candidate_power_product) + (1))) /\ ((((exists ff_h_search_candidate_power_product_terminal. ff_h_search_candidate_power_product_terminal + S (bpv_result_search_candidate) = S ((S (f)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_terminal. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_terminal * S ((S (f)) * ff_v_search_candidate_power_product) + (bpv_result_search_candidate))) /\ forall ff_i_search_candidate_power_product. (exists ff_lt_search_candidate_power_product_bound. ff_lt_search_candidate_power_product_bound + S ff_i_search_candidate_power_product = f) -> exists ff_p_search_candidate_power_product ff_r_search_candidate_power_product ff_s_search_candidate_power_product. ((((exists ff_h_search_candidate_power_product_factor. ff_h_search_candidate_power_product_factor + S (ff_p_search_candidate_power_product) = S ((S (ff_i_search_candidate_power_product)) * ff_c_search_candidate_power)) /\ exists ff_q_search_candidate_power_product_factor. ff_b_search_candidate_power = ff_q_search_candidate_power_product_factor * S ((S (ff_i_search_candidate_power_product)) * ff_c_search_candidate_power) + (ff_p_search_candidate_power_product))) /\ ((((exists ff_h_search_candidate_power_product_partial. ff_h_search_candidate_power_product_partial + S (ff_r_search_candidate_power_product) = S ((S (ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_partial. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_partial * S ((S (ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product) + (ff_r_search_candidate_power_product))) /\ ((((exists ff_h_search_candidate_power_product_successor. ff_h_search_candidate_power_product_successor + S (ff_s_search_candidate_power_product) = S ((S (S ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_successor. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_successor * S ((S (S ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product) + (ff_s_search_candidate_power_product))) /\ ff_s_search_candidate_power_product = ff_r_search_candidate_power_product * ff_p_search_candidate_power_product)))))))) /\ (exists bpv_factor_search_candidate_divides. a = bpv_result_search_candidate * bpv_factor_search_candidate_divides))) -> (exists bpv_gap_search_maximal. bpv_gap_search_maximal + f = e)) - 0061
specialize IH p - 0062
specialize IH a - 0063
exact IH - 0064
cases hprevious - 0065
left - 0066
intro f - 0067
intro hf - 0068
intro hproperty - 0069
have hsplit : f = S B ∨ Lt(f,S B)Exact native replay line
have hsplit : f = S B \/ exists h. h + S f = S B - 0070
specialize le_eq_or_lt f - 0071
specialize le_eq_or_lt (S B) - 0072
apply le_eq_or_lt - 0073
exact hf - 0074
cases hsplit - 0075
apply hboundary_right - 0076
rewrite hsplit_left at hproperty - 0077
rewrite hsplit_left at hproperty - 0078
rewrite hsplit_left at hproperty - 0079
rewrite hsplit_left at hproperty - 0080
exact hproperty - 0081
specialize hprevious_left f - 0082
apply hprevious_left - 0083
specialize le_of_succ_le_succ f - 0084
specialize le_of_succ_le_succ B - 0085
apply le_of_succ_le_succ - 0086
exact hsplit_right - 0087
exact hproperty - 0088
right - 0089
cases hprevious_right - 0090
cases hprevious_right_witness - 0091
cases hprevious_right_witness_left - 0092
exists x - 0093
split - 0094
split - 0095
specialize le_succ x - 0096
specialize le_succ B - 0097
apply le_succ - 0098
exact hprevious_right_witness_left_left - 0099
exact hprevious_right_witness_left_right - 0100
intro f - 0101
intro hf - 0102
intro hproperty - 0103
have hsplit : f = S B ∨ Lt(f,S B)Exact native replay line
have hsplit : f = S B \/ exists h. h + S f = S B - 0104
specialize le_eq_or_lt f - 0105
specialize le_eq_or_lt (S B) - 0106
apply le_eq_or_lt - 0107
exact hf - 0108
cases hsplit - 0109
exfalso - 0110
apply hboundary_right - 0111
rewrite hsplit_left at hproperty - 0112
rewrite hsplit_left at hproperty - 0113
rewrite hsplit_left at hproperty - 0114
rewrite hsplit_left at hproperty - 0115
exact hproperty - 0116
specialize hprevious_right_witness_right f - 0117
apply hprevious_right_witness_right - 0118
specialize le_of_succ_le_succ f - 0119
specialize le_of_succ_le_succ B - 0120
apply le_of_succ_le_succ - 0121
exact hsplit_right - 0122
exact hproperty