BT00Q5

bounded_power_valuation_search

Alpha body-checked · checked-use disabled

Finite search either excludes every power divisor or returns a greatest exponent.

Exact expanded 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))

Structural proof guide

Finite search either excludes every power divisor or returns a greatest exponent.

Direct prerequisites: power_divides_decidable, le_zero, le_refl, le_eq_or_lt, le_of_succ_le_succ, le_succ. The authored body proceeds by structural induction (1), case analysis (8), intermediate claims (7), equality transport (13).

Proof neighborhood

Direct dependencies

BT00Q3 power_divides_decidable BT000Y le_zero BT000E le_refl BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT0018 le_succ

Direct dependents

BT00Q6 bounded_power_valuation_exists

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001induction B
  2. 0002intro p
  3. 0003intro a
  4. 0004have 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))
  5. 0005specialize power_divides_decidable p
  6. 0006specialize power_divides_decidable 0
  7. 0007specialize power_divides_decidable a
  8. 0008exact power_divides_decidable
  9. 0009cases hboundary
  10. 0010right
  11. 0011exists 0
  12. 0012split
  13. 0013split
  14. 0014specialize le_refl 0
  15. 0015exact le_refl
  16. 0016exact hboundary_left
  17. 0017intro f
  18. 0018intro hf
  19. 0019intro hproperty
  20. 0020have hf0 : f = 0
  21. 0021specialize le_zero f
  22. 0022apply le_zero
  23. 0023exact hf
  24. 0024rewrite hf0
  25. 0025specialize le_refl 0
  26. 0026exact le_refl
  27. 0027left
  28. 0028intro f
  29. 0029intro hf
  30. 0030intro hproperty
  31. 0031have hf0 : f = 0
  32. 0032specialize le_zero f
  33. 0033apply le_zero
  34. 0034exact hf
  35. 0035apply hboundary_right
  36. 0036rewrite hf0 at hproperty
  37. 0037rewrite hf0 at hproperty
  38. 0038rewrite hf0 at hproperty
  39. 0039rewrite hf0 at hproperty
  40. 0040exact hproperty
  41. 0041intro p
  42. 0042intro a
  43. 0043have 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))
  44. 0044specialize power_divides_decidable p
  45. 0045specialize power_divides_decidable (S B)
  46. 0046specialize power_divides_decidable a
  47. 0047exact power_divides_decidable
  48. 0048cases hboundary
  49. 0049right
  50. 0050exists S B
  51. 0051split
  52. 0052split
  53. 0053specialize le_refl (S B)
  54. 0054exact le_refl
  55. 0055exact hboundary_left
  56. 0056intro f
  57. 0057intro hf
  58. 0058intro hproperty
  59. 0059exact hf
  60. 0060have 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))
  61. 0061specialize IH p
  62. 0062specialize IH a
  63. 0063exact IH
  64. 0064cases hprevious
  65. 0065left
  66. 0066intro f
  67. 0067intro hf
  68. 0068intro hproperty
  69. 0069have hsplit : f = S B \/ exists h. h + S f = S B
  70. 0070specialize le_eq_or_lt f
  71. 0071specialize le_eq_or_lt (S B)
  72. 0072apply le_eq_or_lt
  73. 0073exact hf
  74. 0074cases hsplit
  75. 0075apply hboundary_right
  76. 0076rewrite hsplit_left at hproperty
  77. 0077rewrite hsplit_left at hproperty
  78. 0078rewrite hsplit_left at hproperty
  79. 0079rewrite hsplit_left at hproperty
  80. 0080exact hproperty
  81. 0081specialize hprevious_left f
  82. 0082apply hprevious_left
  83. 0083specialize le_of_succ_le_succ f
  84. 0084specialize le_of_succ_le_succ B
  85. 0085apply le_of_succ_le_succ
  86. 0086exact hsplit_right
  87. 0087exact hproperty
  88. 0088right
  89. 0089cases hprevious_right
  90. 0090cases hprevious_right_witness
  91. 0091cases hprevious_right_witness_left
  92. 0092exists x
  93. 0093split
  94. 0094split
  95. 0095specialize le_succ x
  96. 0096specialize le_succ B
  97. 0097apply le_succ
  98. 0098exact hprevious_right_witness_left_left
  99. 0099exact hprevious_right_witness_left_right
  100. 0100intro f
  101. 0101intro hf
  102. 0102intro hproperty
  103. 0103have hsplit : f = S B \/ exists h. h + S f = S B
  104. 0104specialize le_eq_or_lt f
  105. 0105specialize le_eq_or_lt (S B)
  106. 0106apply le_eq_or_lt
  107. 0107exact hf
  108. 0108cases hsplit
  109. 0109exfalso
  110. 0110apply hboundary_right
  111. 0111rewrite hsplit_left at hproperty
  112. 0112rewrite hsplit_left at hproperty
  113. 0113rewrite hsplit_left at hproperty
  114. 0114rewrite hsplit_left at hproperty
  115. 0115exact hproperty
  116. 0116specialize hprevious_right_witness_right f
  117. 0117apply hprevious_right_witness_right
  118. 0118specialize le_of_succ_le_succ f
  119. 0119specialize le_of_succ_le_succ B
  120. 0120apply le_of_succ_le_succ
  121. 0121exact hsplit_right
  122. 0122exact hproperty