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.
Exact expanded first-order arithmetic statement
forall p b c l. exists vb vc. (forall mkm_index_exists_result. (exists mkm_lt_exists_result_bound. mkm_lt_exists_result_bound + S (mkm_index_exists_result) = (l)) -> (exists mkm_value_exists_result_point mkm_exponent_exists_result_point. (((exists fs_h_mkm_exists_result_point_source. fs_h_mkm_exists_result_point_source + S (mkm_value_exists_result_point) = S ((S (mkm_index_exists_result)) * c)) /\ exists fs_q_mkm_exists_result_point_source. b = fs_q_mkm_exists_result_point_source * S ((S (mkm_index_exists_result)) * c) + (mkm_value_exists_result_point))) /\ ((((exists fs_h_mkm_exists_result_point_decoded. fs_h_mkm_exists_result_point_decoded + S (mkm_exponent_exists_result_point) = S ((S (mkm_index_exists_result)) * vc)) /\ exists fs_q_mkm_exists_result_point_decoded. vb = fs_q_mkm_exists_result_point_decoded * S ((S (mkm_index_exists_result)) * vc) + (mkm_exponent_exists_result_point))) /\ (((exists bpv_gap_mkm_exists_result_point_valuation_exponent_bound. bpv_gap_mkm_exists_result_point_valuation_exponent_bound + mkm_exponent_exists_result_point = (mkm_value_exists_result_point)) /\ (exists bpv_result_mkm_exists_result_point_valuation_selected. ((exists ff_b_mkm_exists_result_point_valuation_selected_power ff_c_mkm_exists_result_point_valuation_selected_power. ((forall ff_i_mkm_exists_result_point_valuation_selected_power_repeat. (exists ff_lt_mkm_exists_result_point_valuation_selected_power_repeat_bound. ff_lt_mkm_exists_result_point_valuation_selected_power_repeat_bound + S ff_i_mkm_exists_result_point_valuation_selected_power_repeat = mkm_exponent_exists_result_point) -> (((exists ff_h_mkm_exists_result_point_valuation_selected_power_repeat_decoded. ff_h_mkm_exists_result_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_repeat)) * ff_c_mkm_exists_result_point_valuation_selected_power)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_repeat_decoded. ff_b_mkm_exists_result_point_valuation_selected_power = ff_q_mkm_exists_result_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_repeat)) * ff_c_mkm_exists_result_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_exists_result_point_valuation_selected_power_product ff_v_mkm_exists_result_point_valuation_selected_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_start. ff_h_mkm_exists_result_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_start. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_terminal. ff_h_mkm_exists_result_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_exists_result_point_valuation_selected) = S ((S (mkm_exponent_exists_result_point)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_terminal. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_exists_result_point)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (bpv_result_mkm_exists_result_point_valuation_selected))) /\ forall ff_i_mkm_exists_result_point_valuation_selected_power_product. (exists ff_lt_mkm_exists_result_point_valuation_selected_power_product_bound. ff_lt_mkm_exists_result_point_valuation_selected_power_product_bound + S ff_i_mkm_exists_result_point_valuation_selected_power_product = mkm_exponent_exists_result_point) -> exists ff_p_mkm_exists_result_point_valuation_selected_power_product ff_r_mkm_exists_result_point_valuation_selected_power_product ff_s_mkm_exists_result_point_valuation_selected_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_factor. ff_h_mkm_exists_result_point_valuation_selected_power_product_factor + S (ff_p_mkm_exists_result_point_valuation_selected_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_c_mkm_exists_result_point_valuation_selected_power)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_factor. ff_b_mkm_exists_result_point_valuation_selected_power = ff_q_mkm_exists_result_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_c_mkm_exists_result_point_valuation_selected_power) + (ff_p_mkm_exists_result_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_partial. ff_h_mkm_exists_result_point_valuation_selected_power_product_partial + S (ff_r_mkm_exists_result_point_valuation_selected_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_partial. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (ff_r_mkm_exists_result_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_successor. ff_h_mkm_exists_result_point_valuation_selected_power_product_successor + S (ff_s_mkm_exists_result_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_successor. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (ff_s_mkm_exists_result_point_valuation_selected_power_product))) /\ ff_s_mkm_exists_result_point_valuation_selected_power_product = ff_r_mkm_exists_result_point_valuation_selected_power_product * ff_p_mkm_exists_result_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_exists_result_point_valuation_selected_divides. (mkm_value_exists_result_point) = bpv_result_mkm_exists_result_point_valuation_selected * bpv_factor_mkm_exists_result_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_exists_result_point_valuation. (exists bpv_gap_mkm_exists_result_point_valuation_candidate_bound. bpv_gap_mkm_exists_result_point_valuation_candidate_bound + bpv_candidate_mkm_exists_result_point_valuation = (mkm_value_exists_result_point)) -> (exists bpv_result_mkm_exists_result_point_valuation_candidate. ((exists ff_b_mkm_exists_result_point_valuation_candidate_power ff_c_mkm_exists_result_point_valuation_candidate_power. ((forall ff_i_mkm_exists_result_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_exists_result_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_exists_result_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_exists_result_point_valuation_candidate_power_repeat = bpv_candidate_mkm_exists_result_point_valuation) -> (((exists ff_h_mkm_exists_result_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_exists_result_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_repeat)) * ff_c_mkm_exists_result_point_valuation_candidate_power)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_exists_result_point_valuation_candidate_power = ff_q_mkm_exists_result_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_repeat)) * ff_c_mkm_exists_result_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_exists_result_point_valuation_candidate_power_product ff_v_mkm_exists_result_point_valuation_candidate_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_start. ff_h_mkm_exists_result_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_start. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_terminal. ff_h_mkm_exists_result_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_exists_result_point_valuation_candidate) = S ((S (bpv_candidate_mkm_exists_result_point_valuation)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_terminal. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_exists_result_point_valuation)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (bpv_result_mkm_exists_result_point_valuation_candidate))) /\ forall ff_i_mkm_exists_result_point_valuation_candidate_power_product. (exists ff_lt_mkm_exists_result_point_valuation_candidate_power_product_bound. ff_lt_mkm_exists_result_point_valuation_candidate_power_product_bound + S ff_i_mkm_exists_result_point_valuation_candidate_power_product = bpv_candidate_mkm_exists_result_point_valuation) -> exists ff_p_mkm_exists_result_point_valuation_candidate_power_product ff_r_mkm_exists_result_point_valuation_candidate_power_product ff_s_mkm_exists_result_point_valuation_candidate_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_factor. ff_h_mkm_exists_result_point_valuation_candidate_power_product_factor + S (ff_p_mkm_exists_result_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_c_mkm_exists_result_point_valuation_candidate_power)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_factor. ff_b_mkm_exists_result_point_valuation_candidate_power = ff_q_mkm_exists_result_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_c_mkm_exists_result_point_valuation_candidate_power) + (ff_p_mkm_exists_result_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_partial. ff_h_mkm_exists_result_point_valuation_candidate_power_product_partial + S (ff_r_mkm_exists_result_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_partial. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (ff_r_mkm_exists_result_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_successor. ff_h_mkm_exists_result_point_valuation_candidate_power_product_successor + S (ff_s_mkm_exists_result_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_successor. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (ff_s_mkm_exists_result_point_valuation_candidate_power_product))) /\ ff_s_mkm_exists_result_point_valuation_candidate_power_product = ff_r_mkm_exists_result_point_valuation_candidate_power_product * ff_p_mkm_exists_result_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_exists_result_point_valuation_candidate_divides. (mkm_value_exists_result_point) = bpv_result_mkm_exists_result_point_valuation_candidate * bpv_factor_mkm_exists_result_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_exists_result_point_valuation_maximal. bpv_gap_mkm_exists_result_point_valuation_maximal + bpv_candidate_mkm_exists_result_point_valuation = mkm_exponent_exists_result_point)))))Constructive proof overview
Generated structural guide
Every finite decoded list has a genuinely constructed finite table of bounded power valuations.
The unchanged tactic script uses 4 declared prerequisites and contains 39 exact native proof lines.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
MK0001 beta_valuation_prefix_empty beta_at_exists Stable theorem; checked-use authorized power_valuation_exists Alpha theorem; checked-use authorized MK0004 beta_valuation_prefix_extendDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
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 (2)
01Fix variables and assumptionsL1–3
02Induction on lL4–4
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L4
induction l
03Construct an explicit witnessL5–6
04Use earlier factsL7–12
Instantiate or apply named facts and discharge the corresponding proof obligations.
05Establish hprefixL13–14
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L13
have hprefix : ∃ vb. ∃ vc. BetaValuationPrefix(p,b,c,vb,vc,l)Definitions: BetaValuationPrefix - L14
apply IH
06Separate the logical casesL15–16
07Establish hvalueL17–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.
- L17
have hvalue : exists a. ((exists fs_h_mkm_exists_value. fs_h_mkm_exists_value + S (a) = S ((S (l)) * c)) /\ exists fs_q_mkm_exists_value. b = fs_q_mkm_exists_value * S ((S (l)) * c) + (a)) - L18
specialize beta_at_exists b - L19
specialize beta_at_exists c - L20
specialize beta_at_exists l - L21
apply beta_at_exists
08Separate the logical casesL22–22
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
cases hvalue
09Establish hvalL23–26
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation exists.
- L23
have hval : ∃ e. BoundedPowerValuation(p,x2,x2,e)Definitions: BoundedPowerValuation - L24
specialize power_valuation_exists p - L25
specialize power_valuation_exists x2 - L26
apply power_valuation_exists
10Separate the logical casesL27–27
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L27
cases hval
11Use earlier factsL28–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L28
specialize beta_valuation_prefix_extend p - L29
specialize beta_valuation_prefix_extend b - L30
specialize beta_valuation_prefix_extend c - L31
specialize beta_valuation_prefix_extend x - L32
specialize beta_valuation_prefix_extend x1 - L33
specialize beta_valuation_prefix_extend l - L34
specialize beta_valuation_prefix_extend x2 - L35
specialize beta_valuation_prefix_extend x3 - L36
apply beta_valuation_prefix_extend - L37
exact hprefix_witness_witness
Original exact command ledger · 39 lines
- 0001
intro p - 0002
intro b - 0003
intro c - 0004
induction l - 0005
exists 0 - 0006
exists 0 - 0007
specialize beta_valuation_prefix_empty p - 0008
specialize beta_valuation_prefix_empty b - 0009
specialize beta_valuation_prefix_empty c - 0010
specialize beta_valuation_prefix_empty 0 - 0011
specialize beta_valuation_prefix_empty 0 - 0012
apply beta_valuation_prefix_empty - 0013
have hprefix : exists vb vc. (forall mkm_index_exists_prefix. (exists mkm_lt_exists_prefix_bound. mkm_lt_exists_prefix_bound + S (mkm_index_exists_prefix) = (l)) -> (exists mkm_value_exists_prefix_point mkm_exponent_exists_prefix_point. (((exists fs_h_mkm_exists_prefix_point_source. fs_h_mkm_exists_prefix_point_source + S (mkm_value_exists_prefix_point) = S ((S (mkm_index_exists_prefix)) * c)) /\ exists fs_q_mkm_exists_prefix_point_source. b = fs_q_mkm_exists_prefix_point_source * S ((S (mkm_index_exists_prefix)) * c) + (mkm_value_exists_prefix_point))) /\ ((((exists fs_h_mkm_exists_prefix_point_decoded. fs_h_mkm_exists_prefix_point_decoded + S (mkm_exponent_exists_prefix_point) = S ((S (mkm_index_exists_prefix)) * vc)) /\ exists fs_q_mkm_exists_prefix_point_decoded. vb = fs_q_mkm_exists_prefix_point_decoded * S ((S (mkm_index_exists_prefix)) * vc) + (mkm_exponent_exists_prefix_point))) /\ (((exists bpv_gap_mkm_exists_prefix_point_valuation_exponent_bound. bpv_gap_mkm_exists_prefix_point_valuation_exponent_bound + mkm_exponent_exists_prefix_point = (mkm_value_exists_prefix_point)) /\ (exists bpv_result_mkm_exists_prefix_point_valuation_selected. ((exists ff_b_mkm_exists_prefix_point_valuation_selected_power ff_c_mkm_exists_prefix_point_valuation_selected_power. ((forall ff_i_mkm_exists_prefix_point_valuation_selected_power_repeat. (exists ff_lt_mkm_exists_prefix_point_valuation_selected_power_repeat_bound. ff_lt_mkm_exists_prefix_point_valuation_selected_power_repeat_bound + S ff_i_mkm_exists_prefix_point_valuation_selected_power_repeat = mkm_exponent_exists_prefix_point) -> (((exists ff_h_mkm_exists_prefix_point_valuation_selected_power_repeat_decoded. ff_h_mkm_exists_prefix_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_prefix_point_valuation_selected_power_repeat)) * ff_c_mkm_exists_prefix_point_valuation_selected_power)) /\ exists ff_q_mkm_exists_prefix_point_valuation_selected_power_repeat_decoded. ff_b_mkm_exists_prefix_point_valuation_selected_power = ff_q_mkm_exists_prefix_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_exists_prefix_point_valuation_selected_power_repeat)) * ff_c_mkm_exists_prefix_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_exists_prefix_point_valuation_selected_power_product ff_v_mkm_exists_prefix_point_valuation_selected_power_product. ((((exists ff_h_mkm_exists_prefix_point_valuation_selected_power_product_start. ff_h_mkm_exists_prefix_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_selected_power_product_start. ff_u_mkm_exists_prefix_point_valuation_selected_power_product = ff_q_mkm_exists_prefix_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_prefix_point_valuation_selected_power_product_terminal. ff_h_mkm_exists_prefix_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_exists_prefix_point_valuation_selected) = S ((S (mkm_exponent_exists_prefix_point)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_selected_power_product_terminal. ff_u_mkm_exists_prefix_point_valuation_selected_power_product = ff_q_mkm_exists_prefix_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_exists_prefix_point)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product) + (bpv_result_mkm_exists_prefix_point_valuation_selected))) /\ forall ff_i_mkm_exists_prefix_point_valuation_selected_power_product. (exists ff_lt_mkm_exists_prefix_point_valuation_selected_power_product_bound. ff_lt_mkm_exists_prefix_point_valuation_selected_power_product_bound + S ff_i_mkm_exists_prefix_point_valuation_selected_power_product = mkm_exponent_exists_prefix_point) -> exists ff_p_mkm_exists_prefix_point_valuation_selected_power_product ff_r_mkm_exists_prefix_point_valuation_selected_power_product ff_s_mkm_exists_prefix_point_valuation_selected_power_product. ((((exists ff_h_mkm_exists_prefix_point_valuation_selected_power_product_factor. ff_h_mkm_exists_prefix_point_valuation_selected_power_product_factor + S (ff_p_mkm_exists_prefix_point_valuation_selected_power_product) = S ((S (ff_i_mkm_exists_prefix_point_valuation_selected_power_product)) * ff_c_mkm_exists_prefix_point_valuation_selected_power)) /\ exists ff_q_mkm_exists_prefix_point_valuation_selected_power_product_factor. ff_b_mkm_exists_prefix_point_valuation_selected_power = ff_q_mkm_exists_prefix_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_exists_prefix_point_valuation_selected_power_product)) * ff_c_mkm_exists_prefix_point_valuation_selected_power) + (ff_p_mkm_exists_prefix_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_exists_prefix_point_valuation_selected_power_product_partial. ff_h_mkm_exists_prefix_point_valuation_selected_power_product_partial + S (ff_r_mkm_exists_prefix_point_valuation_selected_power_product) = S ((S (ff_i_mkm_exists_prefix_point_valuation_selected_power_product)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_selected_power_product_partial. ff_u_mkm_exists_prefix_point_valuation_selected_power_product = ff_q_mkm_exists_prefix_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_exists_prefix_point_valuation_selected_power_product)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product) + (ff_r_mkm_exists_prefix_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_exists_prefix_point_valuation_selected_power_product_successor. ff_h_mkm_exists_prefix_point_valuation_selected_power_product_successor + S (ff_s_mkm_exists_prefix_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_exists_prefix_point_valuation_selected_power_product)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_selected_power_product_successor. ff_u_mkm_exists_prefix_point_valuation_selected_power_product = ff_q_mkm_exists_prefix_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_exists_prefix_point_valuation_selected_power_product)) * ff_v_mkm_exists_prefix_point_valuation_selected_power_product) + (ff_s_mkm_exists_prefix_point_valuation_selected_power_product))) /\ ff_s_mkm_exists_prefix_point_valuation_selected_power_product = ff_r_mkm_exists_prefix_point_valuation_selected_power_product * ff_p_mkm_exists_prefix_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_exists_prefix_point_valuation_selected_divides. (mkm_value_exists_prefix_point) = bpv_result_mkm_exists_prefix_point_valuation_selected * bpv_factor_mkm_exists_prefix_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_exists_prefix_point_valuation. (exists bpv_gap_mkm_exists_prefix_point_valuation_candidate_bound. bpv_gap_mkm_exists_prefix_point_valuation_candidate_bound + bpv_candidate_mkm_exists_prefix_point_valuation = (mkm_value_exists_prefix_point)) -> (exists bpv_result_mkm_exists_prefix_point_valuation_candidate. ((exists ff_b_mkm_exists_prefix_point_valuation_candidate_power ff_c_mkm_exists_prefix_point_valuation_candidate_power. ((forall ff_i_mkm_exists_prefix_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_exists_prefix_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_exists_prefix_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_exists_prefix_point_valuation_candidate_power_repeat = bpv_candidate_mkm_exists_prefix_point_valuation) -> (((exists ff_h_mkm_exists_prefix_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_exists_prefix_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_prefix_point_valuation_candidate_power_repeat)) * ff_c_mkm_exists_prefix_point_valuation_candidate_power)) /\ exists ff_q_mkm_exists_prefix_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_exists_prefix_point_valuation_candidate_power = ff_q_mkm_exists_prefix_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_exists_prefix_point_valuation_candidate_power_repeat)) * ff_c_mkm_exists_prefix_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_exists_prefix_point_valuation_candidate_power_product ff_v_mkm_exists_prefix_point_valuation_candidate_power_product. ((((exists ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_start. ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_start. ff_u_mkm_exists_prefix_point_valuation_candidate_power_product = ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_terminal. ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_exists_prefix_point_valuation_candidate) = S ((S (bpv_candidate_mkm_exists_prefix_point_valuation)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_terminal. ff_u_mkm_exists_prefix_point_valuation_candidate_power_product = ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_exists_prefix_point_valuation)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product) + (bpv_result_mkm_exists_prefix_point_valuation_candidate))) /\ forall ff_i_mkm_exists_prefix_point_valuation_candidate_power_product. (exists ff_lt_mkm_exists_prefix_point_valuation_candidate_power_product_bound. ff_lt_mkm_exists_prefix_point_valuation_candidate_power_product_bound + S ff_i_mkm_exists_prefix_point_valuation_candidate_power_product = bpv_candidate_mkm_exists_prefix_point_valuation) -> exists ff_p_mkm_exists_prefix_point_valuation_candidate_power_product ff_r_mkm_exists_prefix_point_valuation_candidate_power_product ff_s_mkm_exists_prefix_point_valuation_candidate_power_product. ((((exists ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_factor. ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_factor + S (ff_p_mkm_exists_prefix_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_exists_prefix_point_valuation_candidate_power_product)) * ff_c_mkm_exists_prefix_point_valuation_candidate_power)) /\ exists ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_factor. ff_b_mkm_exists_prefix_point_valuation_candidate_power = ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_exists_prefix_point_valuation_candidate_power_product)) * ff_c_mkm_exists_prefix_point_valuation_candidate_power) + (ff_p_mkm_exists_prefix_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_partial. ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_partial + S (ff_r_mkm_exists_prefix_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_exists_prefix_point_valuation_candidate_power_product)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_partial. ff_u_mkm_exists_prefix_point_valuation_candidate_power_product = ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_exists_prefix_point_valuation_candidate_power_product)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product) + (ff_r_mkm_exists_prefix_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_successor. ff_h_mkm_exists_prefix_point_valuation_candidate_power_product_successor + S (ff_s_mkm_exists_prefix_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_exists_prefix_point_valuation_candidate_power_product)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_successor. ff_u_mkm_exists_prefix_point_valuation_candidate_power_product = ff_q_mkm_exists_prefix_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_exists_prefix_point_valuation_candidate_power_product)) * ff_v_mkm_exists_prefix_point_valuation_candidate_power_product) + (ff_s_mkm_exists_prefix_point_valuation_candidate_power_product))) /\ ff_s_mkm_exists_prefix_point_valuation_candidate_power_product = ff_r_mkm_exists_prefix_point_valuation_candidate_power_product * ff_p_mkm_exists_prefix_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_exists_prefix_point_valuation_candidate_divides. (mkm_value_exists_prefix_point) = bpv_result_mkm_exists_prefix_point_valuation_candidate * bpv_factor_mkm_exists_prefix_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_exists_prefix_point_valuation_maximal. bpv_gap_mkm_exists_prefix_point_valuation_maximal + bpv_candidate_mkm_exists_prefix_point_valuation = mkm_exponent_exists_prefix_point))))) - 0014
apply IH - 0015
cases hprefix - 0016
cases hprefix_witness - 0017
have hvalue : exists a. ((exists fs_h_mkm_exists_value. fs_h_mkm_exists_value + S (a) = S ((S (l)) * c)) /\ exists fs_q_mkm_exists_value. b = fs_q_mkm_exists_value * S ((S (l)) * c) + (a)) - 0018
specialize beta_at_exists b - 0019
specialize beta_at_exists c - 0020
specialize beta_at_exists l - 0021
apply beta_at_exists - 0022
cases hvalue - 0023
have hval : exists e. ((exists bpv_gap_mkm_exists_val_exponent_bound. bpv_gap_mkm_exists_val_exponent_bound + e = (x2)) /\ (exists bpv_result_mkm_exists_val_selected. ((exists ff_b_mkm_exists_val_selected_power ff_c_mkm_exists_val_selected_power. ((forall ff_i_mkm_exists_val_selected_power_repeat. (exists ff_lt_mkm_exists_val_selected_power_repeat_bound. ff_lt_mkm_exists_val_selected_power_repeat_bound + S ff_i_mkm_exists_val_selected_power_repeat = e) -> (((exists ff_h_mkm_exists_val_selected_power_repeat_decoded. ff_h_mkm_exists_val_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_val_selected_power_repeat)) * ff_c_mkm_exists_val_selected_power)) /\ exists ff_q_mkm_exists_val_selected_power_repeat_decoded. ff_b_mkm_exists_val_selected_power = ff_q_mkm_exists_val_selected_power_repeat_decoded * S ((S (ff_i_mkm_exists_val_selected_power_repeat)) * ff_c_mkm_exists_val_selected_power) + (p)))) /\ (exists ff_u_mkm_exists_val_selected_power_product ff_v_mkm_exists_val_selected_power_product. ((((exists ff_h_mkm_exists_val_selected_power_product_start. ff_h_mkm_exists_val_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_val_selected_power_product)) /\ exists ff_q_mkm_exists_val_selected_power_product_start. ff_u_mkm_exists_val_selected_power_product = ff_q_mkm_exists_val_selected_power_product_start * S ((S (0)) * ff_v_mkm_exists_val_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_val_selected_power_product_terminal. ff_h_mkm_exists_val_selected_power_product_terminal + S (bpv_result_mkm_exists_val_selected) = S ((S (e)) * ff_v_mkm_exists_val_selected_power_product)) /\ exists ff_q_mkm_exists_val_selected_power_product_terminal. ff_u_mkm_exists_val_selected_power_product = ff_q_mkm_exists_val_selected_power_product_terminal * S ((S (e)) * ff_v_mkm_exists_val_selected_power_product) + (bpv_result_mkm_exists_val_selected))) /\ forall ff_i_mkm_exists_val_selected_power_product. (exists ff_lt_mkm_exists_val_selected_power_product_bound. ff_lt_mkm_exists_val_selected_power_product_bound + S ff_i_mkm_exists_val_selected_power_product = e) -> exists ff_p_mkm_exists_val_selected_power_product ff_r_mkm_exists_val_selected_power_product ff_s_mkm_exists_val_selected_power_product. ((((exists ff_h_mkm_exists_val_selected_power_product_factor. ff_h_mkm_exists_val_selected_power_product_factor + S (ff_p_mkm_exists_val_selected_power_product) = S ((S (ff_i_mkm_exists_val_selected_power_product)) * ff_c_mkm_exists_val_selected_power)) /\ exists ff_q_mkm_exists_val_selected_power_product_factor. ff_b_mkm_exists_val_selected_power = ff_q_mkm_exists_val_selected_power_product_factor * S ((S (ff_i_mkm_exists_val_selected_power_product)) * ff_c_mkm_exists_val_selected_power) + (ff_p_mkm_exists_val_selected_power_product))) /\ ((((exists ff_h_mkm_exists_val_selected_power_product_partial. ff_h_mkm_exists_val_selected_power_product_partial + S (ff_r_mkm_exists_val_selected_power_product) = S ((S (ff_i_mkm_exists_val_selected_power_product)) * ff_v_mkm_exists_val_selected_power_product)) /\ exists ff_q_mkm_exists_val_selected_power_product_partial. ff_u_mkm_exists_val_selected_power_product = ff_q_mkm_exists_val_selected_power_product_partial * S ((S (ff_i_mkm_exists_val_selected_power_product)) * ff_v_mkm_exists_val_selected_power_product) + (ff_r_mkm_exists_val_selected_power_product))) /\ ((((exists ff_h_mkm_exists_val_selected_power_product_successor. ff_h_mkm_exists_val_selected_power_product_successor + S (ff_s_mkm_exists_val_selected_power_product) = S ((S (S ff_i_mkm_exists_val_selected_power_product)) * ff_v_mkm_exists_val_selected_power_product)) /\ exists ff_q_mkm_exists_val_selected_power_product_successor. ff_u_mkm_exists_val_selected_power_product = ff_q_mkm_exists_val_selected_power_product_successor * S ((S (S ff_i_mkm_exists_val_selected_power_product)) * ff_v_mkm_exists_val_selected_power_product) + (ff_s_mkm_exists_val_selected_power_product))) /\ ff_s_mkm_exists_val_selected_power_product = ff_r_mkm_exists_val_selected_power_product * ff_p_mkm_exists_val_selected_power_product)))))))) /\ (exists bpv_factor_mkm_exists_val_selected_divides. (x2) = bpv_result_mkm_exists_val_selected * bpv_factor_mkm_exists_val_selected_divides)))) /\ forall bpv_candidate_mkm_exists_val. (exists bpv_gap_mkm_exists_val_candidate_bound. bpv_gap_mkm_exists_val_candidate_bound + bpv_candidate_mkm_exists_val = (x2)) -> (exists bpv_result_mkm_exists_val_candidate. ((exists ff_b_mkm_exists_val_candidate_power ff_c_mkm_exists_val_candidate_power. ((forall ff_i_mkm_exists_val_candidate_power_repeat. (exists ff_lt_mkm_exists_val_candidate_power_repeat_bound. ff_lt_mkm_exists_val_candidate_power_repeat_bound + S ff_i_mkm_exists_val_candidate_power_repeat = bpv_candidate_mkm_exists_val) -> (((exists ff_h_mkm_exists_val_candidate_power_repeat_decoded. ff_h_mkm_exists_val_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_val_candidate_power_repeat)) * ff_c_mkm_exists_val_candidate_power)) /\ exists ff_q_mkm_exists_val_candidate_power_repeat_decoded. ff_b_mkm_exists_val_candidate_power = ff_q_mkm_exists_val_candidate_power_repeat_decoded * S ((S (ff_i_mkm_exists_val_candidate_power_repeat)) * ff_c_mkm_exists_val_candidate_power) + (p)))) /\ (exists ff_u_mkm_exists_val_candidate_power_product ff_v_mkm_exists_val_candidate_power_product. ((((exists ff_h_mkm_exists_val_candidate_power_product_start. ff_h_mkm_exists_val_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_val_candidate_power_product)) /\ exists ff_q_mkm_exists_val_candidate_power_product_start. ff_u_mkm_exists_val_candidate_power_product = ff_q_mkm_exists_val_candidate_power_product_start * S ((S (0)) * ff_v_mkm_exists_val_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_val_candidate_power_product_terminal. ff_h_mkm_exists_val_candidate_power_product_terminal + S (bpv_result_mkm_exists_val_candidate) = S ((S (bpv_candidate_mkm_exists_val)) * ff_v_mkm_exists_val_candidate_power_product)) /\ exists ff_q_mkm_exists_val_candidate_power_product_terminal. ff_u_mkm_exists_val_candidate_power_product = ff_q_mkm_exists_val_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_exists_val)) * ff_v_mkm_exists_val_candidate_power_product) + (bpv_result_mkm_exists_val_candidate))) /\ forall ff_i_mkm_exists_val_candidate_power_product. (exists ff_lt_mkm_exists_val_candidate_power_product_bound. ff_lt_mkm_exists_val_candidate_power_product_bound + S ff_i_mkm_exists_val_candidate_power_product = bpv_candidate_mkm_exists_val) -> exists ff_p_mkm_exists_val_candidate_power_product ff_r_mkm_exists_val_candidate_power_product ff_s_mkm_exists_val_candidate_power_product. ((((exists ff_h_mkm_exists_val_candidate_power_product_factor. ff_h_mkm_exists_val_candidate_power_product_factor + S (ff_p_mkm_exists_val_candidate_power_product) = S ((S (ff_i_mkm_exists_val_candidate_power_product)) * ff_c_mkm_exists_val_candidate_power)) /\ exists ff_q_mkm_exists_val_candidate_power_product_factor. ff_b_mkm_exists_val_candidate_power = ff_q_mkm_exists_val_candidate_power_product_factor * S ((S (ff_i_mkm_exists_val_candidate_power_product)) * ff_c_mkm_exists_val_candidate_power) + (ff_p_mkm_exists_val_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_val_candidate_power_product_partial. ff_h_mkm_exists_val_candidate_power_product_partial + S (ff_r_mkm_exists_val_candidate_power_product) = S ((S (ff_i_mkm_exists_val_candidate_power_product)) * ff_v_mkm_exists_val_candidate_power_product)) /\ exists ff_q_mkm_exists_val_candidate_power_product_partial. ff_u_mkm_exists_val_candidate_power_product = ff_q_mkm_exists_val_candidate_power_product_partial * S ((S (ff_i_mkm_exists_val_candidate_power_product)) * ff_v_mkm_exists_val_candidate_power_product) + (ff_r_mkm_exists_val_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_val_candidate_power_product_successor. ff_h_mkm_exists_val_candidate_power_product_successor + S (ff_s_mkm_exists_val_candidate_power_product) = S ((S (S ff_i_mkm_exists_val_candidate_power_product)) * ff_v_mkm_exists_val_candidate_power_product)) /\ exists ff_q_mkm_exists_val_candidate_power_product_successor. ff_u_mkm_exists_val_candidate_power_product = ff_q_mkm_exists_val_candidate_power_product_successor * S ((S (S ff_i_mkm_exists_val_candidate_power_product)) * ff_v_mkm_exists_val_candidate_power_product) + (ff_s_mkm_exists_val_candidate_power_product))) /\ ff_s_mkm_exists_val_candidate_power_product = ff_r_mkm_exists_val_candidate_power_product * ff_p_mkm_exists_val_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_exists_val_candidate_divides. (x2) = bpv_result_mkm_exists_val_candidate * bpv_factor_mkm_exists_val_candidate_divides))) -> (exists bpv_gap_mkm_exists_val_maximal. bpv_gap_mkm_exists_val_maximal + bpv_candidate_mkm_exists_val = e) - 0024
specialize power_valuation_exists p - 0025
specialize power_valuation_exists x2 - 0026
apply power_valuation_exists - 0027
cases hval - 0028
specialize beta_valuation_prefix_extend p - 0029
specialize beta_valuation_prefix_extend b - 0030
specialize beta_valuation_prefix_extend c - 0031
specialize beta_valuation_prefix_extend x - 0032
specialize beta_valuation_prefix_extend x1 - 0033
specialize beta_valuation_prefix_extend l - 0034
specialize beta_valuation_prefix_extend x2 - 0035
specialize beta_valuation_prefix_extend x3 - 0036
apply beta_valuation_prefix_extend - 0037
exact hprefix_witness_witness - 0038
exact hvalue_witness - 0039
exact hval_witness