BD0016

binary_modular_exponent_coded_execution_exists_unique

Every arbitrary natural exponent has exactly one canonical modular result produced by genuine constructed canonical-length beta-coded execution.

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. BinaryCompleteModularExecution(n,a,m,y,z,k,x)) ∧ (∀ y. (∃ z. ∃ k. ∃ i. BinaryCompleteModularExecution(n,a,m,z,k,i,y)) → x = y)

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

Definition DAG

BinaryModulus(m) · 1BinaryCompleteModularExecution(e,a,m,ell,b,c,r) · 2

Actual proof prerequisites

binary_modular_exponent_coded_execution_existsbinary_modular_exponent_coded_execution_result_functional
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 r. ((exists l b c. ((((((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_unique_chosen_canonical_length ff_lower_bl_bd_unique_chosen_canonical_length ff_upper_bl_bd_unique_chosen_canonical_length. (((l) = S ff_exponent_bl_bd_unique_chosen_canonical_length) /\ ((exists ff_positive_bl_bd_unique_chosen_canonical_length. ff_positive_bl_bd_unique_chosen_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_unique_chosen_canonical_length_lower pa_c_bl_bd_unique_chosen_canonical_length_lower. ((forall pa_i_bl_bd_unique_chosen_canonical_length_lower_repeat. (exists pa_lt_bl_bd_unique_chosen_canonical_length_lower_repeat_bound. pa_lt_bl_bd_unique_chosen_canonical_length_lower_repeat_bound + S pa_i_bl_bd_unique_chosen_canonical_length_lower_repeat = ff_exponent_bl_bd_unique_chosen_canonical_length) -> (((exists pa_h_bl_bd_unique_chosen_canonical_length_lower_repeat_decoded. pa_h_bl_bd_unique_chosen_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_unique_chosen_canonical_length_lower_repeat)) * pa_c_bl_bd_unique_chosen_canonical_length_lower)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_lower_repeat_decoded. pa_b_bl_bd_unique_chosen_canonical_length_lower = pa_q_bl_bd_unique_chosen_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_unique_chosen_canonical_length_lower_repeat)) * pa_c_bl_bd_unique_chosen_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_unique_chosen_canonical_length_lower_product pa_v_bl_bd_unique_chosen_canonical_length_lower_product. ((((exists pa_h_bl_bd_unique_chosen_canonical_length_lower_product_start. pa_h_bl_bd_unique_chosen_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_lower_product_start. pa_u_bl_bd_unique_chosen_canonical_length_lower_product = pa_q_bl_bd_unique_chosen_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_unique_chosen_canonical_length_lower_product_terminal. pa_h_bl_bd_unique_chosen_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_unique_chosen_canonical_length) = S ((S (ff_exponent_bl_bd_unique_chosen_canonical_length)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_lower_product_terminal. pa_u_bl_bd_unique_chosen_canonical_length_lower_product = pa_q_bl_bd_unique_chosen_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_unique_chosen_canonical_length)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product) + (ff_lower_bl_bd_unique_chosen_canonical_length))) /\ forall pa_i_bl_bd_unique_chosen_canonical_length_lower_product. (exists pa_lt_bl_bd_unique_chosen_canonical_length_lower_product_bound. pa_lt_bl_bd_unique_chosen_canonical_length_lower_product_bound + S pa_i_bl_bd_unique_chosen_canonical_length_lower_product = ff_exponent_bl_bd_unique_chosen_canonical_length) -> exists pa_p_bl_bd_unique_chosen_canonical_length_lower_product pa_r_bl_bd_unique_chosen_canonical_length_lower_product pa_s_bl_bd_unique_chosen_canonical_length_lower_product. ((((exists pa_h_bl_bd_unique_chosen_canonical_length_lower_product_factor. pa_h_bl_bd_unique_chosen_canonical_length_lower_product_factor + S (pa_p_bl_bd_unique_chosen_canonical_length_lower_product) = S ((S (pa_i_bl_bd_unique_chosen_canonical_length_lower_product)) * pa_c_bl_bd_unique_chosen_canonical_length_lower)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_lower_product_factor. pa_b_bl_bd_unique_chosen_canonical_length_lower = pa_q_bl_bd_unique_chosen_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_unique_chosen_canonical_length_lower_product)) * pa_c_bl_bd_unique_chosen_canonical_length_lower) + (pa_p_bl_bd_unique_chosen_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_unique_chosen_canonical_length_lower_product_partial. pa_h_bl_bd_unique_chosen_canonical_length_lower_product_partial + S (pa_r_bl_bd_unique_chosen_canonical_length_lower_product) = S ((S (pa_i_bl_bd_unique_chosen_canonical_length_lower_product)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_lower_product_partial. pa_u_bl_bd_unique_chosen_canonical_length_lower_product = pa_q_bl_bd_unique_chosen_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_unique_chosen_canonical_length_lower_product)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product) + (pa_r_bl_bd_unique_chosen_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_unique_chosen_canonical_length_lower_product_successor. pa_h_bl_bd_unique_chosen_canonical_length_lower_product_successor + S (pa_s_bl_bd_unique_chosen_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_unique_chosen_canonical_length_lower_product)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_lower_product_successor. pa_u_bl_bd_unique_chosen_canonical_length_lower_product = pa_q_bl_bd_unique_chosen_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_unique_chosen_canonical_length_lower_product)) * pa_v_bl_bd_unique_chosen_canonical_length_lower_product) + (pa_s_bl_bd_unique_chosen_canonical_length_lower_product))) /\ pa_s_bl_bd_unique_chosen_canonical_length_lower_product = pa_r_bl_bd_unique_chosen_canonical_length_lower_product * pa_p_bl_bd_unique_chosen_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_unique_chosen_canonical_length_upper pa_c_bl_bd_unique_chosen_canonical_length_upper. ((forall pa_i_bl_bd_unique_chosen_canonical_length_upper_repeat. (exists pa_lt_bl_bd_unique_chosen_canonical_length_upper_repeat_bound. pa_lt_bl_bd_unique_chosen_canonical_length_upper_repeat_bound + S pa_i_bl_bd_unique_chosen_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_unique_chosen_canonical_length_upper_repeat_decoded. pa_h_bl_bd_unique_chosen_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_unique_chosen_canonical_length_upper_repeat)) * pa_c_bl_bd_unique_chosen_canonical_length_upper)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_upper_repeat_decoded. pa_b_bl_bd_unique_chosen_canonical_length_upper = pa_q_bl_bd_unique_chosen_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_unique_chosen_canonical_length_upper_repeat)) * pa_c_bl_bd_unique_chosen_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_unique_chosen_canonical_length_upper_product pa_v_bl_bd_unique_chosen_canonical_length_upper_product. ((((exists pa_h_bl_bd_unique_chosen_canonical_length_upper_product_start. pa_h_bl_bd_unique_chosen_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_upper_product_start. pa_u_bl_bd_unique_chosen_canonical_length_upper_product = pa_q_bl_bd_unique_chosen_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_unique_chosen_canonical_length_upper_product_terminal. pa_h_bl_bd_unique_chosen_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_unique_chosen_canonical_length) = S ((S (l)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_upper_product_terminal. pa_u_bl_bd_unique_chosen_canonical_length_upper_product = pa_q_bl_bd_unique_chosen_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product) + (ff_upper_bl_bd_unique_chosen_canonical_length))) /\ forall pa_i_bl_bd_unique_chosen_canonical_length_upper_product. (exists pa_lt_bl_bd_unique_chosen_canonical_length_upper_product_bound. pa_lt_bl_bd_unique_chosen_canonical_length_upper_product_bound + S pa_i_bl_bd_unique_chosen_canonical_length_upper_product = l) -> exists pa_p_bl_bd_unique_chosen_canonical_length_upper_product pa_r_bl_bd_unique_chosen_canonical_length_upper_product pa_s_bl_bd_unique_chosen_canonical_length_upper_product. ((((exists pa_h_bl_bd_unique_chosen_canonical_length_upper_product_factor. pa_h_bl_bd_unique_chosen_canonical_length_upper_product_factor + S (pa_p_bl_bd_unique_chosen_canonical_length_upper_product) = S ((S (pa_i_bl_bd_unique_chosen_canonical_length_upper_product)) * pa_c_bl_bd_unique_chosen_canonical_length_upper)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_upper_product_factor. pa_b_bl_bd_unique_chosen_canonical_length_upper = pa_q_bl_bd_unique_chosen_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_unique_chosen_canonical_length_upper_product)) * pa_c_bl_bd_unique_chosen_canonical_length_upper) + (pa_p_bl_bd_unique_chosen_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_unique_chosen_canonical_length_upper_product_partial. pa_h_bl_bd_unique_chosen_canonical_length_upper_product_partial + S (pa_r_bl_bd_unique_chosen_canonical_length_upper_product) = S ((S (pa_i_bl_bd_unique_chosen_canonical_length_upper_product)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_upper_product_partial. pa_u_bl_bd_unique_chosen_canonical_length_upper_product = pa_q_bl_bd_unique_chosen_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_unique_chosen_canonical_length_upper_product)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product) + (pa_r_bl_bd_unique_chosen_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_unique_chosen_canonical_length_upper_product_successor. pa_h_bl_bd_unique_chosen_canonical_length_upper_product_successor + S (pa_s_bl_bd_unique_chosen_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_unique_chosen_canonical_length_upper_product)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_chosen_canonical_length_upper_product_successor. pa_u_bl_bd_unique_chosen_canonical_length_upper_product = pa_q_bl_bd_unique_chosen_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_unique_chosen_canonical_length_upper_product)) * pa_v_bl_bd_unique_chosen_canonical_length_upper_product) + (pa_s_bl_bd_unique_chosen_canonical_length_upper_product))) /\ pa_s_bl_bd_unique_chosen_canonical_length_upper_product = pa_r_bl_bd_unique_chosen_canonical_length_upper_product * pa_p_bl_bd_unique_chosen_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_unique_chosen_canonical_length. ff_lower_gap_bl_bd_unique_chosen_canonical_length + (ff_lower_bl_bd_unique_chosen_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_unique_chosen_canonical_length. ff_upper_gap_bl_bd_unique_chosen_canonical_length + S (n) = (ff_upper_bl_bd_unique_chosen_canonical_length))))))))) /\ (((forall ff_index_be_bd_unique_chosen_canonical_code_digits ff_digit_be_bd_unique_chosen_canonical_code_digits. (exists ff_lt_be_bd_unique_chosen_canonical_code_digits_bound. ff_lt_be_bd_unique_chosen_canonical_code_digits_bound + S ff_index_be_bd_unique_chosen_canonical_code_digits = l) -> (((exists ff_h_be_bd_unique_chosen_canonical_code_digits_digit. ff_h_be_bd_unique_chosen_canonical_code_digits_digit + S (ff_digit_be_bd_unique_chosen_canonical_code_digits) = S ((S (ff_index_be_bd_unique_chosen_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_unique_chosen_canonical_code_digits_digit. b = ff_q_be_bd_unique_chosen_canonical_code_digits_digit * S ((S (ff_index_be_bd_unique_chosen_canonical_code_digits)) * c) + (ff_digit_be_bd_unique_chosen_canonical_code_digits))) -> (ff_digit_be_bd_unique_chosen_canonical_code_digits = 0 \/ ff_digit_be_bd_unique_chosen_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_unique_chosen_canonical_code_horner ff_v_ph_bd_unique_chosen_canonical_code_horner. ((((exists fs_h_ph_bd_unique_chosen_canonical_code_horner_body_start. fs_h_ph_bd_unique_chosen_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_unique_chosen_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_chosen_canonical_code_horner_body_start. ff_u_ph_bd_unique_chosen_canonical_code_horner = fs_q_ph_bd_unique_chosen_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_unique_chosen_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_unique_chosen_canonical_code_horner_body_terminal. fs_h_ph_bd_unique_chosen_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_unique_chosen_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_chosen_canonical_code_horner_body_terminal. ff_u_ph_bd_unique_chosen_canonical_code_horner = fs_q_ph_bd_unique_chosen_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_unique_chosen_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps. (exists ph_bound_bd_unique_chosen_canonical_code_horner_body_steps. ph_bound_bd_unique_chosen_canonical_code_horner_body_steps + S ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_unique_chosen_canonical_code_horner_body_steps ff_previous_ph_bd_unique_chosen_canonical_code_horner_body_steps ff_current_ph_bd_unique_chosen_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_unique_chosen_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_unique_chosen_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_unique_chosen_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_unique_chosen_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_unique_chosen_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_unique_chosen_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_unique_chosen_canonical_code_horner_body_steps_before. fs_h_ph_bd_unique_chosen_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_unique_chosen_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_chosen_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_chosen_canonical_code_horner_body_steps_before. ff_u_ph_bd_unique_chosen_canonical_code_horner = fs_q_ph_bd_unique_chosen_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_chosen_canonical_code_horner) + (ff_previous_ph_bd_unique_chosen_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_unique_chosen_canonical_code_horner_body_steps_after. fs_h_ph_bd_unique_chosen_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_unique_chosen_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_chosen_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_chosen_canonical_code_horner_body_steps_after. ff_u_ph_bd_unique_chosen_canonical_code_horner = fs_q_ph_bd_unique_chosen_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_unique_chosen_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_chosen_canonical_code_horner) + (ff_current_ph_bd_unique_chosen_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_unique_chosen_canonical_code_horner_body_steps = ff_previous_ph_bd_unique_chosen_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_unique_chosen_canonical_code_horner_body_steps)))))))))) /\ ((exists ff_trace_code_be_bd_unique_chosen_execution ff_trace_scale_be_bd_unique_chosen_execution. ((((((exists ff_h_be_bd_unique_chosen_execution_trace_start. ff_h_be_bd_unique_chosen_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_bd_unique_chosen_execution)) /\ exists ff_q_be_bd_unique_chosen_execution_trace_start. ff_trace_code_be_bd_unique_chosen_execution = ff_q_be_bd_unique_chosen_execution_trace_start * S ((S (0)) * ff_trace_scale_be_bd_unique_chosen_execution) + (1))) /\ forall ff_index_be_bd_unique_chosen_execution_trace. (exists ff_lt_be_bd_unique_chosen_execution_trace_bound. ff_lt_be_bd_unique_chosen_execution_trace_bound + S ff_index_be_bd_unique_chosen_execution_trace = l) -> exists ff_digit_be_bd_unique_chosen_execution_trace ff_previous_be_bd_unique_chosen_execution_trace ff_current_be_bd_unique_chosen_execution_trace. ((((exists ff_h_be_bd_unique_chosen_execution_trace_source. ff_h_be_bd_unique_chosen_execution_trace_source + S (ff_digit_be_bd_unique_chosen_execution_trace) = S ((S (ff_index_be_bd_unique_chosen_execution_trace)) * c)) /\ exists ff_q_be_bd_unique_chosen_execution_trace_source. b = ff_q_be_bd_unique_chosen_execution_trace_source * S ((S (ff_index_be_bd_unique_chosen_execution_trace)) * c) + (ff_digit_be_bd_unique_chosen_execution_trace))) /\ ((((exists ff_h_be_bd_unique_chosen_execution_trace_before. ff_h_be_bd_unique_chosen_execution_trace_before + S (ff_previous_be_bd_unique_chosen_execution_trace) = S ((S (ff_index_be_bd_unique_chosen_execution_trace)) * ff_trace_scale_be_bd_unique_chosen_execution)) /\ exists ff_q_be_bd_unique_chosen_execution_trace_before. ff_trace_code_be_bd_unique_chosen_execution = ff_q_be_bd_unique_chosen_execution_trace_before * S ((S (ff_index_be_bd_unique_chosen_execution_trace)) * ff_trace_scale_be_bd_unique_chosen_execution) + (ff_previous_be_bd_unique_chosen_execution_trace))) /\ ((((exists ff_h_be_bd_unique_chosen_execution_trace_after. ff_h_be_bd_unique_chosen_execution_trace_after + S (ff_current_be_bd_unique_chosen_execution_trace) = S ((S (S ff_index_be_bd_unique_chosen_execution_trace)) * ff_trace_scale_be_bd_unique_chosen_execution)) /\ exists ff_q_be_bd_unique_chosen_execution_trace_after. ff_trace_code_be_bd_unique_chosen_execution = ff_q_be_bd_unique_chosen_execution_trace_after * S ((S (S ff_index_be_bd_unique_chosen_execution_trace)) * ff_trace_scale_be_bd_unique_chosen_execution) + (ff_current_be_bd_unique_chosen_execution_trace))) /\ ((((ff_digit_be_bd_unique_chosen_execution_trace = 0) /\ (((exists ff_gap_binary_be_bd_unique_chosen_execution_trace_transition_square. ff_gap_binary_be_bd_unique_chosen_execution_trace_transition_square + S (ff_current_be_bd_unique_chosen_execution_trace) = m) /\ (exists ff_left_binary_be_bd_unique_chosen_execution_trace_transition_square_congruence ff_right_binary_be_bd_unique_chosen_execution_trace_transition_square_congruence. (ff_previous_be_bd_unique_chosen_execution_trace * ff_previous_be_bd_unique_chosen_execution_trace) + m * ff_left_binary_be_bd_unique_chosen_execution_trace_transition_square_congruence = (ff_current_be_bd_unique_chosen_execution_trace) + m * ff_right_binary_be_bd_unique_chosen_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_bd_unique_chosen_execution_trace = 1) /\ (((exists ff_gap_binary_be_bd_unique_chosen_execution_trace_transition_multiply. ff_gap_binary_be_bd_unique_chosen_execution_trace_transition_multiply + S (ff_current_be_bd_unique_chosen_execution_trace) = m) /\ (exists ff_left_binary_be_bd_unique_chosen_execution_trace_transition_multiply_congruence ff_right_binary_be_bd_unique_chosen_execution_trace_transition_multiply_congruence. ((ff_previous_be_bd_unique_chosen_execution_trace * ff_previous_be_bd_unique_chosen_execution_trace) * a) + m * ff_left_binary_be_bd_unique_chosen_execution_trace_transition_multiply_congruence = (ff_current_be_bd_unique_chosen_execution_trace) + m * ff_right_binary_be_bd_unique_chosen_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_bd_unique_chosen_execution_terminal. ff_h_be_bd_unique_chosen_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_bd_unique_chosen_execution)) /\ exists ff_q_be_bd_unique_chosen_execution_terminal. ff_trace_code_be_bd_unique_chosen_execution = ff_q_be_bd_unique_chosen_execution_terminal * S ((S (l)) * ff_trace_scale_be_bd_unique_chosen_execution) + (r))))) /\ (exists ff_power_binary_bd_unique_chosen_power. ((exists ff_b_binary_bd_unique_chosen_power_value ff_c_binary_bd_unique_chosen_power_value. ((forall ff_i_binary_bd_unique_chosen_power_value_repeat. (exists ff_lt_binary_bd_unique_chosen_power_value_repeat_bound. ff_lt_binary_bd_unique_chosen_power_value_repeat_bound + S ff_i_binary_bd_unique_chosen_power_value_repeat = n) -> (((exists ff_h_binary_bd_unique_chosen_power_value_repeat_decoded. ff_h_binary_bd_unique_chosen_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_bd_unique_chosen_power_value_repeat)) * ff_c_binary_bd_unique_chosen_power_value)) /\ exists ff_q_binary_bd_unique_chosen_power_value_repeat_decoded. ff_b_binary_bd_unique_chosen_power_value = ff_q_binary_bd_unique_chosen_power_value_repeat_decoded * S ((S (ff_i_binary_bd_unique_chosen_power_value_repeat)) * ff_c_binary_bd_unique_chosen_power_value) + (a)))) /\ (exists ff_u_binary_bd_unique_chosen_power_value_product ff_v_binary_bd_unique_chosen_power_value_product. ((((exists ff_h_binary_bd_unique_chosen_power_value_product_start. ff_h_binary_bd_unique_chosen_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_bd_unique_chosen_power_value_product)) /\ exists ff_q_binary_bd_unique_chosen_power_value_product_start. ff_u_binary_bd_unique_chosen_power_value_product = ff_q_binary_bd_unique_chosen_power_value_product_start * S ((S (0)) * ff_v_binary_bd_unique_chosen_power_value_product) + (1))) /\ ((((exists ff_h_binary_bd_unique_chosen_power_value_product_terminal. ff_h_binary_bd_unique_chosen_power_value_product_terminal + S (ff_power_binary_bd_unique_chosen_power) = S ((S (n)) * ff_v_binary_bd_unique_chosen_power_value_product)) /\ exists ff_q_binary_bd_unique_chosen_power_value_product_terminal. ff_u_binary_bd_unique_chosen_power_value_product = ff_q_binary_bd_unique_chosen_power_value_product_terminal * S ((S (n)) * ff_v_binary_bd_unique_chosen_power_value_product) + (ff_power_binary_bd_unique_chosen_power))) /\ forall ff_i_binary_bd_unique_chosen_power_value_product. (exists ff_lt_binary_bd_unique_chosen_power_value_product_bound. ff_lt_binary_bd_unique_chosen_power_value_product_bound + S ff_i_binary_bd_unique_chosen_power_value_product = n) -> exists ff_p_binary_bd_unique_chosen_power_value_product ff_r_binary_bd_unique_chosen_power_value_product ff_s_binary_bd_unique_chosen_power_value_product. ((((exists ff_h_binary_bd_unique_chosen_power_value_product_factor. ff_h_binary_bd_unique_chosen_power_value_product_factor + S (ff_p_binary_bd_unique_chosen_power_value_product) = S ((S (ff_i_binary_bd_unique_chosen_power_value_product)) * ff_c_binary_bd_unique_chosen_power_value)) /\ exists ff_q_binary_bd_unique_chosen_power_value_product_factor. ff_b_binary_bd_unique_chosen_power_value = ff_q_binary_bd_unique_chosen_power_value_product_factor * S ((S (ff_i_binary_bd_unique_chosen_power_value_product)) * ff_c_binary_bd_unique_chosen_power_value) + (ff_p_binary_bd_unique_chosen_power_value_product))) /\ ((((exists ff_h_binary_bd_unique_chosen_power_value_product_partial. ff_h_binary_bd_unique_chosen_power_value_product_partial + S (ff_r_binary_bd_unique_chosen_power_value_product) = S ((S (ff_i_binary_bd_unique_chosen_power_value_product)) * ff_v_binary_bd_unique_chosen_power_value_product)) /\ exists ff_q_binary_bd_unique_chosen_power_value_product_partial. ff_u_binary_bd_unique_chosen_power_value_product = ff_q_binary_bd_unique_chosen_power_value_product_partial * S ((S (ff_i_binary_bd_unique_chosen_power_value_product)) * ff_v_binary_bd_unique_chosen_power_value_product) + (ff_r_binary_bd_unique_chosen_power_value_product))) /\ ((((exists ff_h_binary_bd_unique_chosen_power_value_product_successor. ff_h_binary_bd_unique_chosen_power_value_product_successor + S (ff_s_binary_bd_unique_chosen_power_value_product) = S ((S (S ff_i_binary_bd_unique_chosen_power_value_product)) * ff_v_binary_bd_unique_chosen_power_value_product)) /\ exists ff_q_binary_bd_unique_chosen_power_value_product_successor. ff_u_binary_bd_unique_chosen_power_value_product = ff_q_binary_bd_unique_chosen_power_value_product_successor * S ((S (S ff_i_binary_bd_unique_chosen_power_value_product)) * ff_v_binary_bd_unique_chosen_power_value_product) + (ff_s_binary_bd_unique_chosen_power_value_product))) /\ ff_s_binary_bd_unique_chosen_power_value_product = ff_r_binary_bd_unique_chosen_power_value_product * ff_p_binary_bd_unique_chosen_power_value_product)))))))) /\ (((exists ff_gap_binary_bd_unique_chosen_power_residue. ff_gap_binary_bd_unique_chosen_power_residue + S (r) = m) /\ (exists ff_left_binary_bd_unique_chosen_power_residue_congruence ff_right_binary_bd_unique_chosen_power_residue_congruence. (ff_power_binary_bd_unique_chosen_power) + m * ff_left_binary_bd_unique_chosen_power_residue_congruence = (r) + m * ff_right_binary_bd_unique_chosen_power_residue_congruence))))))))) /\ forall s. (exists L B C. ((((((((n) = 0 /\ (L) = 1) \/ exists ff_exponent_bl_bd_unique_other_canonical_length ff_lower_bl_bd_unique_other_canonical_length ff_upper_bl_bd_unique_other_canonical_length. (((L) = S ff_exponent_bl_bd_unique_other_canonical_length) /\ ((exists ff_positive_bl_bd_unique_other_canonical_length. ff_positive_bl_bd_unique_other_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_unique_other_canonical_length_lower pa_c_bl_bd_unique_other_canonical_length_lower. ((forall pa_i_bl_bd_unique_other_canonical_length_lower_repeat. (exists pa_lt_bl_bd_unique_other_canonical_length_lower_repeat_bound. pa_lt_bl_bd_unique_other_canonical_length_lower_repeat_bound + S pa_i_bl_bd_unique_other_canonical_length_lower_repeat = ff_exponent_bl_bd_unique_other_canonical_length) -> (((exists pa_h_bl_bd_unique_other_canonical_length_lower_repeat_decoded. pa_h_bl_bd_unique_other_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_unique_other_canonical_length_lower_repeat)) * pa_c_bl_bd_unique_other_canonical_length_lower)) /\ exists pa_q_bl_bd_unique_other_canonical_length_lower_repeat_decoded. pa_b_bl_bd_unique_other_canonical_length_lower = pa_q_bl_bd_unique_other_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_unique_other_canonical_length_lower_repeat)) * pa_c_bl_bd_unique_other_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_unique_other_canonical_length_lower_product pa_v_bl_bd_unique_other_canonical_length_lower_product. ((((exists pa_h_bl_bd_unique_other_canonical_length_lower_product_start. pa_h_bl_bd_unique_other_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_unique_other_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_lower_product_start. pa_u_bl_bd_unique_other_canonical_length_lower_product = pa_q_bl_bd_unique_other_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_unique_other_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_unique_other_canonical_length_lower_product_terminal. pa_h_bl_bd_unique_other_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_unique_other_canonical_length) = S ((S (ff_exponent_bl_bd_unique_other_canonical_length)) * pa_v_bl_bd_unique_other_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_lower_product_terminal. pa_u_bl_bd_unique_other_canonical_length_lower_product = pa_q_bl_bd_unique_other_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_unique_other_canonical_length)) * pa_v_bl_bd_unique_other_canonical_length_lower_product) + (ff_lower_bl_bd_unique_other_canonical_length))) /\ forall pa_i_bl_bd_unique_other_canonical_length_lower_product. (exists pa_lt_bl_bd_unique_other_canonical_length_lower_product_bound. pa_lt_bl_bd_unique_other_canonical_length_lower_product_bound + S pa_i_bl_bd_unique_other_canonical_length_lower_product = ff_exponent_bl_bd_unique_other_canonical_length) -> exists pa_p_bl_bd_unique_other_canonical_length_lower_product pa_r_bl_bd_unique_other_canonical_length_lower_product pa_s_bl_bd_unique_other_canonical_length_lower_product. ((((exists pa_h_bl_bd_unique_other_canonical_length_lower_product_factor. pa_h_bl_bd_unique_other_canonical_length_lower_product_factor + S (pa_p_bl_bd_unique_other_canonical_length_lower_product) = S ((S (pa_i_bl_bd_unique_other_canonical_length_lower_product)) * pa_c_bl_bd_unique_other_canonical_length_lower)) /\ exists pa_q_bl_bd_unique_other_canonical_length_lower_product_factor. pa_b_bl_bd_unique_other_canonical_length_lower = pa_q_bl_bd_unique_other_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_unique_other_canonical_length_lower_product)) * pa_c_bl_bd_unique_other_canonical_length_lower) + (pa_p_bl_bd_unique_other_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_unique_other_canonical_length_lower_product_partial. pa_h_bl_bd_unique_other_canonical_length_lower_product_partial + S (pa_r_bl_bd_unique_other_canonical_length_lower_product) = S ((S (pa_i_bl_bd_unique_other_canonical_length_lower_product)) * pa_v_bl_bd_unique_other_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_lower_product_partial. pa_u_bl_bd_unique_other_canonical_length_lower_product = pa_q_bl_bd_unique_other_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_unique_other_canonical_length_lower_product)) * pa_v_bl_bd_unique_other_canonical_length_lower_product) + (pa_r_bl_bd_unique_other_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_unique_other_canonical_length_lower_product_successor. pa_h_bl_bd_unique_other_canonical_length_lower_product_successor + S (pa_s_bl_bd_unique_other_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_unique_other_canonical_length_lower_product)) * pa_v_bl_bd_unique_other_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_lower_product_successor. pa_u_bl_bd_unique_other_canonical_length_lower_product = pa_q_bl_bd_unique_other_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_unique_other_canonical_length_lower_product)) * pa_v_bl_bd_unique_other_canonical_length_lower_product) + (pa_s_bl_bd_unique_other_canonical_length_lower_product))) /\ pa_s_bl_bd_unique_other_canonical_length_lower_product = pa_r_bl_bd_unique_other_canonical_length_lower_product * pa_p_bl_bd_unique_other_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_unique_other_canonical_length_upper pa_c_bl_bd_unique_other_canonical_length_upper. ((forall pa_i_bl_bd_unique_other_canonical_length_upper_repeat. (exists pa_lt_bl_bd_unique_other_canonical_length_upper_repeat_bound. pa_lt_bl_bd_unique_other_canonical_length_upper_repeat_bound + S pa_i_bl_bd_unique_other_canonical_length_upper_repeat = L) -> (((exists pa_h_bl_bd_unique_other_canonical_length_upper_repeat_decoded. pa_h_bl_bd_unique_other_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_unique_other_canonical_length_upper_repeat)) * pa_c_bl_bd_unique_other_canonical_length_upper)) /\ exists pa_q_bl_bd_unique_other_canonical_length_upper_repeat_decoded. pa_b_bl_bd_unique_other_canonical_length_upper = pa_q_bl_bd_unique_other_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_unique_other_canonical_length_upper_repeat)) * pa_c_bl_bd_unique_other_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_unique_other_canonical_length_upper_product pa_v_bl_bd_unique_other_canonical_length_upper_product. ((((exists pa_h_bl_bd_unique_other_canonical_length_upper_product_start. pa_h_bl_bd_unique_other_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_unique_other_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_upper_product_start. pa_u_bl_bd_unique_other_canonical_length_upper_product = pa_q_bl_bd_unique_other_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_unique_other_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_unique_other_canonical_length_upper_product_terminal. pa_h_bl_bd_unique_other_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_unique_other_canonical_length) = S ((S (L)) * pa_v_bl_bd_unique_other_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_upper_product_terminal. pa_u_bl_bd_unique_other_canonical_length_upper_product = pa_q_bl_bd_unique_other_canonical_length_upper_product_terminal * S ((S (L)) * pa_v_bl_bd_unique_other_canonical_length_upper_product) + (ff_upper_bl_bd_unique_other_canonical_length))) /\ forall pa_i_bl_bd_unique_other_canonical_length_upper_product. (exists pa_lt_bl_bd_unique_other_canonical_length_upper_product_bound. pa_lt_bl_bd_unique_other_canonical_length_upper_product_bound + S pa_i_bl_bd_unique_other_canonical_length_upper_product = L) -> exists pa_p_bl_bd_unique_other_canonical_length_upper_product pa_r_bl_bd_unique_other_canonical_length_upper_product pa_s_bl_bd_unique_other_canonical_length_upper_product. ((((exists pa_h_bl_bd_unique_other_canonical_length_upper_product_factor. pa_h_bl_bd_unique_other_canonical_length_upper_product_factor + S (pa_p_bl_bd_unique_other_canonical_length_upper_product) = S ((S (pa_i_bl_bd_unique_other_canonical_length_upper_product)) * pa_c_bl_bd_unique_other_canonical_length_upper)) /\ exists pa_q_bl_bd_unique_other_canonical_length_upper_product_factor. pa_b_bl_bd_unique_other_canonical_length_upper = pa_q_bl_bd_unique_other_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_unique_other_canonical_length_upper_product)) * pa_c_bl_bd_unique_other_canonical_length_upper) + (pa_p_bl_bd_unique_other_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_unique_other_canonical_length_upper_product_partial. pa_h_bl_bd_unique_other_canonical_length_upper_product_partial + S (pa_r_bl_bd_unique_other_canonical_length_upper_product) = S ((S (pa_i_bl_bd_unique_other_canonical_length_upper_product)) * pa_v_bl_bd_unique_other_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_upper_product_partial. pa_u_bl_bd_unique_other_canonical_length_upper_product = pa_q_bl_bd_unique_other_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_unique_other_canonical_length_upper_product)) * pa_v_bl_bd_unique_other_canonical_length_upper_product) + (pa_r_bl_bd_unique_other_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_unique_other_canonical_length_upper_product_successor. pa_h_bl_bd_unique_other_canonical_length_upper_product_successor + S (pa_s_bl_bd_unique_other_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_unique_other_canonical_length_upper_product)) * pa_v_bl_bd_unique_other_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_other_canonical_length_upper_product_successor. pa_u_bl_bd_unique_other_canonical_length_upper_product = pa_q_bl_bd_unique_other_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_unique_other_canonical_length_upper_product)) * pa_v_bl_bd_unique_other_canonical_length_upper_product) + (pa_s_bl_bd_unique_other_canonical_length_upper_product))) /\ pa_s_bl_bd_unique_other_canonical_length_upper_product = pa_r_bl_bd_unique_other_canonical_length_upper_product * pa_p_bl_bd_unique_other_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_unique_other_canonical_length. ff_lower_gap_bl_bd_unique_other_canonical_length + (ff_lower_bl_bd_unique_other_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_unique_other_canonical_length. ff_upper_gap_bl_bd_unique_other_canonical_length + S (n) = (ff_upper_bl_bd_unique_other_canonical_length))))))))) /\ (((forall ff_index_be_bd_unique_other_canonical_code_digits ff_digit_be_bd_unique_other_canonical_code_digits. (exists ff_lt_be_bd_unique_other_canonical_code_digits_bound. ff_lt_be_bd_unique_other_canonical_code_digits_bound + S ff_index_be_bd_unique_other_canonical_code_digits = L) -> (((exists ff_h_be_bd_unique_other_canonical_code_digits_digit. ff_h_be_bd_unique_other_canonical_code_digits_digit + S (ff_digit_be_bd_unique_other_canonical_code_digits) = S ((S (ff_index_be_bd_unique_other_canonical_code_digits)) * C)) /\ exists ff_q_be_bd_unique_other_canonical_code_digits_digit. B = ff_q_be_bd_unique_other_canonical_code_digits_digit * S ((S (ff_index_be_bd_unique_other_canonical_code_digits)) * C) + (ff_digit_be_bd_unique_other_canonical_code_digits))) -> (ff_digit_be_bd_unique_other_canonical_code_digits = 0 \/ ff_digit_be_bd_unique_other_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_unique_other_canonical_code_horner ff_v_ph_bd_unique_other_canonical_code_horner. ((((exists fs_h_ph_bd_unique_other_canonical_code_horner_body_start. fs_h_ph_bd_unique_other_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_unique_other_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_other_canonical_code_horner_body_start. ff_u_ph_bd_unique_other_canonical_code_horner = fs_q_ph_bd_unique_other_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_unique_other_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_unique_other_canonical_code_horner_body_terminal. fs_h_ph_bd_unique_other_canonical_code_horner_body_terminal + S (n) = S ((S (L)) * ff_v_ph_bd_unique_other_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_other_canonical_code_horner_body_terminal. ff_u_ph_bd_unique_other_canonical_code_horner = fs_q_ph_bd_unique_other_canonical_code_horner_body_terminal * S ((S (L)) * ff_v_ph_bd_unique_other_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_unique_other_canonical_code_horner_body_steps. (exists ph_bound_bd_unique_other_canonical_code_horner_body_steps. ph_bound_bd_unique_other_canonical_code_horner_body_steps + S ff_i_ph_bd_unique_other_canonical_code_horner_body_steps = L) -> exists ff_coefficient_ph_bd_unique_other_canonical_code_horner_body_steps ff_previous_ph_bd_unique_other_canonical_code_horner_body_steps ff_current_ph_bd_unique_other_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_unique_other_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_unique_other_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_unique_other_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_unique_other_canonical_code_horner_body_steps)) * C)) /\ exists fs_q_ph_bd_unique_other_canonical_code_horner_body_steps_coefficient. B = fs_q_ph_bd_unique_other_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_unique_other_canonical_code_horner_body_steps)) * C) + (ff_coefficient_ph_bd_unique_other_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_unique_other_canonical_code_horner_body_steps_before. fs_h_ph_bd_unique_other_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_unique_other_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_unique_other_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_other_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_other_canonical_code_horner_body_steps_before. ff_u_ph_bd_unique_other_canonical_code_horner = fs_q_ph_bd_unique_other_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_unique_other_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_other_canonical_code_horner) + (ff_previous_ph_bd_unique_other_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_unique_other_canonical_code_horner_body_steps_after. fs_h_ph_bd_unique_other_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_unique_other_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_unique_other_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_other_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_other_canonical_code_horner_body_steps_after. ff_u_ph_bd_unique_other_canonical_code_horner = fs_q_ph_bd_unique_other_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_unique_other_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_other_canonical_code_horner) + (ff_current_ph_bd_unique_other_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_unique_other_canonical_code_horner_body_steps = ff_previous_ph_bd_unique_other_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_unique_other_canonical_code_horner_body_steps)))))))))) /\ ((exists ff_trace_code_be_bd_unique_other_execution ff_trace_scale_be_bd_unique_other_execution. ((((((exists ff_h_be_bd_unique_other_execution_trace_start. ff_h_be_bd_unique_other_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_bd_unique_other_execution)) /\ exists ff_q_be_bd_unique_other_execution_trace_start. ff_trace_code_be_bd_unique_other_execution = ff_q_be_bd_unique_other_execution_trace_start * S ((S (0)) * ff_trace_scale_be_bd_unique_other_execution) + (1))) /\ forall ff_index_be_bd_unique_other_execution_trace. (exists ff_lt_be_bd_unique_other_execution_trace_bound. ff_lt_be_bd_unique_other_execution_trace_bound + S ff_index_be_bd_unique_other_execution_trace = L) -> exists ff_digit_be_bd_unique_other_execution_trace ff_previous_be_bd_unique_other_execution_trace ff_current_be_bd_unique_other_execution_trace. ((((exists ff_h_be_bd_unique_other_execution_trace_source. ff_h_be_bd_unique_other_execution_trace_source + S (ff_digit_be_bd_unique_other_execution_trace) = S ((S (ff_index_be_bd_unique_other_execution_trace)) * C)) /\ exists ff_q_be_bd_unique_other_execution_trace_source. B = ff_q_be_bd_unique_other_execution_trace_source * S ((S (ff_index_be_bd_unique_other_execution_trace)) * C) + (ff_digit_be_bd_unique_other_execution_trace))) /\ ((((exists ff_h_be_bd_unique_other_execution_trace_before. ff_h_be_bd_unique_other_execution_trace_before + S (ff_previous_be_bd_unique_other_execution_trace) = S ((S (ff_index_be_bd_unique_other_execution_trace)) * ff_trace_scale_be_bd_unique_other_execution)) /\ exists ff_q_be_bd_unique_other_execution_trace_before. ff_trace_code_be_bd_unique_other_execution = ff_q_be_bd_unique_other_execution_trace_before * S ((S (ff_index_be_bd_unique_other_execution_trace)) * ff_trace_scale_be_bd_unique_other_execution) + (ff_previous_be_bd_unique_other_execution_trace))) /\ ((((exists ff_h_be_bd_unique_other_execution_trace_after. ff_h_be_bd_unique_other_execution_trace_after + S (ff_current_be_bd_unique_other_execution_trace) = S ((S (S ff_index_be_bd_unique_other_execution_trace)) * ff_trace_scale_be_bd_unique_other_execution)) /\ exists ff_q_be_bd_unique_other_execution_trace_after. ff_trace_code_be_bd_unique_other_execution = ff_q_be_bd_unique_other_execution_trace_after * S ((S (S ff_index_be_bd_unique_other_execution_trace)) * ff_trace_scale_be_bd_unique_other_execution) + (ff_current_be_bd_unique_other_execution_trace))) /\ ((((ff_digit_be_bd_unique_other_execution_trace = 0) /\ (((exists ff_gap_binary_be_bd_unique_other_execution_trace_transition_square. ff_gap_binary_be_bd_unique_other_execution_trace_transition_square + S (ff_current_be_bd_unique_other_execution_trace) = m) /\ (exists ff_left_binary_be_bd_unique_other_execution_trace_transition_square_congruence ff_right_binary_be_bd_unique_other_execution_trace_transition_square_congruence. (ff_previous_be_bd_unique_other_execution_trace * ff_previous_be_bd_unique_other_execution_trace) + m * ff_left_binary_be_bd_unique_other_execution_trace_transition_square_congruence = (ff_current_be_bd_unique_other_execution_trace) + m * ff_right_binary_be_bd_unique_other_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_bd_unique_other_execution_trace = 1) /\ (((exists ff_gap_binary_be_bd_unique_other_execution_trace_transition_multiply. ff_gap_binary_be_bd_unique_other_execution_trace_transition_multiply + S (ff_current_be_bd_unique_other_execution_trace) = m) /\ (exists ff_left_binary_be_bd_unique_other_execution_trace_transition_multiply_congruence ff_right_binary_be_bd_unique_other_execution_trace_transition_multiply_congruence. ((ff_previous_be_bd_unique_other_execution_trace * ff_previous_be_bd_unique_other_execution_trace) * a) + m * ff_left_binary_be_bd_unique_other_execution_trace_transition_multiply_congruence = (ff_current_be_bd_unique_other_execution_trace) + m * ff_right_binary_be_bd_unique_other_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_bd_unique_other_execution_terminal. ff_h_be_bd_unique_other_execution_terminal + S (s) = S ((S (L)) * ff_trace_scale_be_bd_unique_other_execution)) /\ exists ff_q_be_bd_unique_other_execution_terminal. ff_trace_code_be_bd_unique_other_execution = ff_q_be_bd_unique_other_execution_terminal * S ((S (L)) * ff_trace_scale_be_bd_unique_other_execution) + (s))))) /\ (exists ff_power_binary_bd_unique_other_power. ((exists ff_b_binary_bd_unique_other_power_value ff_c_binary_bd_unique_other_power_value. ((forall ff_i_binary_bd_unique_other_power_value_repeat. (exists ff_lt_binary_bd_unique_other_power_value_repeat_bound. ff_lt_binary_bd_unique_other_power_value_repeat_bound + S ff_i_binary_bd_unique_other_power_value_repeat = n) -> (((exists ff_h_binary_bd_unique_other_power_value_repeat_decoded. ff_h_binary_bd_unique_other_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_bd_unique_other_power_value_repeat)) * ff_c_binary_bd_unique_other_power_value)) /\ exists ff_q_binary_bd_unique_other_power_value_repeat_decoded. ff_b_binary_bd_unique_other_power_value = ff_q_binary_bd_unique_other_power_value_repeat_decoded * S ((S (ff_i_binary_bd_unique_other_power_value_repeat)) * ff_c_binary_bd_unique_other_power_value) + (a)))) /\ (exists ff_u_binary_bd_unique_other_power_value_product ff_v_binary_bd_unique_other_power_value_product. ((((exists ff_h_binary_bd_unique_other_power_value_product_start. ff_h_binary_bd_unique_other_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_bd_unique_other_power_value_product)) /\ exists ff_q_binary_bd_unique_other_power_value_product_start. ff_u_binary_bd_unique_other_power_value_product = ff_q_binary_bd_unique_other_power_value_product_start * S ((S (0)) * ff_v_binary_bd_unique_other_power_value_product) + (1))) /\ ((((exists ff_h_binary_bd_unique_other_power_value_product_terminal. ff_h_binary_bd_unique_other_power_value_product_terminal + S (ff_power_binary_bd_unique_other_power) = S ((S (n)) * ff_v_binary_bd_unique_other_power_value_product)) /\ exists ff_q_binary_bd_unique_other_power_value_product_terminal. ff_u_binary_bd_unique_other_power_value_product = ff_q_binary_bd_unique_other_power_value_product_terminal * S ((S (n)) * ff_v_binary_bd_unique_other_power_value_product) + (ff_power_binary_bd_unique_other_power))) /\ forall ff_i_binary_bd_unique_other_power_value_product. (exists ff_lt_binary_bd_unique_other_power_value_product_bound. ff_lt_binary_bd_unique_other_power_value_product_bound + S ff_i_binary_bd_unique_other_power_value_product = n) -> exists ff_p_binary_bd_unique_other_power_value_product ff_r_binary_bd_unique_other_power_value_product ff_s_binary_bd_unique_other_power_value_product. ((((exists ff_h_binary_bd_unique_other_power_value_product_factor. ff_h_binary_bd_unique_other_power_value_product_factor + S (ff_p_binary_bd_unique_other_power_value_product) = S ((S (ff_i_binary_bd_unique_other_power_value_product)) * ff_c_binary_bd_unique_other_power_value)) /\ exists ff_q_binary_bd_unique_other_power_value_product_factor. ff_b_binary_bd_unique_other_power_value = ff_q_binary_bd_unique_other_power_value_product_factor * S ((S (ff_i_binary_bd_unique_other_power_value_product)) * ff_c_binary_bd_unique_other_power_value) + (ff_p_binary_bd_unique_other_power_value_product))) /\ ((((exists ff_h_binary_bd_unique_other_power_value_product_partial. ff_h_binary_bd_unique_other_power_value_product_partial + S (ff_r_binary_bd_unique_other_power_value_product) = S ((S (ff_i_binary_bd_unique_other_power_value_product)) * ff_v_binary_bd_unique_other_power_value_product)) /\ exists ff_q_binary_bd_unique_other_power_value_product_partial. ff_u_binary_bd_unique_other_power_value_product = ff_q_binary_bd_unique_other_power_value_product_partial * S ((S (ff_i_binary_bd_unique_other_power_value_product)) * ff_v_binary_bd_unique_other_power_value_product) + (ff_r_binary_bd_unique_other_power_value_product))) /\ ((((exists ff_h_binary_bd_unique_other_power_value_product_successor. ff_h_binary_bd_unique_other_power_value_product_successor + S (ff_s_binary_bd_unique_other_power_value_product) = S ((S (S ff_i_binary_bd_unique_other_power_value_product)) * ff_v_binary_bd_unique_other_power_value_product)) /\ exists ff_q_binary_bd_unique_other_power_value_product_successor. ff_u_binary_bd_unique_other_power_value_product = ff_q_binary_bd_unique_other_power_value_product_successor * S ((S (S ff_i_binary_bd_unique_other_power_value_product)) * ff_v_binary_bd_unique_other_power_value_product) + (ff_s_binary_bd_unique_other_power_value_product))) /\ ff_s_binary_bd_unique_other_power_value_product = ff_r_binary_bd_unique_other_power_value_product * ff_p_binary_bd_unique_other_power_value_product)))))))) /\ (((exists ff_gap_binary_bd_unique_other_power_residue. ff_gap_binary_bd_unique_other_power_residue + S (s) = m) /\ (exists ff_left_binary_bd_unique_other_power_residue_congruence ff_right_binary_bd_unique_other_power_residue_congruence. (ff_power_binary_bd_unique_other_power) + m * ff_left_binary_bd_unique_other_power_residue_congruence = (s) + m * ff_right_binary_bd_unique_other_power_residue_congruence))))))))) -> r = s)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

40 script commands · 11 reading checkpoints · 1 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.

Named ingredients (2)
binary modular exponent coded execution existsbinary modular exponent coded execution result functional

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

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary modular exponent coded execution exists.

  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
04Construct an explicit witnessL15–15

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

  1. L15
    exists x3
05Separate the logical casesL16–16

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

  1. L16
    split
06Construct an explicit witnessL17–19

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

  1. L17
    exists x
  2. L18
    exists x1
  3. L19
    exists x2
07Use earlier factsL20–20

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

  1. L20
    exact hfull_witness_witness_witness_witness
08Fix variables and assumptionsL21–22

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

  1. L21
    intro s
  2. L22
    intro hother
09Separate the logical casesL23–25

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

  1. L23
    cases hother
  2. L24
    cases hother_witness
  3. L25
    cases hother_witness_witness
10Use earlier factsL26–35

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

  1. L26
    specialize binary_modular_exponent_coded_execution_result_functional n
  2. L27
    specialize binary_modular_exponent_coded_execution_result_functional a
  3. L28
    specialize binary_modular_exponent_coded_execution_result_functional m
  4. L29
    specialize binary_modular_exponent_coded_execution_result_functional x
  5. L30
    specialize binary_modular_exponent_coded_execution_result_functional x1
  6. L31
    specialize binary_modular_exponent_coded_execution_result_functional x2
  7. L32
    specialize binary_modular_exponent_coded_execution_result_functional x3
  8. L33
    specialize binary_modular_exponent_coded_execution_result_functional x4
  9. L34
    specialize binary_modular_exponent_coded_execution_result_functional x5
  10. L35
    specialize binary_modular_exponent_coded_execution_result_functional x6
11Use earlier factsL36–40

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

  1. L36
    specialize binary_modular_exponent_coded_execution_result_functional s
  2. L37
    apply binary_modular_exponent_coded_execution_result_functional
  3. L38
    exact hmodulus
  4. L39
    exact hfull_witness_witness_witness_witness
  5. L40
    exact hother_witness_witness_witness

Library-wide reading audit

Original defined command ledger · 40 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_unique_source_canonical_length ff_lower_bl_bd_unique_source_canonical_length ff_upper_bl_bd_unique_source_canonical_length. (((l) = S ff_exponent_bl_bd_unique_source_canonical_length) /\ ((exists ff_positive_bl_bd_unique_source_canonical_length. ff_positive_bl_bd_unique_source_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_unique_source_canonical_length_lower pa_c_bl_bd_unique_source_canonical_length_lower. ((forall pa_i_bl_bd_unique_source_canonical_length_lower_repeat. (exists pa_lt_bl_bd_unique_source_canonical_length_lower_repeat_bound. pa_lt_bl_bd_unique_source_canonical_length_lower_repeat_bound + S pa_i_bl_bd_unique_source_canonical_length_lower_repeat = ff_exponent_bl_bd_unique_source_canonical_length) -> (((exists pa_h_bl_bd_unique_source_canonical_length_lower_repeat_decoded. pa_h_bl_bd_unique_source_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_unique_source_canonical_length_lower_repeat)) * pa_c_bl_bd_unique_source_canonical_length_lower)) /\ exists pa_q_bl_bd_unique_source_canonical_length_lower_repeat_decoded. pa_b_bl_bd_unique_source_canonical_length_lower = pa_q_bl_bd_unique_source_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_unique_source_canonical_length_lower_repeat)) * pa_c_bl_bd_unique_source_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_unique_source_canonical_length_lower_product pa_v_bl_bd_unique_source_canonical_length_lower_product. ((((exists pa_h_bl_bd_unique_source_canonical_length_lower_product_start. pa_h_bl_bd_unique_source_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_unique_source_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_lower_product_start. pa_u_bl_bd_unique_source_canonical_length_lower_product = pa_q_bl_bd_unique_source_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_unique_source_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_unique_source_canonical_length_lower_product_terminal. pa_h_bl_bd_unique_source_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_unique_source_canonical_length) = S ((S (ff_exponent_bl_bd_unique_source_canonical_length)) * pa_v_bl_bd_unique_source_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_lower_product_terminal. pa_u_bl_bd_unique_source_canonical_length_lower_product = pa_q_bl_bd_unique_source_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_unique_source_canonical_length)) * pa_v_bl_bd_unique_source_canonical_length_lower_product) + (ff_lower_bl_bd_unique_source_canonical_length))) /\ forall pa_i_bl_bd_unique_source_canonical_length_lower_product. (exists pa_lt_bl_bd_unique_source_canonical_length_lower_product_bound. pa_lt_bl_bd_unique_source_canonical_length_lower_product_bound + S pa_i_bl_bd_unique_source_canonical_length_lower_product = ff_exponent_bl_bd_unique_source_canonical_length) -> exists pa_p_bl_bd_unique_source_canonical_length_lower_product pa_r_bl_bd_unique_source_canonical_length_lower_product pa_s_bl_bd_unique_source_canonical_length_lower_product. ((((exists pa_h_bl_bd_unique_source_canonical_length_lower_product_factor. pa_h_bl_bd_unique_source_canonical_length_lower_product_factor + S (pa_p_bl_bd_unique_source_canonical_length_lower_product) = S ((S (pa_i_bl_bd_unique_source_canonical_length_lower_product)) * pa_c_bl_bd_unique_source_canonical_length_lower)) /\ exists pa_q_bl_bd_unique_source_canonical_length_lower_product_factor. pa_b_bl_bd_unique_source_canonical_length_lower = pa_q_bl_bd_unique_source_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_unique_source_canonical_length_lower_product)) * pa_c_bl_bd_unique_source_canonical_length_lower) + (pa_p_bl_bd_unique_source_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_unique_source_canonical_length_lower_product_partial. pa_h_bl_bd_unique_source_canonical_length_lower_product_partial + S (pa_r_bl_bd_unique_source_canonical_length_lower_product) = S ((S (pa_i_bl_bd_unique_source_canonical_length_lower_product)) * pa_v_bl_bd_unique_source_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_lower_product_partial. pa_u_bl_bd_unique_source_canonical_length_lower_product = pa_q_bl_bd_unique_source_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_unique_source_canonical_length_lower_product)) * pa_v_bl_bd_unique_source_canonical_length_lower_product) + (pa_r_bl_bd_unique_source_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_unique_source_canonical_length_lower_product_successor. pa_h_bl_bd_unique_source_canonical_length_lower_product_successor + S (pa_s_bl_bd_unique_source_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_unique_source_canonical_length_lower_product)) * pa_v_bl_bd_unique_source_canonical_length_lower_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_lower_product_successor. pa_u_bl_bd_unique_source_canonical_length_lower_product = pa_q_bl_bd_unique_source_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_unique_source_canonical_length_lower_product)) * pa_v_bl_bd_unique_source_canonical_length_lower_product) + (pa_s_bl_bd_unique_source_canonical_length_lower_product))) /\ pa_s_bl_bd_unique_source_canonical_length_lower_product = pa_r_bl_bd_unique_source_canonical_length_lower_product * pa_p_bl_bd_unique_source_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_unique_source_canonical_length_upper pa_c_bl_bd_unique_source_canonical_length_upper. ((forall pa_i_bl_bd_unique_source_canonical_length_upper_repeat. (exists pa_lt_bl_bd_unique_source_canonical_length_upper_repeat_bound. pa_lt_bl_bd_unique_source_canonical_length_upper_repeat_bound + S pa_i_bl_bd_unique_source_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_unique_source_canonical_length_upper_repeat_decoded. pa_h_bl_bd_unique_source_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_unique_source_canonical_length_upper_repeat)) * pa_c_bl_bd_unique_source_canonical_length_upper)) /\ exists pa_q_bl_bd_unique_source_canonical_length_upper_repeat_decoded. pa_b_bl_bd_unique_source_canonical_length_upper = pa_q_bl_bd_unique_source_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_unique_source_canonical_length_upper_repeat)) * pa_c_bl_bd_unique_source_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_unique_source_canonical_length_upper_product pa_v_bl_bd_unique_source_canonical_length_upper_product. ((((exists pa_h_bl_bd_unique_source_canonical_length_upper_product_start. pa_h_bl_bd_unique_source_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_unique_source_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_upper_product_start. pa_u_bl_bd_unique_source_canonical_length_upper_product = pa_q_bl_bd_unique_source_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_unique_source_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_unique_source_canonical_length_upper_product_terminal. pa_h_bl_bd_unique_source_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_unique_source_canonical_length) = S ((S (l)) * pa_v_bl_bd_unique_source_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_upper_product_terminal. pa_u_bl_bd_unique_source_canonical_length_upper_product = pa_q_bl_bd_unique_source_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_unique_source_canonical_length_upper_product) + (ff_upper_bl_bd_unique_source_canonical_length))) /\ forall pa_i_bl_bd_unique_source_canonical_length_upper_product. (exists pa_lt_bl_bd_unique_source_canonical_length_upper_product_bound. pa_lt_bl_bd_unique_source_canonical_length_upper_product_bound + S pa_i_bl_bd_unique_source_canonical_length_upper_product = l) -> exists pa_p_bl_bd_unique_source_canonical_length_upper_product pa_r_bl_bd_unique_source_canonical_length_upper_product pa_s_bl_bd_unique_source_canonical_length_upper_product. ((((exists pa_h_bl_bd_unique_source_canonical_length_upper_product_factor. pa_h_bl_bd_unique_source_canonical_length_upper_product_factor + S (pa_p_bl_bd_unique_source_canonical_length_upper_product) = S ((S (pa_i_bl_bd_unique_source_canonical_length_upper_product)) * pa_c_bl_bd_unique_source_canonical_length_upper)) /\ exists pa_q_bl_bd_unique_source_canonical_length_upper_product_factor. pa_b_bl_bd_unique_source_canonical_length_upper = pa_q_bl_bd_unique_source_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_unique_source_canonical_length_upper_product)) * pa_c_bl_bd_unique_source_canonical_length_upper) + (pa_p_bl_bd_unique_source_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_unique_source_canonical_length_upper_product_partial. pa_h_bl_bd_unique_source_canonical_length_upper_product_partial + S (pa_r_bl_bd_unique_source_canonical_length_upper_product) = S ((S (pa_i_bl_bd_unique_source_canonical_length_upper_product)) * pa_v_bl_bd_unique_source_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_upper_product_partial. pa_u_bl_bd_unique_source_canonical_length_upper_product = pa_q_bl_bd_unique_source_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_unique_source_canonical_length_upper_product)) * pa_v_bl_bd_unique_source_canonical_length_upper_product) + (pa_r_bl_bd_unique_source_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_unique_source_canonical_length_upper_product_successor. pa_h_bl_bd_unique_source_canonical_length_upper_product_successor + S (pa_s_bl_bd_unique_source_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_unique_source_canonical_length_upper_product)) * pa_v_bl_bd_unique_source_canonical_length_upper_product)) /\ exists pa_q_bl_bd_unique_source_canonical_length_upper_product_successor. pa_u_bl_bd_unique_source_canonical_length_upper_product = pa_q_bl_bd_unique_source_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_unique_source_canonical_length_upper_product)) * pa_v_bl_bd_unique_source_canonical_length_upper_product) + (pa_s_bl_bd_unique_source_canonical_length_upper_product))) /\ pa_s_bl_bd_unique_source_canonical_length_upper_product = pa_r_bl_bd_unique_source_canonical_length_upper_product * pa_p_bl_bd_unique_source_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_unique_source_canonical_length. ff_lower_gap_bl_bd_unique_source_canonical_length + (ff_lower_bl_bd_unique_source_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_unique_source_canonical_length. ff_upper_gap_bl_bd_unique_source_canonical_length + S (n) = (ff_upper_bl_bd_unique_source_canonical_length))))))))) /\ (((forall ff_index_be_bd_unique_source_canonical_code_digits ff_digit_be_bd_unique_source_canonical_code_digits. (exists ff_lt_be_bd_unique_source_canonical_code_digits_bound. ff_lt_be_bd_unique_source_canonical_code_digits_bound + S ff_index_be_bd_unique_source_canonical_code_digits = l) -> (((exists ff_h_be_bd_unique_source_canonical_code_digits_digit. ff_h_be_bd_unique_source_canonical_code_digits_digit + S (ff_digit_be_bd_unique_source_canonical_code_digits) = S ((S (ff_index_be_bd_unique_source_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_unique_source_canonical_code_digits_digit. b = ff_q_be_bd_unique_source_canonical_code_digits_digit * S ((S (ff_index_be_bd_unique_source_canonical_code_digits)) * c) + (ff_digit_be_bd_unique_source_canonical_code_digits))) -> (ff_digit_be_bd_unique_source_canonical_code_digits = 0 \/ ff_digit_be_bd_unique_source_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_unique_source_canonical_code_horner ff_v_ph_bd_unique_source_canonical_code_horner. ((((exists fs_h_ph_bd_unique_source_canonical_code_horner_body_start. fs_h_ph_bd_unique_source_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_unique_source_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_source_canonical_code_horner_body_start. ff_u_ph_bd_unique_source_canonical_code_horner = fs_q_ph_bd_unique_source_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_unique_source_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_unique_source_canonical_code_horner_body_terminal. fs_h_ph_bd_unique_source_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_unique_source_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_source_canonical_code_horner_body_terminal. ff_u_ph_bd_unique_source_canonical_code_horner = fs_q_ph_bd_unique_source_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_unique_source_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_unique_source_canonical_code_horner_body_steps. (exists ph_bound_bd_unique_source_canonical_code_horner_body_steps. ph_bound_bd_unique_source_canonical_code_horner_body_steps + S ff_i_ph_bd_unique_source_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_unique_source_canonical_code_horner_body_steps ff_previous_ph_bd_unique_source_canonical_code_horner_body_steps ff_current_ph_bd_unique_source_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_unique_source_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_unique_source_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_unique_source_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_unique_source_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_unique_source_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_unique_source_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_unique_source_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_unique_source_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_unique_source_canonical_code_horner_body_steps_before. fs_h_ph_bd_unique_source_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_unique_source_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_unique_source_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_source_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_source_canonical_code_horner_body_steps_before. ff_u_ph_bd_unique_source_canonical_code_horner = fs_q_ph_bd_unique_source_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_unique_source_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_source_canonical_code_horner) + (ff_previous_ph_bd_unique_source_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_unique_source_canonical_code_horner_body_steps_after. fs_h_ph_bd_unique_source_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_unique_source_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_unique_source_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_source_canonical_code_horner)) /\ exists fs_q_ph_bd_unique_source_canonical_code_horner_body_steps_after. ff_u_ph_bd_unique_source_canonical_code_horner = fs_q_ph_bd_unique_source_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_unique_source_canonical_code_horner_body_steps)) * ff_v_ph_bd_unique_source_canonical_code_horner) + (ff_current_ph_bd_unique_source_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_unique_source_canonical_code_horner_body_steps = ff_previous_ph_bd_unique_source_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_unique_source_canonical_code_horner_body_steps)))))))))) /\ ((exists ff_trace_code_be_bd_unique_source_execution ff_trace_scale_be_bd_unique_source_execution. ((((((exists ff_h_be_bd_unique_source_execution_trace_start. ff_h_be_bd_unique_source_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_bd_unique_source_execution)) /\ exists ff_q_be_bd_unique_source_execution_trace_start. ff_trace_code_be_bd_unique_source_execution = ff_q_be_bd_unique_source_execution_trace_start * S ((S (0)) * ff_trace_scale_be_bd_unique_source_execution) + (1))) /\ forall ff_index_be_bd_unique_source_execution_trace. (exists ff_lt_be_bd_unique_source_execution_trace_bound. ff_lt_be_bd_unique_source_execution_trace_bound + S ff_index_be_bd_unique_source_execution_trace = l) -> exists ff_digit_be_bd_unique_source_execution_trace ff_previous_be_bd_unique_source_execution_trace ff_current_be_bd_unique_source_execution_trace. ((((exists ff_h_be_bd_unique_source_execution_trace_source. ff_h_be_bd_unique_source_execution_trace_source + S (ff_digit_be_bd_unique_source_execution_trace) = S ((S (ff_index_be_bd_unique_source_execution_trace)) * c)) /\ exists ff_q_be_bd_unique_source_execution_trace_source. b = ff_q_be_bd_unique_source_execution_trace_source * S ((S (ff_index_be_bd_unique_source_execution_trace)) * c) + (ff_digit_be_bd_unique_source_execution_trace))) /\ ((((exists ff_h_be_bd_unique_source_execution_trace_before. ff_h_be_bd_unique_source_execution_trace_before + S (ff_previous_be_bd_unique_source_execution_trace) = S ((S (ff_index_be_bd_unique_source_execution_trace)) * ff_trace_scale_be_bd_unique_source_execution)) /\ exists ff_q_be_bd_unique_source_execution_trace_before. ff_trace_code_be_bd_unique_source_execution = ff_q_be_bd_unique_source_execution_trace_before * S ((S (ff_index_be_bd_unique_source_execution_trace)) * ff_trace_scale_be_bd_unique_source_execution) + (ff_previous_be_bd_unique_source_execution_trace))) /\ ((((exists ff_h_be_bd_unique_source_execution_trace_after. ff_h_be_bd_unique_source_execution_trace_after + S (ff_current_be_bd_unique_source_execution_trace) = S ((S (S ff_index_be_bd_unique_source_execution_trace)) * ff_trace_scale_be_bd_unique_source_execution)) /\ exists ff_q_be_bd_unique_source_execution_trace_after. ff_trace_code_be_bd_unique_source_execution = ff_q_be_bd_unique_source_execution_trace_after * S ((S (S ff_index_be_bd_unique_source_execution_trace)) * ff_trace_scale_be_bd_unique_source_execution) + (ff_current_be_bd_unique_source_execution_trace))) /\ ((((ff_digit_be_bd_unique_source_execution_trace = 0) /\ (((exists ff_gap_binary_be_bd_unique_source_execution_trace_transition_square. ff_gap_binary_be_bd_unique_source_execution_trace_transition_square + S (ff_current_be_bd_unique_source_execution_trace) = m) /\ (exists ff_left_binary_be_bd_unique_source_execution_trace_transition_square_congruence ff_right_binary_be_bd_unique_source_execution_trace_transition_square_congruence. (ff_previous_be_bd_unique_source_execution_trace * ff_previous_be_bd_unique_source_execution_trace) + m * ff_left_binary_be_bd_unique_source_execution_trace_transition_square_congruence = (ff_current_be_bd_unique_source_execution_trace) + m * ff_right_binary_be_bd_unique_source_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_bd_unique_source_execution_trace = 1) /\ (((exists ff_gap_binary_be_bd_unique_source_execution_trace_transition_multiply. ff_gap_binary_be_bd_unique_source_execution_trace_transition_multiply + S (ff_current_be_bd_unique_source_execution_trace) = m) /\ (exists ff_left_binary_be_bd_unique_source_execution_trace_transition_multiply_congruence ff_right_binary_be_bd_unique_source_execution_trace_transition_multiply_congruence. ((ff_previous_be_bd_unique_source_execution_trace * ff_previous_be_bd_unique_source_execution_trace) * a) + m * ff_left_binary_be_bd_unique_source_execution_trace_transition_multiply_congruence = (ff_current_be_bd_unique_source_execution_trace) + m * ff_right_binary_be_bd_unique_source_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_bd_unique_source_execution_terminal. ff_h_be_bd_unique_source_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_bd_unique_source_execution)) /\ exists ff_q_be_bd_unique_source_execution_terminal. ff_trace_code_be_bd_unique_source_execution = ff_q_be_bd_unique_source_execution_terminal * S ((S (l)) * ff_trace_scale_be_bd_unique_source_execution) + (r))))) /\ (exists ff_power_binary_bd_unique_source_power. ((exists ff_b_binary_bd_unique_source_power_value ff_c_binary_bd_unique_source_power_value. ((forall ff_i_binary_bd_unique_source_power_value_repeat. (exists ff_lt_binary_bd_unique_source_power_value_repeat_bound. ff_lt_binary_bd_unique_source_power_value_repeat_bound + S ff_i_binary_bd_unique_source_power_value_repeat = n) -> (((exists ff_h_binary_bd_unique_source_power_value_repeat_decoded. ff_h_binary_bd_unique_source_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_bd_unique_source_power_value_repeat)) * ff_c_binary_bd_unique_source_power_value)) /\ exists ff_q_binary_bd_unique_source_power_value_repeat_decoded. ff_b_binary_bd_unique_source_power_value = ff_q_binary_bd_unique_source_power_value_repeat_decoded * S ((S (ff_i_binary_bd_unique_source_power_value_repeat)) * ff_c_binary_bd_unique_source_power_value) + (a)))) /\ (exists ff_u_binary_bd_unique_source_power_value_product ff_v_binary_bd_unique_source_power_value_product. ((((exists ff_h_binary_bd_unique_source_power_value_product_start. ff_h_binary_bd_unique_source_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_bd_unique_source_power_value_product)) /\ exists ff_q_binary_bd_unique_source_power_value_product_start. ff_u_binary_bd_unique_source_power_value_product = ff_q_binary_bd_unique_source_power_value_product_start * S ((S (0)) * ff_v_binary_bd_unique_source_power_value_product) + (1))) /\ ((((exists ff_h_binary_bd_unique_source_power_value_product_terminal. ff_h_binary_bd_unique_source_power_value_product_terminal + S (ff_power_binary_bd_unique_source_power) = S ((S (n)) * ff_v_binary_bd_unique_source_power_value_product)) /\ exists ff_q_binary_bd_unique_source_power_value_product_terminal. ff_u_binary_bd_unique_source_power_value_product = ff_q_binary_bd_unique_source_power_value_product_terminal * S ((S (n)) * ff_v_binary_bd_unique_source_power_value_product) + (ff_power_binary_bd_unique_source_power))) /\ forall ff_i_binary_bd_unique_source_power_value_product. (exists ff_lt_binary_bd_unique_source_power_value_product_bound. ff_lt_binary_bd_unique_source_power_value_product_bound + S ff_i_binary_bd_unique_source_power_value_product = n) -> exists ff_p_binary_bd_unique_source_power_value_product ff_r_binary_bd_unique_source_power_value_product ff_s_binary_bd_unique_source_power_value_product. ((((exists ff_h_binary_bd_unique_source_power_value_product_factor. ff_h_binary_bd_unique_source_power_value_product_factor + S (ff_p_binary_bd_unique_source_power_value_product) = S ((S (ff_i_binary_bd_unique_source_power_value_product)) * ff_c_binary_bd_unique_source_power_value)) /\ exists ff_q_binary_bd_unique_source_power_value_product_factor. ff_b_binary_bd_unique_source_power_value = ff_q_binary_bd_unique_source_power_value_product_factor * S ((S (ff_i_binary_bd_unique_source_power_value_product)) * ff_c_binary_bd_unique_source_power_value) + (ff_p_binary_bd_unique_source_power_value_product))) /\ ((((exists ff_h_binary_bd_unique_source_power_value_product_partial. ff_h_binary_bd_unique_source_power_value_product_partial + S (ff_r_binary_bd_unique_source_power_value_product) = S ((S (ff_i_binary_bd_unique_source_power_value_product)) * ff_v_binary_bd_unique_source_power_value_product)) /\ exists ff_q_binary_bd_unique_source_power_value_product_partial. ff_u_binary_bd_unique_source_power_value_product = ff_q_binary_bd_unique_source_power_value_product_partial * S ((S (ff_i_binary_bd_unique_source_power_value_product)) * ff_v_binary_bd_unique_source_power_value_product) + (ff_r_binary_bd_unique_source_power_value_product))) /\ ((((exists ff_h_binary_bd_unique_source_power_value_product_successor. ff_h_binary_bd_unique_source_power_value_product_successor + S (ff_s_binary_bd_unique_source_power_value_product) = S ((S (S ff_i_binary_bd_unique_source_power_value_product)) * ff_v_binary_bd_unique_source_power_value_product)) /\ exists ff_q_binary_bd_unique_source_power_value_product_successor. ff_u_binary_bd_unique_source_power_value_product = ff_q_binary_bd_unique_source_power_value_product_successor * S ((S (S ff_i_binary_bd_unique_source_power_value_product)) * ff_v_binary_bd_unique_source_power_value_product) + (ff_s_binary_bd_unique_source_power_value_product))) /\ ff_s_binary_bd_unique_source_power_value_product = ff_r_binary_bd_unique_source_power_value_product * ff_p_binary_bd_unique_source_power_value_product)))))))) /\ (((exists ff_gap_binary_bd_unique_source_power_residue. ff_gap_binary_bd_unique_source_power_residue + S (r) = m) /\ (exists ff_left_binary_bd_unique_source_power_residue_congruence ff_right_binary_bd_unique_source_power_residue_congruence. (ff_power_binary_bd_unique_source_power) + m * ff_left_binary_bd_unique_source_power_residue_congruence = (r) + m * ff_right_binary_bd_unique_source_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. 0015exists x3
  16. 0016split
  17. 0017exists x
  18. 0018exists x1
  19. 0019exists x2
  20. 0020exact hfull_witness_witness_witness_witness
  21. 0021intro s
  22. 0022intro hother
  23. 0023cases hother
  24. 0024cases hother_witness
  25. 0025cases hother_witness_witness
  26. 0026specialize binary_modular_exponent_coded_execution_result_functional n
  27. 0027specialize binary_modular_exponent_coded_execution_result_functional a
  28. 0028specialize binary_modular_exponent_coded_execution_result_functional m
  29. 0029specialize binary_modular_exponent_coded_execution_result_functional x
  30. 0030specialize binary_modular_exponent_coded_execution_result_functional x1
  31. 0031specialize binary_modular_exponent_coded_execution_result_functional x2
  32. 0032specialize binary_modular_exponent_coded_execution_result_functional x3
  33. 0033specialize binary_modular_exponent_coded_execution_result_functional x4
  34. 0034specialize binary_modular_exponent_coded_execution_result_functional x5
  35. 0035specialize binary_modular_exponent_coded_execution_result_functional x6
  36. 0036specialize binary_modular_exponent_coded_execution_result_functional s
  37. 0037apply binary_modular_exponent_coded_execution_result_functional
  38. 0038exact hmodulus
  39. 0039exact hfull_witness_witness_witness_witness
  40. 0040exact hother_witness_witness_witness