BD0018

binary_modular_execution_logarithmic_bound

For every arbitrary natural exponent and guarded modulus, construct canonical BitLen digits, an actual beta-coded square-and-multiply trace and modular power, the exact beta-counted operation cost, and the constructive bound operations <= 3*BitLen(exponent)+2.

Alpha v34 checked-use · first admitted v23 · independently kernel and Lean verified; not Stable

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.

The exact G102 milestone is fully proved for every natural exponent and every modulus greater than one, including actual canonical digits, a beta-coded accumulator execution, modular-power correctness, and the formal bound k≤3·BitLen(e)+2. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ n. ∀ a. ∀ m. BinaryModulus(m) → ∃ x. ∃ y. ∃ z. ∃ k. ∃ i. BinaryCompleteModularExecution(n,a,m,x,y,z,k) ∧ (BinaryExecutionOperationCount(y,z,x,i) ∧ Le(i,3 · x + 2))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BinaryModulus(m) · 1BinaryCompleteModularExecution(e,a,m,ell,b,c,r) · 1BinaryExecutionOperationCount(b,c,ell,k) · 1Le(a,b) · 1

Actual proof prerequisites

binary_modular_exponent_coded_execution_existsbinary_digit_operation_count_existsbinary_modular_execution_bitlength_bound
Original expanded first-order statement 
forall n a m. (exists ff_modulus_gap_binary_bd_modulus. ff_modulus_gap_binary_bd_modulus + S 1 = m) -> exists l b c r operations. (((((((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_full_run_canonical_length ff_lower_bl_bd_full_run_canonical_length ff_upper_bl_bd_full_run_canonical_length. (((l) = S ff_exponent_bl_bd_full_run_canonical_length) /\ ((exists ff_positive_bl_bd_full_run_canonical_length. ff_positive_bl_bd_full_run_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_full_run_canonical_length_lower pa_c_bl_bd_full_run_canonical_length_lower. ((forall pa_i_bl_bd_full_run_canonical_length_lower_repeat. (exists pa_lt_bl_bd_full_run_canonical_length_lower_repeat_bound. pa_lt_bl_bd_full_run_canonical_length_lower_repeat_bound + S pa_i_bl_bd_full_run_canonical_length_lower_repeat = ff_exponent_bl_bd_full_run_canonical_length) -> (((exists pa_h_bl_bd_full_run_canonical_length_lower_repeat_decoded. pa_h_bl_bd_full_run_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_full_run_canonical_length_lower_repeat)) * pa_c_bl_bd_full_run_canonical_length_lower)) /\ exists pa_q_bl_bd_full_run_canonical_length_lower_repeat_decoded. pa_b_bl_bd_full_run_canonical_length_lower = pa_q_bl_bd_full_run_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_full_run_canonical_length_lower_repeat)) * pa_c_bl_bd_full_run_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_full_run_canonical_length_lower_product pa_v_bl_bd_full_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_full_run_canonical_length_lower_product_start. pa_h_bl_bd_full_run_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_full_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_lower_product_start. pa_u_bl_bd_full_run_canonical_length_lower_product = pa_q_bl_bd_full_run_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_full_run_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_full_run_canonical_length_lower_product_terminal. pa_h_bl_bd_full_run_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_full_run_canonical_length) = S ((S (ff_exponent_bl_bd_full_run_canonical_length)) * pa_v_bl_bd_full_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_lower_product_terminal. pa_u_bl_bd_full_run_canonical_length_lower_product = pa_q_bl_bd_full_run_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_full_run_canonical_length)) * pa_v_bl_bd_full_run_canonical_length_lower_product) + (ff_lower_bl_bd_full_run_canonical_length))) /\ forall pa_i_bl_bd_full_run_canonical_length_lower_product. (exists pa_lt_bl_bd_full_run_canonical_length_lower_product_bound. pa_lt_bl_bd_full_run_canonical_length_lower_product_bound + S pa_i_bl_bd_full_run_canonical_length_lower_product = ff_exponent_bl_bd_full_run_canonical_length) -> exists pa_p_bl_bd_full_run_canonical_length_lower_product pa_r_bl_bd_full_run_canonical_length_lower_product pa_s_bl_bd_full_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_full_run_canonical_length_lower_product_factor. pa_h_bl_bd_full_run_canonical_length_lower_product_factor + S (pa_p_bl_bd_full_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_full_run_canonical_length_lower_product)) * pa_c_bl_bd_full_run_canonical_length_lower)) /\ exists pa_q_bl_bd_full_run_canonical_length_lower_product_factor. pa_b_bl_bd_full_run_canonical_length_lower = pa_q_bl_bd_full_run_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_full_run_canonical_length_lower_product)) * pa_c_bl_bd_full_run_canonical_length_lower) + (pa_p_bl_bd_full_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_full_run_canonical_length_lower_product_partial. pa_h_bl_bd_full_run_canonical_length_lower_product_partial + S (pa_r_bl_bd_full_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_full_run_canonical_length_lower_product)) * pa_v_bl_bd_full_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_lower_product_partial. pa_u_bl_bd_full_run_canonical_length_lower_product = pa_q_bl_bd_full_run_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_full_run_canonical_length_lower_product)) * pa_v_bl_bd_full_run_canonical_length_lower_product) + (pa_r_bl_bd_full_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_full_run_canonical_length_lower_product_successor. pa_h_bl_bd_full_run_canonical_length_lower_product_successor + S (pa_s_bl_bd_full_run_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_full_run_canonical_length_lower_product)) * pa_v_bl_bd_full_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_lower_product_successor. pa_u_bl_bd_full_run_canonical_length_lower_product = pa_q_bl_bd_full_run_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_full_run_canonical_length_lower_product)) * pa_v_bl_bd_full_run_canonical_length_lower_product) + (pa_s_bl_bd_full_run_canonical_length_lower_product))) /\ pa_s_bl_bd_full_run_canonical_length_lower_product = pa_r_bl_bd_full_run_canonical_length_lower_product * pa_p_bl_bd_full_run_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_full_run_canonical_length_upper pa_c_bl_bd_full_run_canonical_length_upper. ((forall pa_i_bl_bd_full_run_canonical_length_upper_repeat. (exists pa_lt_bl_bd_full_run_canonical_length_upper_repeat_bound. pa_lt_bl_bd_full_run_canonical_length_upper_repeat_bound + S pa_i_bl_bd_full_run_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_full_run_canonical_length_upper_repeat_decoded. pa_h_bl_bd_full_run_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_full_run_canonical_length_upper_repeat)) * pa_c_bl_bd_full_run_canonical_length_upper)) /\ exists pa_q_bl_bd_full_run_canonical_length_upper_repeat_decoded. pa_b_bl_bd_full_run_canonical_length_upper = pa_q_bl_bd_full_run_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_full_run_canonical_length_upper_repeat)) * pa_c_bl_bd_full_run_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_full_run_canonical_length_upper_product pa_v_bl_bd_full_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_full_run_canonical_length_upper_product_start. pa_h_bl_bd_full_run_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_full_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_upper_product_start. pa_u_bl_bd_full_run_canonical_length_upper_product = pa_q_bl_bd_full_run_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_full_run_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_full_run_canonical_length_upper_product_terminal. pa_h_bl_bd_full_run_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_full_run_canonical_length) = S ((S (l)) * pa_v_bl_bd_full_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_upper_product_terminal. pa_u_bl_bd_full_run_canonical_length_upper_product = pa_q_bl_bd_full_run_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_full_run_canonical_length_upper_product) + (ff_upper_bl_bd_full_run_canonical_length))) /\ forall pa_i_bl_bd_full_run_canonical_length_upper_product. (exists pa_lt_bl_bd_full_run_canonical_length_upper_product_bound. pa_lt_bl_bd_full_run_canonical_length_upper_product_bound + S pa_i_bl_bd_full_run_canonical_length_upper_product = l) -> exists pa_p_bl_bd_full_run_canonical_length_upper_product pa_r_bl_bd_full_run_canonical_length_upper_product pa_s_bl_bd_full_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_full_run_canonical_length_upper_product_factor. pa_h_bl_bd_full_run_canonical_length_upper_product_factor + S (pa_p_bl_bd_full_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_full_run_canonical_length_upper_product)) * pa_c_bl_bd_full_run_canonical_length_upper)) /\ exists pa_q_bl_bd_full_run_canonical_length_upper_product_factor. pa_b_bl_bd_full_run_canonical_length_upper = pa_q_bl_bd_full_run_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_full_run_canonical_length_upper_product)) * pa_c_bl_bd_full_run_canonical_length_upper) + (pa_p_bl_bd_full_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_full_run_canonical_length_upper_product_partial. pa_h_bl_bd_full_run_canonical_length_upper_product_partial + S (pa_r_bl_bd_full_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_full_run_canonical_length_upper_product)) * pa_v_bl_bd_full_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_upper_product_partial. pa_u_bl_bd_full_run_canonical_length_upper_product = pa_q_bl_bd_full_run_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_full_run_canonical_length_upper_product)) * pa_v_bl_bd_full_run_canonical_length_upper_product) + (pa_r_bl_bd_full_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_full_run_canonical_length_upper_product_successor. pa_h_bl_bd_full_run_canonical_length_upper_product_successor + S (pa_s_bl_bd_full_run_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_full_run_canonical_length_upper_product)) * pa_v_bl_bd_full_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_full_run_canonical_length_upper_product_successor. pa_u_bl_bd_full_run_canonical_length_upper_product = pa_q_bl_bd_full_run_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_full_run_canonical_length_upper_product)) * pa_v_bl_bd_full_run_canonical_length_upper_product) + (pa_s_bl_bd_full_run_canonical_length_upper_product))) /\ pa_s_bl_bd_full_run_canonical_length_upper_product = pa_r_bl_bd_full_run_canonical_length_upper_product * pa_p_bl_bd_full_run_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_full_run_canonical_length. ff_lower_gap_bl_bd_full_run_canonical_length + (ff_lower_bl_bd_full_run_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_full_run_canonical_length. ff_upper_gap_bl_bd_full_run_canonical_length + S (n) = (ff_upper_bl_bd_full_run_canonical_length))))))))) /\ (((forall ff_index_be_bd_full_run_canonical_code_digits ff_digit_be_bd_full_run_canonical_code_digits. (exists ff_lt_be_bd_full_run_canonical_code_digits_bound. ff_lt_be_bd_full_run_canonical_code_digits_bound + S ff_index_be_bd_full_run_canonical_code_digits = l) -> (((exists ff_h_be_bd_full_run_canonical_code_digits_digit. ff_h_be_bd_full_run_canonical_code_digits_digit + S (ff_digit_be_bd_full_run_canonical_code_digits) = S ((S (ff_index_be_bd_full_run_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_full_run_canonical_code_digits_digit. b = ff_q_be_bd_full_run_canonical_code_digits_digit * S ((S (ff_index_be_bd_full_run_canonical_code_digits)) * c) + (ff_digit_be_bd_full_run_canonical_code_digits))) -> (ff_digit_be_bd_full_run_canonical_code_digits = 0 \/ ff_digit_be_bd_full_run_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_full_run_canonical_code_horner ff_v_ph_bd_full_run_canonical_code_horner. ((((exists fs_h_ph_bd_full_run_canonical_code_horner_body_start. fs_h_ph_bd_full_run_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_full_run_canonical_code_horner)) /\ exists fs_q_ph_bd_full_run_canonical_code_horner_body_start. ff_u_ph_bd_full_run_canonical_code_horner = fs_q_ph_bd_full_run_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_full_run_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_full_run_canonical_code_horner_body_terminal. fs_h_ph_bd_full_run_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_full_run_canonical_code_horner)) /\ exists fs_q_ph_bd_full_run_canonical_code_horner_body_terminal. ff_u_ph_bd_full_run_canonical_code_horner = fs_q_ph_bd_full_run_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_full_run_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_full_run_canonical_code_horner_body_steps. (exists ph_bound_bd_full_run_canonical_code_horner_body_steps. ph_bound_bd_full_run_canonical_code_horner_body_steps + S ff_i_ph_bd_full_run_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_full_run_canonical_code_horner_body_steps ff_previous_ph_bd_full_run_canonical_code_horner_body_steps ff_current_ph_bd_full_run_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_full_run_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_full_run_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_full_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_full_run_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_full_run_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_full_run_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_full_run_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_full_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_full_run_canonical_code_horner_body_steps_before. fs_h_ph_bd_full_run_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_full_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_full_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_full_run_canonical_code_horner)) /\ exists fs_q_ph_bd_full_run_canonical_code_horner_body_steps_before. ff_u_ph_bd_full_run_canonical_code_horner = fs_q_ph_bd_full_run_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_full_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_full_run_canonical_code_horner) + (ff_previous_ph_bd_full_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_full_run_canonical_code_horner_body_steps_after. fs_h_ph_bd_full_run_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_full_run_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_full_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_full_run_canonical_code_horner)) /\ exists fs_q_ph_bd_full_run_canonical_code_horner_body_steps_after. ff_u_ph_bd_full_run_canonical_code_horner = fs_q_ph_bd_full_run_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_full_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_full_run_canonical_code_horner) + (ff_current_ph_bd_full_run_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_full_run_canonical_code_horner_body_steps = ff_previous_ph_bd_full_run_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_full_run_canonical_code_horner_body_steps)))))))))) /\ ((exists ff_trace_code_be_bd_full_run_execution ff_trace_scale_be_bd_full_run_execution. ((((((exists ff_h_be_bd_full_run_execution_trace_start. ff_h_be_bd_full_run_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_bd_full_run_execution)) /\ exists ff_q_be_bd_full_run_execution_trace_start. ff_trace_code_be_bd_full_run_execution = ff_q_be_bd_full_run_execution_trace_start * S ((S (0)) * ff_trace_scale_be_bd_full_run_execution) + (1))) /\ forall ff_index_be_bd_full_run_execution_trace. (exists ff_lt_be_bd_full_run_execution_trace_bound. ff_lt_be_bd_full_run_execution_trace_bound + S ff_index_be_bd_full_run_execution_trace = l) -> exists ff_digit_be_bd_full_run_execution_trace ff_previous_be_bd_full_run_execution_trace ff_current_be_bd_full_run_execution_trace. ((((exists ff_h_be_bd_full_run_execution_trace_source. ff_h_be_bd_full_run_execution_trace_source + S (ff_digit_be_bd_full_run_execution_trace) = S ((S (ff_index_be_bd_full_run_execution_trace)) * c)) /\ exists ff_q_be_bd_full_run_execution_trace_source. b = ff_q_be_bd_full_run_execution_trace_source * S ((S (ff_index_be_bd_full_run_execution_trace)) * c) + (ff_digit_be_bd_full_run_execution_trace))) /\ ((((exists ff_h_be_bd_full_run_execution_trace_before. ff_h_be_bd_full_run_execution_trace_before + S (ff_previous_be_bd_full_run_execution_trace) = S ((S (ff_index_be_bd_full_run_execution_trace)) * ff_trace_scale_be_bd_full_run_execution)) /\ exists ff_q_be_bd_full_run_execution_trace_before. ff_trace_code_be_bd_full_run_execution = ff_q_be_bd_full_run_execution_trace_before * S ((S (ff_index_be_bd_full_run_execution_trace)) * ff_trace_scale_be_bd_full_run_execution) + (ff_previous_be_bd_full_run_execution_trace))) /\ ((((exists ff_h_be_bd_full_run_execution_trace_after. ff_h_be_bd_full_run_execution_trace_after + S (ff_current_be_bd_full_run_execution_trace) = S ((S (S ff_index_be_bd_full_run_execution_trace)) * ff_trace_scale_be_bd_full_run_execution)) /\ exists ff_q_be_bd_full_run_execution_trace_after. ff_trace_code_be_bd_full_run_execution = ff_q_be_bd_full_run_execution_trace_after * S ((S (S ff_index_be_bd_full_run_execution_trace)) * ff_trace_scale_be_bd_full_run_execution) + (ff_current_be_bd_full_run_execution_trace))) /\ ((((ff_digit_be_bd_full_run_execution_trace = 0) /\ (((exists ff_gap_binary_be_bd_full_run_execution_trace_transition_square. ff_gap_binary_be_bd_full_run_execution_trace_transition_square + S (ff_current_be_bd_full_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_full_run_execution_trace_transition_square_congruence ff_right_binary_be_bd_full_run_execution_trace_transition_square_congruence. (ff_previous_be_bd_full_run_execution_trace * ff_previous_be_bd_full_run_execution_trace) + m * ff_left_binary_be_bd_full_run_execution_trace_transition_square_congruence = (ff_current_be_bd_full_run_execution_trace) + m * ff_right_binary_be_bd_full_run_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_bd_full_run_execution_trace = 1) /\ (((exists ff_gap_binary_be_bd_full_run_execution_trace_transition_multiply. ff_gap_binary_be_bd_full_run_execution_trace_transition_multiply + S (ff_current_be_bd_full_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_full_run_execution_trace_transition_multiply_congruence ff_right_binary_be_bd_full_run_execution_trace_transition_multiply_congruence. ((ff_previous_be_bd_full_run_execution_trace * ff_previous_be_bd_full_run_execution_trace) * a) + m * ff_left_binary_be_bd_full_run_execution_trace_transition_multiply_congruence = (ff_current_be_bd_full_run_execution_trace) + m * ff_right_binary_be_bd_full_run_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_bd_full_run_execution_terminal. ff_h_be_bd_full_run_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_bd_full_run_execution)) /\ exists ff_q_be_bd_full_run_execution_terminal. ff_trace_code_be_bd_full_run_execution = ff_q_be_bd_full_run_execution_terminal * S ((S (l)) * ff_trace_scale_be_bd_full_run_execution) + (r))))) /\ (exists ff_power_binary_bd_full_run_power. ((exists ff_b_binary_bd_full_run_power_value ff_c_binary_bd_full_run_power_value. ((forall ff_i_binary_bd_full_run_power_value_repeat. (exists ff_lt_binary_bd_full_run_power_value_repeat_bound. ff_lt_binary_bd_full_run_power_value_repeat_bound + S ff_i_binary_bd_full_run_power_value_repeat = n) -> (((exists ff_h_binary_bd_full_run_power_value_repeat_decoded. ff_h_binary_bd_full_run_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_bd_full_run_power_value_repeat)) * ff_c_binary_bd_full_run_power_value)) /\ exists ff_q_binary_bd_full_run_power_value_repeat_decoded. ff_b_binary_bd_full_run_power_value = ff_q_binary_bd_full_run_power_value_repeat_decoded * S ((S (ff_i_binary_bd_full_run_power_value_repeat)) * ff_c_binary_bd_full_run_power_value) + (a)))) /\ (exists ff_u_binary_bd_full_run_power_value_product ff_v_binary_bd_full_run_power_value_product. ((((exists ff_h_binary_bd_full_run_power_value_product_start. ff_h_binary_bd_full_run_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_bd_full_run_power_value_product)) /\ exists ff_q_binary_bd_full_run_power_value_product_start. ff_u_binary_bd_full_run_power_value_product = ff_q_binary_bd_full_run_power_value_product_start * S ((S (0)) * ff_v_binary_bd_full_run_power_value_product) + (1))) /\ ((((exists ff_h_binary_bd_full_run_power_value_product_terminal. ff_h_binary_bd_full_run_power_value_product_terminal + S (ff_power_binary_bd_full_run_power) = S ((S (n)) * ff_v_binary_bd_full_run_power_value_product)) /\ exists ff_q_binary_bd_full_run_power_value_product_terminal. ff_u_binary_bd_full_run_power_value_product = ff_q_binary_bd_full_run_power_value_product_terminal * S ((S (n)) * ff_v_binary_bd_full_run_power_value_product) + (ff_power_binary_bd_full_run_power))) /\ forall ff_i_binary_bd_full_run_power_value_product. (exists ff_lt_binary_bd_full_run_power_value_product_bound. ff_lt_binary_bd_full_run_power_value_product_bound + S ff_i_binary_bd_full_run_power_value_product = n) -> exists ff_p_binary_bd_full_run_power_value_product ff_r_binary_bd_full_run_power_value_product ff_s_binary_bd_full_run_power_value_product. ((((exists ff_h_binary_bd_full_run_power_value_product_factor. ff_h_binary_bd_full_run_power_value_product_factor + S (ff_p_binary_bd_full_run_power_value_product) = S ((S (ff_i_binary_bd_full_run_power_value_product)) * ff_c_binary_bd_full_run_power_value)) /\ exists ff_q_binary_bd_full_run_power_value_product_factor. ff_b_binary_bd_full_run_power_value = ff_q_binary_bd_full_run_power_value_product_factor * S ((S (ff_i_binary_bd_full_run_power_value_product)) * ff_c_binary_bd_full_run_power_value) + (ff_p_binary_bd_full_run_power_value_product))) /\ ((((exists ff_h_binary_bd_full_run_power_value_product_partial. ff_h_binary_bd_full_run_power_value_product_partial + S (ff_r_binary_bd_full_run_power_value_product) = S ((S (ff_i_binary_bd_full_run_power_value_product)) * ff_v_binary_bd_full_run_power_value_product)) /\ exists ff_q_binary_bd_full_run_power_value_product_partial. ff_u_binary_bd_full_run_power_value_product = ff_q_binary_bd_full_run_power_value_product_partial * S ((S (ff_i_binary_bd_full_run_power_value_product)) * ff_v_binary_bd_full_run_power_value_product) + (ff_r_binary_bd_full_run_power_value_product))) /\ ((((exists ff_h_binary_bd_full_run_power_value_product_successor. ff_h_binary_bd_full_run_power_value_product_successor + S (ff_s_binary_bd_full_run_power_value_product) = S ((S (S ff_i_binary_bd_full_run_power_value_product)) * ff_v_binary_bd_full_run_power_value_product)) /\ exists ff_q_binary_bd_full_run_power_value_product_successor. ff_u_binary_bd_full_run_power_value_product = ff_q_binary_bd_full_run_power_value_product_successor * S ((S (S ff_i_binary_bd_full_run_power_value_product)) * ff_v_binary_bd_full_run_power_value_product) + (ff_s_binary_bd_full_run_power_value_product))) /\ ff_s_binary_bd_full_run_power_value_product = ff_r_binary_bd_full_run_power_value_product * ff_p_binary_bd_full_run_power_value_product)))))))) /\ (((exists ff_gap_binary_bd_full_run_power_residue. ff_gap_binary_bd_full_run_power_residue + S (r) = m) /\ (exists ff_left_binary_bd_full_run_power_residue_congruence ff_right_binary_bd_full_run_power_residue_congruence. (ff_power_binary_bd_full_run_power) + m * ff_left_binary_bd_full_run_power_residue_congruence = (r) + m * ff_right_binary_bd_full_run_power_residue_congruence)))))))) /\ ((exists ff_ones_bd_logarithmic_cost. ((((exists ff_u_bd_logarithmic_cost_count_sum ff_v_bd_logarithmic_cost_count_sum. ((((exists ff_h_bd_logarithmic_cost_count_sum_start. ff_h_bd_logarithmic_cost_count_sum_start + S (0) = S ((S (0)) * ff_v_bd_logarithmic_cost_count_sum)) /\ exists ff_q_bd_logarithmic_cost_count_sum_start. ff_u_bd_logarithmic_cost_count_sum = ff_q_bd_logarithmic_cost_count_sum_start * S ((S (0)) * ff_v_bd_logarithmic_cost_count_sum) + (0))) /\ ((((exists ff_h_bd_logarithmic_cost_count_sum_terminal. ff_h_bd_logarithmic_cost_count_sum_terminal + S (ff_ones_bd_logarithmic_cost) = S ((S (l)) * ff_v_bd_logarithmic_cost_count_sum)) /\ exists ff_q_bd_logarithmic_cost_count_sum_terminal. ff_u_bd_logarithmic_cost_count_sum = ff_q_bd_logarithmic_cost_count_sum_terminal * S ((S (l)) * ff_v_bd_logarithmic_cost_count_sum) + (ff_ones_bd_logarithmic_cost))) /\ forall ff_i_bd_logarithmic_cost_count_sum. (exists ff_lt_bd_logarithmic_cost_count_sum_bound. ff_lt_bd_logarithmic_cost_count_sum_bound + S ff_i_bd_logarithmic_cost_count_sum = l) -> exists ff_a_bd_logarithmic_cost_count_sum ff_r_bd_logarithmic_cost_count_sum ff_s_bd_logarithmic_cost_count_sum. ((((exists ff_h_bd_logarithmic_cost_count_sum_summand. ff_h_bd_logarithmic_cost_count_sum_summand + S (ff_a_bd_logarithmic_cost_count_sum) = S ((S (ff_i_bd_logarithmic_cost_count_sum)) * c)) /\ exists ff_q_bd_logarithmic_cost_count_sum_summand. b = ff_q_bd_logarithmic_cost_count_sum_summand * S ((S (ff_i_bd_logarithmic_cost_count_sum)) * c) + (ff_a_bd_logarithmic_cost_count_sum))) /\ ((((exists ff_h_bd_logarithmic_cost_count_sum_partial. ff_h_bd_logarithmic_cost_count_sum_partial + S (ff_r_bd_logarithmic_cost_count_sum) = S ((S (ff_i_bd_logarithmic_cost_count_sum)) * ff_v_bd_logarithmic_cost_count_sum)) /\ exists ff_q_bd_logarithmic_cost_count_sum_partial. ff_u_bd_logarithmic_cost_count_sum = ff_q_bd_logarithmic_cost_count_sum_partial * S ((S (ff_i_bd_logarithmic_cost_count_sum)) * ff_v_bd_logarithmic_cost_count_sum) + (ff_r_bd_logarithmic_cost_count_sum))) /\ ((((exists ff_h_bd_logarithmic_cost_count_sum_successor. ff_h_bd_logarithmic_cost_count_sum_successor + S (ff_s_bd_logarithmic_cost_count_sum) = S ((S (S ff_i_bd_logarithmic_cost_count_sum)) * ff_v_bd_logarithmic_cost_count_sum)) /\ exists ff_q_bd_logarithmic_cost_count_sum_successor. ff_u_bd_logarithmic_cost_count_sum = ff_q_bd_logarithmic_cost_count_sum_successor * S ((S (S ff_i_bd_logarithmic_cost_count_sum)) * ff_v_bd_logarithmic_cost_count_sum) + (ff_s_bd_logarithmic_cost_count_sum))) /\ ff_s_bd_logarithmic_cost_count_sum = ff_r_bd_logarithmic_cost_count_sum + ff_a_bd_logarithmic_cost_count_sum)))))) /\ (forall ff_i_bd_logarithmic_cost_count_bits. (exists ff_lt_bd_logarithmic_cost_count_bits_bound. ff_lt_bd_logarithmic_cost_count_bits_bound + S ff_i_bd_logarithmic_cost_count_bits = l) -> exists ff_bit_bd_logarithmic_cost_count_bits. ((((exists ff_h_bd_logarithmic_cost_count_bits_decoded. ff_h_bd_logarithmic_cost_count_bits_decoded + S (ff_bit_bd_logarithmic_cost_count_bits) = S ((S (ff_i_bd_logarithmic_cost_count_bits)) * c)) /\ exists ff_q_bd_logarithmic_cost_count_bits_decoded. b = ff_q_bd_logarithmic_cost_count_bits_decoded * S ((S (ff_i_bd_logarithmic_cost_count_bits)) * c) + (ff_bit_bd_logarithmic_cost_count_bits))) /\ (ff_bit_bd_logarithmic_cost_count_bits = 0 \/ ff_bit_bd_logarithmic_cost_count_bits = 1))))) /\ operations = (2 + (l + l)) + ff_ones_bd_logarithmic_cost)) /\ (exists gap. gap + operations = 3 * l + 2)))

Complete unchanged native tactic proof

All 46 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

46 script commands · 14 reading checkpoints · 3 local claims

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Combine an actual execution, its operation count, and a length bound

First use the existing construction of canonical exponent digits and a complete modular-exponentiation execution. The large local fact hfull packages the digit length, beta codes, accumulator trace, and modular-power result; it does not guess a new invariant.

Extract the binary-digit condition from that execution and use the operation-count theorem to obtain an actual counted cost. The last theorem bounds that cost by three times the canonical binary length plus two. The same witnesses are retained throughout, so the result couples an execution with its cost bound. This counts the formal execution operations; it is not a claim about the bit-complexity of arbitrary-precision multiplication.

Mathematical commentary bound to this exact script; it grants no proof authority.

Named ingredients (3)
binary modular exponent coded execution existsbinary digit operation count existsbinary modular execution bitlength bound

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro a
  3. L3
    intro m
  4. L4
    intro hmodulus
02Establish hfullL5–10

Apply binary_modular_exponent_coded_execution_exists to the exponent n, base a, modulus m, and its guard. The resulting existential package is exactly the long hfull formula.

  1. L5
    have hfull : ∃ l. ∃ b. ∃ c. ∃ r. BinaryCompleteModularExecution(n,a,m,l,b,c,r)Definitions: BinaryCompleteModularExecutionOriginal native command in the exact edition
  2. L6
    specialize binary_modular_exponent_coded_execution_exists n
  3. L7
    specialize binary_modular_exponent_coded_execution_exists a
  4. L8
    specialize binary_modular_exponent_coded_execution_exists m
  5. L9
    apply binary_modular_exponent_coded_execution_exists
  6. L10
    exact hmodulus
03Separate the logical casesL11–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L11
    cases hfull
  2. L12
    cases hfull_witness
  3. L13
    cases hfull_witness_witness
  4. L14
    cases hfull_witness_witness_witness
04Establish hdigitsL15–15

Project the binary-digit property from the completed execution. This is an existing component of hfull, not an extra assumption about the digits.

  1. L15
    have hdigits : BinaryDigitPrefix(x1,x2,x)Definitions: BinaryDigitPrefixOriginal native command in the exact edition
05Separate the logical casesL16–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    cases hfull_witness_witness_witness_witness
  2. L17
    cases hfull_witness_witness_witness_witness_left
  3. L18
    cases hfull_witness_witness_witness_witness_left_right
06Use earlier factsL19–19

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L19
    exact hfull_witness_witness_witness_witness_left_right_left
07Establish hcostL20–25

Use that digit property to obtain the beta-counted number of operations for these very same digit codes. The final application combines this witness with the existing execution bound.

  1. L20
    have hcost : ∃ operations. BinaryExecutionOperationCount(x1,x2,x,operations)Definitions: BinaryExecutionOperationCountOriginal native command in the exact edition
  2. L21
    specialize binary_digit_operation_count_exists x1
  3. L22
    specialize binary_digit_operation_count_exists x2
  4. L23
    specialize binary_digit_operation_count_exists x
  5. L24
    apply binary_digit_operation_count_exists
  6. L25
    exact hdigits
08Separate the logical casesL26–26

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L26
    cases hcost
09Construct an explicit witnessL27–31

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists x
  2. L28
    exists x1
  3. L29
    exists x2
  4. L30
    exists x3
  5. L31
    exists x4
10Separate the logical casesL32–32

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L32
    split
11Use earlier factsL33–33

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L33
    exact hfull_witness_witness_witness_witness
12Separate the logical casesL34–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L34
    split
13Use earlier factsL35–44

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L35
    exact hcost_witness
  2. L36
    specialize binary_modular_execution_bitlength_bound n
  3. L37
    specialize binary_modular_execution_bitlength_bound a
  4. L38
    specialize binary_modular_execution_bitlength_bound m
  5. L39
    specialize binary_modular_execution_bitlength_bound x
  6. L40
    specialize binary_modular_execution_bitlength_bound x1
  7. L41
    specialize binary_modular_execution_bitlength_bound x2
  8. L42
    specialize binary_modular_execution_bitlength_bound x3
  9. L43
    specialize binary_modular_execution_bitlength_bound x4
  10. L44
    apply binary_modular_execution_bitlength_bound
14Use earlier factsL45–46

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L45
    exact hfull_witness_witness_witness_witness
  2. L46
    exact hcost_witness

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro m
  4. 0004intro hmodulus
  5. 0005have hfull : exists l b c r. ((((((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_logarithmic_run_canonical_length ff_lower_bl_bd_logarithmic_run_canonical_length ff_upper_bl_bd_logarithmic_run_canonical_length. (((l) = S ff_exponent_bl_bd_logarithmic_run_canonical_length) /\ ((exists ff_positive_bl_bd_logarithmic_run_canonical_length. ff_positive_bl_bd_logarithmic_run_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_logarithmic_run_canonical_length_lower pa_c_bl_bd_logarithmic_run_canonical_length_lower. ((forall pa_i_bl_bd_logarithmic_run_canonical_length_lower_repeat. (exists pa_lt_bl_bd_logarithmic_run_canonical_length_lower_repeat_bound. pa_lt_bl_bd_logarithmic_run_canonical_length_lower_repeat_bound + S pa_i_bl_bd_logarithmic_run_canonical_length_lower_repeat = ff_exponent_bl_bd_logarithmic_run_canonical_length) -> (((exists pa_h_bl_bd_logarithmic_run_canonical_length_lower_repeat_decoded. pa_h_bl_bd_logarithmic_run_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_lower_repeat)) * pa_c_bl_bd_logarithmic_run_canonical_length_lower)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_lower_repeat_decoded. pa_b_bl_bd_logarithmic_run_canonical_length_lower = pa_q_bl_bd_logarithmic_run_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_lower_repeat)) * pa_c_bl_bd_logarithmic_run_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_logarithmic_run_canonical_length_lower_product pa_v_bl_bd_logarithmic_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_start. pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_start. pa_u_bl_bd_logarithmic_run_canonical_length_lower_product = pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_terminal. pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_logarithmic_run_canonical_length) = S ((S (ff_exponent_bl_bd_logarithmic_run_canonical_length)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_terminal. pa_u_bl_bd_logarithmic_run_canonical_length_lower_product = pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_logarithmic_run_canonical_length)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product) + (ff_lower_bl_bd_logarithmic_run_canonical_length))) /\ forall pa_i_bl_bd_logarithmic_run_canonical_length_lower_product. (exists pa_lt_bl_bd_logarithmic_run_canonical_length_lower_product_bound. pa_lt_bl_bd_logarithmic_run_canonical_length_lower_product_bound + S pa_i_bl_bd_logarithmic_run_canonical_length_lower_product = ff_exponent_bl_bd_logarithmic_run_canonical_length) -> exists pa_p_bl_bd_logarithmic_run_canonical_length_lower_product pa_r_bl_bd_logarithmic_run_canonical_length_lower_product pa_s_bl_bd_logarithmic_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_factor. pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_factor + S (pa_p_bl_bd_logarithmic_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_lower_product)) * pa_c_bl_bd_logarithmic_run_canonical_length_lower)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_factor. pa_b_bl_bd_logarithmic_run_canonical_length_lower = pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_lower_product)) * pa_c_bl_bd_logarithmic_run_canonical_length_lower) + (pa_p_bl_bd_logarithmic_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_partial. pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_partial + S (pa_r_bl_bd_logarithmic_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_lower_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_partial. pa_u_bl_bd_logarithmic_run_canonical_length_lower_product = pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_lower_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product) + (pa_r_bl_bd_logarithmic_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_successor. pa_h_bl_bd_logarithmic_run_canonical_length_lower_product_successor + S (pa_s_bl_bd_logarithmic_run_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_logarithmic_run_canonical_length_lower_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_successor. pa_u_bl_bd_logarithmic_run_canonical_length_lower_product = pa_q_bl_bd_logarithmic_run_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_logarithmic_run_canonical_length_lower_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_lower_product) + (pa_s_bl_bd_logarithmic_run_canonical_length_lower_product))) /\ pa_s_bl_bd_logarithmic_run_canonical_length_lower_product = pa_r_bl_bd_logarithmic_run_canonical_length_lower_product * pa_p_bl_bd_logarithmic_run_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_logarithmic_run_canonical_length_upper pa_c_bl_bd_logarithmic_run_canonical_length_upper. ((forall pa_i_bl_bd_logarithmic_run_canonical_length_upper_repeat. (exists pa_lt_bl_bd_logarithmic_run_canonical_length_upper_repeat_bound. pa_lt_bl_bd_logarithmic_run_canonical_length_upper_repeat_bound + S pa_i_bl_bd_logarithmic_run_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_logarithmic_run_canonical_length_upper_repeat_decoded. pa_h_bl_bd_logarithmic_run_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_upper_repeat)) * pa_c_bl_bd_logarithmic_run_canonical_length_upper)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_upper_repeat_decoded. pa_b_bl_bd_logarithmic_run_canonical_length_upper = pa_q_bl_bd_logarithmic_run_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_upper_repeat)) * pa_c_bl_bd_logarithmic_run_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_logarithmic_run_canonical_length_upper_product pa_v_bl_bd_logarithmic_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_start. pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_start. pa_u_bl_bd_logarithmic_run_canonical_length_upper_product = pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_terminal. pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_logarithmic_run_canonical_length) = S ((S (l)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_terminal. pa_u_bl_bd_logarithmic_run_canonical_length_upper_product = pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product) + (ff_upper_bl_bd_logarithmic_run_canonical_length))) /\ forall pa_i_bl_bd_logarithmic_run_canonical_length_upper_product. (exists pa_lt_bl_bd_logarithmic_run_canonical_length_upper_product_bound. pa_lt_bl_bd_logarithmic_run_canonical_length_upper_product_bound + S pa_i_bl_bd_logarithmic_run_canonical_length_upper_product = l) -> exists pa_p_bl_bd_logarithmic_run_canonical_length_upper_product pa_r_bl_bd_logarithmic_run_canonical_length_upper_product pa_s_bl_bd_logarithmic_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_factor. pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_factor + S (pa_p_bl_bd_logarithmic_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_upper_product)) * pa_c_bl_bd_logarithmic_run_canonical_length_upper)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_factor. pa_b_bl_bd_logarithmic_run_canonical_length_upper = pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_upper_product)) * pa_c_bl_bd_logarithmic_run_canonical_length_upper) + (pa_p_bl_bd_logarithmic_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_partial. pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_partial + S (pa_r_bl_bd_logarithmic_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_upper_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_partial. pa_u_bl_bd_logarithmic_run_canonical_length_upper_product = pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_logarithmic_run_canonical_length_upper_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product) + (pa_r_bl_bd_logarithmic_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_successor. pa_h_bl_bd_logarithmic_run_canonical_length_upper_product_successor + S (pa_s_bl_bd_logarithmic_run_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_logarithmic_run_canonical_length_upper_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_successor. pa_u_bl_bd_logarithmic_run_canonical_length_upper_product = pa_q_bl_bd_logarithmic_run_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_logarithmic_run_canonical_length_upper_product)) * pa_v_bl_bd_logarithmic_run_canonical_length_upper_product) + (pa_s_bl_bd_logarithmic_run_canonical_length_upper_product))) /\ pa_s_bl_bd_logarithmic_run_canonical_length_upper_product = pa_r_bl_bd_logarithmic_run_canonical_length_upper_product * pa_p_bl_bd_logarithmic_run_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_logarithmic_run_canonical_length. ff_lower_gap_bl_bd_logarithmic_run_canonical_length + (ff_lower_bl_bd_logarithmic_run_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_logarithmic_run_canonical_length. ff_upper_gap_bl_bd_logarithmic_run_canonical_length + S (n) = (ff_upper_bl_bd_logarithmic_run_canonical_length))))))))) /\ (((forall ff_index_be_bd_logarithmic_run_canonical_code_digits ff_digit_be_bd_logarithmic_run_canonical_code_digits. (exists ff_lt_be_bd_logarithmic_run_canonical_code_digits_bound. ff_lt_be_bd_logarithmic_run_canonical_code_digits_bound + S ff_index_be_bd_logarithmic_run_canonical_code_digits = l) -> (((exists ff_h_be_bd_logarithmic_run_canonical_code_digits_digit. ff_h_be_bd_logarithmic_run_canonical_code_digits_digit + S (ff_digit_be_bd_logarithmic_run_canonical_code_digits) = S ((S (ff_index_be_bd_logarithmic_run_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_logarithmic_run_canonical_code_digits_digit. b = ff_q_be_bd_logarithmic_run_canonical_code_digits_digit * S ((S (ff_index_be_bd_logarithmic_run_canonical_code_digits)) * c) + (ff_digit_be_bd_logarithmic_run_canonical_code_digits))) -> (ff_digit_be_bd_logarithmic_run_canonical_code_digits = 0 \/ ff_digit_be_bd_logarithmic_run_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_logarithmic_run_canonical_code_horner ff_v_ph_bd_logarithmic_run_canonical_code_horner. ((((exists fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_start. fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner)) /\ exists fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_start. ff_u_ph_bd_logarithmic_run_canonical_code_horner = fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_terminal. fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner)) /\ exists fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_terminal. ff_u_ph_bd_logarithmic_run_canonical_code_horner = fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps. (exists ph_bound_bd_logarithmic_run_canonical_code_horner_body_steps. ph_bound_bd_logarithmic_run_canonical_code_horner_body_steps + S ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_logarithmic_run_canonical_code_horner_body_steps ff_previous_ph_bd_logarithmic_run_canonical_code_horner_body_steps ff_current_ph_bd_logarithmic_run_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_logarithmic_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_logarithmic_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_steps_before. fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_logarithmic_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner)) /\ exists fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_steps_before. ff_u_ph_bd_logarithmic_run_canonical_code_horner = fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner) + (ff_previous_ph_bd_logarithmic_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_steps_after. fs_h_ph_bd_logarithmic_run_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_logarithmic_run_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner)) /\ exists fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_steps_after. ff_u_ph_bd_logarithmic_run_canonical_code_horner = fs_q_ph_bd_logarithmic_run_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_logarithmic_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_logarithmic_run_canonical_code_horner) + (ff_current_ph_bd_logarithmic_run_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_logarithmic_run_canonical_code_horner_body_steps = ff_previous_ph_bd_logarithmic_run_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_logarithmic_run_canonical_code_horner_body_steps)))))))))) /\ ((exists ff_trace_code_be_bd_logarithmic_run_execution ff_trace_scale_be_bd_logarithmic_run_execution. ((((((exists ff_h_be_bd_logarithmic_run_execution_trace_start. ff_h_be_bd_logarithmic_run_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_bd_logarithmic_run_execution)) /\ exists ff_q_be_bd_logarithmic_run_execution_trace_start. ff_trace_code_be_bd_logarithmic_run_execution = ff_q_be_bd_logarithmic_run_execution_trace_start * S ((S (0)) * ff_trace_scale_be_bd_logarithmic_run_execution) + (1))) /\ forall ff_index_be_bd_logarithmic_run_execution_trace. (exists ff_lt_be_bd_logarithmic_run_execution_trace_bound. ff_lt_be_bd_logarithmic_run_execution_trace_bound + S ff_index_be_bd_logarithmic_run_execution_trace = l) -> exists ff_digit_be_bd_logarithmic_run_execution_trace ff_previous_be_bd_logarithmic_run_execution_trace ff_current_be_bd_logarithmic_run_execution_trace. ((((exists ff_h_be_bd_logarithmic_run_execution_trace_source. ff_h_be_bd_logarithmic_run_execution_trace_source + S (ff_digit_be_bd_logarithmic_run_execution_trace) = S ((S (ff_index_be_bd_logarithmic_run_execution_trace)) * c)) /\ exists ff_q_be_bd_logarithmic_run_execution_trace_source. b = ff_q_be_bd_logarithmic_run_execution_trace_source * S ((S (ff_index_be_bd_logarithmic_run_execution_trace)) * c) + (ff_digit_be_bd_logarithmic_run_execution_trace))) /\ ((((exists ff_h_be_bd_logarithmic_run_execution_trace_before. ff_h_be_bd_logarithmic_run_execution_trace_before + S (ff_previous_be_bd_logarithmic_run_execution_trace) = S ((S (ff_index_be_bd_logarithmic_run_execution_trace)) * ff_trace_scale_be_bd_logarithmic_run_execution)) /\ exists ff_q_be_bd_logarithmic_run_execution_trace_before. ff_trace_code_be_bd_logarithmic_run_execution = ff_q_be_bd_logarithmic_run_execution_trace_before * S ((S (ff_index_be_bd_logarithmic_run_execution_trace)) * ff_trace_scale_be_bd_logarithmic_run_execution) + (ff_previous_be_bd_logarithmic_run_execution_trace))) /\ ((((exists ff_h_be_bd_logarithmic_run_execution_trace_after. ff_h_be_bd_logarithmic_run_execution_trace_after + S (ff_current_be_bd_logarithmic_run_execution_trace) = S ((S (S ff_index_be_bd_logarithmic_run_execution_trace)) * ff_trace_scale_be_bd_logarithmic_run_execution)) /\ exists ff_q_be_bd_logarithmic_run_execution_trace_after. ff_trace_code_be_bd_logarithmic_run_execution = ff_q_be_bd_logarithmic_run_execution_trace_after * S ((S (S ff_index_be_bd_logarithmic_run_execution_trace)) * ff_trace_scale_be_bd_logarithmic_run_execution) + (ff_current_be_bd_logarithmic_run_execution_trace))) /\ ((((ff_digit_be_bd_logarithmic_run_execution_trace = 0) /\ (((exists ff_gap_binary_be_bd_logarithmic_run_execution_trace_transition_square. ff_gap_binary_be_bd_logarithmic_run_execution_trace_transition_square + S (ff_current_be_bd_logarithmic_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_logarithmic_run_execution_trace_transition_square_congruence ff_right_binary_be_bd_logarithmic_run_execution_trace_transition_square_congruence. (ff_previous_be_bd_logarithmic_run_execution_trace * ff_previous_be_bd_logarithmic_run_execution_trace) + m * ff_left_binary_be_bd_logarithmic_run_execution_trace_transition_square_congruence = (ff_current_be_bd_logarithmic_run_execution_trace) + m * ff_right_binary_be_bd_logarithmic_run_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_bd_logarithmic_run_execution_trace = 1) /\ (((exists ff_gap_binary_be_bd_logarithmic_run_execution_trace_transition_multiply. ff_gap_binary_be_bd_logarithmic_run_execution_trace_transition_multiply + S (ff_current_be_bd_logarithmic_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_logarithmic_run_execution_trace_transition_multiply_congruence ff_right_binary_be_bd_logarithmic_run_execution_trace_transition_multiply_congruence. ((ff_previous_be_bd_logarithmic_run_execution_trace * ff_previous_be_bd_logarithmic_run_execution_trace) * a) + m * ff_left_binary_be_bd_logarithmic_run_execution_trace_transition_multiply_congruence = (ff_current_be_bd_logarithmic_run_execution_trace) + m * ff_right_binary_be_bd_logarithmic_run_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_bd_logarithmic_run_execution_terminal. ff_h_be_bd_logarithmic_run_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_bd_logarithmic_run_execution)) /\ exists ff_q_be_bd_logarithmic_run_execution_terminal. ff_trace_code_be_bd_logarithmic_run_execution = ff_q_be_bd_logarithmic_run_execution_terminal * S ((S (l)) * ff_trace_scale_be_bd_logarithmic_run_execution) + (r))))) /\ (exists ff_power_binary_bd_logarithmic_run_power. ((exists ff_b_binary_bd_logarithmic_run_power_value ff_c_binary_bd_logarithmic_run_power_value. ((forall ff_i_binary_bd_logarithmic_run_power_value_repeat. (exists ff_lt_binary_bd_logarithmic_run_power_value_repeat_bound. ff_lt_binary_bd_logarithmic_run_power_value_repeat_bound + S ff_i_binary_bd_logarithmic_run_power_value_repeat = n) -> (((exists ff_h_binary_bd_logarithmic_run_power_value_repeat_decoded. ff_h_binary_bd_logarithmic_run_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_bd_logarithmic_run_power_value_repeat)) * ff_c_binary_bd_logarithmic_run_power_value)) /\ exists ff_q_binary_bd_logarithmic_run_power_value_repeat_decoded. ff_b_binary_bd_logarithmic_run_power_value = ff_q_binary_bd_logarithmic_run_power_value_repeat_decoded * S ((S (ff_i_binary_bd_logarithmic_run_power_value_repeat)) * ff_c_binary_bd_logarithmic_run_power_value) + (a)))) /\ (exists ff_u_binary_bd_logarithmic_run_power_value_product ff_v_binary_bd_logarithmic_run_power_value_product. ((((exists ff_h_binary_bd_logarithmic_run_power_value_product_start. ff_h_binary_bd_logarithmic_run_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_bd_logarithmic_run_power_value_product)) /\ exists ff_q_binary_bd_logarithmic_run_power_value_product_start. ff_u_binary_bd_logarithmic_run_power_value_product = ff_q_binary_bd_logarithmic_run_power_value_product_start * S ((S (0)) * ff_v_binary_bd_logarithmic_run_power_value_product) + (1))) /\ ((((exists ff_h_binary_bd_logarithmic_run_power_value_product_terminal. ff_h_binary_bd_logarithmic_run_power_value_product_terminal + S (ff_power_binary_bd_logarithmic_run_power) = S ((S (n)) * ff_v_binary_bd_logarithmic_run_power_value_product)) /\ exists ff_q_binary_bd_logarithmic_run_power_value_product_terminal. ff_u_binary_bd_logarithmic_run_power_value_product = ff_q_binary_bd_logarithmic_run_power_value_product_terminal * S ((S (n)) * ff_v_binary_bd_logarithmic_run_power_value_product) + (ff_power_binary_bd_logarithmic_run_power))) /\ forall ff_i_binary_bd_logarithmic_run_power_value_product. (exists ff_lt_binary_bd_logarithmic_run_power_value_product_bound. ff_lt_binary_bd_logarithmic_run_power_value_product_bound + S ff_i_binary_bd_logarithmic_run_power_value_product = n) -> exists ff_p_binary_bd_logarithmic_run_power_value_product ff_r_binary_bd_logarithmic_run_power_value_product ff_s_binary_bd_logarithmic_run_power_value_product. ((((exists ff_h_binary_bd_logarithmic_run_power_value_product_factor. ff_h_binary_bd_logarithmic_run_power_value_product_factor + S (ff_p_binary_bd_logarithmic_run_power_value_product) = S ((S (ff_i_binary_bd_logarithmic_run_power_value_product)) * ff_c_binary_bd_logarithmic_run_power_value)) /\ exists ff_q_binary_bd_logarithmic_run_power_value_product_factor. ff_b_binary_bd_logarithmic_run_power_value = ff_q_binary_bd_logarithmic_run_power_value_product_factor * S ((S (ff_i_binary_bd_logarithmic_run_power_value_product)) * ff_c_binary_bd_logarithmic_run_power_value) + (ff_p_binary_bd_logarithmic_run_power_value_product))) /\ ((((exists ff_h_binary_bd_logarithmic_run_power_value_product_partial. ff_h_binary_bd_logarithmic_run_power_value_product_partial + S (ff_r_binary_bd_logarithmic_run_power_value_product) = S ((S (ff_i_binary_bd_logarithmic_run_power_value_product)) * ff_v_binary_bd_logarithmic_run_power_value_product)) /\ exists ff_q_binary_bd_logarithmic_run_power_value_product_partial. ff_u_binary_bd_logarithmic_run_power_value_product = ff_q_binary_bd_logarithmic_run_power_value_product_partial * S ((S (ff_i_binary_bd_logarithmic_run_power_value_product)) * ff_v_binary_bd_logarithmic_run_power_value_product) + (ff_r_binary_bd_logarithmic_run_power_value_product))) /\ ((((exists ff_h_binary_bd_logarithmic_run_power_value_product_successor. ff_h_binary_bd_logarithmic_run_power_value_product_successor + S (ff_s_binary_bd_logarithmic_run_power_value_product) = S ((S (S ff_i_binary_bd_logarithmic_run_power_value_product)) * ff_v_binary_bd_logarithmic_run_power_value_product)) /\ exists ff_q_binary_bd_logarithmic_run_power_value_product_successor. ff_u_binary_bd_logarithmic_run_power_value_product = ff_q_binary_bd_logarithmic_run_power_value_product_successor * S ((S (S ff_i_binary_bd_logarithmic_run_power_value_product)) * ff_v_binary_bd_logarithmic_run_power_value_product) + (ff_s_binary_bd_logarithmic_run_power_value_product))) /\ ff_s_binary_bd_logarithmic_run_power_value_product = ff_r_binary_bd_logarithmic_run_power_value_product * ff_p_binary_bd_logarithmic_run_power_value_product)))))))) /\ (((exists ff_gap_binary_bd_logarithmic_run_power_residue. ff_gap_binary_bd_logarithmic_run_power_residue + S (r) = m) /\ (exists ff_left_binary_bd_logarithmic_run_power_residue_congruence ff_right_binary_bd_logarithmic_run_power_residue_congruence. (ff_power_binary_bd_logarithmic_run_power) + m * ff_left_binary_bd_logarithmic_run_power_residue_congruence = (r) + m * ff_right_binary_bd_logarithmic_run_power_residue_congruence))))))))
  6. 0006specialize binary_modular_exponent_coded_execution_exists n
  7. 0007specialize binary_modular_exponent_coded_execution_exists a
  8. 0008specialize binary_modular_exponent_coded_execution_exists m
  9. 0009apply binary_modular_exponent_coded_execution_exists
  10. 0010exact hmodulus
  11. 0011cases hfull
  12. 0012cases hfull_witness
  13. 0013cases hfull_witness_witness
  14. 0014cases hfull_witness_witness_witness
  15. 0015have hdigits : (forall ff_index_be_bd_logarithmic_digits ff_digit_be_bd_logarithmic_digits. (exists ff_lt_be_bd_logarithmic_digits_bound. ff_lt_be_bd_logarithmic_digits_bound + S ff_index_be_bd_logarithmic_digits = x) -> (((exists ff_h_be_bd_logarithmic_digits_digit. ff_h_be_bd_logarithmic_digits_digit + S (ff_digit_be_bd_logarithmic_digits) = S ((S (ff_index_be_bd_logarithmic_digits)) * x2)) /\ exists ff_q_be_bd_logarithmic_digits_digit. x1 = ff_q_be_bd_logarithmic_digits_digit * S ((S (ff_index_be_bd_logarithmic_digits)) * x2) + (ff_digit_be_bd_logarithmic_digits))) -> (ff_digit_be_bd_logarithmic_digits = 0 \/ ff_digit_be_bd_logarithmic_digits = 1))
  16. 0016cases hfull_witness_witness_witness_witness
  17. 0017cases hfull_witness_witness_witness_witness_left
  18. 0018cases hfull_witness_witness_witness_witness_left_right
  19. 0019exact hfull_witness_witness_witness_witness_left_right_left
  20. 0020have hcost : exists operations. (exists ff_ones_bd_logarithmic_chosen. ((((exists ff_u_bd_logarithmic_chosen_count_sum ff_v_bd_logarithmic_chosen_count_sum. ((((exists ff_h_bd_logarithmic_chosen_count_sum_start. ff_h_bd_logarithmic_chosen_count_sum_start + S (0) = S ((S (0)) * ff_v_bd_logarithmic_chosen_count_sum)) /\ exists ff_q_bd_logarithmic_chosen_count_sum_start. ff_u_bd_logarithmic_chosen_count_sum = ff_q_bd_logarithmic_chosen_count_sum_start * S ((S (0)) * ff_v_bd_logarithmic_chosen_count_sum) + (0))) /\ ((((exists ff_h_bd_logarithmic_chosen_count_sum_terminal. ff_h_bd_logarithmic_chosen_count_sum_terminal + S (ff_ones_bd_logarithmic_chosen) = S ((S (x)) * ff_v_bd_logarithmic_chosen_count_sum)) /\ exists ff_q_bd_logarithmic_chosen_count_sum_terminal. ff_u_bd_logarithmic_chosen_count_sum = ff_q_bd_logarithmic_chosen_count_sum_terminal * S ((S (x)) * ff_v_bd_logarithmic_chosen_count_sum) + (ff_ones_bd_logarithmic_chosen))) /\ forall ff_i_bd_logarithmic_chosen_count_sum. (exists ff_lt_bd_logarithmic_chosen_count_sum_bound. ff_lt_bd_logarithmic_chosen_count_sum_bound + S ff_i_bd_logarithmic_chosen_count_sum = x) -> exists ff_a_bd_logarithmic_chosen_count_sum ff_r_bd_logarithmic_chosen_count_sum ff_s_bd_logarithmic_chosen_count_sum. ((((exists ff_h_bd_logarithmic_chosen_count_sum_summand. ff_h_bd_logarithmic_chosen_count_sum_summand + S (ff_a_bd_logarithmic_chosen_count_sum) = S ((S (ff_i_bd_logarithmic_chosen_count_sum)) * x2)) /\ exists ff_q_bd_logarithmic_chosen_count_sum_summand. x1 = ff_q_bd_logarithmic_chosen_count_sum_summand * S ((S (ff_i_bd_logarithmic_chosen_count_sum)) * x2) + (ff_a_bd_logarithmic_chosen_count_sum))) /\ ((((exists ff_h_bd_logarithmic_chosen_count_sum_partial. ff_h_bd_logarithmic_chosen_count_sum_partial + S (ff_r_bd_logarithmic_chosen_count_sum) = S ((S (ff_i_bd_logarithmic_chosen_count_sum)) * ff_v_bd_logarithmic_chosen_count_sum)) /\ exists ff_q_bd_logarithmic_chosen_count_sum_partial. ff_u_bd_logarithmic_chosen_count_sum = ff_q_bd_logarithmic_chosen_count_sum_partial * S ((S (ff_i_bd_logarithmic_chosen_count_sum)) * ff_v_bd_logarithmic_chosen_count_sum) + (ff_r_bd_logarithmic_chosen_count_sum))) /\ ((((exists ff_h_bd_logarithmic_chosen_count_sum_successor. ff_h_bd_logarithmic_chosen_count_sum_successor + S (ff_s_bd_logarithmic_chosen_count_sum) = S ((S (S ff_i_bd_logarithmic_chosen_count_sum)) * ff_v_bd_logarithmic_chosen_count_sum)) /\ exists ff_q_bd_logarithmic_chosen_count_sum_successor. ff_u_bd_logarithmic_chosen_count_sum = ff_q_bd_logarithmic_chosen_count_sum_successor * S ((S (S ff_i_bd_logarithmic_chosen_count_sum)) * ff_v_bd_logarithmic_chosen_count_sum) + (ff_s_bd_logarithmic_chosen_count_sum))) /\ ff_s_bd_logarithmic_chosen_count_sum = ff_r_bd_logarithmic_chosen_count_sum + ff_a_bd_logarithmic_chosen_count_sum)))))) /\ (forall ff_i_bd_logarithmic_chosen_count_bits. (exists ff_lt_bd_logarithmic_chosen_count_bits_bound. ff_lt_bd_logarithmic_chosen_count_bits_bound + S ff_i_bd_logarithmic_chosen_count_bits = x) -> exists ff_bit_bd_logarithmic_chosen_count_bits. ((((exists ff_h_bd_logarithmic_chosen_count_bits_decoded. ff_h_bd_logarithmic_chosen_count_bits_decoded + S (ff_bit_bd_logarithmic_chosen_count_bits) = S ((S (ff_i_bd_logarithmic_chosen_count_bits)) * x2)) /\ exists ff_q_bd_logarithmic_chosen_count_bits_decoded. x1 = ff_q_bd_logarithmic_chosen_count_bits_decoded * S ((S (ff_i_bd_logarithmic_chosen_count_bits)) * x2) + (ff_bit_bd_logarithmic_chosen_count_bits))) /\ (ff_bit_bd_logarithmic_chosen_count_bits = 0 \/ ff_bit_bd_logarithmic_chosen_count_bits = 1))))) /\ operations = (2 + (x + x)) + ff_ones_bd_logarithmic_chosen))
  21. 0021specialize binary_digit_operation_count_exists x1
  22. 0022specialize binary_digit_operation_count_exists x2
  23. 0023specialize binary_digit_operation_count_exists x
  24. 0024apply binary_digit_operation_count_exists
  25. 0025exact hdigits
  26. 0026cases hcost
  27. 0027exists x
  28. 0028exists x1
  29. 0029exists x2
  30. 0030exists x3
  31. 0031exists x4
  32. 0032split
  33. 0033exact hfull_witness_witness_witness_witness
  34. 0034split
  35. 0035exact hcost_witness
  36. 0036specialize binary_modular_execution_bitlength_bound n
  37. 0037specialize binary_modular_execution_bitlength_bound a
  38. 0038specialize binary_modular_execution_bitlength_bound m
  39. 0039specialize binary_modular_execution_bitlength_bound x
  40. 0040specialize binary_modular_execution_bitlength_bound x1
  41. 0041specialize binary_modular_execution_bitlength_bound x2
  42. 0042specialize binary_modular_execution_bitlength_bound x3
  43. 0043specialize binary_modular_execution_bitlength_bound x4
  44. 0044apply binary_modular_execution_bitlength_bound
  45. 0045exact hfull_witness_witness_witness_witness
  46. 0046exact hcost_witness